OpenRaiser/Intern-Atlas huggingface dataset:
Deriving a Simple Gradual Security Language
Venue: arXiv cs.PL 2015
Year: 2015

Abstracting Gradual Typing (AGT) is an approach to systematically deriving gradual counterparts to static type disciplines. The approach consists of defining the semantics of gradual types by interpreting them as sets of static types, and then defining an optimal abstraction back to gradual types. These operations are used to lift the static discipline to the gradual setting. The runtime semantics of the gradual language then arises as reductions on gradual typing derivations. To demonstrate the flexibility of AGT, we gradualize $λ_\text{SEC}$, the prototypical security-typed language, with respect to only security labels rather than entire types, yielding a type system that ranges gradually from simply-typed to securely-typed. We establish noninterference for the gradual language, called $λ_{\widetilde{\text{SEC}}}$, using Zdancewic's logical relation proof method. Whereas prior work presents gradual security cast languages, which require explicit security casts, this work yields the first gradual security source language, which requires no explicit casts.
Turing Computation with Recurrent Artificial Neural Networks
Venue: arXiv cs.NE 2015
Year: 2015

We improve the results by Siegelmann & Sontag (1995) by providing a novel and parsimonious constructive mapping between Turing Machines and Recurrent Artificial Neural Networks, based on recent developments of Nonlinear Dynamical Automata. The architecture of the resulting R-ANNs is simple and elegant, stemming from its transparent relation with the underlying NDAs. These characteristics yield promise for developments in machine learning methods and symbolic computation with continuous time dynamical systems. A framework is provided to directly program the R-ANNs from Turing Machine descriptions, in absence of network training. At the same time, the network can potentially be trained to perform algorithmic tasks, with exciting possibilities in the integration of approaches akin to Google DeepMind's Neural Turing Machines.
Efficient Gossip Protocols for Verifying the Consistency of Certificate Logs
Venue: arXiv cs.CR 2015
Year: 2015

The level of trust accorded to certification authorities has been decreasing over the last few years as several cases of misbehavior and compromise have been observed. Log-based approaches, such as Certificate Transparency, ensure that fraudulent TLS certificates become publicly visible. However, a key element that log-based approaches still lack is a way for clients to verify that the log behaves in a consistent and honest manner. This task is challenging due to privacy, efficiency, and deployability reasons. In this paper, we propose the first (to the best of our knowledge) gossip protocols that enable the detection of log inconsistencies. We analyze these protocols and present the results of a simulation based on real Internet traffic traces. We also give a deployment plan, discuss technical issues, and present an implementation.
Regularization and Bayesian Learning in Dynamical Systems: Past, Present and Future
Venue: arXiv cs.SY 2015
Year: 2015

Regularization and Bayesian methods for system identification have been repopularized in the recent years, and proved to be competitive w.r.t. classical parametric approaches. In this paper we shall make an attempt to illustrate how the use of regularization in system identification has evolved over the years, starting from the early contributions both in the Automatic Control as well as Econometrics and Statistics literature. In particular we shall discuss some fundamental issues such as compound estimation problems and exchangeability which play and important role in regularization and Bayesian approaches, as also illustrated in early publications in Statistics. The historical and foundational issues will be given more emphasis (and space), at the expense of the more recent developments which are only briefly discussed. The main reason for such a choice is that, while the recent literature is readily available, and surveys have already been published on the subject, in the author's opinion a clear link with past work had not been completely clarified.
DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics
Venue: arXiv cs.LO 2015
Year: 2015

