OpenRaiser/Intern-Atlas huggingface dataset:
Vehicular Fog Computing Enabled Real-time Collision Warning via Trajectory Calibration
Venue: arXiv cs.NI 2020
Year: 2020

Vehicular fog computing (VFC) has been envisioned as a promising paradigm for enabling a variety of emerging intelligent transportation systems (ITS). However, due to inevitable as well as non-negligible issues in wireless communication, including transmission latency and packet loss, it is still challenging in implementing safety-critical applications, such as real-time collision warning in vehicular networks. In this paper, we present a vehicular fog computing architecture, aiming at supporting effective and real-time collision warning by offloading computation and communication overheads to distributed fog nodes. With the system architecture, we further propose a trajectory calibration based collision warning (TCCW) algorithm along with tailored communication protocols. Specifically, an application-layer vehicular-to-infrastructure (V2I) communication delay is fitted by the Stable distribution with real-world field testing data. Then, a packet loss detection mechanism is designed. Finally, TCCW calibrates real-time vehicle trajectories based on received vehicle status including GPS coordinates, velocity, acceleration, heading direction, as well as the estimation of communication delay and the detection of packet loss. For performance evaluation, we build the simulation model and implement conventional solutions including cloud-based warning and fog-based warning without calibration for comparison. Real-vehicle trajectories are extracted as the input, and the simulation results demonstrate that the effectiveness of TCCW in terms of the highest precision and recall in a wide range of scenarios.
The Threat to the Validity of Predictive Mutation Testing: The Impact of Uncovered Mutants
Venue: arXiv cs.SE 2020
Year: 2020

Predictive Mutation Testing (PMT) is a technique to predict whether a mutant will be killed by using machine learning approaches. Researchers have proposed various machine learning methods for PMT under the cross-project setting. However, they did not consider the impact of uncovered mutants. A mutant is uncovered if the statement on which the mutant is generated is not executed by any test cases. We show that uncovered mutants inflate previous PMT results. Moreover, we aim at proposing an alternative approach to improve PMT and suggesting a different interpretation for cross-project PMT. We replicated the previous PMT research. We also proposed an approach based on the combination of Random Forest and Gradient Boosting to improve the PMT results. We empirically evaluated our approach on the same 654 Java projects provided by the previous PMT literature. Our results indicate that the performance of PMT drastically decreases in terms of AUC from 0.83 to 0.51. Furthermore, PMT performs worse than random guesses on 27% of the test projects. The proposed approach improves the PMT results by achieving the average AUC value of 0.61.
Token-curated registry (TCR) in a scholarly journal: blockchain meets invisible colleges
Venue: arXiv cs.SI 2020
Year: 2020

In this paper, we propose a novel framework for a scholarly journal, a token-curated registry (TCR). This model originates in the field of blockchain and cryptoeconomics and is essentially a decentralized system where tokens (digital currency) are used to incentivize quality curation of information. TCR is an automated way to create lists of any kind where decisions (whether to include N or not) are made through voting that brings benefit or loss to voters. In an academic journal, TCR could act as a tool to introduce community-driven decisions on papers to be published, thus encouraging more active participation of authors and reviewers in editorial policy and elaborating the idea of a journal as a club. TCR could also provide a novel solution to the problems of editorial bias and the lack of rewards/incentives for reviewers. In the paper, we discuss core principles of TCR, its technological and cultural foundations, and finally analyze the risks and challenges it could bring to scholarly publishing.
Minimisation in Logical Form
Venue: arXiv cs.FL 2020
Year: 2020

Stone-type dualities provide a powerful mathematical framework for studying properties of logical systems. They have recently been fruitfully explored in understanding minimisation of various types of automata. In Bezhanishvili et al. (2012), a dual equivalence between a category of coalgebras and a category of algebras was used to explain minimisation. The algebraic semantics is dual to a coalgebraic semantics in which logical equivalence coincides with trace equivalence. It follows that maximal quotients of coalgebras correspond to minimal subobjects of algebras. Examples include partially observable deterministic finite automata, linear weighted automata viewed as coalgebras over finite-dimensional vector spaces, and belief automata, which are coalgebras on compact Hausdorff spaces. In Bonchi et al. (2014), Brzozowski's double-reversal minimisation algorithm for deterministic finite automata was described categorically and its correctness explained via the duality between reachability and observability. This work includes generalisations of Brzozowski's algorithm to Moore and weighted automata over commutative semirings. In this paper we propose a general categorical framework within which such minimisation algorithms can be understood. The goal is to provide a unifying perspective based on duality. Our framework consists of a stack of three interconnected adjunctions: a base dual adjunction that can be lifted to a dual adjunction between coalgebras and algebras and also to a dual adjunction between automata. The approach provides an abstract understanding of reachability and observability. We illustrate the general framework on range of concrete examples, including deterministic Kripke frames, weighted automata, topological automata (belief automata), and alternating automata.
How Effective are Smart Contract Analysis Tools? Evaluating Smart Contract Static Analysis Tools Using Bug Injection
Venue: arXiv cs.SE 2020
Year: 2020

