OpenRaiser/Intern-Atlas huggingface dataset:
Learning-Assisted Automated Reasoning with Flyspeck
Venue: arXiv cs.AI 2014
Year: 2014

The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.
Euclidean Partitions Optimizing Noise Stability
Venue: arXiv cs.CC 2014
Year: 2014

The Standard Simplex Conjecture of Isaksson and Mossel asks for the partition $\{A_{i}\}_{i=1}^{k}$ of $\mathbb{R}^{n}$ into $k\leq n+1$ pieces of equal Gaussian measure of optimal noise stability. That is, for $ρ>0$, we maximize $$ \sum_{i=1}^{k}\int_{\mathbb{R}^{n}}\int_{\mathbb{R}^{n}}1_{A_{i}}(x)1_{A_{i}}(xρ+y\sqrt{1-ρ^{2}}) e^{-(x_{1}^{2}+\cdots+x_{n}^{2})/2}e^{-(y_{1}^{2}+\cdots+y_{n}^{2})/2}dxdy. $$ Isaksson and Mossel guessed the best partition for this problem and proved some applications of their conjecture. For example, the Standard Simplex Conjecture implies the Plurality is Stablest Conjecture. For $k=3,n\geq2$ and $0<ρ<ρ_{0}(k,n)$, we prove the Standard Simplex Conjecture. The full conjecture has applications to theoretical computer science, and to geometric multi-bubble problems (after Isaksson and Mossel).
Kernel Estimation from Salient Structure for Robust Motion Deblurring
Venue: arXiv cs.CV 2014
Year: 2014

Blind image deblurring algorithms have been improving steadily in the past years. Most state-of-the-art algorithms, however, still cannot perform perfectly in challenging cases, especially in large blur setting. In this paper, we focus on how to estimate a good kernel estimate from a single blurred image based on the image structure. We found that image details caused by blurring could adversely affect the kernel estimation, especially when the blur kernel is large. One effective way to eliminate these details is to apply image denoising model based on the Total Variation (TV). First, we developed a novel method for computing image structures based on TV model, such that the structures undermining the kernel estimation will be removed. Second, to mitigate the possible adverse effect of salient edges and improve the robustness of kernel estimation, we applied a gradient selection method. Third, we proposed a novel kernel estimation method, which is capable of preserving the continuity and sparsity of the kernel and reducing the noises. Finally, we developed an adaptive weighted spatial prior, for the purpose of preserving sharp edges in latent image restoration. The effectiveness of our method is demonstrated by experiments on various kinds of challenging examples.
A metric for software vulnerabilities classification
Venue: arXiv cs.SE 2014
Year: 2014

Vulnerability discovery and exploits detection are two wide areas of study in software engineering. This preliminary work tries to combine existing methods with machine learning techniques to define a metric classification of vulnerable computer programs. First a feature set has been defined and later two models have been tested against real world vulnerabilities. A relation between the classifier choice and the features has also been outlined.
Denotational semantics for modal systems S3--S5 extended by axioms for propositional quantifiers and identity
Venue: arXiv cs.LO 2014
Year: 2014

There are logics where necessity is defined by means of a given identity connective: $\squareφ:= φ\equiv\top$ ($\top$ is a tautology). On the other hand, in many standard modal logics the concept of propositional identity (PI) $φ\equivψ$ can be defined by strict equivalence (SE) $\square(φ\leftrightarrowψ)$. All these approaches to modality involve a principle that we call the Collapse Axiom (CA): "There is only one necessary proposition." In this paper, we consider a notion of PI which relies on the identity axioms of Suszko's non-Fregean logic $\mathit{SCI}$. Then $S3$ proves to be the smallest Lewis modal system where PI can be defined as SE. We extend $S3$ to a non-Fregean logic with propositional quantifiers such that necessity and PI are integrated as non-interdefinable concepts. CA is not valid and PI refines SE. Models are expansions of $\mathit{SCI}$-models. We show that $\mathit{SCI}$-models are Boolean prealgebras, and vice-versa. This associates Non-Fregean Logic with research on Hyperintensional Semantics. PI equals SE iff models are Boolean algebras and CA holds. A representation result establishes a connection to Fine's approach to propositional quantifiers and shows that our theories are \textit{conservative} extensions of $S3$--$S5$, respectively. If we exclude the Barcan formula and a related axiom, then the resulting systems are still complete w.r.t. a simpler denotational semantics.
A Dichotomy on the Complexity of Consistent Query Answering for Atoms with Simple Keys
Venue: arXiv cs.DB 2014
Year: 2014

