OpenRaiser/Intern-Atlas huggingface dataset:
On the Existence of a Sample Mean in Dynamic Time Warping Spaces
Venue: arXiv cs.CV 2018
Year: 2018

The concept of sample mean in dynamic time warping (DTW) spaces has been successfully applied to improve pattern recognition systems and generalize centroid-based clustering algorithms. Its existence has neither been proved nor challenged. This article presents sufficient conditions for existence of a sample mean in DTW spaces. The proposed result justifies prior work on approximate mean algorithms, sets the stage for constructing exact mean algorithms, and is a first step towards a statistical theory of DTW spaces.
Feasibility Based Large Margin Nearest Neighbor Metric Learning
Venue: arXiv cs.DS 2018
Year: 2018

Large margin nearest neighbor (LMNN) is a metric learner which optimizes the performance of the popular $k$NN classifier. However, its resulting metric relies on pre-selected target neighbors. In this paper, we address the feasibility of LMNN's optimization constraints regarding these target points, and introduce a mathematical measure to evaluate the size of the feasible region of the optimization problem. We enhance the optimization framework of LMNN by a weighting scheme which prefers data triplets which yield a larger feasible region. This increases the chances to obtain a good metric as the solution of LMNN's problem. We evaluate the performance of the resulting feasibility-based LMNN algorithm using synthetic and real datasets. The empirical results show an improved accuracy for different types of datasets in comparison to regular LMNN.
K-clique-graphs for Dense Subgraph Discovery
Venue: arXiv cs.DS 2018
Year: 2018

Finding dense subgraphs in a graph is a fundamental graph mining task, with applications in several fields. Algorithms for identifying dense subgraphs are used in biology, in finance, in spam detection, etc. Standard formulations of this problem such as the problem of finding the maximum clique of a graph are hard to solve. However, some tractable formulations of the problem have also been proposed, focusing mainly on optimizing some density function, such as the degree density and the triangle density. However, maximization of degree density usually leads to large subgraphs with small density. In this paper, we introduce the k-clique-graph densest subgraph problem, k >= 3, a novel formulation for the discovery of dense subgraphs. Given an input graph, its k-clique-graph is a new graph created from the input graph where each vertex of the new graph corresponds to a k-clique of the input graph and two vertices are connected with an edge if they share a common (k-1)-clique. We define a simple density function, the k-clique-graph density, which gives compact and at the same time dense subgraphs, and we project its resulting subgraphs back to the input graph. In this paper we focus on the triangle-graph densest subgraph problem obtained for k=3. To optimize the proposed function, we present an efficient greedy approximation algorithm that scales well to larger graphs. We evaluate the proposed algorithm on real datasets and compare it with other algorithms in terms of the size and the density of the extracted subgraphs. The results verify the ability of the proposed algorithm in finding high-quality subgraphs in terms of size and density. Finally, we apply the proposed method to the important problem of keyword extraction from textual documents.
Representing permutations without permutations, or the expressive power of sequence types
Venue: arXiv cs.LO 2018
Year: 2018

Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduction paths and their effects on e.g., typing derivations. We previously introduced a very constrained coinductive type system (system S) in which permutation is completely disallowed. One may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths, compared to a usual multiset framework or a rigid one allowing permutations. We answer this question in the most general case i.e. coinductive type grammars without validity conditions. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid, permutation-free derivation, but also that any dynamic behavior may be captured in this way. In other words, we prove that system S has full expressive power over multiset/permutation-inclusive intersection.
Iterative Refinement for Machine Translation
Venue: arXiv cs.CL 2018
Year: 2018

Existing machine translation decoding algorithms generate translations in a strictly monotonic fashion and never revisit previous decisions. As a result, earlier mistakes cannot be corrected at a later stage. In this paper, we present a translation scheme that starts from an initial guess and then makes iterative improvements that may revisit previous decisions. We parameterize our model as a convolutional neural network that predicts discrete substitutions to an existing translation based on an attention mechanism over both the source sentence as well as the current translation output. By making less than one modification per sentence, we improve the output of a phrase-based translation system by up to 0.4 BLEU on WMT15 German-English translation.
Efficient verification of imperative programs using auto2
Venue: arXiv cs.LO 2018
Year: 2018

Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the setup of auto2 for both stages of the proof process: verification of a functional version of the program, and refining to the imperative version using separation logic. As examples, we verify several data structures, including red-black trees, interval trees, priority queues, and union-find. We also verify several algorithms making use of these data structures. These examples show that our framework is able to verify complex algorithms efficiently and in a modular manner.
DeepSpace: An Online Deep Learning Framework for Mobile Big Data to Understand Human Mobility Patterns
Venue: arXiv cs.CY 2018
Year: 2018

