OpenRaiser/Intern-Atlas huggingface dataset:
A Framework for Dependent Types and Effects
Venue: arXiv cs.LO 2016
Year: 2016

We generalise Levy's call-by-push-value (CBPV) to dependent type theory, to gain a better understanding of how to combine dependent types with effects. We define a dependently typed extension of CBPV, dCBPV-, and show that it has a very natural small-step operational semantics, which satisfies subject reduction and (depending on the effects present) determinism and strong normalization, and an elegant categorical semantics, which - surprisingly - is no more complicated than the simply typed semantics. We have full and faithful translations from a dependently typed version of Moggi's monadic metalanguage and of a call-by-name (CBN) dependent type theory into dCBPV- which give rise to the expected operational behaviour. However, it turns out that dCBPV- does not suffice to encode call-by-value (CBV) dependent type theory or the strong (dependent) elimination rules for positive connectives in CBN-dependent type theory. To mend this problem, we discuss a second, more expressive system dCBPV+, which additionally has a principle of Kleisli extension for dependent functions. We obtain the desired CBV- and CBN-translations of dependent type theory into dCBPV+. It too has a natural categorical semantics and operational semantics. However, depending on the effects we consider, we may lose uniqueness of typing, as the type of a computation may become more specified as certain effects are executed. This idea can be neatly formalized using a notion of subtyping. We hope that the theoretical framework of this paper on the one hand provides at least a partial answer to the fundamental type theoretic question of how one can understand the relationship between computational effects and dependent types. On the other hand, we hope it can contribute a small-step towards the ultimate goal of an elegant fully fledged language for certified effectful programming.
Device and System Level Design Considerations for Analog-Non-Volatile-Memory Based Neuromorphic Architectures
Venue: arXiv cs.NE 2016
Year: 2016

This paper gives an overview of recent progress in the brain inspired computing field with a focus on implementation using emerging memories as electronic synapses. Design considerations and challenges such as requirements and design targets on multilevel states, device variability, programming energy, array-level connectivity, fan-in/fanout, wire energy, and IR drop are presented. Wires are increasingly important in design decisions, especially for large systems, and cycle-to-cycle variations have large impact on learning performance.
Learning Document Embeddings by Predicting N-grams for Sentiment Classification of Long Movie Reviews
Venue: arXiv cs.CL 2016
Year: 2016

Despite the loss of semantic information, bag-of-ngram based methods still achieve state-of-the-art results for tasks such as sentiment classification of long movie reviews. Many document embeddings methods have been proposed to capture semantics, but they still can't outperform bag-of-ngram based methods on this task. In this paper, we modify the architecture of the recently proposed Paragraph Vector, allowing it to learn document vectors by predicting not only words, but n-gram features as well. Our model is able to capture both semantics and word order in documents while keeping the expressive power of learned vectors. Experimental results on IMDB movie review dataset shows that our model outperforms previous deep learning models and bag-of-ngram based models due to the above advantages. More robust results are also obtained when our model is combined with other models. The source code of our model will be also published together with this paper.
Computing Theory Prime Implicates in Modal Logic
Venue: arXiv cs.LO 2016
Year: 2016

The algorithm to compute theory prime implicates, a generalization of prime implicates, in propositional logic has been suggested in \cite{Marquis}. In this paper we have extended that algorithm to compute theory prime implicates of a knowledge base $X$ with respect to another knowledge base $\Box Y$ using \cite{Bienvenu}, where $Y$ is a propositional knowledge base and $X\models Y$, in modal system $\mathcal{T}$ and we have also proved its correctness. We have also proved that it is an equivalence preserving knowledge compilation and the size of theory prime implicates of $X$ with respect to $\Box Y$ is less than the size of the prime implicates of $X\cup\Box Y$.
Visually Indicated Sounds
Venue: arXiv cs.CV 2016
Year: 2016

Objects make distinctive sounds when they are hit or scratched. These sounds reveal aspects of an object's material properties, as well as the actions that produced them. In this paper, we propose the task of predicting what sound an object makes when struck as a way of studying physical interactions within a visual scene. We present an algorithm that synthesizes sound from silent videos of people hitting and scratching objects with a drumstick. This algorithm uses a recurrent neural network to predict sound features from videos and then produces a waveform from these features with an example-based synthesis procedure. We show that the sounds predicted by our model are realistic enough to fool participants in a "real or fake" psychophysical experiment, and that they convey significant information about material properties and physical interactions.
T2: Temporal Property Verification
Venue: arXiv cs.LO 2016
Year: 2016