Security attacks targeting smart contracts have been on the rise, which have led to financial loss and erosion of trust. Therefore, it is important to enable developers to discover security vulnerabilities in smart contracts before deployment. A number of static analysis tools have been developed for finding security bugs in smart contracts. However, despite the numerous bug-finding tools, there is no systematic approach to evaluate the proposed tools and gauge their effectiveness. This paper proposes SolidiFI, an automated and systematic approach for evaluating smart contract static analysis tools. SolidiFI is based on injecting bugs (i.e., code defects) into all potential locations in a smart contract to introduce targeted security vulnerabilities. SolidiFI then checks the generated buggy contract using the static analysis tools, and identifies the bugs that the tools are unable to detect (false-negatives) along with identifying the bugs reported as false-positives. SolidiFI is used to evaluate six widely-used static analysis tools, namely, Oyente, Securify, Mythril, SmartCheck, Manticore and Slither, using a set of 50 contracts injected by 9369 distinct bugs. It finds several instances of bugs that are not detected by the evaluated tools despite their claims of being able to detect such bugs, and all the tools report many false positives
Stacked Bidirectional and Unidirectional LSTM Recurrent Neural Network for Forecasting Network-wide Traffic State with Missing Values
Venue: arXiv cs.LG 2020
Year: 2020

Short-term traffic forecasting based on deep learning methods, especially recurrent neural networks (RNN), has received much attention in recent years. However, the potential of RNN-based models in traffic forecasting has not yet been fully exploited in terms of the predictive power of spatial-temporal data and the capability of handling missing data. In this paper, we focus on RNN-based models and attempt to reformulate the way to incorporate RNN and its variants into traffic prediction models. A stacked bidirectional and unidirectional LSTM network architecture (SBU-LSTM) is proposed to assist the design of neural network structures for traffic state forecasting. As a key component of the architecture, the bidirectional LSTM (BDLSM) is exploited to capture the forward and backward temporal dependencies in spatiotemporal data. To deal with missing values in spatial-temporal data, we also propose a data imputation mechanism in the LSTM structure (LSTM-I) by designing an imputation unit to infer missing values and assist traffic prediction. The bidirectional version of LSTM-I is incorporated in the SBU-LSTM architecture. Two real-world network-wide traffic state datasets are used to conduct experiments and published to facilitate further traffic prediction research. The prediction performance of multiple types of multi-layer LSTM or BDLSTM models is evaluated. Experimental results indicate that the proposed SBU-LSTM architecture, especially the two-layer BDLSTM network, can achieve superior performance for the network-wide traffic prediction in both accuracy and robustness. Further, comprehensive comparison results show that the proposed data imputation mechanism in the RNN-based models can achieve outstanding prediction performance when the model's input data contains different patterns of missing values.
Joint learning of interpretation and distillation
Venue: arXiv cs.LG 2020
Year: 2020

The extra trust brought by the model interpretation has made it an indispensable part of machine learning systems. But to explain a distilled model's prediction, one may either work with the student model itself, or turn to its teacher model. This leads to a more fundamental question: if a distilled model should give a similar prediction for a similar reason as its teacher model on the same input? This question becomes even more crucial when the two models have dramatically different structure, taking GBDT2NN for example. This paper conducts an empirical study on the new approach to explaining each prediction of GBDT2NN, and how imitating the explanation can further improve the distillation process as an auxiliary learning task. Experiments on several benchmarks show that the proposed methods achieve better performance on both explanations and predictions.
Physics-based polynomial neural networks for one-shot learning of dynamical systems from one or a few samples
Venue: arXiv cs.NE 2020
Year: 2020

This paper discusses an approach for incorporating prior physical knowledge into the neural network to improve data efficiency and the generalization of predictive models. If the dynamics of a system approximately follows a given differential equation, the Taylor mapping method can be used to initialize the weights of a polynomial neural network. This allows the fine-tuning of the model from one training sample of real system dynamics. The paper describes practical results on real experiments with both a simple pendulum and one of the largest worldwide X-ray source. It is demonstrated in practice that the proposed approach allows recovering complex physics from noisy, limited, and partial observations and provides meaningful predictions for previously unseen inputs. The approach mainly targets the learning of physical systems when state-of-the-art models are difficult to apply given the lack of training data.
Featherweight Go
Venue: arXiv cs.PL 2020
Year: 2020