Maxwell's Demon, 'a being whose faculties are so sharpened that he can follow every molecule in its course', has been the centre of much debate about its abilities to violate the second law of thermodynamics. Landauer's hypothesis, that the Demon must erase its memory and incur a thermodynamic cost, has become the standard response to Maxwell's dilemma, and its implications for the thermodynamics of computation reach into many areas of quantum and classical computing. It remains, however, still a hypothesis. Debate has often centred around simple toy models of a single particle in a box. Despite their simplicity, the ability of these systems to accurately represent thermodynamics (specifically to satisfy the second law) and whether or not they display Landauer Erasure, has been a matter of ongoing argument. The recent Norton-Ladyman controversy is one such example. In this paper we introduce a programming language to describe these simple thermodynamic processes, and give a formal operational semantics and program logic as a basis for formal reasoning about thermodynamic systems. We formalise the basic single-particle operations as statements in the language, and then show that the second law must be satisfied by any composition of these basic operations. This is done by finding a computational invariant of the system. We show, furthermore, that this invariant requires an erasure cost to exist within the system, equal to kTln2 for a bit of information: Landauer Erasure becomes a theorem of the formal system. The Norton-Ladyman controversy can therefore be resolved in a rigorous fashion, and moreover the formalism we introduce gives a set of reasoning tools for further analysis of Landauer erasure, which are provably consistent with the second law of thermodynamics.
Quotient-Comprehension Chains
Venue: arXiv cs.LO 2015
Year: 2015

Quotients and comprehension are fundamental mathematical constructions that can be described via adjunctions in categorical logic. This paper reveals that quotients and comprehension are related to measurement, not only in quantum logic, but also in probabilistic and classical logic. This relation is presented by a long series of examples, some of them easy, and some also highly non-trivial (esp. for von Neumann algebras). We have not yet identified a unifying theory. Nevertheless, the paper contributes towards such a theory by introducing the new quotient-and-comprehension perspective on measurement instruments, and by describing the examples on which such a theory should be built.
Encoding !-tensors as !-graphs with neighbourhood orders
Venue: arXiv cs.LO 2015
Year: 2015

Diagrammatic reasoning using string diagrams provides an intuitive language for reasoning about morphisms in a symmetric monoidal category. To allow working with infinite families of string diagrams, !-graphs were introduced as a method to mark repeated structure inside a diagram. This led to !-graphs being implemented in the diagrammatic proof assistant Quantomatic. Having a partially automated program for rewriting diagrams has proven very useful, but being based on !-graphs, only commutative theories are allowed. An enriched abstract tensor notation, called !-tensors, has been used to formalise the notion of !-boxes in non-commutative structures. This work-in-progress paper presents a method to encode !-tensors as !-graphs with some additional structure. This will allow us to leverage the existing code from Quantomatic and quickly provide various tools for non-commutative diagrammatic reasoning.
New constructions of quantum MDS convolutional codes derived from generalized Reed-Solomon codes
Venue: arXiv cs.IT 2015
Year: 2015

Quantum convolutional codes can be used to protect a sequence of qubits of arbitrary length against decoherence. In this paper, we give two new constructions of quantum MDS convolutional codes derived from generalized Reed-Solomon codes and obtain eighteen new classes of quantum MDS convolutional codes. Most of them are new in the sense that the parameters of the codes are different from all the previously known ones.
Computing sets of graded attribute implications with witnessed non-redundancy
Venue: arXiv cs.AI 2015
Year: 2015

In this paper we extend our previous results on sets of graded attribute implications with witnessed non-redundancy. We assume finite residuated lattices as structures of truth degrees and use arbitrary idempotent truth-stressing linguistic hedges as parameters which influence the semantics of graded attribute implications. In this setting, we introduce algorithm which transforms any set of graded attribute implications into an equivalent non-redundant set of graded attribute implications with saturated consequents whose non-redundancy is witnessed by antecedents of the formulas. As a consequence, we solve the open problem regarding the existence of general systems of pseudo-intents which appear in formal concept analysis of object-attribute data with graded attributes and linguistic hedges. Furthermore, we show a polynomial-time procedure for determining bases given by general systems of pseudo-intents from sets of graded attribute implications which are complete in data.
Stochastic Proximal Gradient Descent for Nuclear Norm Regularization
Venue: arXiv cs.LG 2015
Year: 2015

