OpenRaiser/Intern-Atlas huggingface dataset:
Bridging the Gap: FPGAs as Programmable Switches
Venue: arXiv cs.AR 2020
Year: 2020

The emergence of P4, a domain specific language, coupled to PISA, a domain specific architecture, is revolutionizing the networking field. P4 allows to describe how packets are processed by a programmable data plane, spanning ASICs and CPUs, implementing PISA. Because the processing flexibility can be limited on ASICs, while the CPUs performance for networking tasks lag behind, recent works have proposed to implement PISA on FPGAs. However, little effort has been dedicated to analyze whether FPGAs are good candidates to implement PISA. In this work, we take a step back and evaluate the micro-architecture efficiency of various PISA blocks. We demonstrate, supported by a theoretical and experimental analysis, that the performance of a few PISA blocks is severely limited by the current FPGA architectures. Specifically, we show that match tables and programmable packet schedulers represent the main performance bottlenecks for FPGA-based programmable switches. Thus, we explore two avenues to alleviate these shortcomings. First, we identify network applications well tailored to current FPGAs. Second, to support a wider range of networking applications, we propose modifications to the FPGA architectures which can also be of interest out of the networking field.
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Venue: arXiv cs.PL 2020
Year: 2020

We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates corresponding to the lemmas that are often needed when making inductive proofs. We present an algorithm that uses the new rule, together with the traditional folding/unfolding transformation rules, for the automatic removal of ADTs. We prove that if the set of the transformed clauses is satisfiable, then so is the set of the original clauses. By an experimental evaluation, we show that the use of the differential replacement rule significantly improves the effectiveness of ADT removal, and we show that our transformation-based approach is competitive with respect to a well-established technique that extends the CVC4 solver with induction.
Investigating Efficient Learning and Compositionality in Generative LSTM Networks
Venue: arXiv cs.LG 2020
Year: 2020

When comparing human with artificial intelligence, one major difference is apparent: Humans can generalize very broadly from sparse data sets because they are able to recombine and reintegrate data components in compositional manners. To investigate differences in efficient learning, Joshua B. Tenenbaum and colleagues developed the character challenge: First an algorithm is trained in generating handwritten characters. In a next step, one version of a new type of character is presented. An efficient learning algorithm is expected to be able to re-generate this new character, to identify similar versions of this character, to generate new variants of it, and to create completely new character types. In the past, the character challenge was only met by complex algorithms that were provided with stochastic primitives. Here, we tackle the challenge without providing primitives. We apply a minimal recurrent neural network (RNN) model with one feedforward layer and one LSTM layer and train it to generate sequential handwritten character trajectories from one-hot encoded inputs. To manage the re-generation of untrained characters, when presented with only one example of them, we introduce a one-shot inference mechanism: the gradient signal is backpropagated to the feedforward layer weights only, leaving the LSTM layer untouched. We show that our model is able to meet the character challenge by recombining previously learned dynamic substructures, which are visible in the hidden LSTM states. Making use of the compositional abilities of RNNs in this way might be an important step towards bridging the gap between human and artificial intelligence.
Deep Generation of Coq Lemma Names Using Elaborated Terms
Venue: arXiv cs.PL 2020
Year: 2020

Coding conventions for naming, spacing, and other essentially stylistic properties are necessary for developers to effectively understand, review, and modify source code in large software projects. Consistent conventions in verification projects based on proof assistants, such as Coq, increase in importance as projects grow in size and scope. While conventions can be documented and enforced manually at high cost, emerging approaches automatically learn and suggest idiomatic names in Java-like languages by applying statistical language models on large code corpora. However, due to its powerful language extension facilities and fusion of type checking and computation, Coq is a challenging target for automated learning techniques. We present novel generation models for learning and suggesting lemma names for Coq projects. Our models, based on multi-input neural networks, are the first to leverage syntactic and semantic information from Coq's lexer (tokens in lemma statements), parser (syntax trees), and kernel (elaborated terms) for naming; the key insight is that learning from elaborated terms can substantially boost model performance. We implemented our models in a toolchain, dubbed Roosterize, and applied it on a large corpus of code derived from the Mathematical Components family of projects, known for its stringent coding conventions. Our results show that Roosterize substantially outperforms baselines for suggesting lemma names, highlighting the importance of using multi-input models and elaborated terms.
Multi-Object Tracking with Siamese Track-RCNN
Venue: arXiv cs.CV 2020
Year: 2020

