OpenRaiser/Intern-Atlas huggingface dataset:
Verification of Asynchronous Systems with an Unspecified Component
Venue: arXiv cs.FL 2017
Year: 2017

Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.
Mining relevant interval rules
Venue: arXiv cs.AI 2017
Year: 2017

This article extends the method of Garriga et al. for mining relevant rules to numerical attributes by extracting interval-based pattern rules. We propose an algorithm that extracts such rules from numerical datasets using the interval-pattern approach from Kaytoue et al. This algorithm has been implemented and evaluated on real datasets.
On A New Convergence Class in Sup-sober Spaces
Venue: arXiv cs.LO 2017
Year: 2017

Recently, J. D. Lawson encouraged the domain theory community to consider the scientific program of developing domain theory in the wider context of $T_0$-spaces instead of restricting to posets. In this paper, we respond to this calling by proving a topological parallel of a 2005 result due to B. Zhao and D. Zhao, i.e., an order-theoretic characterisation of those posets for which the Scott-convergence is topological. We do this by adopting a recent approach due to D. Zhao and W. K. Ho by replacing directed subsets with irreducible sets. As a result, we formulate a new convergence class $\mathcal{I}$ in $T_0$-spaces called ${\operatorname{Irr}}$-convergence and establish that a sup-sober space $X$ is ${\operatorname{SI}}^{-}$-continuous if and only if it satisfies $*$-property and the convergence class $\mathcal{I}$ in it is topological.
Pilot Optimization and Power Allocation for OFDM-based Full-duplex Relay Networks with IQ-imbalances
Venue: arXiv cs.IT 2017
Year: 2017

In OFDM relay networks with IQ imbalances and full-duplex relay station (RS), how to optimize pilot pattern and power allocation using the criterion of minimizing the sum of mean square errors (Sum-MSE) for the frequency-domain least-squares channel estimator has a heavy impact on self-interference cancellation. Firstly, the design problem of pilot pattern is casted as a convex optimization. From the KKT conditions, the optimal analytical expression is derived given the fixed source power and RS power. Subsequently, an optimal power allocation (OPA) strategy is proposed and presented to further alleviate the effect of Sum-MSE under the total transmit power sum constraint of source node and RS. Simulation results show that the proposed OPA performs better than equal power allocation (EPA) in terms of Sum-MSE, and the Sum-MSE performance gain grows with deviating $ρ$ from the value of $ρ^o$ minimizing the Sum-MSE, where $ρ$ is defined as the average ratio of the residual SI channel at RS to the intended channel from source to RS. For example, the OPA achieves about 5dB SNR gain over EPA by shrinking or stretching $ρ$ with a factor $4$. More importantly, as $ρ$ decreases or increases more, the performance gain becomes more significant.
Low-memory GEMM-based convolution algorithms for deep neural networks
Venue: arXiv cs.CV 2017
Year: 2017

Deep neural networks (DNNs) require very large amounts of computation both for training and for inference when deployed in the field. A common approach to implementing DNNs is to recast the most computationally expensive operations as general matrix multiplication (GEMM). However, as we demonstrate in this paper, there are a great many different ways to express DNN convolution operations using GEMM. Although different approaches all perform the same number of operations, the size of temporary data structures differs significantly. Convolution of an input matrix with dimensions $C \times H \times W$, requires $O(K^2CHW)$ additional space using the classical im2col approach. More recently memory-efficient approaches requiring just $O(KCHW)$ auxiliary space have been proposed. We present two novel GEMM-based algorithms that require just $O(MHW)$ and $O(KW)$ additional space respectively, where $M$ is the number of channels in the result of the convolution. These algorithms dramatically reduce the space overhead of DNN convolution, making it much more suitable for memory-limited embedded systems. Experimental evaluation shows that our low-memory algorithms are just as fast as the best patch-building approaches despite requiring just a fraction of the amount of additional memory. Our low-memory algorithms have excellent data locality which gives them a further edge over patch-building algorithms when multiple cores are used. As a result, our low memory algorithms often outperform the best patch-building algorithms using multiple threads.
Trajectory Synthesis for Fisher Information Maximization
Venue: arXiv cs.RO 2017
Year: 2017