We present the open-source tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporal-logic proving techniques and to handle a general class of user-provided liveness and safety properties. Input can be provided in a native format and in C, via the support of the LLVM compiler framework. We briefly discuss T2's architecture, its underlying techniques, and conclude with an experimental illustration of its competitiveness and directions for future extensions.
Feed-Forward Networks with Attention Can Solve Some Long-Term Memory Problems
Venue: arXiv cs.LG 2016
Year: 2016

We propose a simplified model of attention which is applicable to feed-forward neural networks and demonstrate that the resulting model can solve the synthetic "addition" and "multiplication" long-term memory problems for sequence lengths which are both longer and more widely varying than the best published results for these tasks.
Sparse group factor analysis for biclustering of multiple data sources
Venue: arXiv cs.LG 2016
Year: 2016

Motivation: Modelling methods that find structure in data are necessary with the current large volumes of genomic data, and there have been various efforts to find subsets of genes exhibiting consistent patterns over subsets of treatments. These biclustering techniques have focused on one data source, often gene expression data. We present a Bayesian approach for joint biclustering of multiple data sources, extending a recent method Group Factor Analysis (GFA) to have a biclustering interpretation with additional sparsity assumptions. The resulting method enables data-driven detection of linear structure present in parts of the data sources. Results: Our simulation studies show that the proposed method reliably infers bi-clusters from heterogeneous data sources. We tested the method on data from the NCI-DREAM drug sensitivity prediction challenge, resulting in an excellent prediction accuracy. Moreover, the predictions are based on several biclusters which provide insight into the data sources, in this case on gene expression, DNA methylation, protein abundance, exome sequence, functional connectivity fingerprints and drug sensitivity.
Clustering scientific publications based on citation relations: A systematic comparison of different methods
Venue: arXiv cs.DL 2016
Year: 2016

Clustering methods are applied regularly in the bibliometric literature to identify research areas or scientific fields. These methods are for instance used to group publications into clusters based on their relations in a citation network. In the network science literature, many clustering methods, often referred to as graph partitioning or community detection techniques, have been developed. Focusing on the problem of clustering the publications in a citation network, we present a systematic comparison of the performance of a large number of these clustering methods. Using a number of different citation networks, some of them relatively small and others very large, we extensively study the statistical properties of the results provided by different methods. In addition, we also carry out an expert-based assessment of the results produced by different methods. The expert-based assessment focuses on publications in the field of scientometrics. Our findings seem to indicate that there is a trade-off between different properties that may be considered desirable for a good clustering of publications. Overall, map equation methods appear to perform best in our analysis, suggesting that these methods deserve more attention from the bibliometric community.
Personalized Course Sequence Recommendations
Venue: arXiv cs.CY 2016
Year: 2016

Given the variability in student learning it is becoming increasingly important to tailor courses as well as course sequences to student needs. This paper presents a systematic methodology for offering personalized course sequence recommendations to students. First, a forward-search backward-induction algorithm is developed that can optimally select course sequences to decrease the time required for a student to graduate. The algorithm accounts for prerequisite requirements (typically present in higher level education) and course availability. Second, using the tools of multi-armed bandits, an algorithm is developed that can optimally recommend a course sequence that both reduces the time to graduate while also increasing the overall GPA of the student. The algorithm dynamically learns how students with different contextual backgrounds perform for given course sequences and then recommends an optimal course sequence for new students. Using real-world student data from the UCLA Mechanical and Aerospace Engineering department, we illustrate how the proposed algorithms outperform other methods that do not include student contextual information when making course sequence recommendations.
A $4/5$ - Approximation Algorithm for the Maximum Traveling Salesman Problem
Venue: arXiv cs.DS 2016
Year: 2016

In the maximum traveling salesman problem (Max TSP) we are given a complete undirected graph with nonnegative weights on the edges and we wish to compute a traveling salesman tour of maximum weight. We present a fast combinatorial $\frac 45$ - approximation algorithm for Max TSP. The previous best approximation for this problem was $\frac 79$. The new algorithm is based on a novel technique of eliminating difficult subgraphs via half-edges, a new method of edge coloring and a technique of exchanging edges. A half-edge of edge $e=(u,v)$ is informally speaking "a half of $e$ containing either $u$ or $v$".
Network Flow Routing under Strategic Link Disruptions
Venue: arXiv cs.GT 2016
Year: 2016

