OpenRaiser/Intern-Atlas huggingface dataset:
Solving QBF by Abstraction
Venue: arXiv cs.LO 2018
Year: 2018

Many verification and synthesis approaches rely on solving techniques for quantified Boolean formulas (QBF). Consequently, solution witnesses, in the form of Boolean functions, become more and more important as they represent implementations or counterexamples. We present a recursive counterexample guided abstraction and refinement algorithm (CEGAR) for solving and certifying QBFs that exploits structural reasoning on the formula level. The algorithm decomposes the given QBF into one propositional formula for every block of quantifiers that abstracts from assignments of variables not bound by this quantifier block. Further, we show how to derive an efficient certification extraction method on top of the algorithm. We report on experimental evaluation of this algorithm in the solver QuAbS (Quantified Abstraction Solver) which won the most recent QBF competition (QBFEVAL'18). Further, we show the effectiveness of the certification approach using synthesis benchmarks and a case study for synthesizing winning strategies in Petri Games.
On the algebraic structure of Weihrauch degrees
Venue: arXiv cs.LO 2018
Year: 2018

We introduce two new operations (compositional products and implication) on Weihrauch degrees, and investigate the overall algebraic structure. The validity of the various distributivity laws is studied and forms the basis for a comparison with similar structures such as residuated lattices and concurrent Kleene algebras. Introducing the notion of an ideal with respect to the compositional product, we can consider suitable quotients of the Weihrauch degrees. We also prove some specific characterizations using the implication. In order to introduce and study compositional products and implications, we introduce and study a function space of multi-valued continuous functions. This space turns out to be particularly well-behaved for effectively traceable spaces that are closely related to admissibly represented spaces.
An Information Theoretic Framework For Designing Information Elicitation Mechanisms That Reward Truth-telling
Venue: arXiv cs.GT 2018
Year: 2018

In the setting where information cannot be verified, we propose a simple yet powerful information theoretical framework---the Mutual Information Paradigm---for information elicitation mechanisms. Our framework pays every agent a measure of mutual information between her signal and a peer's signal. We require that the mutual information measurement has the key property that any "data processing" on the two random variables will decrease the mutual information between them. We identify such information measures that generalize Shannon mutual information. Our Mutual Information Paradigm overcomes the two main challenges in information elicitation without verification: (1) how to incentivize effort and avoid agents colluding to report random or identical responses (2) how to motivate agents who believe they are in the minority to report truthfully. Aided by the information measures we found, (1) we use the paradigm to design a family of novel mechanisms where truth-telling is a dominant strategy and any other strategy will decrease every agent's expected payment (in the multi-question, detail free, minimal setting where the number of questions is large); (2) we show the versatility of our framework by providing a unified theoretical understanding of existing mechanisms---Peer Prediction [Miller 2005], Bayesian Truth Serum [Prelec 2004], and Dasgupta and Ghosh [2013]---by mapping them into our framework such that theoretical results of those existing mechanisms can be reconstructed easily. We also give an impossibility result which illustrates, in a certain sense, the the optimality of our framework.
Communication Cost for Updating Linear Functions when Message Updates are Sparse: Connections to Maximally Recoverable Codes
Venue: arXiv cs.IT 2018
Year: 2018

We consider a communication problem in which an update of the source message needs to be conveyed to one or more distant receivers that are interested in maintaining specific linear functions of the source message. The setting is one in which the updates are sparse in nature, and where neither the source nor the receiver(s) is aware of the exact {\em difference vector}, but only know the amount of sparsity that is present in the difference-vector. Under this setting, we are interested in devising linear encoding and decoding schemes that minimize the communication cost involved. We show that the optimal solution to this problem is closely related to the notion of maximally recoverable codes (MRCs), which were originally introduced in the context of coding for storage systems. In the context of storage, MRCs guarantee optimal erasure protection when the system is partially constrained to have local parity relations among the storage nodes. In our problem, we show that optimal solutions exist if and only if MRCs of certain kind (identified by the desired linear functions) exist. We consider point-to-point and broadcast versions of the problem, and identify connections to MRCs under both these settings. For the point-to-point setting, we show that our linear-encoder based achievable scheme is optimal even when non-linear encoding is permitted. The theory is illustrated in the context of updating erasure coded storage nodes. We present examples based on modern storage codes such as the minimum bandwidth regenerating codes.
Sharp Sufficient Conditions for Stable Recovery of Block Sparse Signals by Block Orthogonal Matching Pursuit
Venue: arXiv cs.IT 2018
Year: 2018

In this paper, we use the block orthogonal matching pursuit (BOMP) algorithm to recover block sparse signals $\x$ from measurements $\y=\A\x+\v$, where $\v$ is an $\ell_2$-bounded noise vector (i.e., $\|\v\|_2\leq ε$ for some constant $ε$). We investigate some sufficient conditions based on the block restricted isometry property (block-RIP) for exact (when $\v=\0$) and stable (when $\v\neq\0$) recovery of block sparse signals $\x$. First, on the one hand, we show that if $\A$ satisfies the block-RIP with $δ_{K+1}<1/\sqrt{K+1}$, then every block $K$-sparse signal $\x$ can be exactly or stably recovered by BOMP in $K$ iterations. On the other hand, we show that, for any $K\geq 1$ and $1/\sqrt{K+1}\leq δ<1$, there exists a matrix $\A$ satisfying the block-RIP with $δ_{K+1}=δ$ and a block $K$-sparse signal $\x$ such that BOMP may fail to recover $\x$ in $K$ iterations. Then, we study some sufficient conditions for recovering block $α$-strongly-decaying $K$-sparse signals. We show that if $\A$ satisfies the block-RIP with $δ_{K+1}<\sqrt{2}/2$, then every $α$-strongly-decaying block $K$-sparse signal can be exactly or stably recovered by BOMP in $K$ iterations under some conditions on $α$. Our newly found sufficient condition on the block-RIP of $\A$ is less restrictive than that for $\ell_1$ minimization for this special class of sparse signals. Furthermore, for any $K\geq 1$, $α>1$ and $\sqrt{2}/2\leq δ<1$, the recovery of $\x$ may fail in $K$ iterations for a sensing matrix $\A$ which satisfies the block-RIP with $δ_{K+1}=δ$. Finally, we study some sufficient conditions for partial recovery of block sparse signals. Specifically, if $\A$ satisfies the block-RIP with $δ_{K+1}<\sqrt{2}/2$, then BOMP is guaranteed to recover some blocks of $\x$ if these blocks satisfy a sufficient condition.
Yarrp'ing the Internet: Randomized High-Speed Active Topology Discovery
Venue: arXiv cs.NI 2018
Year: 2018

Obtaining a "snapshot" of the Internet topology remains an elusive task. Existing active topology discovery techniques and systems require significant probing time -- time during which the underlying network may experience transient dynamics. This work considers how active probing can gather the Internet topology in minutes rather than days. Conventional approaches to active topology mapping face two primary speed and scale impediments: i) per-trace state maintenance; and ii) a low-degree of parallelism. Based on this observation, we develop Yarrp (Yelling at Random Routers Progressively), a new traceroute technique designed for high-rate, Internet-scale probing. Yarrp is stateless, reconstituting all necessary information from ICMP replies as they arrive asynchronously. To avoid overloading routers or links with probe traffic, Yarrp randomly permutes an input IP x TTL space. We run Yarrp at 100Kpps, a rate at which the paths to all /24's on the IPv4 Internet can be mapped in approximately one hour from a single vantage point. We compare Yarrp against existing systems, and present examples of topological dynamics exposed via the high sampling rates Yarrp enables.
Data-driven root-cause analysis for distributed system anomalies
Venue: arXiv cs.LG 2018
Year: 2018