Multi-object tracking systems often consist of a combination of a detector, a short term linker, a re-identification feature extractor and a solver that takes the output from these separate components and makes a final prediction. Differently, this work aims to unify all these in a single tracking system. Towards this, we propose Siamese Track-RCNN, a two stage detect-and-track framework which consists of three functional branches: (1) the detection branch localizes object instances; (2) the Siamese-based track branch estimates the object motion and (3) the object re-identification branch re-activates the previously terminated tracks when they re-emerge. We test our tracking system on two popular datasets of the MOTChallenge. Siamese Track-RCNN achieves significantly higher results than the state-of-the-art, while also being much more efficient, thanks to its unified design.
Enhancing Routing Security in IoT: Performance Evaluation of RPL Secure Mode under Attacks
Venue: arXiv cs.NI 2020
Year: 2020

As the Routing Protocol for Low Power and Lossy Networks (RPL) became the standard for routing in the Internet of Things (IoT) networks, many researchers had investigated the security aspects of this protocol. However, no work (to the best of our knowledge) has investigated the use of the security mechanisms included in RPL standard, mainly because there was no implementation for these features in any IoT operating systems yet. A partial implementation of RPL security mechanisms was presented recently for the Contiki operating system (by Perazzo et al.), which provided us with an opportunity to examine RPL security mechanisms. In this paper, we investigate the effects and challenges of using RPL security mechanisms under common routing attacks. First, a comparison of RPL performance, with and without its security mechanisms, under four routing attacks (Blackhole, Selective-Forward, Neighbor, and Wormhole attacks) is conducted using several metrics (e.g., average data packet delivery rate, average data packet delay, average power consumption, etc.). This comparison is performed using two commonly used Radio Duty-Cycle protocols. Secondly, and based on the observations from this comparison, we propose two techniques that could reduce the effects of such attacks, without having added security mechanisms for RPL. An evaluation of these techniques shows improved performance of RPL under the investigated attacks, except for the Wormhole attack.
Divergent Search for Few-Shot Image Classification
Venue: arXiv cs.NE 2020
Year: 2020

