OpenRaiser/Intern-Atlas huggingface dataset:
Monadic second order finite satisfiability and unbounded tree-width
Venue: arXiv cs.LO 2016
Year: 2016

The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable: Input: (i) A monadic second order logic sentence $α$, and (ii) a sentence $β$ in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of $α$ and $β$ may intersect. Output: Is there a finite structure which satisfies $α\landβ$ such that the restriction of the structure to the vocabulary of $α$ has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form $|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$, where the $X_{i}$ and $Y_{j}$ are monadic second order variables. We prove the decidability of a similar extension of WS1S.
Successive Concave Sparsity Approximation for Compressed Sensing
Venue: arXiv cs.IT 2016
Year: 2016

In this paper, based on a successively accuracy-increasing approximation of the $\ell_0$ norm, we propose a new algorithm for recovery of sparse vectors from underdetermined measurements. The approximations are realized with a certain class of concave functions that aggressively induce sparsity and their closeness to the $\ell_0$ norm can be controlled. We prove that the series of the approximations asymptotically coincides with the $\ell_1$ and $\ell_0$ norms when the approximation accuracy changes from the worst fitting to the best fitting. When measurements are noise-free, an optimization scheme is proposed which leads to a number of weighted $\ell_1$ minimization programs, whereas, in the presence of noise, we propose two iterative thresholding methods that are computationally appealing. A convergence guarantee for the iterative thresholding method is provided, and, for a particular function in the class of the approximating functions, we derive the closed-form thresholding operator. We further present some theoretical analyses via the restricted isometry, null space, and spherical section properties. Our extensive numerical simulations indicate that the proposed algorithm closely follows the performance of the oracle estimator for a range of sparsity levels wider than those of the state-of-the-art algorithms.
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL (full version)
Venue: arXiv cs.LO 2016
Year: 2016

We continue the investigation of parameterized extensions of Linear Temporal Logic (LTL) that retain the attractive algorithmic properties of LTL: a polynomial space model checking algorithm and a doubly-exponential time algorithm for solving games. Alur et al. and Kupferman et al. showed that this is the case for Parametric LTL (PLTL) and PROMPT-LTL respectively, which have temporal operators equipped with variables that bound their scope in time. Later, this was also shown to be true for Parametric LDL (PLDL), which extends PLTL to be able to express all omega-regular properties. Here, we generalize PLTL to systems with costs, i.e., we do not bound the scope of operators in time, but bound the scope in terms of the cost accumulated during time. Again, we show that model checking and solving games for specifications in PLTL with costs is not harder than the corresponding problems for LTL. Finally, we discuss PLDL with costs and extensions to multiple cost functions.
SYM-ILDL: Incomplete $LDL^{T}$ Factorization of Symmetric Indefinite and Skew-Symmetric Matrices
Venue: arXiv cs.MS 2016
Year: 2016

