OpenRaiser/Intern-Atlas huggingface dataset:
Variations on Noetherianness
Venue: arXiv cs.LO 2016
Year: 2016

In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We want to say that a set is Noetherian, if, when we are shown elements from it one after another, we will sooner or later have seen some element twice. This idea can be made precise in a number of ways. We explore the properties and connections of some of the possible encodings. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally, we explore the relation between Noetherianness and other notions of finiteness.
Feature extraction using Latent Dirichlet Allocation and Neural Networks: A case study on movie synopses
Venue: arXiv cs.CL 2016
Year: 2016

Feature extraction has gained increasing attention in the field of machine learning, as in order to detect patterns, extract information, or predict future observations from big data, the urge of informative features is crucial. The process of extracting features is highly linked to dimensionality reduction as it implies the transformation of the data from a sparse high-dimensional space, to higher level meaningful abstractions. This dissertation employs Neural Networks for distributed paragraph representations, and Latent Dirichlet Allocation to capture higher level features of paragraph vectors. Although Neural Networks for distributed paragraph representations are considered the state of the art for extracting paragraph vectors, we show that a quick topic analysis model such as Latent Dirichlet Allocation can provide meaningful features too. We evaluate the two methods on the CMU Movie Summary Corpus, a collection of 25,203 movie plot summaries extracted from Wikipedia. Finally, for both approaches, we use K-Nearest Neighbors to discover similar movies, and plot the projected representations using T-Distributed Stochastic Neighbor Embedding to depict the context similarities. These similarities, expressed as movie distances, can be used for movies recommendation. The recommended movies of this approach are compared with the recommended movies from IMDB, which use a collaborative filtering recommendation approach, to show that our two models could constitute either an alternative or a supplementary recommendation approach.
Unsatisfiable hitting clause-sets with three more clauses than variables
Venue: arXiv cs.DM 2016
Year: 2016

The topic of this paper is the Finiteness Conjecture for minimally unsatisfiable clause-sets (MUs), stating that for each fixed deficiency (number of clauses minus number of variables) there are only finitely many patterns, given a certain basic reduction (generalising unit-clause propagation). We focus our attention on hitting clause-sets (every two clauses have at least one clash), where the conjecture says that there are only finitely many isomorphism types. The Finiteness Conjecture is here known to hold for deficiency at most 2, and we now prove it for deficiency 3. An important tool is the notion of "(ir)reducible clause-sets": we show how to reduce the general question to the irreducible case, and then solve this case (for deficiency 3). This notion comes from number theory (Korec 1984, Berger et al 1990), and we rediscovered it in our studies.
Implementation of the Programming Language Dino -- A Case Study in Dynamic Language Performance
Venue: arXiv cs.PL 2016
Year: 2016

The article gives a brief overview of the current state of programming language Dino in order to see where its stands between other dynamic programming languages. Then it describes the current implementation, used tools and major implementation decisions including how to implement a stable, portable and simple JIT compiler. We study the effect of major implementation decisions on the performance of Dino on x86-64, AARCH64, and Powerpc64. In brief, the performance of some model benchmark on x86-64 was improved by $\textbf{3.1}$ times after moving from a stack based virtual machine to a register-transfer architecture, a further $\textbf{1.5}$ times by adding byte code combining, a further $\textbf{2.3}$ times through the use of JIT, and a further $\textbf{4.4}$ times by performing type inference with byte code specialization, with a resulting overall performance improvement of about $\textbf{47}$ times. To put these results in context, we include performance comparisons of Dino with widely used implementations of Ruby, Python 3, PyPy and JavaScript on the three platforms mentioned above. The goal of this article is to share the experience of Dino implementation with other dynamic language implementors in hope that it can help them to improve implementation of popular dynamic languages to make them probably faster and more portable, using less developer resources, and may be to avoid some mistakes and wrong directions which were experienced during Dino development.
Convergence of MCMC and Loopy BP in the Tree Uniqueness Region for the Hard-Core Model
Venue: arXiv cs.DM 2016
Year: 2016