We study the problem of consistent query answering under primary key violations. In this setting, the relations in a database violate the key constraints and we are interested in maximal subsets of the database that satisfy the constraints, which we call repairs. For a boolean query Q, the problem CERTAINTY(Q) asks whether every such repair satisfies the query or not; the problem is known to be always in coNP for conjunctive queries. However, there are queries for which it can be solved in polynomial time. It has been conjectured that there exists a dichotomy on the complexity of CERTAINTY(Q) for conjunctive queries: it is either in PTIME or coNP-complete. In this paper, we prove that the conjecture is indeed true for the case of conjunctive queries without self-joins, where each atom has as a key either a single attribute (simple key) or all attributes of the atom.
Robustness of Sparse Recovery via $F$-minimization: A Topological Viewpoint
Venue: arXiv cs.IT 2014
Year: 2014

A recent trend in compressed sensing is to consider non-convex optimization techniques for sparse recovery. The important case of $F$-minimization has become of particular interest, for which the exact reconstruction condition (ERC) in the noiseless setting can be precisely characterized by the null space property (NSP). However, little work has been done concerning its robust reconstruction condition (RRC) in the noisy setting. We look at the null space of the measurement matrix as a point on the Grassmann manifold, and then study the relation between the ERC and RRC sets, denoted as $Ω_J$ and $Ω_J^r$, respectively. It is shown that $Ω_J^r$ is the interior of $Ω_J$, from which a previous result of the equivalence of ERC and RRC for $\ell_p$-minimization follows easily as a special case. Moreover, when $F$ is non-decreasing, it is shown that $\overlineΩ_J\setminus\interior(Ω_J)$ is a set of measure zero and of the first category. As a consequence, the probabilities of ERC and RRC are the same if the measurement matrix $\mathbf{A}$ is randomly generated according to a continuous distribution. Quantitatively, if the null space $\mathcal{N}(\bf A)$ lies in the "$d$-interior" of $Ω_J$, then RRC will be satisfied with the robustness constant $C=\frac{2+2d}{dσ_{\min}(\mathbf{A}^{\top})}$; and conversely if RRC holds with $C=\frac{2-2d}{dσ_{\max}(\mathbf{A}^{\top})}$, then $\mathcal{N}(\bf A)$ must lie in $d$-interior of $Ω_J$. We also present several rules for comparing the performances of different cost functions. Finally, these results are capitalized to derive achievable tradeoffs between the measurement rate and robustness with the aid of Gordon's escape through the mesh theorem or a connection between NSP and the restricted eigenvalue condition.
Modeling complex systems by Generalized Factor Analysis
Venue: arXiv cs.SY 2014
Year: 2014

We propose a new modeling paradigm for large dimensional aggregates of stochastic systems by Generalized Factor Analysis (GFA) models. These models describe the data as the sum of a flocking plus an uncorrelated idiosyncratic component. The flocking component describes a sort of collective orderly motion which admits a much simpler mathematical description than the whole ensemble while the idiosyncratic component describes weakly correlated noise. We first discuss static GFA representations and characterize in a rigorous way the properties of the two components. The extraction of the dynamic flocking component is discussed for time-stationary linear systems and for a simple classes of separable random fields.
Optimal Coding Functions for Pairwise Message Sharing on Finite-Field Multi-Way Relay Channels
Venue: arXiv cs.IT 2014
Year: 2014

This paper considers the finite-field multi-way relay channel with pairwise message sharing, where multiple users exchange messages through a single relay and where the users may share parts of their source messages (meaning that some message parts are known/common to more than one user). In this paper, we design an optimal functional-decode-forward coding scheme that takes the shared messages into account. More specifically, we design an optimal function for the relay to decode (from the users on the uplink) and forward (back to the users on the downlink). We then show that this proposed function-decode-forward coding scheme can achieve the capacity region of the finite-field multi-way relay channel with pairwise message sharing. This paper generalizes our previous result for the case of three users to any number of users.
From Approximate Factorization to Root Isolation with Application to Cylindrical Algebraic Decomposition
Venue: arXiv cs.SC 2014
Year: 2014

We present an algorithm for isolating the roots of an arbitrary complex polynomial $p$ that also works for polynomials with multiple roots provided that the number $k$ of distinct roots is given as part of the input. It outputs $k$ pairwise disjoint disks each containing one of the distinct roots of $p$, and its multiplicity. The algorithm uses approximate factorization as a subroutine. In addition, we apply the new root isolation algorithm to a recent algorithm for computing the topology of a real planar algebraic curve specified as the zero set of a bivariate integer polynomial and for isolating the real solutions of a bivariate polynomial system. For input polynomials of degree $n$ and bitsize $τ$, we improve the currently best running time from $\tO(n^{9}τ+n^{8}τ^{2})$ (deterministic) to $\tO(n^{6}+n^{5}τ)$ (randomized) for topology computation and from $\tO(n^{8}+n^{7}τ)$ (deterministic) to $\tO(n^{6}+n^{5}τ)$ (randomized) for solving bivariate systems.
Minimax Filtering via Relations between Information and Estimation
Venue: arXiv cs.IT 2014
Year: 2014