In the recent years, the rapid spread of mobile device has create the vast amount of mobile data. However, some shallow-structure models such as support vector machine (SVM) have difficulty dealing with high dimensional data with the development of mobile network. In this paper, we analyze mobile data to predict human trajectories in order to understand human mobility pattern via a deep-structure model called "DeepSpace". To the best of out knowledge, it is the first time that the deep learning approach is applied to predicting human trajectories. Furthermore, we develop the vanilla convolutional neural network (CNN) to be an online learning system, which can deal with the continuous mobile data stream. In general, "DeepSpace" consists of two different prediction models corresponding to different scales in space (the coarse prediction model and fine prediction models). This two models constitute a hierarchical structure, which enable the whole architecture to be run in parallel. Finally, we test our model based on the data usage detail records (UDRs) from the mobile cellular network in a city of southeastern China, instead of the call detail records (CDRs) which are widely used by others as usual. The experiment results show that "DeepSpace" is promising in human trajectories prediction.
pg-Causality: Identifying Spatiotemporal Causal Pathways for Air Pollutants with Urban Big Data
Venue: arXiv cs.AI 2018
Year: 2018

Many countries are suffering from severe air pollution. Understanding how different air pollutants accumulate and propagate is critical to making relevant public policies. In this paper, we use urban big data (air quality data and meteorological data) to identify the \emph{spatiotemporal (ST) causal pathways} for air pollutants. This problem is challenging because: (1) there are numerous noisy and low-pollution periods in the raw air quality data, which may lead to unreliable causality analysis, (2) for large-scale data in the ST space, the computational complexity of constructing a causal structure is very high, and (3) the \emph{ST causal pathways} are complex due to the interactions of multiple pollutants and the influence of environmental factors. Therefore, we present \emph{p-Causality}, a novel pattern-aided causality analysis approach that combines the strengths of \emph{pattern mining} and \emph{Bayesian learning} to efficiently and faithfully identify the \emph{ST causal pathways}. First, \emph{Pattern mining} helps suppress the noise by capturing frequent evolving patterns (FEPs) of each monitoring sensor, and greatly reduce the complexity by selecting the pattern-matched sensors as "causers". Then, \emph{Bayesian learning} carefully encodes the local and ST causal relations with a Gaussian Bayesian network (GBN)-based graphical model, which also integrates environmental influences to minimize biases in the final results. We evaluate our approach with three real-world data sets containing 982 air quality sensors, in three regions of China from 01-Jun-2013 to 19-Dec-2015. Results show that our approach outperforms the traditional causal structure learning methods in time efficiency, inference accuracy and interpretability.
Encoding Temporal Markov Dynamics in Graph for Visualizing and Mining Time Series
Venue: arXiv cs.LG 2018
Year: 2018

Time series and signals are attracting more attention across statistics, machine learning and pattern recognition as it appears widely in the industry especially in sensor and IoT related research and applications, but few advances has been achieved in effective time series visual analytics and interaction due to its temporal dimensionality and complex dynamics. Inspired by recent effort on using network metrics to characterize time series for classification, we present an approach to visualize time series as complex networks based on the first order Markov process in its temporal ordering. In contrast to the classical bar charts, line plots and other statistics based graph, our approach delivers more intuitive visualization that better preserves both the temporal dependency and frequency structures. It provides a natural inverse operation to map the graph back to raw signals, making it possible to use graph statistics to characterize time series for better visual exploration and statistical analysis. Our experimental results suggest the effectiveness on various tasks such as pattern discovery and classification on both synthetic and the real time series and sensor data.
Neural-like computing with populations of superparamagnetic basis functions
Venue: arXiv cs.ET 2018
Year: 2018

In neuroscience, population coding theory demonstrates that neural assemblies can achieve fault-tolerant information processing. Mapped to nanoelectronics, this strategy could allow for reliable computing with scaled-down, noisy, imperfect devices. Doing so requires that the population components form a set of basis functions in terms of their response functions to inputs, offering a physical substrate for calculating. For this purpose, the responses of the nanodevices should be non-linear, and each tuned to different values of the input. These strong requirements have prevented a demonstration of population coding with nanodevices. Here, we show that nanoscale magnetic tunnel junctions can be assembled to meet these requirements. We demonstrate experimentally that a population of nine junctions can implement a basis set of functions, providing the data to achieve, for example, the generation of cursive letters. We design hybrid magnetic-CMOS systems based on interlinked populations of junctions and show that they can learn to realize non-linear variability-resilient transformations with a low imprint area and low power.
An Experimental Survey on Big Data Frameworks
Venue: arXiv cs.DC 2018
Year: 2018

