OpenRaiser/Intern-Atlas huggingface dataset:
An Improved Lower Bound for General Position Subset Selection
Venue: arXiv cs.CG 2018
Year: 2018

In the General Position Subset Selection (GPSS) problem, the goal is to find the largest possible subset of a set of points such that no three of its members are collinear. If $s_{\mathrm{GPSS}}$ is the size of the optimal solution, $\sqrt{s_{\mathrm{GPSS}}}$ is the current best guarantee for the size of the solution obtained using a polynomial time algorithm. In this paper we present an algorithm for GPSS to improve this bound based on the number of collinear pairs of points. We experimentally evaluate this and few other GPSS algorithms; the result of these experiments suggests further opportunities for obtaining tighter lower bounds for GPSS.
Improving the Neural GPU Architecture for Algorithm Learning
Venue: arXiv cs.NE 2018
Year: 2018

Algorithm learning is a core problem in artificial intelligence with significant implications on automation level that can be achieved by machines. Recently deep learning methods are emerging for synthesizing an algorithm from its input-output examples, the most successful being the Neural GPU, capable of learning multiplication. We present several improvements to the Neural GPU that substantially reduces training time and improves generalization. We introduce a new technique - hard nonlinearities with saturation costs- that has general applicability. We also introduce a technique of diagonal gates that can be applied to active-memory models. The proposed architecture is the first capable of learning decimal multiplication end-to-end.
Verified Low-Level Programming Embedded in F*
Venue: arXiv cs.PL 2018
Year: 2018

We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code. By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance. We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code, specification and proof. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.
Privacy-Preserving Personal Model Training
Venue: arXiv cs.LG 2018
Year: 2018

Many current Internet services rely on inferences from models trained on user data. Commonly, both the training and inference tasks are carried out using cloud resources fed by personal data collected at scale from users. Holding and using such large collections of personal data in the cloud creates privacy risks to the data subjects, but is currently required for users to benefit from such services. We explore how to provide for model training and inference in a system where computation is pushed to the data in preference to moving data to the cloud, obviating many current privacy risks. Specifically, we take an initial model learnt from a small set of users and retrain it locally using data from a single user. We evaluate on two tasks: one supervised learning task, using a neural network to recognise users' current activity from accelerometer traces; and one unsupervised learning task, identifying topics in a large set of documents. In both cases the accuracy is improved. We also analyse the robustness of our approach against adversarial attacks, as well as its feasibility by presenting a performance evaluation on a representative resource-constrained device (a Raspberry Pi).
On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping
Venue: arXiv cs.PL 2018
Year: 2018

Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.
Adaptive Matching for Expert Systems with Uncertain Task Types
Venue: arXiv cs.AI 2018
Year: 2018