This paper considers a 2-player strategic game for network routing under link disruptions. Player 1 (defender) routes flow through a network to maximize her value of effective flow while facing transportation costs. Player 2 (attacker) simultaneously disrupts one or more links to maximize her value of lost flow but also faces cost of disrupting links. This game is strategically equivalent to a zero-sum game. Linear programming duality and the max-flow min-cut theorem are applied to obtain properties that are satisfied in any mixed Nash equilibrium. In any equilibrium, both players achieve identical payoffs. While the defender's expected transportation cost decreases in attacker's marginal value of lost flow, the attacker's expected cost of attack increases in defender's marginal value of effective flow. Interestingly, the expected amount of effective flow decreases in both these parameters. These results can be viewed as a generalization of the classical max-flow with minimum transportation cost problem to adversarial environments.
Fast, Safe, and Propellant-Efficient Spacecraft Planning under Clohessy-Wiltshire-Hill Dynamics
Venue: arXiv cs.SY 2016
Year: 2016

This paper presents a sampling-based motion planning algorithm for real-time and propellant-optimized autonomous spacecraft trajectory generation in near-circular orbits. Specifically, this paper leverages recent algorithmic advances in the field of robot motion planning to the problem of impulsively-actuated, propellant-optimized rendezvous and proximity operations under the Clohessy-Wiltshire-Hill (CWH) dynamics model. The approach calls upon a modified version of the Fast Marching Tree (FMT*) algorithm to grow a set of feasible trajectories over a deterministic, low-dispersion set of sample points covering the free state space. To enforce safety, the tree is only grown over the subset of actively-safe samples, from which there exists a feasible one-burn collision avoidance maneuver that can safely circularize the spacecraft orbit along its coasting arc under a given set of potential thruster failures. Key features of the proposed algorithm include: (i) theoretical guarantees in terms of trajectory safety and performance, (ii) amenability to real-time implementation, and (iii) generality, in the sense that a large class of constraints can be handled directly. As a result, the proposed algorithm offers the potential for widespread application, ranging from on-orbit satellite servicing to orbital debris removal and autonomous inspection missions.
Mimir: Bringing CTables into Practice
Venue: arXiv cs.DB 2016
Year: 2016

The present state of the art in analytics requires high upfront investment of human effort and computational resources to curate datasets, even before the first query is posed. So-called pay-as-you-go data curation techniques allow these high costs to be spread out, first by enabling queries over uncertain and incomplete data, and then by assessing the quality of the query results. We describe the design of a system, called Mimir, around a recently introduced class of probabilistic pay-as-you-go data cleaning operators called Lenses. Mimir wraps around any deterministic database engine using JDBC, extending it with support for probabilistic query processing. Queries processed through Mimir produce uncertainty-annotated result cursors that allow client applications to quickly assess result quality and provenance. We also present a GUI that provides analysts with an interactive tool for exploring the uncertainty exposed by the system. Finally, we present optimizations that make Lenses scalable, and validate this claim through experimental evidence.
A wireless physically secure key distribution system
Venue: arXiv cs.CR 2016
Year: 2016

A secure key distribution protocol protected by light's noise was introduced in 2003 [Phys. Rev. A 68, 052307 (2003)]. That protocol utilized the shot noise of light present in the optical channel (eg., an optical fiber) to restrict information leaks to an adversary. An initial shared information between the legitimate users allowed them to extract more information from the channel than the one obtained by the adversary. That original paper recognized the need for a privacy amplification step but no specific protocol was presented. More recently that original idea was improved with a specific privacy amplification protocol [arXiv:1406.1543v2 [cs.CR] 8 Jul 2015] while keeping the use of an optical communication channel. This work merges main ideas of the protection given by the light's noise in a protocol applied to wireless channels. The use of a wireless channels together with recorded physical noise was introduced from 2005 to 2007 (see eg, arXiv:quant-ph/0510011 v2 16 Nov 2005 and arXiv:0705.2243v2 [quant-ph] 17 May 2007). This work improves those embrionary ideas of wireless channels secured by recorded optical noise. The need for specific optical channels is eliminated with the wireless variation and opens up the possibility to apply the technique to mobile devices. This work introduces this new scheme and calculates the associated security level.
The Reduced-Order Hybrid Monte Carlo Sampling Smoother
Venue: arXiv cs.NA 2016
Year: 2016

Hybrid Monte-Carlo (HMC) sampling smoother is a fully non-Gaussian four-dimensional data assimilation algorithm that works by directly sampling the posterior distribution formulated in the Bayesian framework. The smoother in its original formulation is computationally expensive due to the intrinsic requirement of running the forward and adjoint models repeatedly. Here we present computationally efficient versions of the HMC sampling smoother based on reduced-order approximations of the underlying model dynamics. The schemes developed herein are tested numerically using the shallow-water equations model on Cartesian coordinates. The results reveal that the reduced-order versions of the smoother are capable of accurately capturing the posterior probability density, while being significantly faster than the original full order formulation.
Information Exchange in Randomly Deployed Dense WSNs with Wireless Energy Harvesting Capabilities
Venue: arXiv cs.IT 2016
Year: 2016