Recently, increasingly large amounts of data are generated from a variety of sources. Existing data processing technologies are not suitable to cope with the huge amounts of generated data. Yet, many research works focus on Big Data, a buzzword referring to the processing of massive volumes of (unstructured) data. Recently proposed frameworks for Big Data applications help to store, analyze and process the data. In this paper, we discuss the challenges of Big Data and we survey existing Big Data frameworks. We also present an experimental evaluation and a comparative study of the most popular Big Data frameworks. This survey is concluded with a presentation of best practices related to the use of the studied frameworks in several application domains such as machine learning, graph processing and real-world applications.
Symmetry, Outer Bounds, and Code Constructions: A Computer-Aided Investigation on the Fundamental Limits of Caching
Venue: arXiv cs.IT 2018
Year: 2018

We illustrate how computer-aided methods can be used to investigate the fundamental limits of the caching systems, which are significantly different from the conventional analytical approach usually seen in the information theory literature. The linear programming (LP) outer bound of the entropy space serves as the starting point of this approach; however, our effort goes significantly beyond using it to prove information inequalities. We first identify and formalize the symmetry structure in the problem, which enables us to show the existence of optimal symmetric solutions. A symmetry-reduced linear program is then used to identify the boundary of the memory-transmission-rate tradeoff for several small cases, for which we obtain a set of tight outer bounds. General hypotheses on the optimal tradeoff region are formed from these computed data, which are then analytically proven. This leads to a complete characterization of the optimal tradeoff for systems with only two users, and certain partial characterization for systems with only two files. Next, we show that by carefully analyzing the joint entropy structure of the outer bounds for certain cases, a novel code construction can be reverse-engineered, which eventually leads to a general class of codes. Finally, we show that outer bounds can be computed through strategically relaxing the LP in different ways, which can be used to explore the problem computationally. This allows us firstly to deduce generic characteristic of the converse proof, and secondly to compute outer bounds for larger problem cases, despite the seemingly impossible computation scale.
Dual Quaternion Variational Integrator for Rigid Body Dynamic Simulation
Venue: arXiv cs.CE 2018
Year: 2018

We introduce a symplectic dual quaternion variational integrator(DQVI) for simulating single rigid body motion in all six degrees of freedom. Dual quaternion is used to represent rigid body kinematics and one-step Lie group variational integrator is used to conserve the geometric structure, energy and momentum of the system during the simulation. The combination of these two becomes the first Lie group variational integrator for rigid body simulation without decoupling translations and rotations. Newton-Raphson method is used to solve the recursive dynamic equation. This method is suitable for real-time rigid body simulations with high precision under large time step. DQVI respects the symplectic structure of the system with excellent long-term conservation of geometry structure, momentum and energy. It also allows the reference point and 6-by-6 inertia matrix to be arbitrarily defined, which is very convenient for a variety of engineering problems.
Spatio-temporal Dynamics of Intrinsic Networks in Functional Magnetic Imaging Data Using Recurrent Neural Networks
Venue: arXiv cs.NE 2018
Year: 2018

We introduce a novel recurrent neural network (RNN) approach to account for temporal dynamics and dependencies in brain networks observed via functional magnetic resonance imaging (fMRI). Our approach directly parameterizes temporal dynamics through recurrent connections, which can be used to formulate blind source separation with a conditional (rather than marginal) independence assumption, which we call RNN-ICA. This formulation enables us to visualize the temporal dynamics of both first order (activity) and second order (directed connectivity) information in brain networks that are widely studied in a static sense, but not well-characterized dynamically. RNN-ICA predicts dynamics directly from the recurrent states of the RNN in both task and resting state fMRI. Our results show both task-related and group-differentiating directed connectivity.
Semi-supervised deep learning by metric embedding
Venue: arXiv cs.LG 2018
Year: 2018

Deep networks are successfully used as classification models yielding state-of-the-art results when trained on a large number of labeled samples. These models, however, are usually much less suited for semi-supervised problems because of their tendency to overfit easily when trained on small amounts of data. In this work we will explore a new training objective that is targeting a semi-supervised regime with only a small subset of labeled data. This criterion is based on a deep metric embedding over distance relations within the set of labeled samples, together with constraints over the embeddings of the unlabeled set. The final learned representations are discriminative in euclidean space, and hence can be used with subsequent nearest-neighbor classification using the labeled samples.
CoCoA: A General Framework for Communication-Efficient Distributed Optimization
Venue: arXiv cs.LG 2018
Year: 2018