We study the hard-core model defined on independent sets of an input graph where the independent sets are weighted by a parameter $λ>0$. For constant $Δ$, previous work of Weitz (2006) established an FPTAS for the partition function for graphs of maximum degree $Δ$ when $λ< λ_c(Δ)$. The threshold $λ_c(Δ)$ is the critical point for the phase transition for uniqueness/non-uniqueness on the infinite $Δ$-regular trees. Sly (2010) showed that there is no FPRAS, unless NP=RP, when $λ>λ_c(Δ)$. The running time of Weitz's algorithm is exponential in $\log(Δ)$. Here we present an FPRAS for the partition function whose running time is $O^*(n^2)$. We analyze the simple single-site Glauber dynamics for sampling from the associated Gibbs distribution. We prove there exists a constant $Δ_0$ such that for all graphs with maximum degree $Δ\geqΔ_0$ and girth $\geq 7$, the mixing time of the Glauber dynamics is $O(n\log(n))$ when $λ<λ_c(Δ)$. Our work complements that of Weitz which applies for constant $Δ$ whereas our work applies for all $Δ\geq Δ_0$. We utilize loopy BP (belief propagation), a widely-used inference algorithm. A novel aspect of our work is using the principal eigenvector for the BP operator to design a distance function which contracts in expectation for pairs of states that behave like the BP fixed point. We also prove that the Glauber dynamics behaves locally like loopy BP. As a byproduct we obtain that the Glauber dynamics converges, after a short burn-in period, close to the BP fixed point, and this implies that the fixed point of loopy BP is a close approximation to the Gibbs distribution. Using these connections we establish that loopy BP quickly converges to the Gibbs distribution when the girth $\geq 6$ and $λ<λ_c(Δ)$.
A Focused Dynamic Attention Model for Visual Question Answering
Venue: arXiv cs.CV 2016
Year: 2016

Visual Question and Answering (VQA) problems are attracting increasing interest from multiple research disciplines. Solving VQA problems requires techniques from both computer vision for understanding the visual contents of a presented image or video, as well as the ones from natural language processing for understanding semantics of the question and generating the answers. Regarding visual content modeling, most of existing VQA methods adopt the strategy of extracting global features from the image or video, which inevitably fails in capturing fine-grained information such as spatial configuration of multiple objects. Extracting features from auto-generated regions -- as some region-based image recognition methods do -- cannot essentially address this problem and may introduce some overwhelming irrelevant features with the question. In this work, we propose a novel Focused Dynamic Attention (FDA) model to provide better aligned image content representation with proposed questions. Being aware of the key words in the question, FDA employs off-the-shelf object detector to identify important regions and fuse the information from the regions and global features via an LSTM unit. Such question-driven representations are then combined with question representation and fed into a reasoning unit for generating the answers. Extensive evaluation on a large-scale benchmark dataset, VQA, clearly demonstrate the superior performance of FDA over well-established baselines.
Training Constrained Deconvolutional Networks for Road Scene Semantic Segmentation
Venue: arXiv cs.CV 2016
Year: 2016