Estimation of model parameters in a dynamic system can be significantly improved with the choice of experimental trajectory. For general, nonlinear dynamic systems, finding globally "best" trajectories is typically not feasible; however, given an initial estimate of the model parameters and an initial trajectory, we present a continuous-time optimization method that produces a locally optimal trajectory for parameter estimation in the presence of measurement noise. The optimization algorithm is formulated to find system trajectories that improve a norm on the Fisher information matrix. A double-pendulum cart apparatus is used to numerically and experimentally validate this technique. In simulation, the optimized trajectory increases the minimum eigenvalue of the Fisher information matrix by three orders of magnitude compared to the initial trajectory. Experimental results show that this optimized trajectory translates to an order of magnitude improvement in the parameter estimate error in practice.
Why Do Deep Neural Networks Still Not Recognize These Images?: A Qualitative Analysis on Failure Cases of ImageNet Classification
Venue: arXiv cs.CV 2017
Year: 2017

In a recent decade, ImageNet has become the most notable and powerful benchmark database in computer vision and machine learning community. As ImageNet has emerged as a representative benchmark for evaluating the performance of novel deep learning models, its evaluation tends to include only quantitative measures such as error rate, rather than qualitative analysis. Thus, there are few studies that analyze the failure cases of deep learning models in ImageNet, though there are numerous works analyzing the networks themselves and visualizing them. In this abstract, we qualitatively analyze the failure cases of ImageNet classification results from recent deep learning model, and categorize these cases according to the certain image patterns. Through this failure analysis, we believe that it can be discovered what the final challenges are in ImageNet database, which the current deep learning model is still vulnerable to.
Combining Strategic Learning and Tactical Search in Real-Time Strategy Games
Venue: arXiv cs.AI 2017
Year: 2017

A commonly used technique for managing AI complexity in real-time strategy (RTS) games is to use action and/or state abstractions. High-level abstractions can often lead to good strategic decision making, but tactical decision quality may suffer due to lost details. A competing method is to sample the search space which often leads to good tactical performance in simple scenarios, but poor high-level planning. We propose to use a deep convolutional neural network (CNN) to select among a limited set of abstract action choices, and to utilize the remaining computation time for game tree search to improve low level tactics. The CNN is trained by supervised learning on game states labelled by Puppet Search, a strategic search algorithm that uses action abstractions. The network is then used to select a script --- an abstract action --- to produce low level actions for all units. Subsequently, the game tree search algorithm improves the tactical actions of a subset of units using a limited view of the game state only considering units close to opponent units. Experiments in the microRTS game show that the combined algorithm results in higher win-rates than either of its two independent components and other state-of-the-art microRTS agents. To the best of our knowledge, this is the first successful application of a convolutional network to play a full RTS game on standard game maps, as previous work has focused on sub-problems, such as combat, or on very small maps.
Finite-state Strategies in Delay Games
Venue: arXiv cs.GT 2017
Year: 2017

What is a finite-state strategy in a delay game? We answer this surprisingly non-trivial question and present a very general framework for computing such strategies: they exist for all winning conditions that are recognized by automata with acceptance conditions that satisfy a certain aggregation property. Our framework also yields upper bounds on the complexity of determining the winner of such delay games and upper bounds on the necessary lookahead to win the game. In particular, we cover all previous results of that kind as special cases of our uniform approach.
Real-Time Multiple Object Tracking - A Study on the Importance of Speed
Venue: arXiv cs.CV 2017
Year: 2017

In this project, we implement a multiple object tracker, following the tracking-by-detection paradigm, as an extension of an existing method. It works by modelling the movement of objects by solving the filtering problem, and associating detections with predicted new locations in new frames using the Hungarian algorithm. Three different similarity measures are used, which use the location and shape of the bounding boxes. Compared to other trackers on the MOTChallenge leaderboard, our method, referred to as C++SORT, is the fastest non-anonymous submission, while also achieving decent score on other metrics. By running our model on the Okutama-Action dataset, sampled at different frame-rates, we show that the performance is greatly reduced when running the model - including detecting objects - in real-time. In most metrics, the score is reduced by 50%, but in certain cases as much as 90%. We argue that this indicates that other, slower methods could not be used for tracking in real-time, but that more research is required specifically on this.
Conceptual Modeling for Control of a Physical Engineering Plant: A Case Study
Venue: arXiv cs.CY 2017
Year: 2017

We examine the problem of weaknesses in frameworks of conceptual modeling for handling certain aspects of the system being modeled. We propose the use of a flow-based modeling methodology at the conceptual level. Specifically, and without loss of generality, we develop a conceptual description that can be used for controlling the maintenance of a physical system, and demonstrate it by applying it to an existing electrical power plant system. Recent studies reveal difficulties in finding comprehensive answers for monitoring operations and identifying risks as well as the fact that incomplete information can easily lead to incorrect maintenance. A unified framework for integrated conceptualization is therefore needed. The conceptual modeling approach integrates maintenance operations into a total system comprising humans, physical objects, and information. The proposed model is constructed of (abstract) machines of things connected by flows, forming an integrated whole. It represents a man-made, intentionally constructed system and includes technical and human things observable in the real world, exemplified by the study case described in this paper. A specification is constructed from a maximum of five basic operations: creation, processing, releasing, transferring, and receiving.
Capturing Long-range Contextual Dependencies with Memory-enhanced Conditional Random Fields
Venue: arXiv cs.CL 2017
Year: 2017

