OpenRaiser/Intern-Atlas huggingface dataset:
On the Impact of Random Actions on Opinion Dynamics
Venue: arXiv cs.SI 2020
Year: 2020

We study opinion dynamics in a social network with stubborn agents who influence their neighbors but who themselves always stick to their initial opinion. We consider first the well-known DeGroot model. While it is known in the literature that this model can lead to consensus even in the presence of a stubborn agent, we show that the same result holds under weaker assumptions than has been previously reported. We then consider a recent extension of the DeGroot model in which the opinion of each agent is a random Bernoulli distributed variable, and by leveraging on the first result we establish that this model also leads to consensus, in the sense of convergence in probability, in the presence of a stubborn agent. Moreover, all agents' opinions converge to that of the stubborn agent. We also consider a variation on this model where the stubborn agent is replaced with a drifting agent and show that herding is achieved also in this case. Finally, we offer a detailed critique of a proof regarding a claim about a closely related model in the recent literature.
Simplifying Impact Prediction for Scientific Articles
Venue: arXiv cs.IR 2020
Year: 2020

Estimating the expected impact of an article is valuable for various applications (e.g., article/cooperator recommendation). Most existing approaches attempt to predict the exact number of citations each article will receive in the near future, however this is a difficult regression analysis problem. Moreover, most approaches rely on the existence of rich metadata for each article, a requirement that cannot be adequately fulfilled for a large number of them. In this work, we take advantage of the fact that solving a simpler machine learning problem, that of classifying articles based on their expected impact, is adequate for many real world applications and we propose a simplified model that can be trained using minimal article metadata. Finally, we examine various configurations of this model and evaluate their effectiveness in solving the aforementioned classification problem.
A Novel Resampling Technique for Imbalanced Dataset Optimization
Venue: arXiv cs.LG 2020
Year: 2020

Despite the enormous amount of data, particular events of interest can still be quite rare. Classification of rare events is a common problem in many domains, such as fraudulent transactions, malware traffic analysis and network intrusion detection. Many studies have been developed for malware detection using machine learning approaches on various datasets, but as far as we know only the MTA-KDD'19 dataset has the peculiarity of updating the representative set of malicious traffic on a daily basis. This daily updating is the added value of the dataset, but it translates into a potential due to the class imbalance problem that the RRw-Optimized MTA-KDD'19 will occur. We capture difficulties of class distribution in real datasets by considering four types of minority class examples: safe, borderline, rare and outliers. In this work, we developed two versions of Generative Silhouette Resampling 1-Nearest Neighbour (G1Nos) oversampling algorithms for dealing with class imbalance problem. The first module of G1Nos algorithms performs a coefficient-based instance selection silhouette identifying the critical threshold of Imbalance Degree. (ID), the second module generates synthetic samples using a SMOTE-like oversampling algorithm. The balancing of the classes is done by our G1Nos algorithms to re-establish the proportions between the two classes of the used dataset. The experimental results show that our oversampling algorithm work better than the other two SOTA methodologies in all the metrics considered.
SDN helps Big Data to optimize access to data
Venue: arXiv cs.DC 2020
Year: 2020

This chapter introduces the state-of-the-art in the emerging area of combining High Performance Computing (HPC) with Big Data Analysis. To understand the new area, the chapter first surveys the existing approaches to integrating HPC with Big Data. Next, the chapter introduces several optimization solutions that focus on how to minimize the data transfer time from computation-intensive applications to analysis-intensive applications as well as minimizing the end-to-end time-to-solution. The solutions utilize SDN to adaptively use both high speed interconnect network and high performance parallel file systems to optimize the application performance. A computational framework called DataBroker is designed and developed to enable a tight integration of HPC with data analysis. Multiple types of experiments have been conducted to show different performance issues in both message passing and parallel file systems and to verify the effectiveness of the proposed research approaches.
Solving Interactive Fiction Games via Partial Evaluation and Bounded Model Checking
Venue: arXiv cs.PL 2020
Year: 2020

We present a case study on using program verification tools, specifically model-checkers for C programs, to solve simple interactive fiction games from around 1980. Off-the-shelf model-checking tools are unable to handle the games in their original form. In order to work around this, we apply a series of program transformations that do not change the behaviour of the program. An interesting aspect of these games is that they use a simple, interpreted language to script in-game events. This turns out to be the most difficult part of the program for verification tools to handle; we tackle this using partial evaluation. Our case study thus provides some insights that are applicable more generally to verification and analysis of programs that interpret scripting languages. To the best of our knowledge, this is the first example of a commercially released game being solved by application of a program model-checker to the game's code.
Generalized Operating Procedure for Deep Learning: an Unconstrained Optimal Design Perspective
Venue: arXiv cs.LG 2020
Year: 2020