In this work we investigate the problem of road scene semantic segmentation using Deconvolutional Networks (DNs). Several constraints limit the practical performance of DNs in this context: firstly, the paucity of existing pixel-wise labelled training data, and secondly, the memory constraints of embedded hardware, which rule out the practical use of state-of-the-art DN architectures such as fully convolutional networks (FCN). To address the first constraint, we introduce a Multi-Domain Road Scene Semantic Segmentation (MDRS3) dataset, aggregating data from six existing densely and sparsely labelled datasets for training our models, and two existing, separate datasets for testing their generalisation performance. We show that, while MDRS3 offers a greater volume and variety of data, end-to-end training of a memory efficient DN does not yield satisfactory performance. We propose a new training strategy to overcome this, based on (i) the creation of a best-possible source network (S-Net) from the aggregated data, ignoring time and memory constraints; and (ii) the transfer of knowledge from S-Net to the memory-efficient target network (T-Net). We evaluate different techniques for S-Net creation and T-Net transferral, and demonstrate that training a constrained deconvolutional network in this manner can unlock better performance than existing training approaches. Specifically, we show that a target network can be trained to achieve improved accuracy versus an FCN despite using less than 1\% of the memory. We believe that our approach can be useful beyond automotive scenarios where labelled data is similarly scarce or fragmented and where practical constraints exist on the desired model size. We make available our network models and aggregated multi-domain dataset for reproducibility.
On Word and Frontier Languages of Unsafe Higher-Order Grammars
Venue: arXiv cs.FL 2016
Year: 2016

Higher-order grammars are extensions of regular and context-free grammars, where non-terminals may take parameters. They have been extensively studied in 1980's, and restudied recently in the context of model checking and program verification. We show that the class of unsafe order-(n+1) word languages coincides with the class of frontier languages of unsafe order-n tree languages. We use intersection types for transforming an order-(n+1) word grammar to a corresponding order-n tree grammar. The result has been proved for safe languages by Damm in 1982, but it has been open for unsafe languages, to our knowledge. Various known results on higher-order grammars can be obtained as almost immediate corollaries of our result.
R-FUSE: Robust Fast Fusion of Multi-Band Images Based on Solving a Sylvester Equation
Venue: arXiv cs.CV 2016
Year: 2016

This paper proposes a robust fast multi-band image fusion method to merge a high-spatial low-spectral resolution image and a low-spatial high-spectral resolution image. Following the method recently developed in [1], the generalized Sylvester matrix equation associated with the multi-band image fusion problem is solved in a more robust and efficient way by exploiting the Woodbury formula, avoiding any permutation operation in the frequency domain as well as the blurring kernel invertibility assumption required in [1]. Thanks to this improvement, the proposed algorithm requires fewer computational operations and is also more robust with respect to the blurring kernel compared with the one in [1]. The proposed new algorithm is tested with different priors considered in [1]. Our conclusion is that the proposed fusion algorithm is more robust than the one in [1] with a reduced computational cost.
Optimizing Performance of Recurrent Neural Networks on GPUs
Venue: arXiv cs.LG 2016
Year: 2016

As recurrent neural networks become larger and deeper, training times for single networks are rising into weeks or even months. As such there is a significant incentive to improve the performance and scalability of these networks. While GPUs have become the hardware of choice for training and deploying recurrent models, the implementations employed often make use of only basic optimizations for these architectures. In this article we demonstrate that by exposing parallelism between operations within the network, an order of magnitude speedup across a range of network sizes can be achieved over a naive implementation. We describe three stages of optimization that have been incorporated into the fifth release of NVIDIA's cuDNN: firstly optimizing a single cell, secondly a single layer, and thirdly the entire network.
Toric Difference Variety
Venue: arXiv cs.SC 2016
Year: 2016

In this paper, the concept of toric difference varieties is defined and four equivalent descriptions for toric difference varieties are presented in terms of difference rational parametrization, difference coordinate rings, toric difference ideals, and group actions by difference tori. Connections between toric difference varieties and affine N[x]-semimodules are established by proving the correspondence between the irreducible invariant difference subvarieties and the faces of the N[x]-submodules and the orbit-face correspondence. Finally, an algorithm is given to decide whether a binomial difference ideal represented by a Z[x]-lattice defines a toric difference variety.
Online Optimization of Smoothed Piecewise Constant Functions
Venue: arXiv cs.LG 2016
Year: 2016