Despite successful applications across a broad range of NLP tasks, conditional random fields ("CRFs"), in particular the linear-chain variant, are only able to model local features. While this has important benefits in terms of inference tractability, it limits the ability of the model to capture long-range dependencies between items. Attempts to extend CRFs to capture long-range dependencies have largely come at the cost of computational complexity and approximate inference. In this work, we propose an extension to CRFs by integrating external memory, taking inspiration from memory networks, thereby allowing CRFs to incorporate information far beyond neighbouring steps. Experiments across two tasks show substantial improvements over strong CRF and LSTM baselines.
Semi-centralized control for multi-robot formation and theoretical lower bound
Venue: arXiv cs.RO 2017
Year: 2017

Multi-robot formation control enables robots to cooperate as a working group in completing complex tasks, which has been widely used in both civilian and military scenarios. Before moving to reach a given formation, each robot should choose a position from the formation so that the whole system cost is minimized. To solve the problem, we formulate an optimization problem in terms of the total moving distance and give a solution by the Hungarian method. To analyze the deviation of the achieved formation from the ideal one, we obtain the lower bound of formation bias with respect to system's parameters based on notions in information theory. As an extension, we discuss methods of transformation between different formations. Some theoretical results are obtained to give a guidance of the system design.
A certified reference validation mechanism for the permission model of Android
Venue: arXiv cs.PL 2017
Year: 2017

Android embodies security mechanisms at both OS and application level. In this platform application security is built primarily upon a system of permissions which specify restrictions on the operations a particular process can perform. The critical role of these security mechanisms makes them a prime target for (formal) verification. We present an idealized model of a reference monitor of the novel mechanisms of Android 6 (and further), where it is possible to grant permissions at run time. Using the programming language of the proof-assistant Coq we have developed a functional implementation of the reference validation mechanism and certified its correctness with respect to the specified reference monitor. Several properties concerning the permission model of Android 6 and its security mechanisms have been formally formulated and proved. Applying the program extraction mechanism provided by Coq we have also derived a certified Haskell prototype of the reference validation mechanism.
Rapid Near-Neighbor Interaction of High-dimensional Data via Hierarchical Clustering
Venue: arXiv cs.LG 2017
Year: 2017

Calculation of near-neighbor interactions among high dimensional, irregularly distributed data points is a fundamental task to many graph-based or kernel-based machine learning algorithms and applications. Such calculations, involving large, sparse interaction matrices, expose the limitation of conventional data-and-computation reordering techniques for improving space and time locality on modern computer memory hierarchies. We introduce a novel method for obtaining a matrix permutation that renders a desirable sparsity profile. The method is distinguished by the guiding principle to obtain a profile that is block-sparse with dense blocks. Our profile model and measure capture the essential properties affecting space and time locality, and permit variation in sparsity profile without imposing a restriction to a fixed pattern. The second distinction lies in an efficient algorithm for obtaining a desirable profile, via exploring and exploiting multi-scale cluster structure hidden in but intrinsic to the data. The algorithm accomplishes its task with key components for lower-dimensional embedding with data-specific principal feature axes, hierarchical data clustering, multi-level matrix compression storage, and multi-level interaction computations. We provide experimental results from case studies with two important data analysis algorithms. The resulting performance is remarkably comparable to the BLAS performance for the best-case interaction governed by a regularly banded matrix with the same sparsity.
Reversible Architectures for Arbitrarily Deep Residual Neural Networks
Venue: arXiv cs.CV 2017
Year: 2017

Recently, deep residual networks have been successfully applied in many computer vision and natural language processing tasks, pushing the state-of-the-art performance with deeper and wider architectures. In this work, we interpret deep residual networks as ordinary differential equations (ODEs), which have long been studied in mathematics and physics with rich theoretical and empirical success. From this interpretation, we develop a theoretical framework on stability and reversibility of deep neural networks, and derive three reversible neural network architectures that can go arbitrarily deep in theory. The reversibility property allows a memory-efficient implementation, which does not need to store the activations for most hidden layers. Together with the stability of our architectures, this enables training deeper networks using only modest computational resources. We provide both theoretical analyses and empirical results. Experimental results demonstrate the efficacy of our architectures against several strong baselines on CIFAR-10, CIFAR-100 and STL-10 with superior or on-par state-of-the-art performance. Furthermore, we show our architectures yield superior results when trained using fewer training data.
OCCAM: a flexible, multi-purpose and extendable HPC cluster
Venue: arXiv cs.DC 2017
Year: 2017