Deep learning (DL) has brought about remarkable breakthrough in processing images, video and speech due to its efficacy in extracting highly abstract representation and learning very complex functions. However, there is seldom operating procedure reported on how to make it for real use cases. In this paper, we intend to address this problem by presenting a generalized operating procedure for DL from the perspective of unconstrained optimal design, which is motivated by a simple intension to remove the barrier of using DL, especially for those scientists or engineers who are new but eager to use it. Our proposed procedure contains seven steps, which are project/problem statement, data collection, architecture design, initialization of parameters, defining loss function, computing optimal parameters, and inference, respectively. Following this procedure, we build a multi-stream end-to-end speaker verification system, in which the input speech utterance is processed by multiple parallel streams within different frequency range, so that the acoustic modeling can be more robust resulting from the diversity of features. Trained with VoxCeleb dataset, our experimental results verify the effectiveness of our proposed operating procedure, and also show that our multi-stream framework outperforms single-stream baseline with 20 % relative reduction in minimum decision cost function (minDCF).
Unified Mandarin TTS Front-end Based on Distilled BERT Model
Venue: arXiv cs.SD 2020
Year: 2020

The front-end module in a typical Mandarin text-to-speech system (TTS) is composed of a long pipeline of text processing components, which requires extensive efforts to build and is prone to large accumulative model size and cascade errors. In this paper, a pre-trained language model (PLM) based model is proposed to simultaneously tackle the two most important tasks in TTS front-end, i.e., prosodic structure prediction (PSP) and grapheme-to-phoneme (G2P) conversion. We use a pre-trained Chinese BERT[1] as the text encoder and employ multi-task learning technique to adapt it to the two TTS front-end tasks. Then, the BERT encoder is distilled into a smaller model by employing a knowledge distillation technique called TinyBERT[2], making the whole model size 25% of that of benchmark pipeline models while maintaining competitive performance on both tasks. With the proposed the methods, we are able to run the whole TTS front-end module in a light and unified manner, which is more friendly to deployment on mobile devices.
SharpGAN: Receptive Field Block Net for Dynamic Scene Deblurring
Venue: arXiv cs.CV 2020
Year: 2020

When sailing at sea, the smart ship will inevitably produce swaying motion due to the action of wind, wave and current, which makes the image collected by the visual sensor appear motion blur. This will have an adverse effect on the object detection algorithm based on the vision sensor, thereby affect the navigation safety of the smart ship. In order to remove the motion blur in the images during the navigation of the smart ship, we propose SharpGAN, a new image deblurring method based on the generative adversarial network. First of all, the Receptive Field Block Net (RFBNet) is introduced to the deblurring network to strengthen the network's ability to extract the features of blurred image. Secondly, we propose a feature loss that combines different levels of image features to guide the network to perform higher-quality deblurring and improve the feature similarity between the restored images and the sharp image. Finally, we propose to use the lightweight RFB-s module to improve the real-time performance of deblurring network. Compared with the existing deblurring methods on large-scale real sea image datasets and large-scale deblurring datasets, the proposed method not only has better deblurring performance in visual perception and quantitative criteria, but also has higher deblurring efficiency.
Automatic Historical Feature Generation through Tree-based Method in Ads Prediction
Venue: arXiv cs.LG 2020
Year: 2020

Historical features are important in ads click-through rate (CTR) prediction, because they account for past engagements between users and ads. In this paper, we study how to efficiently construct historical features through counting features. The key challenge of such problem lies in how to automatically identify counting keys. We propose a tree-based method for counting key selection. The intuition is that a decision tree naturally provides various combinations of features, which could be used as counting key candidate. In order to select personalized counting features, we train one decision tree model per user, and the counting keys are selected across different users with a frequency-based importance measure. To validate the effectiveness of proposed solution, we conduct large scale experiments on Twitter video advertising data. In both online learning and offline training settings, the automatically identified counting features outperform the manually curated counting features.
bloomRF: On Performing Range-Queries with Bloom-Filters based on Piecewise-Monotone Hash Functions and Dyadic Trace-Trees
Venue: arXiv cs.DB 2020
Year: 2020

