OpenRaiser/Intern-Atlas huggingface dataset:
Distributed Computation in Node-Capacitated Networks
Venue: arXiv cs.DC 2019
Year: 2019

In this paper, we study distributed graph algorithms in networks in which the nodes have a limited communication capacity. Many distributed systems are built on top of an underlying networking infrastructure, for example by using a virtual communication topology known as an overlay network. Although this underlying network might allow each node to directly communicate with a large number of other nodes, the amount of communication that a node can perform in a fixed amount of time is typically much more limited. We introduce the Node-Capacitated Clique model as an abstract communication model, which allows us to study the effect of nodes having limited communication capacity on the complexity of distributed graph computations. In this model, the $n$ nodes of a network are connected as a clique and communicate in synchronous rounds. In each round, every node can exchange messages of $O(\log n)$ bits with at most $O(\log n)$ other nodes. When solving a graph problem, the input graph $G$ is defined on the same set of $n$ nodes, where each node knows which other nodes are its neighbors in $G$. To initiate research on the Node-Capacitated Clique model, we present distributed algorithms for the Minimum Spanning Tree (MST), BFS Tree, Maximal Independent Set, Maximal Matching, and Vertex Coloring problems. We show that even with only $O(\log n)$ concurrent interactions per node, the MST problem can still be solved in polylogarithmic time. In all other cases, the runtime of our algorithms depends linearly on the arboricity of $G$, which is a constant for many important graph families such as planar graphs.
DeepLogic: Towards End-to-End Differentiable Logical Reasoning
Venue: arXiv cs.NE 2019
Year: 2019

Combining machine learning with logic-based expert systems in order to get the best of both worlds are becoming increasingly popular. However, to what extent machine learning can already learn to reason over rule-based knowledge is still an open problem. In this paper, we explore how symbolic logic, defined as logic programs at a character level, is learned to be represented in a high-dimensional vector space using RNN-based iterative neural networks to perform reasoning. We create a new dataset that defines 12 classes of logic programs exemplifying increased level of complexity of logical reasoning and train the networks in an end-to-end fashion to learn whether a logic program entails a given query. We analyse how learning the inference algorithm gives rise to representations of atoms, literals and rules within logic programs and evaluate against increasing lengths of predicate and constant symbols as well as increasing steps of multi-hop reasoning.
Model Aggregation via Good-Enough Model Spaces
Venue: arXiv cs.LG 2019
Year: 2019

In many applications, the training data for a machine learning task is partitioned across multiple nodes, and aggregating this data may be infeasible due to communication, privacy, or storage constraints. Existing distributed optimization methods for learning global models in these settings typically aggregate local updates from each node in an iterative fashion. However, these approaches require many rounds of communication between nodes, and assume that updates can be synchronously shared across a connected network. In this work, we present Good-Enough Model Spaces (GEMS), a novel framework for learning a global model by carefully intersecting the sets of "good-enough" models across each node. Our approach utilizes minimal communication and does not require sharing of data between nodes. We present methods for learning both convex models and neural networks within this framework and discuss how small samples of held-out data can be used for post-learning fine-tuning. In experiments on image and medical datasets, our approach on average improves upon other baseline aggregation techniques such as ensembling or model averaging by as much as 15 points (accuracy).
Improving Aspect Term Extraction with Bidirectional Dependency Tree Representation
Venue: arXiv cs.CL 2019
Year: 2019

Aspect term extraction is one of the important subtasks in aspect-based sentiment analysis. Previous studies have shown that using dependency tree structure representation is promising for this task. However, most dependency tree structures involve only one directional propagation on the dependency tree. In this paper, we first propose a novel bidirectional dependency tree network to extract dependency structure features from the given sentences. The key idea is to explicitly incorporate both representations gained separately from the bottom-up and top-down propagation on the given dependency syntactic tree. An end-to-end framework is then developed to integrate the embedded representations and BiLSTM plus CRF to learn both tree-structured and sequential features to solve the aspect term extraction problem. Experimental results demonstrate that the proposed model outperforms state-of-the-art baseline models on four benchmark SemEval datasets.
One Monad to Prove Them All
Venue: arXiv cs.PL 2019
Year: 2019