Modern distributed cyber-physical systems encounter a large variety of anomalies and in many cases, they are vulnerable to catastrophic fault propagation scenarios due to strong connectivity among the sub-systems. In this regard, root-cause analysis becomes highly intractable due to complex fault propagation mechanisms in combination with diverse operating modes. This paper presents a new data-driven framework for root-cause analysis for addressing such issues. The framework is based on a spatiotemporal feature extraction scheme for distributed cyber-physical systems built on the concept of symbolic dynamics for discovering and representing causal interactions among subsystems of a complex system. We present two approaches for root-cause analysis, namely the sequential state switching ($S^3$, based on free energy concept of a Restricted Boltzmann Machine, RBM) and artificial anomaly association ($A^3$, a multi-class classification framework using deep neural networks, DNN). Synthetic data from cases with failed pattern(s) and anomalous node are simulated to validate the proposed approaches, then compared with the performance of vector autoregressive (VAR) model-based root-cause analysis. Real dataset based on Tennessee Eastman process (TEP) is also used for validation. The results show that: (1) $S^3$ and $A^3$ approaches can obtain high accuracy in root-cause analysis and successfully handle multiple nominal operation modes, and (2) the proposed tool-chain is shown to be scalable while maintaining high accuracy.
Online Influence Maximization under Independent Cascade Model with Semi-Bandit Feedback
Venue: arXiv cs.LG 2018
Year: 2018