We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is widely used, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.
Multi-view Alignment and Generation in CCA via Consistent Latent Encoding
Venue: arXiv cs.LG 2020
Year: 2020

Multi-view alignment, achieving one-to-one correspondence of multi-view inputs, is critical in many real-world multi-view applications, especially for cross-view data analysis problems. Recently, an increasing number of works study this alignment problem with Canonical Correlation Analysis (CCA). However, existing CCA models are prone to misalign the multiple views due to either the neglect of uncertainty or the inconsistent encoding of the multiple views. To tackle these two issues, this paper studies multi-view alignment from the Bayesian perspective. Delving into the impairments of inconsistent encodings, we propose to recover correspondence of the multi-view inputs by matching the marginalization of the joint distribution of multi-view random variables under different forms of factorization. To realize our design, we present Adversarial CCA (ACCA) which achieves consistent latent encodings by matching the marginalized latent encodings through the adversarial training paradigm. Our analysis based on conditional mutual information reveals that ACCA is flexible for handling implicit distributions. Extensive experiments on correlation analysis and cross-view generation under noisy input settings demonstrate the superiority of our model.
An inequality for the number of periods in a word
Venue: arXiv cs.DM 2020
Year: 2020

We prove an inequality for the number of periods in a word x in terms of the length of x and its initial critical exponent. Next, we characterize all periods of the length-n prefix of a characteristic Sturmian word in terms of the lazy Ostrowski representation of n, and use this result to show that our inequality is tight for infinitely many words x. We propose two related measures of periodicity for infinite words. Finally, we also consider special cases where x is overlap-free or squarefree.
KaLM at SemEval-2020 Task 4: Knowledge-aware Language Models for Comprehension And Generation
Venue: arXiv cs.CL 2020
Year: 2020

This paper presents our strategies in SemEval 2020 Task 4: Commonsense Validation and Explanation. We propose a novel way to search for evidence and choose the different large-scale pre-trained models as the backbone for three subtasks. The results show that our evidence-searching approach improves model performance on commonsense explanation task. Our team ranks 2nd in subtask C according to human evaluation score.
Deep Convolutional Neural Network-based Bernoulli Heatmap for Head Pose Estimation
Venue: arXiv cs.CV 2020
Year: 2020

Head pose estimation is a crucial problem for many tasks, such as driver attention, fatigue detection, and human behaviour analysis. It is well known that neural networks are better at handling classification problems than regression problems. It is an extremely nonlinear process to let the network output the angle value directly for optimization learning, and the weight constraint of the loss function will be relatively weak. This paper proposes a novel Bernoulli heatmap for head pose estimation from a single RGB image. Our method can achieve the positioning of the head area while estimating the angles of the head. The Bernoulli heatmap makes it possible to construct fully convolutional neural networks without fully connected layers and provides a new idea for the output form of head pose estimation. A deep convolutional neural network (CNN) structure with multiscale representations is adopted to maintain high-resolution information and low-resolution information in parallel. This kind of structure can maintain rich, high-resolution representations. In addition, channelwise fusion is adopted to make the fusion weights learnable instead of simple addition with equal weights. As a result, the estimation is spatially more precise and potentially more accurate. The effectiveness of the proposed method is empirically demonstrated by comparing it with other state-of-the-art methods on public datasets.
Recognizing Families through Images with Pretrained Encoder
Venue: arXiv cs.CV 2020
Year: 2020

Kinship verification and kinship retrieval are emerging tasks in computer vision. Kinship verification aims at determining whether two facial images are from related people or not, while kinship retrieval is the task of retrieving possible related facial images to a person from a gallery of images. They introduce unique challenges because of the hidden relations and features that carry inherent characteristics between the facial images. We employ 3 methods, FaceNet, Siamese VGG-Face, and a combination of FaceNet and VGG-Face models as feature extractors, to achieve the 9th standing for kinship verification and the 5th standing for kinship retrieval in the Recognizing Family in The Wild 2020 competition. We then further experimented using StyleGAN2 as another encoder, with no improvement in the result.
Monitoring and Diagnosability of Perception Systems
Venue: arXiv cs.RO 2020
Year: 2020

Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving cars. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies relies on the development of methodologies to guarantee and monitor safe operation as well as detect and mitigate failures. Despite the paramount importance of perception systems, currently there is no formal approach for system-level monitoring. In this work, we propose a mathematical model for runtime monitoring and fault detection of perception systems. Towards this goal, we draw connections with the literature on self-diagnosability for multiprocessor systems, and generalize it to (i) account for modules with heterogeneous outputs, and (ii) add a temporal dimension to the problem, which is crucial to model realistic perception systems where modules interact over time. This contribution results in a graph-theoretic approach that, given a perception system, is able to detect faults at runtime and allows computing an upper-bound on the number of faulty modules that can be detected. Our second contribution is to show that the proposed monitoring approach can be elegantly described with the language of topos theory, which allows formulating diagnosability over arbitrary time intervals.
A Proof Assistant Based Formalisation of Core Erlang
Venue: arXiv cs.PL 2020
Year: 2020

Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language. In this paper, we present our proof-assistant-based formalisation of a subset of Erlang, intended to serve as a base for proving refactorings correct. After discussing how we reused concepts from related work, we show the syntax and semantics of our formal description, including the abstractions involved (e.g. closures). We also present essential properties of the formalisation (e.g. determinism) along with their machine-checked proofs. Finally, we prove the correctness of some simple refactoring strategies.
Reinforcement Learning with Iterative Reasoning for Merging in Dense Traffic
Venue: arXiv cs.AI 2020
Year: 2020