One Monad to Prove Them All is a modern fairy tale about curiosity and perseverance, two important properties of a successful PhD student. We follow the PhD student Mona on her adventure of proving properties about Haskell programs in the proof assistant Coq. On the one hand, as a PhD student in computer science Mona observes an increasing demand for correct software products. In particular, because of the large amount of existing software, verifying existing software products becomes more important. Verifying programs in the functional programming language Haskell is no exception. On the other hand, Mona is delighted to see that communities in the area of theorem proving are becoming popular. Thus, Mona sets out to learn more about the interactive theorem prover Coq and verifying Haskell programs in Coq. To prove properties about a Haskell function in Coq, Mona has to translate the function into Coq code. As Coq programs have to be total and Haskell programs are often not, Mona has to model partiality explicitly in Coq. In her quest for a solution Mona finds an ancient manuscript that explains how properties about Haskell functions can be proven in the proof assistant Agda by translating Haskell programs into monadic Agda programs. By instantiating the monadic program with a concrete monad instance the proof can be performed in either a total or a partial setting. Mona discovers that the proposed transformation does not work in Coq due to a restriction in the termination checker. In fact the transformation does not work in Agda anymore as well, as the termination checker in Agda has been improved. We follow Mona on an educational journey through the land of functional programming where she learns about concepts like free monads and containers as well as basics and restrictions of proof assistants like Coq. These concepts are well-known individually, but their interplay gives rise to a solution for Mona's problem based on the originally proposed monadic tranformation that has not been presented before. When Mona starts to test her approach by proving a statement about simple Haskell functions, she realizes that her approach has an additional advantage over the original idea in Agda. Mona's final solution not only works for a specific monad instance but even allows her to prove monad-generic properties. Instead of proving properties over and over again for specific monad instances she is able to prove properties that hold for all monads representable by a container-based instance of the free monad. In order to strengthen her confidence in the practicability of her approach, Mona evaluates her approach in a case study that compares two implementations for queues. In order to share the results with other functional programmers the fairy tale is available as a literate Coq file. If you are a citizen of the land of functional programming or are at least familiar with its customs, had a journey that involved reasoning about functional programs of your own, or are just a curious soul looking for the next story about monads and proofs, then this tale is for you.
On profitability of selfish mining
Venue: arXiv cs.GT 2019
Year: 2019

We review the so called selfish mining strategy in the Bitcoin network and compare its profitability to honest mining.We build a rigorous profitability model for repetition games. The time analysis of the attack has been ignored in the previous literature based on a Markov model,but is critical. Using martingale's techniques and Doob Stopping Time Theorem we compute the expected duration of attack cycles. We discover a remarkable property of the bitcoin network: no strategy is more profitable than the honest strategy before a difficulty adjustment. So selfish mining can only become profitable afterwards, thus it is an attack on the difficulty adjustment algorithm. We propose an improvement of Bitcoin protocol making it immune to selfish mining attacks. We also study miner's attraction to selfish mining pools. We calculate the expected duration time before profit for the selfish miner, a computation that is out of reach by the previous Markov models.
Resilient consensus for multi-agent systems subject to differential privacy requirements
Venue: arXiv cs.SY 2019
Year: 2019

We consider multi-agent systems interacting over directed network topologies where a subset of agents is adversary/faulty and where the non-faulty agents have the goal of reaching consensus, while fulfilling a differential privacy requirement on their initial conditions. To address this problem, we develop an update law for the non-faulty agents. Specifically, we propose a modification of the so-called Mean-Subsequence-Reduced (MSR) algorithm, the Differentially Private MSR (DP-MSR) algorithm, and characterize three important properties of the algorithm: correctness, accuracy and differential privacy. We show that if the network topology is $(2f +1)$-robust, then the algorithm allows the non-faulty agents to reach consensus despite the presence of up to $f$ faulty agents and we characterize the accuracy of the algorithm. Furthermore, we also show in two important cases that our distributed algorithm can be tuned to guarantees differential privacy of the initial conditions and the differential privacy requirement is related to the maximum network degree. The results are illustrated via simulations.
A 2D laser rangefinder scans dataset of standard EUR pallets
Venue: arXiv cs.RO 2019
Year: 2019

In the past few years, the technology of automated guided vehicles (AGVs) has notably advanced. In particular, in the context of factory and warehouse automation, different approaches have been presented for detecting and localizing pallets inside warehouses and shop-floor environments. In a related research paper [1], we show that an AGVs can detect, localize, and track pallets using machine learning techniques based only on the data of an on-board 2D laser rangefinder. Such sensor is very common in industrial scenarios due to its simplicity and robustness, but it can only provide a limited amount of data. Therefore, it has been neglected in the past in favor of more complex solutions. In this paper, we release to the community the data we collected in [1] for further research activities in the field of pallet localization and tracking. The dataset comprises a collection of 565 2D scans from real-world environments, which are divided into 340 samples where pallets are present, and 225 samples where they are not. The data have been manually labelled and are provided in different formats.
On the Worst-Case Complexity of TimSort
Venue: arXiv cs.DS 2019
Year: 2019