As large-scale dense and often randomly deployed wireless sensor networks (WSNs) become widespread, local information exchange between co-located sets of nodes may play a significant role in handling the excessive traffic volume. Moreover, to account for the limited life-span of the wireless devices, harvesting the energy of the network transmissions provides significant benefits to the lifetime of such networks. In this paper, we study the performance of communication in dense networks with wireless energy harvesting (WEH)-enabled sensor nodes. In particular, we examine two different communication scenarios (direct and cooperative) for data exchange and we provide theoretical expressions for the probability of successful communication. Then, considering the importance of lifetime in WSNs, we employ state-of-the-art WEH techniques and realistic energy converters, quantifying the potential energy gains that can be achieved in the network. Our analytical derivations, which are validated by extensive Monte-Carlo simulations, highlight the importance of WEH in dense networks and identify the trade-offs between the direct and cooperative communication scenarios.
A Parameterized Algorithm for Bounded-Degree Vertex Deletion
Venue: arXiv cs.DS 2016
Year: 2016

The $d$-bounded-degree vertex deletion problem, to delete at most $k$ vertices in a given graph to make the maximum degree of the remaining graph at most $d$, finds applications in computational biology, social network analysis and some others. It can be regarded as a special case of the $(d+2)$-hitting set problem and generates the famous vertex cover problem. The $d$-bounded-degree vertex deletion problem is NP-hard for each fixed $d\geq 0$. In terms of parameterized complexity, the problem parameterized by $k$ is W[2]-hard for unbounded $d$ and fixed-parameter tractable for each fixed $d\geq 0$. Previously, (randomized) parameterized algorithms for this problem with running time bound $O^*((d+1)^k)$ are only known for $d\leq2$. In this paper, we give a uniform parameterized algorithm deterministically solving this problem in $O^*((d+1)^k)$ time for each $d\geq 3$. Note that it is an open problem whether the $d'$-hitting set problem can be solved in $O^*((d'-1)^k)$ time for $d'\geq 3$. Our result answers this challenging open problem affirmatively for a special case. Furthermore, our algorithm also gets a running time bound of $O^*(3.0645^k)$ for the case that $d=2$, improving the previous deterministic bound of $O^*(3.24^k)$.
Interdependent Relationships in Game Theory: A Generalized Model
Venue: arXiv cs.GT 2016
Year: 2016

A generalized model of games is proposed, in which cooperative games and non-cooperative games are special cases. Some games that are neither cooperative nor non-cooperative can be expressed and analyzed. The model is based on relationships and supposed relationships between players. A relationship is a numerical value that denotes how one player cares for the payoffs of another player, while a supposed relationship is another numerical value that denotes a player's belief about the relationship between two players. The players choose their strategies by taking into consideration not only the material payoffs but also relationships and their change. Two games, a prisoners' dilemma and a repeated ultimatum game, are analyzed as examples of application of this model.
A Unified Framework for Compositional Fitting of Active Appearance Models
Venue: arXiv cs.CV 2016
Year: 2016

Active Appearance Models (AAMs) are one of the most popular and well-established techniques for modeling deformable objects in computer vision. In this paper, we study the problem of fitting AAMs using Compositional Gradient Descent (CGD) algorithms. We present a unified and complete view of these algorithms and classify them with respect to three main characteristics: i) cost function; ii) type of composition; and iii) optimization method. Furthermore, we extend the previous view by: a) proposing a novel Bayesian cost function that can be interpreted as a general probabilistic formulation of the well-known project-out loss; b) introducing two new types of composition, asymmetric and bidirectional, that combine the gradients of both image and appearance model to derive better conver- gent and more robust CGD algorithms; and c) providing new valuable insights into existent CGD algorithms by reinterpreting them as direct applications of the Schur complement and the Wiberg method. Finally, in order to encourage open research and facilitate future comparisons with our work, we make the implementa- tion of the algorithms studied in this paper publicly available as part of the Menpo Project.
Fixed points of adjoint functors enriched in a quantaloid
Venue: arXiv cs.LO 2016
Year: 2016

Representation theorems are established for fixed points of adjoint functors between categories enriched in a small quantaloid. In a very general setting these results set up a common framework for representation theorems of concept lattices in formal concept analysis (FCA) and rough set theory (RST), which not only extend the realm of formal contexts to multi-typed and multi-valued ones, but also provide a general approach to construct various kinds of representation theorems. Besides incorporating several well-known representation theorems in FCA and RST as well as formulating new ones, it is shown that concept lattices in RST can always be represented as those in FCA through relative pseudo-complements of the given contexts, especially if the contexts are valued in a non-Girard quantaloid.