The Open Computing Cluster for Advanced data Manipulation (OCCAM) is a multi-purpose flexible HPC cluster designed and operated by a collaboration between the University of Torino and the Sezione di Torino of the Istituto Nazionale di Fisica Nucleare. It is aimed at providing a flexible, reconfigurable and extendable infrastructure to cater to a wide range of different scientific computing use cases, including ones from solid-state chemistry, high-energy physics, computer science, big data analytics, computational biology, genomics and many others. Furthermore, it will serve as a platform for R&D activities on computational technologies themselves, with topics ranging from GPU acceleration to Cloud Computing technologies. A heterogeneous and reconfigurable system like this poses a number of challenges related to the frequency at which heterogeneous hardware resources might change their availability and shareability status, which in turn affect methods and means to allocate, manage, optimize, bill, monitor VMs, containers, virtual farms, jobs, interactive bare-metal sessions, etc. This work describes some of the use cases that prompted the design and construction of the HPC cluster, its architecture and resource provisioning model, along with a first characterization of its performance by some synthetic benchmark tools and a few realistic use-case tests.
Cross-lingual Word Segmentation and Morpheme Segmentation as Sequence Labelling
Venue: arXiv cs.CL 2017
Year: 2017

This paper presents our segmentation system developed for the MLP 2017 shared tasks on cross-lingual word segmentation and morpheme segmentation. We model both word and morpheme segmentation as character-level sequence labelling tasks. The prevalent bidirectional recurrent neural network with conditional random fields as the output interface is adapted as the baseline system, which is further improved via ensemble decoding. Our universal system is applied to and extensively evaluated on all the official data sets without any language-specific adjustment. The official evaluation results indicate that the proposed model achieves outstanding accuracies both for word and morpheme segmentation on all the languages in various types when compared to the other participating systems.
Forbidden triads and Creative Success in Jazz: The Miles Davis Factor
Venue: arXiv cs.SI 2017
Year: 2017

This article argues for the importance of forbidden triads - open triads with high-weight edges - in predicting success in creative fields. Forbidden triads had been treated as a residual category beyond closed and open triads, yet I argue that these structures provide opportunities to combine socially evolved styles in new ways. Using data on the entire history of recorded jazz from 1896 to 2010, I show that observed collaborations have tolerated the openness of high weight triads more than expected, observed jazz sessions had more forbidden triads than expected, and the density of forbidden triads contributed to the success of recording sessions, measured by the number of record releases of session material. The article also shows that the sessions of Miles Davis had received an especially high boost from forbidden triads.
Sparse Representation Based Augmented Multinomial Logistic Extreme Learning Machine with Weighted Composite Features for Spectral Spatial Hyperspectral Image Classification
Venue: arXiv cs.CV 2017
Year: 2017

Although extreme learning machine (ELM) has been successfully applied to a number of pattern recognition problems, it fails to pro-vide sufficient good results in hyperspectral image (HSI) classification due to two main drawbacks. The first is due to the random weights and bias of ELM, which may lead to ill-posed problems. The second is the lack of spatial information for classification. To tackle these two problems, in this paper, we propose a new framework for ELM based spectral-spatial classification of HSI, where probabilistic modelling with sparse representation and weighted composite features (WCF) are employed respectively to derive the op-timized output weights and extract spatial features. First, the ELM is represented as a concave logarithmic likelihood function under statistical modelling using the maximum a posteriori (MAP). Second, the sparse representation is applied to the Laplacian prior to effi-ciently determine a logarithmic posterior with a unique maximum in order to solve the ill-posed problem of ELM. The variable splitting and the augmented Lagrangian are subsequently used to further reduce the computation complexity of the proposed algorithm and it has been proven a more efficient method for speed improvement. Third, the spatial information is extracted using the weighted compo-site features (WCFs) to construct the spectral-spatial classification framework. In addition, the lower bound of the proposed method is derived by a rigorous mathematical proof. Experimental results on two publicly available HSI data sets demonstrate that the proposed methodology outperforms ELM and a number of state-of-the-art approaches.
OpenNMT: Open-source Toolkit for Neural Machine Translation
Venue: arXiv cs.CL 2017
Year: 2017

We introduce an open-source toolkit for neural machine translation (NMT) to support research into model architectures, feature representations, and source modalities, while maintaining competitive performance, modularity and reasonable training requirements.