We investigate the problem of continuous-time causal estimation under a minimax criterion. Let $X^T = \{X_t,0\leq t\leq T\}$ be governed by the probability law $P_θ$ from a class of possible laws indexed by $θ\in Λ$, and $Y^T$ be the noise corrupted observations of $X^T$ available to the estimator. We characterize the estimator minimizing the worst case regret, where regret is the difference between the causal estimation loss of the estimator and that of the optimum estimator. One of the main contributions of this paper is characterizing the minimax estimator, showing that it is in fact a Bayesian estimator. We then relate minimax regret to the channel capacity when the channel is either Gaussian or Poisson. In this case, we characterize the minimax regret and the minimax estimator more explicitly. If we further assume that the uncertainty set consists of deterministic signals, the worst case regret is exactly equal to the corresponding channel capacity, namely the maximal mutual information attainable across the channel among all possible distributions on the uncertainty set of signals. The corresponding minimax estimator is the Bayesian estimator assuming the capacity-achieving prior. Using this relation, we also show that the capacity achieving prior coincides with the least favorable input. Moreover, we show that this minimax estimator is not only minimizing the worst case regret but also essentially minimizing regret for "most" of the other sources in the uncertainty set. We present a couple of examples for the construction of an minimax filter via an approximation of the associated capacity achieving distribution.
Efficient MRF Energy Propagation for Video Segmentation via Bilateral Filters
Venue: arXiv cs.CV 2014
Year: 2014

Segmentation of an object from a video is a challenging task in multimedia applications. Depending on the application, automatic or interactive methods are desired; however, regardless of the application type, efficient computation of video object segmentation is crucial for time-critical applications; specifically, mobile and interactive applications require near real-time efficiencies. In this paper, we address the problem of video segmentation from the perspective of efficiency. We initially redefine the problem of video object segmentation as the propagation of MRF energies along the temporal domain. For this purpose, a novel and efficient method is proposed to propagate MRF energies throughout the frames via bilateral filters without using any global texture, color or shape model. Recently presented bi-exponential filter is utilized for efficiency, whereas a novel technique is also developed to dynamically solve graph-cuts for varying, non-lattice graphs in general linear filtering scenario. These improvements are experimented for both automatic and interactive video segmentation scenarios. Moreover, in addition to the efficiency, segmentation quality is also tested both quantitatively and qualitatively. Indeed, for some challenging examples, significant time efficiency is observed without loss of segmentation quality.
The Power of Priority Channel Systems
Venue: arXiv cs.LO 2014
Year: 2014

We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing functions and prove that the aforementioned verification problems are $\mathbf{F}_{\varepsilon_{0}}$-complete.
Deterministic Constructions of Binary Measurement Matrices from Finite Geometry
Venue: arXiv cs.IT 2014
Year: 2014

Deterministic constructions of measurement matrices in compressed sensing (CS) are considered in this paper. The constructions are inspired by the recent discovery of Dimakis, Smarandache and Vontobel which says that parity-check matrices of good low-density parity-check (LDPC) codes can be used as {provably} good measurement matrices for compressed sensing under $\ell_1$-minimization. The performance of the proposed binary measurement matrices is mainly theoretically analyzed with the help of the analyzing methods and results from (finite geometry) LDPC codes. Particularly, several lower bounds of the spark (i.e., the smallest number of columns that are linearly dependent, which totally characterizes the recovery performance of $\ell_0$-minimization) of general binary matrices and finite geometry matrices are obtained and they improve the previously known results in most cases. Simulation results show that the proposed matrices perform comparably to, sometimes even better than, the corresponding Gaussian random matrices. Moreover, the proposed matrices are sparse, binary, and most of them have cyclic or quasi-cyclic structure, which will make the hardware realization convenient and easy.
Recycling Proof Patterns in Coq: Case Studies
Venue: arXiv cs.AI 2014
Year: 2014

Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.
Skeletal Representations and Applications
Venue: arXiv cs.GR 2014
Year: 2014

When representing a solid object there are alternatives to the use of traditional explicit (surface meshes) or implicit (zero crossing of implicit functions) methods. Skeletal representations encode shape information in a mixed fashion: they are composed of a set of explicit primitives, yet they are able to efficiently encode the shape's volume as well as its topology. I will discuss, in two dimensions, how symmetry can be used to reduce the dimensionality of the data (from a 2D solid to a 1D curve), and how this relates to the classical definition of skeletons by Medial Axis Transform. While the medial axis of a 2D shape is composed of a set of curves, in 3D it results in a set of sheets connected in a complex fashion. Because of this complexity, medial skeletons are difficult to use in practical applications. Curve skeletons address this problem by strictly requiring their geometry to be one dimensional, resulting in an intuitive yet powerful shape representation. In this report I will define both medial and curve skeletons and discuss their mutual relationship. I will also present several algorithms for their computation and a variety of scenarios where skeletons are employed, with a special focus on geometry processing and shape analysis.
SMML estimators for exponential families with continuous sufficient statistics
Venue: arXiv cs.IT 2014
Year: 2014