TimSort is an intriguing sorting algorithm designed in 2002 for Python, whose worst-case complexity was announced, but not proved until our recent preprint. In fact, there are two slightly different versions of TimSort that are currently implemented in Python and in Java respectively. We propose a pedagogical and insightful proof that the Python version runs in $\mathcal{O}(n\log n)$. The approach we use in the analysis also applies to the Java version, although not without very involved technical details. As a byproduct of our study, we uncover a bug in the Java implementation that can cause the sorting method to fail during the execution. We also give a proof that Python's TimSort running time is in $\mathcal{O}(n + n\log ρ)$, where $ρ$ is the number of runs (i.e. maximal monotonic sequences), which is quite a natural parameter here and part of the explanation for the good behavior of TimSort on partially sorted inputs.
Complexity of Stability in Trading Networks
Venue: arXiv cs.CC 2019
Year: 2019

Efficient computability is an important property of solution concepts in matching markets. We consider the computational complexity of finding and verifying various solution concepts in trading networks-multi-sided matching markets with bilateral contracts-under the assumption of full substitutability of agents' preferences. It is known that outcomes that satisfy trail stability always exist and can be found in linear time. Here we consider a slightly stronger solution concept in which agents can simultaneously offer an upstream and a downstream contract. We show that deciding the existence of outcomes satisfying this solution concept is an NP-complete problem even in a special (flow network) case of our model. It follows that the existence of stable outcomes--immune to deviations by arbitrary sets of agents-is also an NP-hard problem in trading networks (and in flow networks). Finally, we show that even verifying whether a given outcome is stable is NP-complete in trading networks.
Approximate Newton-based statistical inference using only stochastic gradients
Venue: arXiv cs.LG 2019
Year: 2019

We present a novel statistical inference framework for convex empirical risk minimization, using approximate stochastic Newton steps. The proposed algorithm is based on the notion of finite differences and allows the approximation of a Hessian-vector product from first-order information. In theory, our method efficiently computes the statistical error covariance in $M$-estimation, both for unregularized convex learning problems and high-dimensional LASSO regression, without using exact second order information, or resampling the entire data set. We also present a stochastic gradient sampling scheme for statistical inference in non-i.i.d. time series analysis, where we sample contiguous blocks of indices. In practice, we demonstrate the effectiveness of our framework on large-scale machine learning problems, that go even beyond convexity: as a highlight, our work can be used to detect certain adversarial attacks on neural networks.
Amortized Context Vector Inference for Sequence-to-Sequence Networks
Venue: arXiv cs.LG 2019
Year: 2019

Neural attention (NA) has become a key component of sequence-to-sequence models that yield state-of-the-art performance in as hard tasks as abstractive document summarization (ADS) and video captioning (VC). NA mechanisms perform inference of context vectors; these constitute weighted sums of deterministic input sequence encodings, adaptively sourced over long temporal horizons. Inspired from recent work in the field of amortized variational inference (AVI), in this work we consider treating the context vectors generated by soft-attention (SA) models as latent variables, with approximate finite mixture model posteriors inferred via AVI. We posit that this formulation may yield stronger generalization capacity, in line with the outcomes of existing applications of AVI to deep networks. To illustrate our method, we implement it and experimentally evaluate it considering challenging ADS, VC, and MT benchmarks. This way, we exhibit its improved effectiveness over state-of-the-art alternatives.
Cramer-Wold AutoEncoder
Venue: arXiv cs.LG 2019
Year: 2019

We propose a new generative model, Cramer-Wold Autoencoder (CWAE). Following WAE, we directly encourage normality of the latent space. Our paper uses also the recent idea from Sliced WAE (SWAE) model, which uses one-dimensional projections as a method of verifying closeness of two distributions. The crucial new ingredient is the introduction of a new (Cramer-Wold) metric in the space of densities, which replaces the Wasserstein metric used in SWAE. We show that the Cramer-Wold metric between Gaussian mixtures is given by a simple analytic formula, which results in the removal of sampling necessary to estimate the cost function in WAE and SWAE models. As a consequence, while drastically simplifying the optimization procedure, CWAE produces samples of a matching perceptual quality to other SOTA models.
Decentralized MPC based Obstacle Avoidance for Multi-Robot Target Tracking Scenarios
Venue: arXiv cs.RO 2019
Year: 2019