We introduce bloomRF as a unified method for approximate membership testing that supports both point- and range-queries on a single data structure. bloomRF extends Bloom-Filters with range query support and may replace them. The core idea is to employ a dyadic interval scheme to determine the set of dyadic intervals covering a data point, which are then encoded and inserted. bloomRF introduces Dyadic Trace-Trees as novel data structure that represents those covering intervals implicitly. A Trace-Tree encoding scheme represents the set of covering intervals efficiently, in a compact bit representation. Furthermore, bloomRF introduces novel piecewise-monotone hash functions that are locally order-preserving and thus support range querying. We present an efficient membership computation method for range-queries. Although, bloomRF is designed for integers it also supports string and floating-point data types. It can also handle multiple attributes and serve as multi-attribute filter. We evaluate bloomRF in RocksDB and in a standalone library. bloomRF is more efficient and outperforms existing point-range-filters by up to 4x across a range of settings.
Quantitative Evaluations on Saliency Methods: An Experimental Study
Venue: arXiv cs.AI 2020
Year: 2020

It has been long debated that eXplainable AI (XAI) is an important topic, but it lacks rigorous definition and fair metrics. In this paper, we briefly summarize the status quo of the metrics, along with an exhaustive experimental study based on them, including faithfulness, localization, false-positives, sensitivity check, and stability. With the experimental results, we conclude that among all the methods we compare, no single explanation method dominates others in all metrics. Nonetheless, Gradient-weighted Class Activation Mapping (Grad-CAM) and Randomly Input Sampling for Explanation (RISE) perform fairly well in most of the metrics. Utilizing a set of filtered metrics, we further present a case study to diagnose the classification bases for models. While providing a comprehensive experimental study of metrics, we also examine measuring factors that are missed in current metrics and hope this valuable work could serve as a guide for future research.
Regular expression length via arithmetic formula complexity
Venue: arXiv cs.FL 2020
Year: 2020

We prove lower bounds on the length of regular expressions for finite languages by methods from arithmetic circuit complexity. First, we show a reduction: the length of a regular expression for a language $L\subseteq \{0,1\}^n$ is bounded from below by the minimum size of a monotone arithmetic formula computing a polynomial that has $L$ as its set of exponent vectors, viewing words as vectors. This result yields lower bounds for the binomial language of all words with exactly $k$ ones and $n-k$ zeros and for the language of all Dyck words of length $2n$. We also determine the blow-up of language operations (intersection and shuffle) of regular expressions for finite languages. Second, we adapt a lower bound method for multilinear arithmetic formulas by so-called log-product polynomials to regular expressions. With this method we show almost tight lower bounds for the language of all binary numbers with $n$ bits that are divisible by a given odd integer $p$, for the language of all words of length $n$ over a $k$ letter alphabet with an even number of occurrences of each letter and for the language of all permutations of $\{1,\dots, n\}$.
Persistence and Synchronization: Friends or Foes?
Venue: arXiv cs.DC 2020
Year: 2020

Emerging non-volatile memory (NVM) technologies promise memory speed byte-addressable persistent storage with a load/store interface. However, programming applications to directly manipulate NVM data is complex and error-prone. Applications generally employ libraries that hide the low-level details of the hardware and provide a transactional programming model to achieve crash-consistency. Furthermore, applications continue to expect correctness during concurrent executions, achieved through the use of synchronization. To achieve this, applications seek well-known ACID guarantees. However, realizing this presents designers of transactional systems with a range of choices in how to combine several low-level techniques, given target hardware features and workload characteristics. In this paper, we provide a comprehensive evaluation of the impact of combining existing crash-consistency and synchronization methods for achieving performant and correct NVM transactional systems. We consider different hardware characteristics, in terms of support for hardware transactional memory (HTM) and the boundaries of the persistence domain (transient or persistent caches). By characterizing persistent transactional systems in terms of their properties, we make it possible to better understand the tradeoffs of different implementations and to arrive at better design choices for providing ACID guarantees. We use both real hardware with Intel Optane DC persistent memory and simulation to evaluate a persistent version of hardware transactional memory, a persistent version of software transactional memory, and undo/redo logging. Through our empirical study, we show two major factors that impact the cost of supporting persistence in transactional systems: the persistence domain (transient or persistent caches) and application characteristics, such as transaction size and parallelism.
Fully Non-autoregressive Neural Machine Translation: Tricks of the Trade
Venue: arXiv cs.CL 2020
Year: 2020

Fully non-autoregressive neural machine translation (NAT) is proposed to simultaneously predict tokens with single forward of neural networks, which significantly reduces the inference latency at the expense of quality drop compared to the Transformer baseline. In this work, we target on closing the performance gap while maintaining the latency advantage. We first inspect the fundamental issues of fully NAT models, and adopt dependency reduction in the learning space of output tokens as the basic guidance. Then, we revisit methods in four different aspects that have been proven effective for improving NAT models, and carefully combine these techniques with necessary modifications. Our extensive experiments on three translation benchmarks show that the proposed system achieves the new state-of-the-art results for fully NAT models, and obtains comparable performance with the autoregressive and iterative NAT systems. For instance, one of the proposed models achieves 27.49 BLEU points on WMT14 En-De with approximately 16.5X speed up at inference time.
Yet another argument in favour of NP=CoNP
Venue: arXiv cs.CC 2020
Year: 2020

