OpenRaiser/Intern-Atlas huggingface dataset:
Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants
Venue: arXiv cs.NE 2016
Year: 2016

Mathematical theorems are human knowledge able to be accumulated in the form of symbolic representation, and proving theorems has been considered intelligent behavior. Based on the BHK interpretation and the Curry-Howard isomorphism, proof assistants, software capable of interacting with human for constructing formal proofs, have been developed in the past several decades. Since proofs can be considered and expressed as programs, proof assistants simplify and verify a proof by computationally evaluating the program corresponding to the proof. Thanks to the transformation from logic to computation, it is now possible to generate or search for formal proofs directly in the realm of computation. Evolutionary algorithms, known to be flexible and versatile, have been successfully applied to handle a variety of scientific and engineering problems in numerous disciplines for also several decades. Examining the feasibility of establishing the link between evolutionary algorithms, as the program generator, and proof assistants, as the proof verifier, in order to automatically find formal proofs to a given logic sentence is the primary goal of this study. In the article, we describe in detail our first, ad-hoc attempt to fully automatically prove theorems as well as the preliminary results. Ten simple theorems from various branches of mathematics were proven, and most of these theorems cannot be proven by using the tactic auto alone in Coq, the adopted proof assistant. The implication and potential influence of this study are discussed, and the developed source code with the obtained experimental results are released as open source.
New Stability and Exact Observability Conditions for Semilinear Wave Equations
Venue: arXiv cs.SY 2016
Year: 2016

The problem of estimating the initial state of 1-D wave equations with globally Lipschitz nonlinearities from boundary measurements on a finite interval was solved recently by using the sequence of forward and backward observers, and deriving the upper bound for exact observability time in terms of Linear Matrix Inequalities (LMIs) [5]. In the present paper, we generalize this result to n-D wave equations on a hypercube. This extension includes new LMI-based exponential stability conditions for n-D wave equations, as well as an upper bound on the minimum exact observability time in terms of LMIs. For 1-D wave equations with locally Lipschitz nonlinearities, we find an estimate on the region of initial conditions that are guaranteed to be uniquely recovered from the measurements. The efficiency of the results is illustrated by numerical examples.
Listen-and-Talk: Protocol Design and Analysis for Full-duplex Cognitive Radio Networks
Venue: arXiv cs.NI 2016
Year: 2016

In traditional cognitive radio networks, secondary users (SUs) typically access the spectrum of primary users (PUs) by a two-stage "listen-before-talk" (LBT) protocol, i.e., SUs sense the spectrum holes in the first stage before transmitting in the second. However, there exist two major problems: 1) transmission time reduction due to sensing, and 2) sensing accuracy impairment due to data transmission. In this paper, we propose a "listen-and-talk" (LAT) protocol with the help of full-duplex (FD) technique that allows SUs to simultaneously sense and access the vacant spectrum. Spectrum utilization performance is carefully analyzed, with the closed-form spectrum waste ratio and collision ratio with the PU provided. Also, regarding the secondary throughput, we report the existence of a tradeoff between the secondary transmit power and throughput. Based on the power-throughput tradeoff, we derive the analytical local optimal transmit power for SUs to achieve both high throughput and satisfying sensing accuracy. Numerical results are given to verify the proposed protocol and the theoretical results.
Content Providers Volunteering to Pay Network Providers: Better than Neutrality?
Venue: arXiv cs.NI 2016
Year: 2016

This paper studies the effects on user welfare of imposing network neutrality, using a game-theoretic model of provider interactions based on a two-sided market framework: we assume that the platform--the last-mile access providers (ISPs)--are monopolists, and consider content providers (CPs) entry decisions. All decisions affect the choices made by users, who are sensitive both to CP and ISP investments (in content creation and quality-of-service, respectively). In a non-neutral regime, CPs and ISPs can charge each other, while such charges are prohibited in the neutral regime. We assume those charges (if any) are chosen by CPs, a direction rarely considered in the literature, where they are assumed fixed by ISPs. Our analysis suggests that, unexpectedly, more CPs enter the market in a non-neutral regime where they pay ISPs, than without such payments. Additionally, in this case ISPs tend to invest more than in the neutral regime. From our results, the best regime in terms of user welfare is parameter dependent, calling for caution in designing neutrality regulations.
A Note on Modeling Self-Suspending Time as Blocking Time in Real-Time Systems
Venue: arXiv cs.DS 2016
Year: 2016

This report presents a proof to support the correctness of the schedulability test for self-suspending real-time task systems proposed by Jane W. S. Liu in her book titled "Real-Time Systems" (Pages 164-165). The same concept was also implicitly used by Rajkumar, Sha, and Lehoczky in RTSS 1988 (Page 267) for analyzing self-suspending behaviour due to synchronization protocols in multiprocessor systems.
Low Complexity Sparse Bayesian Learning Using Combined BP and MF with a Stretched Factor Graph
Venue: arXiv cs.IT 2016
Year: 2016