In this paper, we utilize stochastic optimization to reduce the space complexity of convex composite optimization with a nuclear norm regularizer, where the variable is a matrix of size $m \times n$. By constructing a low-rank estimate of the gradient, we propose an iterative algorithm based on stochastic proximal gradient descent (SPGD), and take the last iterate of SPGD as the final solution. The main advantage of the proposed algorithm is that its space complexity is $O(m+n)$, in contrast, most of previous algorithms have a $O(mn)$ space complexity. Theoretical analysis shows that it achieves $O(\log T/\sqrt{T})$ and $O(\log T/T)$ convergence rates for general convex functions and strongly convex functions, respectively.
Partial Spread and Vectorial Generalized Bent Functions
Venue: arXiv cs.IT 2015
Year: 2015

In this paper we generalize the partial spread class and completely describe it for generalized Boolean functions from $\F_2^n$ to $\mathbb{Z}_{2^t}$. Explicitly, we describe gbent functions from $\F_2^n$ to $\mathbb{Z}_{2^t}$, which can be seen as a gbent version of Dillon's $PS_{ap}$ class. For the first time, we also introduce the concept of a vectorial gbent function from $\F_2^n$ to $\Z_q^m$, and determine the maximal value which $m$ can attain for the case $q=2^t$. Finally we point to a relation between vectorial gbent functions and relative difference sets.
Image classification based on support vector machine and the fusion of complementary features
Venue: arXiv cs.CV 2015
Year: 2015

Image Classification based on BOW (Bag-of-words) has broad application prospect in pattern recognition field but the shortcomings are existed because of single feature and low classification accuracy. To this end we combine three ingredients: (i) Three features with functions of mutual complementation are adopted to describe the images, including PHOW (Pyramid Histogram of Words), PHOC (Pyramid Histogram of Color) and PHOG (Pyramid Histogram of Orientated Gradients). (ii) The improvement of traditional BOW model is presented by using dense sample and an improved K-means clustering method for constructing the visual dictionary. (iii) An adaptive feature-weight adjusted image categorization algorithm based on the SVM and the fusion of multiple features is adopted. Experiments carried out on Caltech 101 database confirm the validity of the proposed approach. From the experimental results can be seen that the classification accuracy rate of the proposed method is improved by 7%-17% higher than that of the traditional BOW methods. This algorithm makes full use of global, local and spatial information and has significant improvements to the classification accuracy.
Adaptive information-theoretic bounded rational decision-making with parametric priors
Venue: arXiv cs.AI 2015
Year: 2015

Deviations from rational decision-making due to limited computational resources have been studied in the field of bounded rationality, originally proposed by Herbert Simon. There have been a number of different approaches to model bounded rationality ranging from optimality principles to heuristics. Here we take an information-theoretic approach to bounded rationality, where information-processing costs are measured by the relative entropy between a posterior decision strategy and a given fixed prior strategy. In the case of multiple environments, it can be shown that there is an optimal prior rendering the bounded rationality problem equivalent to the rate distortion problem for lossy compression in information theory. Accordingly, the optimal prior and posterior strategies can be computed by the well-known Blahut-Arimoto algorithm which requires the computation of partition sums over all possible outcomes and cannot be applied straightforwardly to continuous problems. Here we derive a sampling-based alternative update rule for the adaptation of prior behaviors of decision-makers and we show convergence to the optimal prior predicted by rate distortion theory. Importantly, the update rule avoids typical infeasible operations such as the computation of partition sums. We show in simulations a proof of concept for discrete action and environment domains. This approach is not only interesting as a generic computational method, but might also provide a more realistic model of human decision-making processes occurring on a fast and a slow time scale.
On the Role of Artificial Noise in Training and Data Transmission for Secret Communications
Venue: arXiv cs.IT 2015
Year: 2015