We study the online influence maximization problem in social networks under the independent cascade model. Specifically, we aim to learn the set of "best influencers" in a social network online while repeatedly interacting with it. We address the challenges of (i) combinatorial action space, since the number of feasible influencer sets grows exponentially with the maximum number of influencers, and (ii) limited feedback, since only the influenced portion of the network is observed. Under a stochastic semi-bandit feedback, we propose and analyze IMLinUCB, a computationally efficient UCB-based algorithm. Our bounds on the cumulative regret are polynomial in all quantities of interest, achieve near-optimal dependence on the number of interactions and reflect the topology of the network and the activation probabilities of its edges, thereby giving insights on the problem complexity. To the best of our knowledge, these are the first such results. Our experiments show that in several representative graph topologies, the regret of IMLinUCB scales as suggested by our upper bounds. IMLinUCB permits linear generalization and thus is both statistically and computationally suitable for large-scale problems. Our experiments also show that IMLinUCB with linear generalization can lead to low regret in real-world online influence maximization.
As-exact-as-possible repair of unprintable STL files
Venue: arXiv cs.GR 2018
Year: 2018

Purpose: The class of models that can be represented by STL files is larger than the class of models that can be printed using additive manufacturing technologies. Stated differently, there exist well-formed STL files that cannot be printed. In this paper such a gap is formalized and a fully automatic procedure is described to turn any such file into a printable model. Approach: Based on well-established concepts from combinatorial topology, we provide an unambiguous description of all the mathematical entities involved in the modeling-printing pipeline. Specifically, we formally define the conditions that an STL file must satisfy to be printable and, based on these, we design an as-exact-as-possible repairing algorithm. Findings: We have found that, in order to cope with all the possible triangle configurations, the algorithm must distinguish between triangles that bound solid parts and triangles that constitute zero-thickness sheets. Only the former set can be fixed without distortion. Originality: Previous methods that are guaranteed to fix all the possible configurations provide only approximate solutions with an unnecessary distortion. Conversely, our procedure is as exact as possible, meaning that no visible distortion is introduced unless it is strictly imposed by limitations of the printing device. Thanks to such an unprecedented flexibility and accuracy, this algorithm is expected to significantly simplify the modeling-printing process, in particular within the continuously emerging non-professional "maker" communities.
Parameterized Resiliency Problems via Integer Linear Programming
Venue: arXiv cs.DS 2018
Year: 2018

We introduce an extension of decision problems called resiliency problems. In resiliency problems, the goal is to decide whether an instance remains positive after any (appropriately defined) perturbation has been applied to it. To tackle these kinds of problems, some of which might be of practical interest, we introduce a notion of resiliency for Integer Linear Programs (ILP) and show how to use a result of Eisenbrand and Shmonin (Math. Oper. Res., 2008) on Parametric Linear Programming to prove that ILP Resiliency is fixed-parameter tractable (FPT) under a certain parameterization. To demonstrate the utility of our result, we consider natural resiliency versions of several concrete problems, and prove that they are FPT under natural parameterizations. Our first results concern a four-variate problem which generalizes the Disjoint Set Cover problem and which is of interest in access control. We obtain a complete parameterized complexity classification for every possible combination of the parameters. Then, we introduce and study a resiliency version of the Closest String problem, for which we extend an FPT result of Gramm et al. (Algorithmica, 2003). We also consider problems in the fields of scheduling and social choice. We believe that many other problems can be tackled by our framework.
Diachronic Word Embeddings Reveal Statistical Laws of Semantic Change
Venue: arXiv cs.CL 2018
Year: 2018