In this work, we consider the problem of decentralized multi-robot target tracking and obstacle avoidance in dynamic environments. Each robot executes a local motion planning algorithm which is based on model predictive control (MPC). The planner is designed as a quadratic program, subject to constraints on robot dynamics and obstacle avoidance. Repulsive potential field functions are employed to avoid obstacles. The novelty of our approach lies in embedding these non-linear potential field functions as constraints within a convex optimization framework. Our method convexifies non-convex constraints and dependencies, by replacing them as pre-computed external input forces in robot dynamics. The proposed algorithm additionally incorporates different methods to avoid field local minima problems associated with using potential field functions in planning. The motion planner does not enforce predefined trajectories or any formation geometry on the robots and is a comprehensive solution for cooperative obstacle avoidance in the context of multi-robot target tracking. We perform simulation studies in different environmental scenarios to showcase the convergence and efficacy of the proposed algorithm. Video of simulation studies: \url{https://youtu.be/umkdm82Tt0M}
Learning compositionally through attentive guidance
Venue: arXiv cs.CL 2019
Year: 2019

While neural network models have been successfully applied to domains that require substantial generalisation skills, recent studies have implied that they struggle when solving the task they are trained on requires inferring its underlying compositional structure. In this paper, we introduce Attentive Guidance, a mechanism to direct a sequence to sequence model equipped with attention to find more compositional solutions. We test it on two tasks, devised precisely to assess the compositional capabilities of neural models, and we show that vanilla sequence to sequence models with attention overfit the training distribution, while the guided versions come up with compositional solutions that fit the training and testing distributions almost equally well. Moreover, the learned solutions generalise even in cases where the training and testing distributions strongly diverge. In this way, we demonstrate that sequence to sequence models are capable of finding compositional solutions without requiring extra components. These results helps to disentangle the causes for the lack of systematic compositionality in neural networks, which can in turn fuel future work.
Checking Deadlock-Freedom of Parametric Component-Based Systems
Venue: arXiv cs.LO 2019
Year: 2019

We propose an automated method for computing inductive invariants applied to check deadlock-freedom for parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from a monadic interaction formula characterizing the system architecture. The paper presents the theoretical foundations of the method including new results for the first order monadic logic and proves its soundness. It also provides preliminary illustrations on examples.
A Double-Deep Spatio-Angular Learning Framework for Light Field based Face Recognition
Venue: arXiv cs.CV 2019
Year: 2019

Face recognition has attracted increasing attention due to its wide range of applications, but it is still challenging when facing large variations in the biometric data characteristics. Lenslet light field cameras have recently come into prominence to capture rich spatio-angular information, thus offering new possibilities for advanced biometric recognition systems. This paper proposes a double-deep spatio-angular learning framework for light field based face recognition, which is able to learn both texture and angular dynamics in sequence using convolutional representations; this is a novel recognition framework that has never been proposed before for either face recognition or any other visual recognition task. The proposed double-deep learning framework includes a long short-term memory (LSTM) recurrent network whose inputs are VGG-Face descriptions that are computed using a VGG-Very-Deep-16 convolutional neural network (CNN). The VGG-16 network uses different face viewpoints rendered from a full light field image, which are organised as a pseudo-video sequence. A comprehensive set of experiments has been conducted with the IST-EURECOM light field face database, for varied and challenging recognition tasks. Results show that the proposed framework achieves superior face recognition performance when compared to the state-of-the-art.
Ergodic Inference: Accelerate Convergence by Optimisation
Venue: arXiv cs.LG 2019
Year: 2019

Statistical inference methods are fundamentally important in machine learning. Most state-of-the-art inference algorithms are variants of Markov chain Monte Carlo (MCMC) or variational inference (VI). However, both methods struggle with limitations in practice: MCMC methods can be computationally demanding; VI methods may have large bias. In this work, we aim to improve upon MCMC and VI by a novel hybrid method based on the idea of reducing simulation bias of finite-length MCMC chains using gradient-based optimisation. The proposed method can generate low-biased samples by increasing the length of MCMC simulation and optimising the MCMC hyper-parameters, which offers attractive balance between approximation bias and computational efficiency. We show that our method produces promising results on popular benchmarks when compared to recent hybrid methods of MCMC and VI.