This work considers the joint design of training and data transmission in physical-layer secret communication systems, and examines the role of artificial noise (AN) in both of these phases. In particular, AN in the training phase is used to prevent the eavesdropper from obtaining accurate channel state information (CSI) whereas AN in the data transmission phase can be used to mask the transmission of the confidential message. By considering AN-assisted training and secrecy beamforming schemes, we first derive bounds on the achievable secrecy rate and obtain a closed-form approximation that is asymptotically tight at high SNR. Then, by maximizing the approximate achievable secrecy rate, the optimal power allocation between signal and AN in both training and data transmission phases is obtained for both conventional and AN-assisted training based schemes. We show that the use of AN is necessary to achieve a high secrecy rate at high SNR, and its use in the training phase can be more efficient than that in the data transmission phase when the coherence time is large. However, at low SNR, the use of AN provides no advantage since CSI is difficult to obtain in this case. Numerical results are presented to verify our theoretical claims.
Flood-it on AT-Free Graphs
Venue: arXiv cs.DM 2015
Year: 2015

Solitaire {\sc Flood-it}, or {\sc Honey-Bee}, is a game played on a colored graph. The player resides in a source vertex. Originally his territory is the maximal connected, monochromatic subgraph that contains the source. A move consists of calling a color. This conquers all the nodes of the graph that can be reached by a monochromatic path of that color from the current territory of the player. It is the aim of the player to add all vertices to his territory in a minimal number of moves. We show that the minimal number of moves can be computed in polynomial time when the game is played on AT-free graphs.
Multi-lingual Geoparsing based on Machine Translation
Venue: arXiv cs.CL 2015
Year: 2015

Our method for multi-lingual geoparsing uses monolingual tools and resources along with machine translation and alignment to return location words in many languages. Not only does our method save the time and cost of developing geoparsers for each language separately, but also it allows the possibility of a wide range of language capabilities within a single interface. We evaluated our method in our LanguageBridge prototype on location named entities using newswire, broadcast news and telephone conversations in English, Arabic and Chinese data from the Linguistic Data Consortium (LDC). Our results for geoparsing Chinese and Arabic text using our multi-lingual geoparsing method are comparable to our results for geoparsing English text with our English tools. Furthermore, experiments using our machine translation approach results in accuracy comparable to results from the same data that was translated manually.
Distributed User Association in Energy Harvesting Small Cell Networks: A Competitive Market Model with Uncertainty
Venue: arXiv cs.GT 2015
Year: 2015

We consider a distributed user association problem in the downlink of a small cell network, where small cells obtain the required energy for providing wireless services to users through ambient energy harvesting. Since energy harvesting is opportunistic in nature, the amount of harvested energy is a random variable, without a priori known characteristics. We model the network as a competitive market with uncertainty, where self-interested small cells, modeled as consumers, are willing to maximize their utility scores by selecting users, represented by commodities. The utility scores of small cells depend on the amount of harvested energy, formulated as natures' state. Under this model, the problem is to assign users to small cells, so that the aggregate network utility is maximized. The solution is the general equilibrium under uncertainty, also called Arrow-Debreu equilibrium. We show that in our setting, such equilibrium not only exists, but also is unique and is Pareto optimal in the sense of expected aggregate network utility. We use the Walras' tatonnement process with some modifications in order to implement the equilibrium efficiently.
Towards a Better Understanding of Predict and Count Models
Venue: arXiv cs.LG 2015
Year: 2015

In a recent paper, Levy and Goldberg pointed out an interesting connection between prediction-based word embedding models and count models based on pointwise mutual information. Under certain conditions, they showed that both models end up optimizing equivalent objective functions. This paper explores this connection in more detail and lays out the factors leading to differences between these models. We find that the most relevant differences from an optimization perspective are (i) predict models work in a low dimensional space where embedding vectors can interact heavily; (ii) since predict models have fewer parameters, they are less prone to overfitting. Motivated by the insight of our analysis, we show how count models can be regularized in a principled manner and provide closed-form solutions for L1 and L2 regularization. Finally, we propose a new embedding model with a convex objective and the additional benefit of being intelligible.
ALOJA: A Framework for Benchmarking and Predictive Analytics in Big Data Deployments
Venue: arXiv cs.LG 2015
Year: 2015