Understanding how words change their meanings over time is key to models of language and cultural evolution, but historical data on meaning is scarce, making theories hard to develop and test. Word embeddings show promise as a diachronic tool, but have not been carefully evaluated. We develop a robust methodology for quantifying semantic change by evaluating word embeddings (PPMI, SVD, word2vec) against known historical changes. We then use this methodology to reveal statistical laws of semantic evolution. Using six historical corpora spanning four languages and two centuries, we propose two quantitative laws of semantic change: (i) the law of conformity---the rate of semantic change scales with an inverse power-law of word frequency; (ii) the law of innovation---independent of frequency, words that are more polysemous have higher rates of semantic change.
Less is More: Micro-expression Recognition from Video using Apex Frame
Venue: arXiv cs.CV 2018
Year: 2018

Despite recent interest and advances in facial micro-expression research, there is still plenty room for improvement in terms of micro-expression recognition. Conventional feature extraction approaches for micro-expression video consider either the whole video sequence or a part of it, for representation. However, with the high-speed video capture of micro-expressions (100-200 fps), are all frames necessary to provide a sufficiently meaningful representation? Is the luxury of data a bane to accurate recognition? A novel proposition is presented in this paper, whereby we utilize only two images per video: the apex frame and the onset frame. The apex frame of a video contains the highest intensity of expression changes among all frames, while the onset is the perfect choice of a reference frame with neutral expression. A new feature extractor, Bi-Weighted Oriented Optical Flow (Bi-WOOF) is proposed to encode essential expressiveness of the apex frame. We evaluated the proposed method on five micro-expression databases: CAS(ME)$^2$, CASME II, SMIC-HS, SMIC-NIR and SMIC-VIS. Our experiments lend credence to our hypothesis, with our proposed technique achieving a state-of-the-art F1-score recognition performance of 61% and 62% in the high frame rate CASME II and SMIC-HS databases respectively.
Progressive Attention Networks for Visual Attribute Prediction
Venue: arXiv cs.CV 2018
Year: 2018

We propose a novel attention model that can accurately attends to target objects of various scales and shapes in images. The model is trained to gradually suppress irrelevant regions in an input image via a progressive attentive process over multiple layers of a convolutional neural network. The attentive process in each layer determines whether to pass or block features at certain spatial locations for use in the subsequent layers. The proposed progressive attention mechanism works well especially when combined with hard attention. We further employ local contexts to incorporate neighborhood features of each location and estimate a better attention probability map. The experiments on synthetic and real datasets show that the proposed attention networks outperform traditional attention methods in visual attribute prediction tasks.
On Continuous-space Embedding of Discrete-parameter Queueing Systems
Venue: arXiv cs.PF 2018
Year: 2018

Motivated by the problem of discrete-parameter simulation optimization (DPSO) of queueing systems, we consider the problem of embedding the discrete parameter space into a continuous one so that descent-based continuous-space methods could be directly applied for efficient optimization. We show that a randomization of the simulation model itself can be used to achieve such an embedding when the objective function is a long-run average measure. Unlike spatial interpolation, the computational cost of this embedding is independent of the number of parameters in the system, making the approach ideally suited to high-dimensional problems. We describe in detail the application of this technique to discrete-time queues for embedding queue capacities, number of servers and server-delay parameters into continuous space and empirically show that the technique can produce smooth interpolations of the objective function. Through an optimization case-study of a queueing network with $10^7$ design points, we demonstrate that existing continuous optimizers can be effectively applied over such an embedding to find good solutions.
Experimental and causal view on information integration in autonomous agents
Venue: arXiv cs.AI 2018
Year: 2018