SYM-ILDL is a numerical software package that computes incomplete $LDL^{T}$ (or `ILDL') factorizations of symmetric indefinite and real skew-symmetric matrices. The core of the algorithm is a Crout variant of incomplete LU (ILU), originally introduced and implemented for symmetric matrices by [Li and Saad, Crout versions of ILU factorization with pivoting for sparse symmetric matrices, Transactions on Numerical Analysis 20, pp. 75--85, 2005]. Our code is economical in terms of storage and it deals with real skew-symmetric matrices as well, in addition to symmetric ones. The package is written in C++ and it is templated, open source, and includes a MATLAB interface. The code includes built-in RCM and AMD reordering, two equilibration strategies, threshold Bunch-Kaufman pivoting and rook pivoting, as well as a wrapper to MC64, a popular matching based equilibration and reordering algorithm. We also include two built-in iterative solvers: SQMR preconditioned with ILDL, or MINRES preconditioned with a symmetric positive definite preconditioner based on the ILDL factorization.
MPI Benchmarking Revisited: Experimental Design and Reproducibility
Venue: arXiv cs.DC 2016
Year: 2016

The Message Passing Interface (MPI) is the prevalent programming model used on today's supercomputers. Therefore, MPI library developers are looking for the best possible performance (shortest run-time) of individual MPI functions across many different supercomputer architectures. Several MPI benchmark suites have been developed to assess the performance of MPI implementations. Unfortunately, the outcome of these benchmarks is often neither reproducible nor statistically sound. To overcome these issues, we show which experimental factors have an impact on the run-time of blocking collective MPI operations and how to control them. We address the problem of process and clock synchronization in MPI benchmarks. Finally, we present a new experimental method that allows us to obtain reproducible and statistically sound MPI measurements.
Secure Cascade Channel Synthesis
Venue: arXiv cs.IT 2016
Year: 2016

We consider the problem of generating correlated random variables in a distributed fashion, where communication is constrained to a cascade network. The first node in the cascade observes an i.i.d. sequence $X^n$ locally before initiating communication along the cascade. All nodes share bits of common randomness that are independent of $X^n$. We consider secure synthesis - random variables produced by the system appear to be appropriately correlated and i.i.d. even to an eavesdropper who is cognizant of the communication transmissions. We characterize the optimal tradeoff between the amount of common randomness used and the required rates of communication. We find that not only does common randomness help, its usage exceeds the communication rate requirements. The most efficient scheme is based on a superposition codebook, with the first node selecting messages for all downstream nodes. We also provide a fleeting view of related problems, demonstrating how the optimal rate region may shrink or expand.
Monolingually Derived Phrase Scores for Phrase Based SMT Using Neural Networks Vector Representations
Venue: arXiv cs.CL 2016
Year: 2016

In this paper, we propose two new features for estimating phrase-based machine translation parameters from mainly monolingual data. Our method is based on two recently introduced neural network vector representation models for words and sentences. It is the first time that these models have been used in an end to end phrase-based machine translation system. Scores obtained from our method can recover more than 80% of BLEU loss caused by removing phrase table probabilities. We also show that our features combined with the phrase table probabilities improve the BLEU score by absolute 0.74 points.
Group buying with bundle discounts: computing efficient, stable and fair solutions
Venue: arXiv cs.GT 2016
Year: 2016

We model a market in which nonstrategic vendors sell items of different types and offer bundles at discounted prices triggered by demand volumes. Each buyer acts strategically in order to maximize her utility, given by the difference between product valuation and price paid. Buyers report their valuations in terms of reserve prices on sets of items, and might be willing to pay prices different than the market price in order to subsidize other buyers and to trigger discounts. The resulting price discrimination can be interpreted as a redistribution of the total discount. We consider a notion of stability that looks at unilateral deviations, and show that efficient allocations - the ones maximizing the social welfare - can be stabilized by prices that enjoy desirable properties of rationality and fairness. These dictate that buyers pay higher prices only to subsidize others who contribute to the activation of the desired discounts, and that they pay premiums over the discounted price proportionally to their surplus - the difference between their current utility and the utility of their best alternative. Therefore, the resulting price discrimination appears to be desirable to buyers. Building on this existence result, and letting N, M and c be the numbers of buyers, vendors and product types, we propose a O(N^2+NM^c) algorithm that, given an efficient allocation, computes prices that are rational and fair and that stabilize the market. The algorithm first determines the redistribution of the discount between groups of buyers with an equal product choice, and then computes single buyers' prices. Our results show that if a desirable form of price discrimination is implemented then social efficiency and stability can coexists in a market presenting subtle externalities, and computing individual prices from market prices is tractable.
Peer Grading in a Course on Algorithms and Data Structures: Machine Learning Algorithms do not Improve over Simple Baselines
Venue: arXiv cs.LG 2016
Year: 2016

Peer grading is the process of students reviewing each others' work, such as homework submissions, and has lately become a popular mechanism used in massive open online courses (MOOCs). Intrigued by this idea, we used it in a course on algorithms and data structures at the University of Hamburg. Throughout the whole semester, students repeatedly handed in submissions to exercises, which were then evaluated both by teaching assistants and by a peer grading mechanism, yielding a large dataset of teacher and peer grades. We applied different statistical and machine learning methods to aggregate the peer grades in order to come up with accurate final grades for the submissions (supervised and unsupervised, methods based on numeric scores and ordinal rankings). Surprisingly, none of them improves over the baseline of using the mean peer grade as the final grade. We discuss a number of possible explanations for these results and present a thorough analysis of the generated dataset.
Summarization of Films and Documentaries Based on Subtitles and Scripts
Venue: arXiv cs.CL 2016
Year: 2016

We assess the performance of generic text summarization algorithms applied to films and documentaries, using the well-known behavior of summarization of news articles as reference. We use three datasets: (i) news articles, (ii) film scripts and subtitles, and (iii) documentary subtitles. Standard ROUGE metrics are used for comparing generated summaries against news abstracts, plot summaries, and synopses. We show that the best performing algorithms are LSA, for news articles and documentaries, and LexRank and Support Sets, for films. Despite the different nature of films and documentaries, their relative behavior is in accordance with that obtained for news articles.
One-to-many face recognition with bilinear CNNs
Venue: arXiv cs.CV 2016
Year: 2016

The recent explosive growth in convolutional neural network (CNN) research has produced a variety of new architectures for deep learning. One intriguing new architecture is the bilinear CNN (B-CNN), which has shown dramatic performance gains on certain fine-grained recognition problems [15]. We apply this new CNN to the challenging new face recognition benchmark, the IARPA Janus Benchmark A (IJB-A) [12]. It features faces from a large number of identities in challenging real-world conditions. Because the face images were not identified automatically using a computerized face detection system, it does not have the bias inherent in such a database. We demonstrate the performance of the B-CNN model beginning from an AlexNet-style network pre-trained on ImageNet. We then show results for fine-tuning using a moderate-sized and public external database, FaceScrub [17]. We also present results with additional fine-tuning on the limited training data provided by the protocol. In each case, the fine-tuned bilinear model shows substantial improvements over the standard CNN. Finally, we demonstrate how a standard CNN pre-trained on a large face database, the recently released VGG-Face model [20], can be converted into a B-CNN without any additional feature training. This B-CNN improves upon the CNN performance on the IJB-A benchmark, achieving 89.5% rank-1 recall.
Finding the Optimal Demodulator Under Implementation Constraints
Venue: arXiv cs.IT 2016
Year: 2016

The common approach of designing a communication device is to maximize a well-defined objective function, e.g., the channel capacity and the cut-off rate. We propose easy-to-implement solutions for Gaussian channels that approximate the optimal results for these maximization problems. Three topics are addressed. First, we consider the case where the channel output is quantized, and we find the quantization thresholds that maximize the mutual information. The approximation derived from the asymptotic solution has a negligible loss on the entire range of SNR when 2-PAM modulation is used, and its quantization thresholds linearly depend on the standard deviation of noise. We also derive a simple estimator of the relative capacity loss due to quantization, based on the high-rate limit. Then we consider the integer constraint on the decoding metric, and maximize the mismatched channel capacity. We study the asymptotic solution of the optimal metric assignment and show that the same approximation we derived in the matched decoding case still holds for the mismatched decoder. Finally, we consider the demodulation problem for 8PSK bit-interleaved coded modulation(BICM). We derive the approximated optimal demodulation metrics that maximize the general cut-off rate or the mismatched capacity using max-log approximation . The error rate performances of the two metrics' assignments are compared, based on Reed-Solomon-Viterbi(RSV) code, and the mismatched capacity metric turns out to be better. The proposed approximation can be computed using an efficient firmware algorithm, and improves the system performance of commercial chips.
Spatial Transformer Networks
Venue: arXiv cs.CV 2016
Year: 2016

Convolutional Neural Networks define an exceptionally powerful class of models, but are still limited by the lack of ability to be spatially invariant to the input data in a computationally and parameter efficient manner. In this work we introduce a new learnable module, the Spatial Transformer, which explicitly allows the spatial manipulation of data within the network. This differentiable module can be inserted into existing convolutional architectures, giving neural networks the ability to actively spatially transform feature maps, conditional on the feature map itself, without any extra training supervision or modification to the optimisation process. We show that the use of spatial transformers results in models which learn invariance to translation, scale, rotation and more generic warping, resulting in state-of-the-art performance on several benchmarks, and for a number of classes of transformations.
ASlib: A Benchmark Library for Algorithm Selection
Venue: arXiv cs.AI 2016
Year: 2016

The task of algorithm selection involves choosing an algorithm from a set of algorithms on a per-instance basis in order to exploit the varying performance of algorithms over a set of instances. The algorithm selection problem is attracting increasing attention from researchers and practitioners in AI. Years of fruitful applications in a number of domains have resulted in a large amount of data, but the community lacks a standard format or repository for this data. This situation makes it difficult to share and compare different approaches effectively, as is done in other, more established fields. It also unnecessarily hinders new researchers who want to work in this area. To address this problem, we introduce a standardized format for representing algorithm selection scenarios and a repository that contains a growing number of data sets from the literature. Our format has been designed to be able to express a wide variety of different scenarios. Demonstrating the breadth and power of our platform, we describe a set of example experiments that build and evaluate algorithm selection models through a common interface. The results display the potential of algorithm selection to achieve significant performance improvements across a broad range of problems and algorithms.
Guaranteed Blind Sparse Spikes Deconvolution via Lifting and Convex Optimization
Venue: arXiv cs.IT 2016
Year: 2016

Neural recordings, returns from radars and sonars, images in astronomy and single-molecule microscopy can be modeled as a linear superposition of a small number of scaled and delayed copies of a band-limited or diffraction-limited point spread function, which is either determined by the nature or designed by the users; in other words, we observe the convolution between a point spread function and a sparse spike signal with unknown amplitudes and delays. While it is of great interest to accurately resolve the spike signal from as few samples as possible, however, when the point spread function is not known a priori, this problem is terribly ill-posed. This paper proposes a convex optimization framework to simultaneously estimate the point spread function as well as the spike signal, by mildly constraining the point spread function to lie in a known low-dimensional subspace. By applying the lifting trick, we obtain an underdetermined linear system of an ensemble of signals with joint spectral sparsity, to which atomic norm minimization is applied. Under mild randomness assumptions of the low-dimensional subspace as well as a separation condition of the spike signal, we prove the proposed algorithm, dubbed as AtomicLift, is guaranteed to recover the spike signal up to a scaling factor as soon as the number of samples is large enough. The extension of AtomicLift to handle noisy measurements is also discussed. Numerical examples are provided to validate the effectiveness of the proposed approaches.
The gap between the null space property and the restricted isometry property
Venue: arXiv cs.IT 2016
Year: 2016

The null space property (NSP) and the restricted isometry property (RIP) are two properties which have received considerable attention in the compressed sensing literature. As the name suggests, NSP is a property that depends solely on the null space of the measurement procedure and as such, any two matrices which have the same null space will have NSP if either one of them does. On the other hand, RIP is a property of the measurement procedure itself, and given an RIP matrix it is straightforward to construct another matrix with the same null space that is not RIP. %Furthermore, RIP is known to imply NSP and therefore RIP is a strictly stronger assumption than NSP. We say a matrix is RIP-NSP if it has the same null space as an RIP matrix. We show that such matrices can provide robust recovery of compressible signals under Basis pursuit which in many applicable settings is comparable to the guarantee that RIP provides. More importantly, we constructively show that the RIP-NSP is stronger than NSP with the aid of this robust recovery result, which shows that RIP is fundamentally stronger than NSP.
Hierarchical Information and the Synthesis of Distributed Strategies
Venue: arXiv cs.GT 2016
Year: 2016

Infinite games with imperfect information are known to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive. In this paper we consider variations of this hierarchy principle for synchronous games with perfect recall, and identify new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. In particular, we show that decidability is maintained when the information hierarchy may change along the play, or when transient phases without hierarchical information are allowed. Finally, we interpret our result in terms of distributed system architectures.
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
Venue: arXiv cs.LO 2016
Year: 2016

Autonomous critical systems, such as satellites and space rovers, must be able to detect the occurrence of faults in order to ensure correct operation. This task is carried out by Fault Detection and Identification (FDI) components, that are embedded in those systems and are in charge of detecting faults in an automated and timely manner by reading data from sensors and triggering predefined alarms. The design of effective FDI components is an extremely hard problem, also due to the lack of a complete theoretical foundation, and of precise specification and validation techniques. In this paper, we present the first formal approach to the design of FDI components for discrete event systems, both in a synchronous and asynchronous setting. We propose a logical language for the specification of FDI requirements that accounts for a wide class of practical cases, and includes novel aspects such as maximality and trace-diagnosability. The language is equipped with a clear semantics based on temporal epistemic logic, and is proved to enjoy suitable properties. We discuss how to validate the requirements and how to verify that a given FDI component satisfies them. We propose an algorithm for the synthesis of correct-by-construction FDI components, and report on the applicability of the design approach on an industrial case-study coming from aerospace.
Author Identification using Multi-headed Recurrent Neural Networks
Venue: arXiv cs.CL 2016
Year: 2016

Recurrent neural networks (RNNs) are very good at modelling the flow of text, but typically need to be trained on a far larger corpus than is available for the PAN 2015 Author Identification task. This paper describes a novel approach where the output layer of a character-level RNN language model is split into several independent predictive sub-models, each representing an author, while the recurrent layer is shared by all. This allows the recurrent layer to model the language as a whole without over-fitting, while the outputs select aspects of the underlying model that reflect their author's style. The method proves competitive, ranking first in two of the four languages.
Time Series Classification using the Hidden-Unit Logistic Model
Venue: arXiv cs.LG 2016
Year: 2016

We present a new model for time series classification, called the hidden-unit logistic model, that uses binary stochastic hidden units to model latent structure in the data. The hidden units are connected in a chain structure that models temporal dependencies in the data. Compared to the prior models for time series classification such as the hidden conditional random field, our model can model very complex decision boundaries because the number of latent states grows exponentially with the number of hidden units. We demonstrate the strong performance of our model in experiments on a variety of (computer vision) tasks, including handwritten character recognition, speech recognition, facial expression, and action recognition. We also present a state-of-the-art system for facial action unit detection based on the hidden-unit logistic model.