This article presents the ALOJA project and its analytics tools, which leverages machine learning to interpret Big Data benchmark performance data and tuning. ALOJA is part of a long-term collaboration between BSC and Microsoft to automate the characterization of cost-effectiveness on Big Data deployments, currently focusing on Hadoop. Hadoop presents a complex run-time environment, where costs and performance depend on a large number of configuration choices. The ALOJA project has created an open, vendor-neutral repository, featuring over 40,000 Hadoop job executions and their performance details. The repository is accompanied by a test-bed and tools to deploy and evaluate the cost-effectiveness of different hardware configurations, parameters and Cloud services. Despite early success within ALOJA, a comprehensive study requires automation of modeling procedures to allow an analysis of large and resource-constrained search spaces. The predictive analytics extension, ALOJA-ML, provides an automated system allowing knowledge discovery by modeling environments from observed executions. The resulting models can forecast execution behaviors, predicting execution times for new configurations and hardware choices. That also enables model-based anomaly detection or efficient benchmark guidance by prioritizing executions. In addition, the community can benefit from ALOJA data-sets and framework to improve the design and deployment of Big Data applications.
Solving the Join Ordering Problem via Mixed Integer Linear Programming
Venue: arXiv cs.DB 2015
Year: 2015

We transform join ordering into a mixed integer linear program (MILP). This allows to address query optimization by mature MILP solver implementations that have evolved over decades and steadily improved their performance. They offer features such as anytime optimization and parallel search that are highly relevant for query optimization. We present a MILP formulation for searching left-deep query plans. We use sets of binary variables to represent join operands and intermediate results, operator implementation choices or the presence of interesting orders. Linear constraints restrict value assignments to the ones representing valid query plans. We approximate the cost of scan and join operations via linear functions, allowing to increase approximation precision up to arbitrary degrees. Our experimental results are encouraging: we are able to find optimal plans for joins between 60 tables; a query size that is beyond the capabilities of prior exhaustive query optimization methods.
Multi-Threaded Dense Linear Algebra Libraries for Low-Power Asymmetric Multicore Processors
Venue: arXiv cs.MS 2015
Year: 2015

Dense linear algebra libraries, such as BLAS and LAPACK, provide a relevant collection of numerical tools for many scientific and engineering applications. While there exist high performance implementations of the BLAS (and LAPACK) functionality for many current multi-threaded architectures,the adaption of these libraries for asymmetric multicore processors (AMPs)is still pending. In this paper we address this challenge by developing an asymmetry-aware implementation of the BLAS, based on the BLIS framework, and tailored for AMPs equipped with two types of cores: fast/power hungry versus slow/energy efficient. For this purpose, we integrate coarse-grain and fine-grain parallelization strategies into the library routines which, respectively, dynamically distribute the workload between the two core types and statically repartition this work among the cores of the same type. Our results on an ARM big.LITTLE processor embedded in the Exynos 5422 SoC, using the asymmetry-aware version of the BLAS and a plain migration of the legacy version of LAPACK, experimentally assess the benefits, limitations, and potential of this approach.
Fingertip in the Eye: A cascaded CNN pipeline for the real-time fingertip detection in egocentric videos
Venue: arXiv cs.CV 2015
Year: 2015

We introduce a new pipeline for hand localization and fingertip detection. For RGB images captured from an egocentric vision mobile camera, hand and fingertip detection remains a challenging problem due to factors like background complexity and hand shape variety. To address these issues accurately and robustly, we build a large scale dataset named Ego-Fingertip and propose a bi-level cascaded pipeline of convolutional neural networks, namely, Attention-based Hand Detector as well as Multi-point Fingertip Detector. The proposed method significantly tackles challenges and achieves satisfactorily accurate prediction and real-time performance compared to previous hand and fingertip detection methods.