This paper concerns message passing based approaches to sparse Bayesian learning (SBL) with a linear model corrupted by additive white Gaussian noise with unknown variance. With the conventional factor graph, mean field (MF) message passing based algorithms have been proposed in the literature. In this work, instead of using the conventional factor graph, we modify the factor graph by adding some extra hard constraints (the graph looks like being `stretched'), which enables the use of combined belief propagation (BP) and MF message passing. We then propose a low complexity BP-MF SBL algorithm based on which an approximate BP-MF SBL algorithm is also developed to further reduce the complexity. Thanks to the use of BP, the BP-MF SBL algorithms show their merits compared with state-of-the-art MF SBL algorithms: they deliver even better performance with much lower complexity compared with the vector-form MF SBL algorithm and they significantly outperform the scalar-form MF SBL algorithm with similar complexity.
Crisis Analytics: Big Data Driven Crisis Response
Venue: arXiv cs.CY 2016
Year: 2016

Disasters have long been a scourge for humanity. With the advances in technology (in terms of computing, communications, and the ability to process and analyze big data), our ability to respond to disasters is at an inflection point. There is great optimism that big data tools can be leveraged to process the large amounts of crisis-related data (in the form of user generated data in addition to the traditional humanitarian data) to provide an insight into the fast-changing situation and help drive an effective disaster response. This article introduces the history and the future of big crisis data analytics, along with a discussion on its promise, challenges, and pitfalls.
Visualizing Class Information
Venue: arXiv cs.SE 2016
Year: 2016

A class is used in object oriented programming to describe each object in the system. It is as a template contains the methods and attributes for each object. The volume of information within the class has a role in the time required for its implementation, testing and understanding the class. Developers are dealing with large projects that contain a large number of Lines Of Code (LOC). So that, extracting information about the classes requires time and big effort from the developers. To solve this problem, we present a visualization approach to display class information for developers. Our method assumed each class is a cone chart and each cone represents one of the class metrics that include number of methods, attributes and the number of Lines Of Code (LOC). The height of each cone indicates the total number of methods, attributes and number of Lines Of Code (LOC) which found in a class. Also, each cone has a different color from the other to facilitate the distinction among them
Thompson Sampling is Asymptotically Optimal in General Environments
Venue: arXiv cs.LG 2016
Year: 2016

We discuss a variant of Thompson sampling for nonparametric reinforcement learning in a countable classes of general stochastic environments. These environments can be non-Markov, non-ergodic, and partially observable. We show that Thompson sampling learns the environment class in the sense that (1) asymptotically its value converges to the optimal value in mean and (2) given a recoverability assumption regret is sublinear.
Contrasting Effects of Replication in Parallel Systems: From Overload to Underload and Back
Venue: arXiv cs.PF 2016
Year: 2016

Task replication has recently been advocated as a practical solution to reduce latencies in parallel systems. In addition to several convincing empirical studies, some others provide analytical results, yet under some strong assumptions such as Poisson arrivals, exponential service times, or independent service times of the replicas themselves, which may lend themselves to some contrasting and perhaps contriving behavior. For instance, under the second assumption, an overloaded system can be stabilized by a replication factor, but can be sent back in overload through further replication. In turn, under the third assumption, strictly larger stability regions of replication systems do not necessarily imply smaller delays. Motivated by the need to dispense with such common and restricting assumptions, which may additionally cause unexpected behavior, we develop a unified and general theoretical framework to compute tight bounds on the distribution of response times in general replication systems. These results immediately lend themselves to the optimal number of replicas minimizing response time quantiles, depending on the parameters of the system (e.g., the degree of correlation amongst replicas). As a concrete application of our framework, we design a novel replication policy which can improve the stability region of classical fork-join queueing systems by $\mathcal{O}(\ln K)$, in the number of servers $K$.
Zero-Suppressed Computation: A New Computation Inspired by ZDDs
Venue: arXiv cs.CC 2016
Year: 2016

Zero-suppressed binary decision diagrams (ZDDs) are a data structure representing Boolean functions, and one of the most successful variants of binary decision diagrams (BDDs). On the other hand, BDDs are also called branching programs in computational complexity theory, and have been studied as a computation model. In this paper, we consider ZDDs from the viewpoint of computational complexity theory. Our main proposal of this paper is that we regard the basic idea of ZDDs as a new computation, which we call zero-suppressed computation. We consider the zero-suppressed version of two classical computation models, decision trees and branching programs, and show some results. Although this paper is mainly written from the viewpoint of computational complexity theory, the concept of zero-suppressed computation can be widely applied to various areas.
Hierarchical Conflict Propagation: Sequence Learning in a Recurrent Deep Neural Network
Venue: arXiv cs.LG 2016
Year: 2016

Recurrent neural networks (RNN) are capable of learning to encode and exploit activation history over an arbitrary timescale. However, in practice, state of the art gradient descent based training methods are known to suffer from difficulties in learning long term dependencies. Here, we describe a novel training method that involves concurrent parallel cloned networks, each sharing the same weights, each trained at different stimulus phase and each maintaining independent activation histories. Training proceeds by recursively performing batch-updates over the parallel clones as activation history is progressively increased. This allows conflicts to propagate hierarchically from short-term contexts towards longer-term contexts until they are resolved. We illustrate the parallel clones method and hierarchical conflict propagation with a character-level deep RNN tasked with memorizing a paragraph of Moby Dick (by Herman Melville).
Auto-JacoBin: Auto-encoder Jacobian Binary Hashing
Venue: arXiv cs.CV 2016
Year: 2016

Binary codes can be used to speed up nearest neighbor search tasks in large scale data sets as they are efficient for both storage and retrieval. In this paper, we propose a robust auto-encoder model that preserves the geometric relationships of high-dimensional data sets in Hamming space. This is done by considering a noise-removing function in a region surrounding the manifold where the training data points lie. This function is defined with the property that it projects the data points near the manifold into the manifold wisely, and we approximate this function by its first order approximation. Experimental results show that the proposed method achieves better than state-of-the-art results on three large scale high dimensional data sets.
Bandwidth Extension of Narrowband Speech for Low Bit-Rate Wideband Coding
Venue: arXiv cs.SD 2016
Year: 2016

Wireless telephone speech is usually limited to the 300-3400 Hz band, which reduces its quality. There is thus a growing demand for wideband speech systems that transmit from 50 Hz to 8000 Hz. This paper presents an algorithm to generate wideband speech from narrowband speech using as low as 500 bits/s of side information. The 50-300 Hz band is predicted from the narrowband signal. A source-excitation model is used for the 3400-8000 Hz band, where the excitation is extrapolated at the receiver, and the spectral envelope is transmitted. Though some artifacts are present, the resulting wideband speech has enhanced quality compared to narrowband speech.
Cache-enabled Heterogeneous Cellular Networks: Comparison and Tradeoffs
Venue: arXiv cs.IT 2016
Year: 2016

Caching popular contents at base stations (BSs) is a promising way to unleash the potential of cellular heterogeneous networks (HetNets), where backhaul has become a bottleneck. In this paper, we compare a cache-enabled HetNet where a tier of multi-antenna macro BSs is overlaid by a tier of helper nodes having caches but no backhaul with a conventional HetNet where the macro BSs tier is overlaid by a tier of pico BSs with limited-capacity backhaul. We resort stochastic geometry theory to derive the area spectral efficiencies (ASEs) of these two kinds of HetNets and obtain the closed-form expressions under a special case. We use numerical results to show that the helper density is only 1/4 of the pico BS density to achieve the same target ASE, and the helper density can be further reduced by increasing cache capacity. With given total cache capacity within an area, there exists an optimal helper node density that maximizes the ASE.
Explicit back-off rates for achieving target throughputs in CSMA/CA networks
Venue: arXiv cs.NI 2016
Year: 2016

CSMA/CA networks have often been analyzed using a stylized model that is fully characterized by a vector of back-off rates and a conflict graph. Further, for any achievable throughput vector $\vec θ$ the existence of a unique vector $\vec ν(\vec θ)$ of back-off rates that achieves this throughput vector was proven. Although this unique vector can in principle be computed iteratively, the required time complexity grows exponentially in the network size, making this only feasible for small networks. In this paper, we present an explicit formula for the unique vector of back-off rates $\vec ν(\vec θ)$ needed to achieve any achievable throughput vector $\vec θ$ provided that the network has a chordal conflict graph. This class of networks contains a number of special cases of interest such as (inhomogeneous) line networks and networks with an acyclic conflict graph. Moreover, these back-off rates are such that the back-off rate of a node only depends on its own target throughput and the target throughput of its neighbors and can be determined in a distributed manner. We further indicate that back-off rates of this form cannot be obtained in general for networks with non-chordal conflict graphs. For general conflict graphs we nevertheless show how to adapt the back-off rates when a node is added to the network when its interfering nodes form a clique in the conflict graph. Finally, we introduce a distributed chordal approximation algorithm for general conflict graphs which is shown (using numerical examples) to be more accurate than the Bethe approximation.
Graph Isomorphism for unit square graphs
Venue: arXiv cs.DS 2016
Year: 2016

In the past decades for more and more graph classes the Graph Isomorphism Problem was shown to be solvable in polynomial time. An interesting family of graph classes arises from intersection graphs of geometric objects. In this work we show that the Graph Isomorphism Problem for unit square graphs, intersection graphs of axis-parallel unit squares in the plane, can be solved in polynomial time. Since the recognition problem for this class of graphs is NP-hard we can not rely on standard techniques for geometric graphs based on constructing a canonical realization. Instead, we develop new techniques which combine structural insights into the class of unit square graphs with understanding of the automorphism group of such graphs. For the latter we introduce a generalization of bounded degree graphs which is used to capture the main structure of unit square graphs. Using group theoretic algorithms we obtain sufficient information to solve the isomorphism problem for unit square graphs.
Trace semantics for polymorphic references
Venue: arXiv cs.PL 2016
Year: 2016

We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure of typing information in the semantics. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.
Patch-Ordering as a Regularization for Inverse Problems in Image Processing
Venue: arXiv cs.CV 2016
Year: 2016

Recent work in image processing suggests that operating on (overlapping) patches in an image may lead to state-of-the-art results. This has been demonstrated for a variety of problems including denoising, inpainting, deblurring, and super-resolution. The work reported in [1,2] takes an extra step forward by showing that ordering these patches to form an approximate shortest path can be leveraged for better processing. The core idea is to apply a simple filter on the resulting 1D smoothed signal obtained after the patch-permutation. This idea has been also explored in combination with a wavelet pyramid, leading eventually to a sophisticated and highly effective regularizer for inverse problems in imaging. In this work we further study the patch-permutation concept, and harness it to propose a new simple yet effective regularization for image restoration problems. Our approach builds on the classic Maximum A'posteriori probability (MAP), with a penalty function consisting of a regular log-likelihood term and a novel permutation-based regularization term. Using a plain 1D Laplacian, the proposed regularization forces robust smoothness (L1) on the permuted pixels. Since the permutation originates from patch-ordering, we propose to accumulate the smoothness terms over all the patches' pixels. Furthermore, we take into account the found distances between adjacent patches in the ordering, by weighting the Laplacian outcome. We demonstrate the proposed scheme on a diverse set of problems: (i) severe Poisson image denoising, (ii) Gaussian image denoising, (iii) image deblurring, and (iv) single image super-resolution. In all these cases, we use recent methods that handle these problems as initialization to our scheme. This is followed by an L-BFGS optimization of the above-described penalty function, leading to state-of-the-art results, and especially so for highly ill-posed cases.
Multiplier-less Artificial Neurons Exploiting Error Resiliency for Energy-Efficient Neural Computing
Venue: arXiv cs.NE 2016
Year: 2016

Large-scale artificial neural networks have shown significant promise in addressing a wide range of classification and recognition applications. However, their large computational requirements stretch the capabilities of computing platforms. The fundamental components of these neural networks are the neurons and its synapses. The core of a digital hardware neuron consists of multiplier, accumulator and activation function. Multipliers consume most of the processing energy in the digital neurons, and thereby in the hardware implementations of artificial neural networks. We propose an approximate multiplier that utilizes the notion of computation sharing and exploits error resilience of neural network applications to achieve improved energy consumption. We also propose Multiplier-less Artificial Neuron (MAN) for even larger improvement in energy consumption and adapt the training process to ensure minimal degradation in accuracy. We evaluated the proposed design on 5 recognition applications. The results show, 35% and 60% reduction in energy consumption, for neuron sizes of 8 bits and 12 bits, respectively, with a maximum of ~2.83% loss in network accuracy, compared to a conventional neuron implementation. We also achieve 37% and 62% reduction in area for a neuron size of 8 bits and 12 bits, respectively, under iso-speed conditions.
On the Hardness of SAT with Community Structure
Venue: arXiv cs.LO 2016
Year: 2016

Recent attempts to explain the effectiveness of Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) on large industrial benchmarks have focused on the concept of community structure. Specifically, industrial benchmarks have been empirically found to have good community structure, and experiments seem to show a correlation between such structure and the efficiency of CDCL. However, in this paper we establish hardness results suggesting that community structure is not sufficient to explain the success of CDCL in practice. First, we formally characterize a property shared by a wide class of metrics capturing community structure, including "modularity". Next, we show that the SAT instances with good community structure according to any metric with this property are still NP-hard. Finally, we study a class of random instances generated from the "pseudo-industrial" community attachment model of Giráldez-Cru and Levy. We prove that, with high probability, instances from this model that have relatively few communities but are still highly modular require exponentially long resolution proofs and so are hard for CDCL. We also present experimental evidence that our result continues to hold for instances with many more communities. This indicates that actual industrial instances easily solved by CDCL may have some other relevant structure not captured by the community attachment model.