We study online optimization of smoothed piecewise constant functions over the domain [0, 1). This is motivated by the problem of adaptively picking parameters of learning algorithms as in the recently introduced framework by Gupta and Roughgarden (2016). Majority of the machine learning literature has focused on Lipschitz-continuous functions or functions with bounded gradients. 1 This is with good reason---any learning algorithm suffers linear regret even against piecewise constant functions that are chosen adversarially, arguably the simplest of non-Lipschitz continuous functions. The smoothed setting we consider is inspired by the seminal work of Spielman and Teng (2004) and the recent work of Gupta and Roughgarden---in this setting, the sequence of functions may be chosen by an adversary, however, with some uncertainty in the location of discontinuities. We give algorithms that achieve sublinear regret in the full information and bandit settings.
Accelerating Science: A Computing Research Agenda
Venue: arXiv cs.CY 2016
Year: 2016

The emergence of "big data" offers unprecedented opportunities for not only accelerating scientific advances but also enabling new modes of discovery. Scientific progress in many disciplines is increasingly enabled by our ability to examine natural phenomena through the computational lens, i.e., using algorithmic or information processing abstractions of the underlying processes; and our ability to acquire, share, integrate and analyze disparate types of data. However, there is a huge gap between our ability to acquire, store, and process data and our ability to make effective use of the data to advance discovery. Despite successful automation of routine aspects of data management and analytics, most elements of the scientific process currently require considerable human expertise and effort. Accelerating science to keep pace with the rate of data acquisition and data processing calls for the development of algorithmic or information processing abstractions, coupled with formal methods and tools for modeling and simulation of natural processes as well as major innovations in cognitive tools for scientists, i.e., computational tools that leverage and extend the reach of human intellect, and partner with humans on a broad range of tasks in scientific discovery (e.g., identifying, prioritizing formulating questions, designing, prioritizing and executing experiments designed to answer a chosen question, drawing inferences and evaluating the results, and formulating new questions, in a closed-loop fashion). This calls for concerted research agenda aimed at: Development, analysis, integration, sharing, and simulation of algorithmic or information processing abstractions of natural processes, coupled with formal methods and tools for their analyses and simulation; Innovations in cognitive tools that augment and extend human intellect and partner with humans in all aspects of science.
Cooperative Planning of Renewable Generations for Interconnected Microgrids
Venue: arXiv cs.GT 2016
Year: 2016

We study the renewable energy generations in Hong Kong based on realistic meteorological data, and find that different renewable sources exhibit diverse time-varying and location-dependent profiles. To efficiently explore and utilize the diverse renewable energy generations, we propose a theoretical framework for the cooperative planning of renewable generations in a system of interconnected microgrids. The cooperative framework considers the self-interested behaviors of microgrids, and incorporates both their long-term investment costs and short-term operational costs over the planning horizon. Specifically, interconnected microgrids jointly decide where and how much to deploy renewable energy generations, and how to split the associated investment cost. We show that the cooperative framework minimizes the overall system cost. We also design a fair cost sharing method based on Nash bargaining to incentivize cooperative planning, such that all microgrids will benefit from cooperative planning. Using realistic data obtained from the Hong Kong observatory, we validate the cooperative planning framework, and demonstrate that all microgrids benefit through the cooperation, and the overall system cost is reduced by 35.9% compared to the noncooperative planning benchmark.
Distributed Resource Management in Systems of Systems: An Architecture Perspective
Venue: arXiv cs.DC 2016
Year: 2016

This paper introduces a framework for studying the interactions of autonomous system components and the design of the connectivity structure in Systems of Systems (SoSs). This framework, which uses complex network models, is also used to study the connectivity structure's impact on resource management. We discuss resource sharing as a mechanism that adds a level of flexibility to distributed systems and describe the connectivity structures that enhance components' access to the resources available within the system. The framework introduced in this paper explicitly incorporates costs of connection and the benefits that are received by direct and indirect access to resources and provides measures of the optimality of connectivity structures. We discuss central and a distributed schemes that, respectively, represent systems in which a central planner determines the connectivity structure and systems in which distributed components are allowed to add and sever connections to improve their own resource access. Furthermore, we identify optimal connectivity structures for systems with various heterogeneity conditions.
Revising Incompletely Specified Convex Probabilistic Belief Bases
Venue: arXiv cs.AI 2016
Year: 2016