This article shows yet another proof of NP=CoNP$. In a previous article, we proved that NP=PSPACE and from it we can conclude that NP=CoNP immediately. The former proof shows how to obtain polynomial and, polynomial in time checkable Dag-like proofs for all purely implicational Minimal logic tautologies. From the fact that Minimal implicational logic is PSPACE-complete we get the proof that NP=PSPACE. This first proof of NP=CoNP uses Hudelmaier linear upper-bound on the height of Sequent Calculus minimal implicational logic proofs. In an addendum to the proof of NP=PSPACE, we observe that we do not need to use Hudelmaier upper-bound since any proof of non-hamiltonicity for any graph is linear upper-bounded. By the CoNP-completeness of non-hamiltonicity, we obtain NP=CoNP as a corollary of the first proof. In this article we show the third proof of CoNP=NP, also providing polynomial size and polynomial verifiable certificates that are Dags. They are generated from normal Natural Deduction proofs, linear height upper-bounded too, by removing redundancy, i.e., repeated parts. The existence of repeated parts is a consequence of the redundancy theorem for a family of super-polynomial proofs in the purely implicational Minimal logic. It is mandatory to read at least two previous articles to get the details of the proof presented here. The article that proves the redundancy theorem and the article that shows how to remove the repeated parts of a normal Natural Deduction proof to have a polynomial Dag certificate for minimal implicational logic tautologies.
The Pile: An 800GB Dataset of Diverse Text for Language Modeling
Venue: arXiv cs.CL 2020
Year: 2020

Recent work has demonstrated that increased training dataset diversity improves general cross-domain knowledge and downstream generalization capability for large-scale language models. With this in mind, we present \textit{the Pile}: an 825 GiB English text corpus targeted at training large-scale language models. The Pile is constructed from 22 diverse high-quality subsets -- both existing and newly constructed -- many of which derive from academic or professional sources. Our evaluation of the untuned performance of GPT-2 and GPT-3 on the Pile shows that these models struggle on many of its components, such as academic writing. Conversely, models trained on the Pile improve significantly over both Raw CC and CC-100 on all components of the Pile, while improving performance on downstream evaluations. Through an in-depth exploratory analysis, we document potentially concerning aspects of the data for prospective users. We make publicly available the code used in its construction.
Explicit regularization and implicit bias in deep network classifiers trained with the square loss
Venue: arXiv cs.LG 2020
Year: 2020

Deep ReLU networks trained with the square loss have been observed to perform well in classification tasks. We provide here a theoretical justification based on analysis of the associated gradient flow. We show that convergence to a solution with the absolute minimum norm is expected when normalization techniques such as Batch Normalization (BN) or Weight Normalization (WN) are used together with Weight Decay (WD). The main property of the minimizers that bounds their expected error is the norm: we prove that among all the close-to-interpolating solutions, the ones associated with smaller Frobenius norms of the unnormalized weight matrices have better margin and better bounds on the expected classification error. With BN but in the absence of WD, the dynamical system is singular. Implicit dynamical regularization -- that is zero-initial conditions biasing the dynamics towards high margin solutions -- is also possible in the no-BN and no-WD case. The theory yields several predictions, including the role of BN and weight decay, aspects of Papyan, Han and Donoho's Neural Collapse and the constraints induced by BN on the network weights.
Verifying a Cruise Control System using Simulink and SpaceEx
Venue: arXiv cs.LO 2020
Year: 2020

This article aims to provide a simple step-by-step guide highlighting the steps needed to verify a control system with formal verification tools. Starting from a description of the physical system and a control objective in natural language, we design the plant and the controller, we use Simulink for simulation and we employ a reachability analysis tool, SpaceEx, for formal verification.
Formal Game Grammar and Equivalence
Venue: arXiv cs.LO 2020
Year: 2020

We develop methods to formally describe and compare games, in order to probe questions of game structure and design, and as a stepping stone to predicting player behavior from design patterns. We define a grammar-like formalism to describe finite discrete games without hidden information, allowing for randomness, and mixed sequential and simultaneous play. We make minimal assumptions about the form or content of game rules or user interface. The associated game trees resemble hybrid extensive- and strategic-form games, in the game theory sense. By transforming and comparing game trees, we develop equivalence relations on the space of game systems, which equate games that give players the same meaningful agency. We bring these together to suggest a method to measure distance between games, insensitive to cosmetic variations in the game logic descriptions.