The minimum message length principle is an information theoretic criterion that links data compression with statistical inference. This paper studies the strict minimum message length (SMML) estimator for $d$-dimensional exponential families with continuous sufficient statistics, for all $d \ge 1$. The partition of an SMML estimator is shown to consist of convex polytopes (i.e. convex polygons when $d=2$) which can be described explicitly in terms of the assertions and coding probabilities. While this result is known, we give a new proof based on the calculus of variations, and this approach gives some interesting new inequalities for SMML estimators. We also use this result to construct an SMML estimator for a $2$-dimensional normal random variable with known variance and a normal prior on its mean.
Secrecy capacities of compound quantum wiretap channels and applications
Venue: arXiv cs.IT 2014
Year: 2014

We determine the secrecy capacity of the compound channel with quantum wiretapper and channel state information at the transmitter. Moreover, we derive a lower bound on the secrecy capacity of this channel without channel state information and determine the secrecy capacity of the compound classical-quantum wiretap channel with channel state information at the transmitter. We use this result to derive a new proof for a lower bound on the entanglement generating capacity of compound quantum channel. We also derive a new proof for the entanglement generating capacity of compound quantum channel with channel state information at the encoder.
One-variable word equations in linear time
Venue: arXiv cs.FL 2014
Year: 2014

In this paper we consider word equations with one variable (and arbitrary many appearances of it). A recent technique of recompression, which is applicable to general word equations, is shown to be suitable also in this case. While in general case it is non-deterministic, it determinises in case of one variable and the obtained running time is O(n + #_X log n), where #_X is the number of appearances of the variable in the equation. This matches the previously-best algorithm due to Dąbrowski and Plandowski. Then, using a couple of heuristics as well as more detailed time analysis the running time is lowered to O(n) in RAM model. Unfortunately no new properties of solutions are shown.
A o(n) monotonicity tester for Boolean functions over the hypercube
Venue: arXiv cs.DM 2014
Year: 2014

A Boolean function $f:\{0,1\}^n \mapsto \{0,1\}$ is said to be $\eps$-far from monotone if $f$ needs to be modified in at least $\eps$-fraction of the points to make it monotone. We design a randomized tester that is given oracle access to $f$ and an input parameter $\eps>0$, and has the following guarantee: It outputs {\sf Yes} if the function is monotonically non-decreasing, and outputs {\sf No} with probability $>2/3$, if the function is $\eps$-far from monotone. This non-adaptive, one-sided tester makes $O(n^{7/8}\eps^{-3/2}\ln(1/\eps))$ queries to the oracle.
Constrained Signaling in Auction Design
Venue: arXiv cs.GT 2014
Year: 2014

We consider the problem of an auctioneer who faces the task of selling a good (drawn from a known distribution) to a set of buyers, when the auctioneer does not have the capacity to describe to the buyers the exact identity of the good that he is selling. Instead, he must come up with a constrained signalling scheme: a (non injective) mapping from goods to signals, that satisfies the constraints of his setting. For example, the auctioneer may be able to communicate only a bounded length message for each good, or he might be legally constrained in how he can advertise the item being sold. Each candidate signaling scheme induces an incomplete-information game among the buyers, and the goal of the auctioneer is to choose the signaling scheme and accompanying auction format that optimizes welfare. In this paper, we use techniques from submodular function maximization and no-regret learning to give algorithms for computing constrained signaling schemes for a variety of constrained signaling problems.
Matching Pursuit LASSO Part II: Applications and Sparse Recovery over Batch Signals
Venue: arXiv cs.CV 2014
Year: 2014

Matching Pursuit LASSIn Part I \cite{TanPMLPart1}, a Matching Pursuit LASSO ({MPL}) algorithm has been presented for solving large-scale sparse recovery (SR) problems. In this paper, we present a subspace search to further improve the performance of MPL, and then continue to address another major challenge of SR -- batch SR with many signals, a consideration which is absent from most of previous $\ell_1$-norm methods. As a result, a batch-mode {MPL} is developed to vastly speed up sparse recovery of many signals simultaneously. Comprehensive numerical experiments on compressive sensing and face recognition tasks demonstrate the superior performance of MPL and BMPL over other methods considered in this paper, in terms of sparse recovery ability and efficiency. In particular, BMPL is up to 400 times faster than existing $\ell_1$-norm methods considered to be state-of-the-art.O Part II: Applications and Sparse Recovery over Batch Signals