We propose a method for an agent to revise its incomplete probabilistic beliefs when a new piece of propositional information is observed. In this work, an agent's beliefs are represented by a set of probabilistic formulae -- a belief base. The method involves determining a representative set of 'boundary' probability distributions consistent with the current belief base, revising each of these probability distributions and then translating the revised information into a new belief base. We use a version of Lewis Imaging as the revision operation. The correctness of the approach is proved. The expressivity of the belief bases under consideration are rather restricted, but has some applications. We also discuss methods of belief base revision employing the notion of optimum entropy, and point out some of the benefits and difficulties in those methods. Both the boundary distribution method and the optimum entropy method are reasonable, yet yield different results.
On Capacity and Delay of Multi-channel Wireless Networks with Infrastructure Support
Venue: arXiv cs.NI 2016
Year: 2016

In this paper, we propose a novel multi-channel network with infrastructure support, called an MC-IS network, which has not been studied in the literature. To the best of our knowledge, we are the first to study such an MC-IS network. Our proposed MC-IS network has a number of advantages over three existing conventional networks, namely a single-channel wireless ad hoc network (called an SC-AH network), a multi-channel wireless ad hoc network (called an MC-AH network) and a single-channel network with infrastructure support (called an SC-IS network). In particular, the network capacity of our proposed MC-IS network is $\sqrt{n \log n}$ times higher than that of an SC-AH network and an MC-AH network and the same as that of an SC-IS network, where $n$ is the number of nodes in the network. The average delay of our MC-IS network is $\sqrt{\log n/n}$ times lower than that of an SC-AH network and an MC-AH network, and $\min\{C_I,m\}$ times lower than the average delay of an SC-IS network, where $C_I$ and $m$ denote the number of channels dedicated for infrastructure communications and the number of interfaces mounted at each infrastructure node, respectively. Our analysis on an MC-IS network equipped with omni-directional antennas only has been extended to an MC-IS network equipped with directional antennas only, which are named as an MC-IS-DA network. We show that an MC-IS-DA network has an even lower delay of $\frac{c}{\lfloor \frac{2π}θ\rfloor \cdot C_I}$ compared with an SC-IS network and our MC-IS network. For example, when $C_I=12$ and $θ=\fracπ{12}$, an MC-IS-DA network can further reduce the delay by 24 times lower that of an MC-IS network and reduce the delay by 288 times lower than that of an SC-IS network.
Infrared Colorization Using Deep Convolutional Neural Networks
Venue: arXiv cs.CV 2016
Year: 2016

This paper proposes a method for transferring the RGB color spectrum to near-infrared (NIR) images using deep multi-scale convolutional neural networks. A direct and integrated transfer between NIR and RGB pixels is trained. The trained model does not require any user guidance or a reference image database in the recall phase to produce images with a natural appearance. To preserve the rich details of the NIR image, its high frequency features are transferred to the estimated RGB image. The presented approach is trained and evaluated on a real-world dataset containing a large amount of road scene images in summer. The dataset was captured by a multi-CCD NIR/RGB camera, which ensures a perfect pixel to pixel registration.
A High-Level LTL Synthesis Format: TLSF v1.1
Venue: arXiv cs.LO 2016
Year: 2016

We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high-level constructs, such as sets and functions, to provide a compact and human-readable representation. Furthermore, the format allows to identify parameters of a specification such that a single description can be used to define a family of problems. Additionally, we present a tool to automatically translate the format into plain LTL, which then can be used for synthesis by a solver. The tool also allows to adjust parameters of the specification and to apply standard transformations on the resulting formula.