A matching in a two-sided market often incurs an externality: a matched resource may become unavailable to the other side of the market, at least for a while. This is especially an issue in online platforms involving human experts as the expert resources are often scarce. The efficient utilization of experts in these platforms is made challenging by the fact that the information available about the parties involved is usually limited. To address this challenge, we develop a model of a task-expert matching system where a task is matched to an expert using not only the prior information about the task but also the feedback obtained from the past matches. In our model the tasks arrive online while the experts are fixed and constrained by a finite service capacity. For this model, we characterize the maximum task resolution throughput a platform can achieve. We show that the natural greedy approaches where each expert is assigned a task most suitable to her skill is suboptimal, as it does not internalize the above externality. We develop a throughput optimal backpressure algorithm which does so by accounting for the `congestion' among different task types. Finally, we validate our model and confirm our theoretical findings with data-driven simulations via logs of Math.StackExchange, a StackOverflow forum dedicated to mathematics.
Being Robust (in High Dimensions) Can Be Practical
Venue: arXiv cs.LG 2018
Year: 2018

Robust estimation is much more challenging in high dimensions than it is in one dimension: Most techniques either lead to intractable optimization problems or estimators that can tolerate only a tiny fraction of errors. Recent work in theoretical computer science has shown that, in appropriate distributional models, it is possible to robustly estimate the mean and covariance with polynomial time algorithms that can tolerate a constant fraction of corruptions, independent of the dimension. However, the sample and time complexity of these algorithms is prohibitively large for high-dimensional applications. In this work, we address both of these issues by establishing sample complexity bounds that are optimal, up to logarithmic factors, as well as giving various refinements that allow the algorithms to tolerate a much larger fraction of corruptions. Finally, we show on both synthetic and real data that our algorithms have state-of-the-art performance and suddenly make high-dimensional robust estimation a realistic possibility.
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
Venue: arXiv cs.SY 2018
Year: 2018

Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learning algorithms aim to generalize from examples, they are only as good as the examples provided, and recent efforts have shown that they can produce inconsistent output under small adversarial perturbations. This raises the question: can the output from learning components can lead to a failure of the entire CPS? In this work, we address this question by formulating it as a problem of falsifying signal temporal logic (STL) specifications for CPS with ML components. We propose a compositional falsification framework where a temporal logic falsifier and a machine learning analyzer cooperate with the aim of finding falsifying executions of the considered model. The efficacy of the proposed technique is shown on an automatic emergency braking system model with a perception component based on deep neural networks.
Assessing the Privacy Cost in Centralized Event-Based Demand Response for Microgrids
Venue: arXiv cs.SY 2018
Year: 2018

Demand response (DR) programs have emerged as a potential key enabling ingredient in the context of smart grid (SG). Nevertheless, the rising concerns over privacy issues raised by customers subscribed to these programs constitute a major threat towards their effective deployment and utilization. This has driven extensive research to resolve the hindrance confronted, resulting in a number of methods being proposed for preserving customers' privacy. While these methods provide stringent privacy guarantees, only limited attention has been paid to their computational efficiency and performance quality. Under the paradigm of differential privacy, this paper initiates a systematic empirical study on quantifying the trade-off between privacy and optimality in centralized DR systems for maximizing cumulative customer utility. Aiming to elucidate the factors governing this trade-off, we analyze the cost of privacy in terms of the effect incurred on the objective value of the DR optimization problem when applying the employed privacy-preserving strategy based on Laplace mechanism. The theoretical results derived from the analysis are complemented with empirical findings, corroborated extensively by simulations on a 4-bus MG system with up to thousands of customers. By evaluating the impact of privacy, this pilot study serves DR practitioners when considering the social and economic implications of deploying privacy-preserving DR programs in practice. Moreover, it stimulates further research on exploring more efficient approaches with bounded performance guarantees for optimizing energy procurement of MGs without infringing the privacy of customers on demand side.
On Structured Prediction Theory with Calibrated Convex Surrogate Losses
Venue: arXiv cs.LG 2018
Year: 2018

We provide novel theoretical insights on structured prediction in the context of efficient convex surrogate loss minimization with consistency guarantees. For any task loss, we construct a convex surrogate that can be optimized via stochastic gradient descent and we prove tight bounds on the so-called "calibration function" relating the excess surrogate risk to the actual risk. In contrast to prior related work, we carefully monitor the effect of the exponential number of classes in the learning guarantees as well as on the optimization complexity. As an interesting consequence, we formalize the intuition that some task losses make learning harder than others, and that the classical 0-1 loss is ill-suited for general structured prediction.
Flow Fields: Dense Correspondence Fields for Highly Accurate Large Displacement Optical Flow Estimation
Venue: arXiv cs.CV 2018
Year: 2018

Modern large displacement optical flow algorithms usually use an initialization by either sparse descriptor matching techniques or dense approximate nearest neighbor fields. While the latter have the advantage of being dense, they have the major disadvantage of being very outlier-prone as they are not designed to find the optical flow, but the visually most similar correspondence. In this article we present a dense correspondence field approach that is much less outlier-prone and thus much better suited for optical flow estimation than approximate nearest neighbor fields. Our approach does not require explicit regularization, smoothing (like median filtering) or a new data term. Instead we solely rely on patch matching techniques and a novel multi-scale matching strategy. We also present enhancements for outlier filtering. We show that our approach is better suited for large displacement optical flow estimation than modern descriptor matching techniques. We do so by initializing EpicFlow with our approach instead of their originally used state-of-the-art descriptor matching technique. We significantly outperform the original EpicFlow on MPI-Sintel, KITTI 2012, KITTI 2015 and Middlebury. In this extended article of our former conference publication we further improve our approach in matching accuracy as well as runtime and present more experiments and insights.
Inference in Sparse Graphs with Pairwise Measurements and Side Information
Venue: arXiv cs.LG 2018
Year: 2018

We consider the statistical problem of recovering a hidden "ground truth" binary labeling for the vertices of a graph up to low Hamming error from noisy edge and vertex measurements. We present new algorithms and a sharp finite-sample analysis for this problem on trees and sparse graphs with poor expansion properties such as hypergrids and ring lattices. Our method generalizes and improves over that of Globerson et al. (2015), who introduced the problem for two-dimensional grid lattices. For trees we provide a simple, efficient, algorithm that infers the ground truth with optimal Hamming error has optimal sample complexity and implies recovery results for all connected graphs. Here, the presence of side information is critical to obtain a non-trivial recovery rate. We then show how to adapt this algorithm to tree decompositions of edge-subgraphs of certain graph families such as lattices, resulting in optimal recovery error rates that can be obtained efficiently The thrust of our analysis is to 1) use the tree decomposition along with edge measurements to produce a small class of viable vertex labelings and 2) apply an analysis influenced by statistical learning theory to show that we can infer the ground truth from this class using vertex measurements. We show the power of our method in several examples including hypergrids, ring lattices, and the Newman-Watts model for small world graphs. For two-dimensional grids, our results improve over Globerson et al. (2015) by obtaining optimal recovery in the constant-height regime.
Causal Data Science for Financial Stress Testing
Venue: arXiv cs.LG 2018
Year: 2018

The most recent financial upheavals have cast doubt on the adequacy of some of the conventional quantitative risk management strategies, such as VaR (Value at Risk), in many common situations. Consequently, there has been an increasing need for verisimilar financial stress testings, namely simulating and analyzing financial portfolios in extreme, albeit rare scenarios. Unlike conventional risk management which exploits statistical correlations among financial instruments, here we focus our analysis on the notion of probabilistic causation, which is embodied by Suppes-Bayes Causal Networks (SBCNs); SBCNs are probabilistic graphical models that have many attractive features in terms of more accurate causal analysis for generating financial stress scenarios. In this paper, we present a novel approach for conducting stress testing of financial portfolios based on SBCNs in combination with classical machine learning classification tools. The resulting method is shown to be capable of correctly discovering the causal relationships among financial factors that affect the portfolios and thus, simulating stress testing scenarios with a higher accuracy and lower computational complexity than conventional Monte Carlo Simulations.
Achievable Rate Region of Non-Orthogonal Multiple Access Systems with Wireless Powered Decoder
Venue: arXiv cs.IT 2018
Year: 2018

Non-orthogonal multiple access (NOMA) is a candidate multiple access scheme in 5G systems for the simultaneous access of tremendous number of wireless nodes. On the other hand, RF-enabled wireless energy harvesting is a promising technology for self-sustainable wireless nodes. In this paper, we consider a NOMA system where the near user harvests energy from the strong radio signal to power-on the information decoder. A generalized energy harvesting scheme is proposed by combining the conventional time switching and power splitting scheme. The achievable rate region of the proposed scheme is characterized under both constant and dynamic decoding power consumption models. If the decoding power is constant, the achievable rate region can be found by solving two convex optimization subproblems, and the regions for two special cases: time switching and power splitting, are characterized in closed-form. If the decoding power is proportional to data rate, the achievable rate region can be found by exhaustive search algorithm. Numerical results show that the achievable rate region of the proposed generalized scheme is larger than those of time switching scheme and power splitting scheme, and rate-dependent decoder design helps to enlarge the achievable rate region.
GUN: Gradual Upsampling Network for Single Image Super-Resolution
Venue: arXiv cs.CV 2018
Year: 2018

In this paper, an efficient super-resolution (SR) method based on deep convolutional neural network (CNN) is proposed, namely Gradual Upsampling Network (GUN). Recent CNN based SR methods often preliminarily magnify the low resolution (LR) input to high resolution (HR) and then reconstruct the HR input, or directly reconstruct the LR input and then recover the HR result at the last layer. The proposed GUN utilizes a gradual process instead of these two commonly used frameworks. The GUN consists of an input layer, multiple upsampling and convolutional layers, and an output layer. By means of the gradual process, the proposed network can simplify the direct SR problem to multistep easier upsampling tasks with very small magnification factor in each step. Furthermore, a gradual training strategy is presented for the GUN. In the proposed training process, an initial network can be easily trained with edge-like samples, and then the weights are gradually tuned with more complex samples. The GUN can recover fine and vivid results, and is easy to be trained. The experimental results on several image sets demonstrate the effectiveness of the proposed network.
C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation
Venue: arXiv cs.LO 2018
Year: 2018

Higher-order recursion schemes (HORS) have received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. C-SHORe implements the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a backwards saturation algorithm for CPDS. Additionally, it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, it uses an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We provide an up-to-date comparison of C-SHORe with the state-of-the-art verification tools for HORS. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.
When are Stochastic Transition Systems Tameable?
Venue: arXiv cs.LO 2018
Year: 2018

A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs.
On packing chromatic number of subcubic outerplanar graphs
Venue: arXiv cs.DM 2018
Year: 2018

Although it has recently been proved that the packing chromatic number is unbounded on the class of subcubic graphs, there exists subclasses in which the packing chromatic number is finite (and small). These subclasses include subcubic trees, base-3 Sierpi{ń}ski graphs and hexagonal lattices.In this paper we are interested in the packing chromatic number of subcubic outerplanar graphs. We provide asymptotic bounds depending on structural properties of the outerplanar graphs and determine sharper bounds for some classes of subcubic outerplanar graphs.