The amount of digitally available but heterogeneous information about the world is remarkable, and new technologies such as self-driving cars, smart homes, or the internet of things may further increase it. In this paper we present preliminary ideas about certain aspects of the problem of how such heterogeneous information can be harnessed by autonomous agents. After discussing potentials and limitations of some existing approaches, we investigate how \emph{experiments} can help to obtain a better understanding of the problem. Specifically, we present a simple agent that integrates video data from a different agent, and implement and evaluate a version of it on the novel experimentation platform \emph{Malmo}. The focus of a second investigation is on how information about the hardware of different agents, the agents' sensory data, and \emph{causal} information can be utilized for knowledge transfer between agents and subsequently more data-efficient decision making. Finally, we discuss potential future steps w.r.t.\ theory and experimentation, and formulate open questions.
A New Training Method for Feedforward Neural Networks Based on Geometric Contraction Property of Activation Functions
Venue: arXiv cs.NE 2018
Year: 2018

We propose a new training method for a feedforward neural network having the activation functions with the geometric contraction property. The method consists of constructing a new functional that is less nonlinear in comparison with the classical functional by removing the nonlinearity of the activation function from the output layer. We validate this new method by a series of experiments that show an improved learning speed and better classification error.
On the Moment Distance Between Sensors and Anchor Points
Venue: arXiv cs.DM 2018
Year: 2018

The present paper contains additional asymptotic result over an earlier investigation of Kapelko and Kranakis. Consider $n$ mobile sensors placed independently at random with the uniform distribution on the unit interval $[0,1]$. Fix $a$ an odd natural number. Let $X_i$ be the the $i-$th closest sensor to $0$ on the interval $[0,1].$ Then the following identity holds $$\sum_{i=1}^n\mathbf{E}\left[\left|X_i-\left(\frac{i}{n}-\frac{1}{2n}\right)\right|^a\right]=\frac{Γ\left(\frac{a}{2}+1\right)}{2^{\frac{a}{2}}(1+a)}\frac{1}{n^{\frac{a}{2}-1}}+O\left(\frac{1}{n^{\frac{a-1}{2}}}\right),$$ when $a$ is an odd natural number, where $Γ(z)$ is the Gamma function.
Comparative analysis on the selection of number of clusters in community detection
Venue: arXiv cs.SI 2018
Year: 2018

We conduct a comparative analysis on various estimates of the number of clusters in community detection. An exhaustive comparison requires testing of all possible combinations of frameworks, algorithms, and assessment criteria. In this paper we focus on the framework based on a stochastic block model, and investigate the performance of greedy algorithms, statistical inference, and spectral methods. For the assessment criteria, we consider modularity, map equation, Bethe free energy, prediction errors, and isolated eigenvalues. From the analysis, the tendency of overfit and underfit that the assessment criteria and algorithms have, becomes apparent. In addition, we propose that the alluvial diagram is a suitable tool to visualize statistical inference results and can be useful to determine the number of clusters.
User Assignment in C-RAN Systems: Algorithms and Bounds
Venue: arXiv cs.IT 2018
Year: 2018

In this work, we investigate the problem of mitigating interference between so called antenna domains of a cloud radio access network (C-RAN). In contrast to previous work, we turn to an approach utilizing primarily the optimal assignment of users to central processors in a C-RAN deployment. We formulate this user assignment problem as an integer optimization problem, and propose an iterative algorithm for obtaining a solution. Motivated by the lack of optimality guarantees on such solutions, we opt to find lower bounds on the problem, and the resulting interference leakage in the network. We thus derive the corresponding Dantzig-Wolfe decomposition, formulate the dual problem, and show that the former offers a tighter bound than the latter. We highlight the fact that the bounds in question consist of linear problems with an exponential number of variables, and adapt the column generation method for solving them. In addition to shedding light on the tightness of the bounds in question, our numerical results show significant sum-rate gains over several comparison schemes. Moreover, the proposed scheme delivers similar performance as W-MMSE with a significantly lower complexity (around 10 times less).