Maneuvering in dense traffic is a challenging task for autonomous vehicles because it requires reasoning about the stochastic behaviors of many other participants. In addition, the agent must achieve the maneuver within a limited time and distance. In this work, we propose a combination of reinforcement learning and game theory to learn merging behaviors. We design a training curriculum for a reinforcement learning agent using the concept of level-$k$ behavior. This approach exposes the agent to a broad variety of behaviors during training, which promotes learning policies that are robust to model discrepancies. We show that our approach learns more efficient policies than traditional training methods.
Improving Web Content Blocking With Event-Loop-Turn Granularity JavaScript Signatures
Venue: arXiv cs.CR 2020
Year: 2020

Content blocking is an important part of a performant, user-serving, privacy respecting web. Most content blockers build trust labels over URLs. While useful, this approach has well understood shortcomings. Attackers may avoid detection by changing URLs or domains, bundling unwanted code with benign code, or inlining code in pages. The common flaw in existing approaches is that they evaluate code based on its delivery mechanism, not its behavior. In this work we address this problem with a system for generating signatures of the privacy-and-security relevant behavior of executed JavaScript. Our system considers script behavior during each turn on the JavaScript event loop. Focusing on event loop turns allows us to build signatures that are robust against code obfuscation, code bundling, URL modification, and other common evasions, as well as handle unique aspects of web applications. This work makes the following contributions to improving content blocking: First, implement a novel system to build per-event-loop-turn signatures of JavaScript code by instrumenting the Blink and V8 runtimes. Second, we apply these signatures to measure filter list evasion, by using EasyList and EasyPrivacy as ground truth and finding other code that behaves identically. We build ~2m signatures of privacy-and-security behaviors from 11,212 unique scripts blocked by filter lists, and find 3,589 more unique scripts including the same harmful code, affecting 12.48% of websites measured. Third, we taxonomize common filter list evasion techniques. Finally, we present defenses; filter list additions where possible, and a proposed, signature based system in other cases. We share the implementation of our signature-generation system, the dataset from applying our system to the Alexa 100K, and 586 AdBlock Plus compatible filter list rules to block instances of currently blocked code being moved to new URLs.
Symmetric Linear Programming Formulations for Minimum Cut with Applications to TSP
Venue: arXiv cs.DS 2020
Year: 2020

We introduce multiple symmetric LP relaxations for minimum cut problems. The relaxations give optimal and approximate solutions when the input is a Hamiltonian cycle. We show that this leads to one of two interesting results. In one case, these LPs always give optimal and near optimal solutions, and then they would be the smallest known symmetric LPs for the problems considered. Otherwise, these LP formulations give strictly better LP relaxations for the traveling salesperson problem than the subtour relaxation. We have the smallest known LP formulation that is a 9/8-approximation or better for min-cut. In addition, the LP relaxation of min-cut investigated in this paper has interesting constraints; the LP contains only a single typical min-cut constraint and all other constraints are typically only used for max-cut relaxations.
Cascade Model-based Propensity Estimation for Counterfactual Learning to Rank
Venue: arXiv cs.IR 2020
Year: 2020

Unbiased CLTR requires click propensities to compensate for the difference between user clicks and true relevance of search results via IPS. Current propensity estimation methods assume that user click behavior follows the PBM and estimate click propensities based on this assumption. However, in reality, user clicks often follow the CM, where users scan search results from top to bottom and where each next click depends on the previous one. In this cascade scenario, PBM-based estimates of propensities are not accurate, which, in turn, hurts CLTR performance. In this paper, we propose a propensity estimation method for the cascade scenario, called CM-IPS. We show that CM-IPS keeps CLTR performance close to the full-information performance in case the user clicks follow the CM, while PBM-based CLTR has a significant gap towards the full-information. The opposite is true if the user clicks follow PBM instead of the CM. Finally, we suggest a way to select between CM- and PBM-based propensity estimation methods based on historical user clicks.