The scale of modern datasets necessitates the development of efficient distributed optimization methods for machine learning. We present a general-purpose framework for distributed computing environments, CoCoA, that has an efficient communication scheme and is applicable to a wide variety of problems in machine learning and signal processing. We extend the framework to cover general non-strongly-convex regularizers, including L1-regularized problems like lasso, sparse logistic regression, and elastic net regularization, and show how earlier work can be derived as a special case. We provide convergence guarantees for the class of convex regularized loss minimization objectives, leveraging a novel approach in handling non-strongly-convex regularizers and non-smooth loss functions. The resulting framework has markedly improved performance over state-of-the-art methods, as we illustrate with an extensive set of experiments on real distributed datasets.
Adversarial Ladder Networks
Venue: arXiv cs.NE 2018
Year: 2018

The use of unsupervised data in addition to supervised data in training discriminative neural networks has improved the performance of this clas- sification scheme. However, the best results were achieved with a training process that is divided in two parts: first an unsupervised pre-training step is done for initializing the weights of the network and after these weights are refined with the use of supervised data. On the other hand adversarial noise has improved the results of clas- sical supervised learning. Recently, a new neural network topology called Ladder Network, where the key idea is based in some properties of hierar- chichal latent variable models, has been proposed as a technique to train a neural network using supervised and unsupervised data at the same time with what is called semi-supervised learning. This technique has reached state of the art classification. In this work we add adversarial noise to the ladder network and get state of the art classification, with several important conclusions on how adversarial noise can help in addition with new possible lines of investi- gation. We also propose an alternative to add adversarial noise to unsu- pervised data.
On coalescence time in graphs--When is coalescing as fast as meeting?
Venue: arXiv cs.DM 2018
Year: 2018

Coalescing random walks is a fundamental stochastic process, where a set of particles perform independent discrete-time random walks on an undirected graph. Whenever two or more particles meet at a given node, they merge and continue as a single random walk. The coalescence time is defined as the expected time until only one particle remains, starting from one particle at every node. Despite recent progress the coalescence time for graphs such as binary trees, d-dimensional tori, hypercubes and more generally, vertex-transitive graphs, remains unresolved. We provide a powerful toolkit that results in tight bounds for various topologies including the aforementioned ones. The meeting time is defined as the worst-case expected time required for two random walks to arrive at the same node at the same time. As a general result, we establish that for graphs whose meeting time is only marginally larger than the mixing time (a factor of log^2 n), the coalescence time of n random walks equals the meeting time up to constant factors. This upper bound is complemented by the construction of a graph family demonstrating that this result is the best possible up to constant factors. For almost-regular graphs, we bound the coalescence time by the hitting time, resolving the discrete-time variant of a conjecture by Aldous for this class of graphs. Finally, we prove that for any graph the coalescence time is bounded by O(n^3) (which is tight for the Barbell graph); surprisingly even such a basic question about the coalescing time was not answered before this work. By duality, our results give bounds on the voter model and therefore give bounds on the consensus time in arbitrary undirected graphs. We also establish a new bound on the hitting time and cover time of regular graphs, improving and tightening previous results by Broder and Karlin, as well as those by Aldous and Fill.
Compatibility Properties of Synchronously and Asynchronously Communicating Components
Venue: arXiv cs.LO 2018
Year: 2018

We study interacting components and their compatibility with respect to synchronous and asynchronous composition. The behavior of components is formalized by I/O-transition systems. Synchronous composition is based on simultaneous execution of shared output and input actions of two components while asynchronous composition uses unbounded FIFO-buffers for message transfer. In both contexts we study compatibility notions based on the idea that any output issued by one component should be accepted as an input by the other. We distinguish between strong and weak versions of compatibility, the latter allowing the execution of internal actions before a message is accepted. We consider open systems and study conditions under which (strong/weak) synchronous compatibility is sufficient and necessary to get (strong/weak) asynchronous compatibility. We show that these conditions characterize half-duplex systems. Then we focus on the verification of weak asynchronous compatibility for possibly non half-duplex systems and provide a decidable criterion that ensures weak asynchronous compatibility. We investigate conditions under which this criterion is complete, i.e. if it is not satisfied then the asynchronous system is not weakly asynchronously compatible. Finally, we discuss deadlock-freeness and investigate relationships between deadlock-freeness in the synchronous and in the asynchronous case.