When data is unlabelled and the target task is not known a priori, divergent search offers a strategy for learning a wide range of skills. Having such a repertoire allows a system to adapt to new, unforeseen tasks. Unlabelled image data is plentiful, but it is not always known which features will be required for downstream tasks. We propose a method for divergent search in the few-shot image classification setting and evaluate with Omniglot and Mini-ImageNet. This high-dimensional behavior space includes all possible ways of partitioning the data. To manage divergent search in this space, we rely on a meta-learning framework to integrate useful features from diverse tasks into a single model. The final layer of this model is used as an index into the `archive' of all past behaviors. We search for regions in the behavior space that the current archive cannot reach. As expected, divergent search is outperformed by models with a strong bias toward the evaluation tasks. But it is able to match and sometimes exceed the performance of models that have a weak bias toward the target task or none at all. This demonstrates that divergent search is a viable approach, even in high-dimensional behavior spaces.
Beyond Tree Embeddings -- a Deterministic Framework for Network Design with Deadlines or Delay
Venue: arXiv cs.DS 2020
Year: 2020

We consider network design problems with deadline or delay. All previous results for these models are based on randomized embedding of the graph into a tree (HST) and then solving the problem on this tree. We show that this is not necessary. In particular, we design a deterministic framework for these problems which is not based on embedding. This enables us to provide deterministic $\text{poly-log}(n)$-competitive algorithms for Steiner tree, generalized Steiner tree, node weighted Steiner tree, (non-uniform) facility location and directed Steiner tree with deadlines or with delay (where $n$ is the number of nodes). Our deterministic algorithms also give improved guarantees over some previous randomized results. In addition, we show a lower bound of $\text{poly-log}(n)$ for some of these problems, which implies that our framework is optimal up to the power of the poly-log. Our algorithms and techniques differ significantly from those in all previous considerations of these problems.
A Resource Allocation and Coordinated Transmission Scheme for Large Cellular Networks
Venue: arXiv cs.NI 2020
Year: 2020

With the increasing number of user equipment (UE) and data demands, denser access points (APs) are being employed. Resource allocation problems have been extensively researched with interference treated as noise. It is well understood that the overall spectral efficiency can be significantly improved if multiple terminals coordinate their transmissions either coherently or non-coherently.The focus of this paper is to study how to select pairs of APs for coordination and allocate resources accordingly. An optimization problem is formulated to maximize the network utility function by optimizing AP paring, spectrum allocation, user association, and power management in a flexible manner. A scalable and efficient algorithm is proposed based on iterative scheme pursuit and fractional programming. Numerical results demonstrate substantial gains in the network utility due to coordinated transmission in a network of 128 APs and 384 UE.
CrossCheck: Rapid, Reproducible, and Interpretable Model Evaluation
Venue: arXiv cs.HC 2020
Year: 2020

Evaluation beyond aggregate performance metrics, e.g. F1-score, is crucial to both establish an appropriate level of trust in machine learning models and identify future model improvements. In this paper we demonstrate CrossCheck, an interactive visualization tool for rapid crossmodel comparison and reproducible error analysis. We describe the tool and discuss design and implementation details. We then present three use cases (named entity recognition, reading comprehension, and clickbait detection) that show the benefits of using the tool for model evaluation. CrossCheck allows data scientists to make informed decisions to choose between multiple models, identify when the models are correct and for which examples, investigate whether the models are making the same mistakes as humans, evaluate models' generalizability and highlight models' limitations, strengths and weaknesses. Furthermore, CrossCheck is implemented as a Jupyter widget, which allows rapid and convenient integration into data scientists' model development workflows.
A generic ensemble based deep convolutional neural network for semi-supervised medical image segmentation
Venue: arXiv cs.CV 2020
Year: 2020

Deep learning based image segmentation has achieved the state-of-the-art performance in many medical applications such as lesion quantification, organ detection, etc. However, most of the methods rely on supervised learning, which require a large set of high-quality labeled data. Data annotation is generally an extremely time-consuming process. To address this problem, we propose a generic semi-supervised learning framework for image segmentation based on a deep convolutional neural network (DCNN). An encoder-decoder based DCNN is initially trained using a few annotated training samples. This initially trained model is then copied into sub-models and improved iteratively using random subsets of unlabeled data with pseudo labels generated from models trained in the previous iteration. The number of sub-models is gradually decreased to one in the final iteration. We evaluate the proposed method on a public grand-challenge dataset for skin lesion segmentation. Our method is able to significantly improve beyond fully supervised model learning by incorporating unlabeled data.
Efficient Constrained Pattern Mining Using Dynamic Item Ordering for Explainable Classification
Venue: arXiv cs.DB 2020
Year: 2020

Learning of interpretable classification models has been attracting much attention for the last few years. Discovery of succinct and contrasting patterns that can highlight the differences between the two classes is very important. Such patterns are useful for human experts, and can be used to construct powerful classifiers. In this paper, we consider mining of minimal emerging patterns from high-dimensional data sets under a variety of constraints in a supervised setting. We focus on an extension in which patterns can contain negative items that designate the absence of an item. In such a case, a database becomes highly dense, and it makes mining more challenging since popular pattern mining techniques such as fp-tree and occurrence deliver do not efficiently work. To cope with this difficulty, we present an efficient algorithm for mining minimal emerging patterns by combining two techniques: dynamic variable-ordering during pattern search for enhancing pruning effect, and the use of a pointer-based dynamic data structure, called dancing links, for efficiently maintaining occurrence lists. Experiments on benchmark data sets showed that our algorithm achieves significant speed-ups over emerging pattern mining approach based on LCM, a very fast depth-first frequent itemset miner using static variable-ordering.
AlloVera: A Multilingual Allophone Database
Venue: arXiv cs.CL 2020
Year: 2020

We introduce a new resource, AlloVera, which provides mappings from 218 allophones to phonemes for 14 languages. Phonemes are contrastive phonological units, and allophones are their various concrete realizations, which are predictable from phonological context. While phonemic representations are language specific, phonetic representations (stated in terms of (allo)phones) are much closer to a universal (language-independent) transcription. AlloVera allows the training of speech recognition models that output phonetic transcriptions in the International Phonetic Alphabet (IPA), regardless of the input language. We show that a "universal" allophone model, Allosaurus, built with AlloVera, outperforms "universal" phonemic models and language-specific models on a speech-transcription task. We explore the implications of this technology (and related technologies) for the documentation of endangered and minority languages. We further explore other applications for which AlloVera will be suitable as it grows, including phonological typology.
Contention Resolution Without Collision Detection
Venue: arXiv cs.DS 2020
Year: 2020

This paper focuses on the contention resolution problem on a shared communication channel that does not support collision detection. A shared communication channel is a multiple access channel, which consists of a sequence of synchronized time slots. Players on the channel may attempt to broadcast a packet (message) in any time slot. A player's broadcast succeeds if no other player broadcasts during that slot. If two or more players broadcast in the same time slot, then the broadcasts collide and both broadcasts fail. The lack of collision detection means that a player monitoring the channel cannot differentiate between the case of two or more players broadcasting in the same slot (a collision) and zero players broadcasting. In the contention-resolution problem, players arrive on the channel over time, and each player has one packet to transmit. The goal is to coordinate the players so that each player is able to successfully transmit its packet within reasonable time. However, the players can only communicate via the shared channel by choosing to either broadcast or not. A contention-resolution protocol is measured in terms of its throughput (channel utilization). Previous work on contention resolution that achieved constant throughput assumed that either players could detect collisions, or the players' arrival pattern is generated by a memoryless (non-adversarial) process. The foundational question answered by this paper is whether collision detection is a luxury or necessity when the objective is to achieve constant throughput. We show that even without collision detection, one can solve contention resolution, achieving constant throughput, with high probability.
Diversity-based Design Assist for Large Legged Robots
Venue: arXiv cs.NE 2020
Year: 2020

We combine MAP-Elites and highly parallelisable simulation to explore the design space of a class of large legged robots, which stand at around 2m tall and whose design and construction is not well-studied. The simulation is modified to account for factors such as motor torque and weight, and presents a reasonable fidelity search space. A novel robot encoding allows for bio-inspired features such as legs scaling along the length of the body. The impact of three possible control generation schemes are assessed in the context of body-brain co-evolution, showing that even constrained problems benefit strongly from coupling-promoting mechanisms. A two stage process in implemented. In the first stage, a library of possible robots is generated, treating user requirements as constraints. In the second stage, the most promising robot niches are analysed and a suite of human-understandable design rules generated related to the values of their feature variables. These rules, together with the library, are then ready to be used by a (human) robot designer as a Design Assist tool.
Intention as Commitment toward Time
Venue: arXiv cs.LO 2020
Year: 2020

In this paper we address the interplay among intention, time, and belief in dynamic environments. The first contribution is a logic for reasoning about intention, time and belief, in which assumptions of intentions are represented by preconditions of intended actions. Intentions and beliefs are coherent as long as these assumptions are not violated, i.e. as long as intended actions can be performed such that their preconditions hold as well. The second contribution is the formalization of what-if scenarios: what happens with intentions and beliefs if a new (possibly conflicting) intention is adopted, or a new fact is learned? An agent is committed to its intended actions as long as its belief-intention database is coherent. We conceptualize intention as commitment toward time and we develop AGM-based postulates for the iterated revision of belief-intention databases, and we prove a Katsuno-Mendelzon-style representation theorem.
Accelerating Physics-Informed Neural Network Training with Prior Dictionaries
Venue: arXiv cs.LG 2020
Year: 2020

Physics-Informed Neural Networks (PINNs) can be regarded as general-purpose PDE solvers, but it might be slow to train PINNs on particular problems, and there is no theoretical guarantee of corresponding error bounds. In this manuscript, we propose a variant called Prior Dictionary based Physics-Informed Neural Networks (PD-PINNs). Equipped with task-dependent dictionaries, PD-PINNs enjoy enhanced representation power on the tasks, which helps to capture features provided by dictionaries so that the proposed neural networks can achieve faster convergence in the process of training. In various numerical simulations, compared with existing PINN methods, combining prior dictionaries can significantly enhance convergence speed. In terms of theory, we obtain the error bounds applicable to PINNs and PD-PINNs for solving elliptic partial differential equations of second order. It is proved that under certain mild conditions, the prediction error made by neural networks can be bounded by expected loss of PDEs and boundary conditions.
The FaceChannel: A Light-weight Deep Neural Network for Facial Expression Recognition
Venue: arXiv cs.CV 2020
Year: 2020

Current state-of-the-art models for automatic FER are based on very deep neural networks that are difficult to train. This makes it challenging to adapt these models to changing conditions, a requirement from FER models given the subjective nature of affect perception and understanding. In this paper, we address this problem by formalizing the FaceChannel, a light-weight neural network that has much fewer parameters than common deep neural networks. We perform a series of experiments on different benchmark datasets to demonstrate how the FaceChannel achieves a comparable, if not better, performance, as compared to the current state-of-the-art in FER.
Women worry about family, men about the economy: Gender differences in emotional responses to COVID-19
Venue: arXiv cs.CL 2020
Year: 2020

Among the critical challenges around the COVID-19 pandemic is dealing with the potentially detrimental effects on people's mental health. Designing appropriate interventions and identifying the concerns of those most at risk requires methods that can extract worries, concerns and emotional responses from text data. We examine gender differences and the effect of document length on worries about the ongoing COVID-19 situation. Our findings suggest that i) short texts do not offer as adequate insights into psychological processes as longer texts. We further find ii) marked gender differences in topics concerning emotional responses. Women worried more about their loved ones and severe health concerns while men were more occupied with effects on the economy and society. This paper adds to the understanding of general gender differences in language found elsewhere, and shows that the current unique circumstances likely amplified these effects. We close this paper with a call for more high-quality datasets due to the limitations of Tweet-sized data.