OpenRaiser/Intern-Atlas huggingface dataset:
Finding Stable Matchings that are Robust to Errors in the Input
Venue: arXiv cs.DS 2018
Year: 2018

We study the problem of finding solutions to the stable matching problem that are robust to errors in the input and we obtain a polynomial time algorithm for a special class of errors. In the process, we also initiate work on a new structural question concerning the stable matching problem, namely finding relationships between the lattices of solutions of two "nearby" instances. Our main algorithmic result is the following: We identify a polynomially large class of errors, $D$, that can be introduced in a stable matching instance. Given an instance $A$ of stable matching, let $B$ be the random variable that represents the instance that results after introducing {\em one} error from $D$, chosen via a given discrete probability distribution. The problem is to find a stable matching for $A$ that maximizes the probability of being stable for $B$ as well. Via new structural properties of the type described in the question stated above, we give a combinatorial polynomial time algorithm for this problem. We also show that the set of robust stable matchings for instance $A$, under probability distribution $p$, forms a sublattice of the lattice of stable matchings for $A$. We give an efficient algorithm for finding a succinct representation for this set; this representation has the property that any member of the set can be efficiently retrieved from it.
Learning to Reason with HOL4 tactics
Venue: arXiv cs.AI 2018
Year: 2018

Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences com- bined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39 percent of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32 percent in the same amount of time.
Updating the generator in PPGN-h with gradients flowing through the encoder
Venue: arXiv cs.CV 2018
Year: 2018

The Generative Adversarial Network framework has shown success in implicitly modeling data distributions and is able to generate realistic samples. Its architecture is comprised of a generator, which produces fake data that superficially seem to belong to the real data distribution, and a discriminator which is to distinguish fake from genuine samples. The Noiseless Joint Plug & Play model offers an extension to the framework by simultaneously training autoencoders. This model uses a pre-trained encoder as a feature extractor, feeding the generator with global information. Using the Plug & Play network as baseline, we design a new model by adding discriminators to the Plug & Play architecture. These additional discriminators are trained to discern real and fake latent codes, which are the output of the encoder using genuine and generated inputs, respectively. We proceed to investigate whether this approach is viable. Experiments conducted for the MNIST manifold show that this indeed is the case.
Synergy: A HW/SW Framework for High Throughput CNNs on Embedded Heterogeneous SoC
Venue: arXiv cs.DC 2018
Year: 2018

Convolutional Neural Networks (CNN) have been widely deployed in diverse application domains. There has been significant progress in accelerating both their training and inference using high-performance GPUs, FPGAs, and custom ASICs for datacenter-scale environments. The recent proliferation of mobile and IoT devices have necessitated real-time, energy-efficient deep neural network inference on embedded-class, resource-constrained platforms. In this context, we present {\em Synergy}, an automated, hardware-software co-designed, pipelined, high-throughput CNN inference framework on embedded heterogeneous system-on-chip (SoC) architectures (Xilinx Zynq). {\em Synergy} leverages, through multi-threading, all the available on-chip resources, which includes the dual-core ARM processor along with the FPGA and the NEON SIMD engines as accelerators. Moreover, {\em Synergy} provides a unified abstraction of the heterogeneous accelerators (FPGA and NEON) and can adapt to different network configurations at runtime without changing the underlying hardware accelerator architecture by balancing workload across accelerators through work-stealing. {\em Synergy} achieves 7.3X speedup, averaged across seven CNN models, over a well-optimized software-only solution. {\em Synergy} demonstrates substantially better throughput and energy-efficiency compared to the contemporary CNN implementations on the same SoC architecture.
Using Unit Testing to Detect Sanitization Flaws
Venue: arXiv cs.CR 2018
Year: 2018

Input sanitization mechanisms are widely used to mitigate vulnerabilities to injection attacks such as cross-site scripting. Static analysis tools and techniques commonly used to ensure that applications utilize sanitization functions. Dynamic analysis must be to evaluate the correctness of sanitization functions. The proposed approach is based on unit testing to bring the advantages of both static and dynamic techniques to the development time. Our approach introduces a technique to automatically extract the sanitization functions and then evaluate their effectiveness against attacks using automatically generated attack vectors. The empirical results show that the proposed technique can detect security flaws cannot find by the static analysis tools.
StarCraft Micromanagement with Reinforcement Learning and Curriculum Transfer Learning
Venue: arXiv cs.AI 2018
Year: 2018

Real-time strategy games have been an important field of game artificial intelligence in recent years. This paper presents a reinforcement learning and curriculum transfer learning method to control multiple units in StarCraft micromanagement. We define an efficient state representation, which breaks down the complexity caused by the large state space in the game environment. Then a parameter sharing multi-agent gradientdescent Sarsa(λ) (PS-MAGDS) algorithm is proposed to train the units. The learning policy is shared among our units to encourage cooperative behaviors. We use a neural network as a function approximator to estimate the action-value function, and propose a reward function to help units balance their move and attack. In addition, a transfer learning method is used to extend our model to more difficult scenarios, which accelerates the training process and improves the learning performance. In small scale scenarios, our units successfully learn to combat and defeat the built-in AI with 100% win rates. In large scale scenarios, curriculum transfer learning method is used to progressively train a group of units, and shows superior performance over some baseline methods in target scenarios. With reinforcement learning and curriculum transfer learning, our units are able to learn appropriate strategies in StarCraft micromanagement scenarios.
Towards whole-body CT Bone Segmentation
Venue: arXiv cs.CV 2018
Year: 2018

Bone segmentation from CT images is a task that has been worked on for decades. It is an important ingredient to several diagnostics or treatment planning approaches and relevant to various diseases. As high-quality manual and semi-automatic bone segmentation is very time-consuming, a reliable and fully automatic approach would be of great interest in many scenarios. In this publication, we propose a UNet inspired architecture to address the task using Deep Learning. We evaluated the approach on whole-body CT scans of patients suffering from multiple myeloma. As the disease decomposes the bone, an accurate segmentation is of utmost importance for the evaluation of bone density, disease staging and localization of focal lesions. The method was evaluated on an in-house data-set of 6000 2D image slices taken from 15 whole-body CT scans, achieving a dice score of 0.96 and an IOU of 0.94.
Attracting Tangles to Solve Parity Games
Venue: arXiv cs.LO 2018
Year: 2018

Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, because they are widely believed to admit a polynomial solution, but so far no such algorithm is known. We propose a new algorithm to solve parity games based on learning tangles, which are strongly connected subgraphs for which one player has a strategy to win all cycles in the subgraph. We argue that tangles play a fundamental role in the prominent parity game solving algorithms. We show that tangle learning is competitive in practice and the fastest solver for large random games.
Cache-Aided Interactive Multiview Video Streaming in Small Cell Wireless Networks
Venue: arXiv cs.NI 2018
Year: 2018

The emergence of novel interactive multimedia applications with high rate and low latency requirements has led to a drastic increase in the video data traffic over wireless cellular networks. Endowing the small base stations of a macro-cell with caches that can store some of the content is a promising technology to cope with the increasing pressure on the backhaul connections, and to reduce the delay for demanding video applications. In this work, delivery of an interactive multiview video to a set of wireless users is studied in an heterogeneous cellular network. Differently from existing works that focus on the optimization of the delivery delay and ignore the video characteristics, the caching and scheduling policies are jointly optimized, taking into account the quality of the delivered video and the video delivery time constraints. We formulate our joint caching and scheduling problem as the average expected video distortion minimization, and show that this problem is NP-hard. We then provide an equivalent formulation based on submodular set function maximization and propose a greedy solution with $\frac{1}{2}(1-\mbox{e}^{-1})$ approximation guarantee. The evaluation of the proposed joint caching and scheduling policy shows that it significantly outperforms benchmark algorithms based on popularity caching and independent scheduling. Another important contribution of this paper is a new constant approximation ratio for the greedy submodular set function maximization subject to a $d$-dimensional knapsack constraint.
Holiest Minimum-Cost Paths and Flows in Surface Graphs
Venue: arXiv cs.DS 2018
Year: 2018

Let $G$ be an edge-weighted directed graph with $n$ vertices embedded on an orientable surface of genus $g$. We describe a simple deterministic lexicographic perturbation scheme that guarantees uniqueness of minimum-cost flows and shortest paths in $G$. The perturbations take $O(gn)$ time to compute. We use our perturbation scheme in a black box manner to derive a deterministic $O(n \log \log n)$ time algorithm for minimum cut in \emph{directed} edge-weighted planar graphs and a deterministic $O(g^2 n \log n)$ time proprocessing scheme for the multiple-source shortest paths problem of computing a shortest path oracle for all vertices lying on a common face of a surface embedded graph. The latter result yields faster deterministic near-linear time algorithms for a variety of problems in constant genus surface embedded graphs. Finally, we open the black box in order to generalize a recent linear-time algorithm for multiple-source shortest paths in unweighted undirected planar graphs to work in arbitrary orientable surfaces. Our algorithm runs in $O(g^2 n \log g)$ time in this setting, and it can be used to give improved linear time algorithms for several problems in unweighted undirected surface embedded graphs of constant genus including the computation of minimum cuts, shortest topologically non-trivial cycles, and minimum homology bases.
Renewal Monte Carlo: Renewal theory based reinforcement learning
Venue: arXiv cs.LG 2018
Year: 2018

In this paper, we present an online reinforcement learning algorithm, called Renewal Monte Carlo (RMC), for infinite horizon Markov decision processes with a designated start state. RMC is a Monte Carlo algorithm and retains the advantages of Monte Carlo methods including low bias, simplicity, and ease of implementation while, at the same time, circumvents their key drawbacks of high variance and delayed (end of episode) updates. The key ideas behind RMC are as follows. First, under any reasonable policy, the reward process is ergodic. So, by renewal theory, the performance of a policy is equal to the ratio of expected discounted reward to the expected discounted time over a regenerative cycle. Second, by carefully examining the expression for performance gradient, we propose a stochastic approximation algorithm that only requires estimates of the expected discounted reward and discounted time over a regenerative cycle and their gradients. We propose two unbiased estimators for evaluating performance gradients---a likelihood ratio based estimator and a simultaneous perturbation based estimator---and show that for both estimators, RMC converges to a locally optimal policy. We generalize the RMC algorithm to post-decision state models and also present a variant that converges faster to an approximately optimal policy. We conclude by presenting numerical experiments on a randomly generated MDP, event-triggered communication, and inventory management.
Real-Time Prediction of the Duration of Distribution System Outages
Venue: arXiv cs.SY 2018
Year: 2018

This paper addresses the problem of predicting duration of unplanned power outages, using historical outage records to train a series of neural network predictors. The initial duration prediction is made based on environmental factors, and it is updated based on incoming field reports using natural language processing to automatically analyze the text. Experiments using 15 years of outage records show good initial results and improved performance leveraging text. Case studies show that the language processing identifies phrases that point to outage causes and repair steps.
A Euclidean Algorithm for Binary Cycles with Minimal Variance
Venue: arXiv cs.DS 2018
Year: 2018

The problem is considered of arranging symbols around a cycle, in such a way that distances between different instances of a same symbol be as uniformly distributed as possible. A sequence of moments is defined for cycles, similarly to the well-known praxis in statistics and including mean and variance. Mean is seen to be invariant under permutations of the cycle. In the case of a binary alphabet of symbols, a fast, constructive, sequencing algorithm is introduced, strongly resembling the celebrated Euclidean method for greatest common divisor computation, and the cycle returned is characterized in terms of symbol distances. A minimal variance condition is proved, and the proposed Euclidean algorithm is proved to satisfy it, thus being optimal. Applications to productive systems and information processing are briefly discussed.
iReplayer: In-situ and Identical Record-and-Replay for Multithreaded Applications
Venue: arXiv cs.OS 2018
Year: 2018

Reproducing executions of multithreaded programs is very challenging due to many intrinsic and external non-deterministic factors. Existing RnR systems achieve significant progress in terms of performance overhead, but none targets the in-situ setting, in which replay occurs within the same process as the recording process. Also, most existing work cannot achieve identical replay, which may prevent the reproduction of some errors. This paper presents iReplayer, which aims to identically replay multithreaded programs in the original process (under the "in-situ" setting). The novel in-situ and identical replay of iReplayer makes it more likely to reproduce errors, and allows it to directly employ debugging mechanisms (e.g. watchpoints) to aid failure diagnosis. Currently, iReplayer only incurs 3% performance overhead on average, which allows it to be always enabled in the production environment. iReplayer enables a range of possibilities, and this paper presents three examples: two automatic tools for detecting buffer overflows and use-after-free bugs, and one interactive debugging tool that is integrated with GDB.
Real-time Detection of Content Polluters in Partially Observable Twitter Networks
Venue: arXiv cs.SI 2018
Year: 2018

Content polluters, or bots that hijack a conversation for political or advertising purposes are a known problem for event prediction, election forecasting and when distinguishing real news from fake news in social media data. Identifying this type of bot is particularly challenging, with state-of-the-art methods utilising large volumes of network data as features for machine learning models. Such datasets are generally not readily available in typical applications which stream social media data for real-time event prediction. In this work we develop a methodology to detect content polluters in social media datasets that are streamed in real-time. Applying our method to the problem of civil unrest event prediction in Australia, we identify content polluters from individual tweets, without collecting social network or historical data from individual accounts. We identify some peculiar characteristics of these bots in our dataset and propose metrics for identification of such accounts. We then pose some research questions around this type of bot detection, including: how good Twitter is at detecting content polluters and how well state-of-the-art methods perform in detecting bots in our dataset.
A Smart Home Gateway Platform for Data Collection and Awareness
Venue: arXiv cs.NI 2018
Year: 2018

Smart homes have attracted much attention due to the expanding of Internet-of-Things (IoT) and smart devices. In this paper, we propose a smart gateway platform for data collection and awareness in smart home networks. A smart gateway will replace the traditional network gateway to connect the home network and the Internet. A smart home network supports different types of smart devices, such as in home IoT devices, smart phones, smart electric appliances, etc. A traditional network gateway is not capable of providing quality-of-service measurement, user behavioral analytics, or network optimization. Such tasks are traditionally performed with measurement agents such as optical splitters or network probes deployed in the core network. Our proposed platform is a lightweight plug-in for the smart gateway to accomplish data collection, awareness and reporting. While the smart gateway is able to adjust the control policy for data collection and awareness locally, a cloud-based controller is also included for more refined control policy updates. Furthermore, we propose a multi-dimensional awareness framework to achieve accurate data awareness at the smart gateway. The efficiency of data collection and accuracy of data awareness of the proposed platform is demonstrated based on the tests using actual data traffic from a large number of smart home users.
NegPSpan: efficient extraction of negative sequential patterns with embedding constraints
Venue: arXiv cs.DB 2018
Year: 2018

Mining frequent sequential patterns consists in extracting recurrent behaviors, modeled as patterns, in a big sequence dataset. Such patterns inform about which events are frequently observed in sequences, i.e. what does really happen. Sometimes, knowing that some specific event does not happen is more informative than extracting a lot of observed events. Negative sequential patterns (NSP) formulate recurrent behaviors by patterns containing both observed events and absent events. Few approaches have been proposed to mine such NSPs. In addition, the syntax and semantics of NSPs differ in the different methods which makes it difficult to compare them. This article provides a unified framework for the formulation of the syntax and the semantics of NSPs. Then, we introduce a new algorithm, NegPSpan, that extracts NSPs using a PrefixSpan depth-first scheme and enabling maxgap constraints that other approaches do not take into account. The formal framework allows for highlighting the differences between the proposed approach wrt to the methods from the literature, especially wrt the state of the art approach eNSP. Intensive experiments on synthetic and real datasets show that NegPSpan can extract meaningful NSPs and that it can process bigger datasets than eNSP thanks to significantly lower memory requirements and better computation times.
Losing Treewidth by Separating Subsets
Venue: arXiv cs.DS 2018
Year: 2018

We study the problem of deleting the smallest set $S$ of vertices (resp. edges) from a given graph $G$ such that the induced subgraph (resp. subgraph) $G \setminus S$ belongs to some class $\mathcal{H}$. We consider the case where graphs in $\mathcal{H}$ have treewidth bounded by $t$, and give a general framework to obtain approximation algorithms for both vertex and edge-deletion settings from approximation algorithms for certain natural graph partitioning problems called $k$-Subset Vertex Separator and $k$-Subset Edge Separator, respectively. For the vertex deletion setting, our framework combined with the current best result for $k$-Subset Vertex Separator, yields a significant improvement in the approximation ratios for basic problems such as $k$-Treewidth Vertex Deletion and Planar-$F$ Vertex Deletion. Our algorithms are simpler than previous works and give the first uniform approximation algorithms under the natural parameterization. For the edge deletion setting, we give improved approximation algorithms for $k$-Subset Edge Separator combining ideas from LP relaxations and important separators. We present their applications in bounded-degree graphs, and also give an APX-hardness result for the edge deletion problems.
Short Proofs for Some Symmetric Quantified Boolean Formulas
Venue: arXiv cs.LO 2018
Year: 2018

We exploit symmetries to give short proofs for two prominent formula families of QBF proof complexity. On the one hand, we employ symmetry breakers. On the other hand, we enrich the (relatively weak) QBF resolution calculus Q-Res with the symmetry rule and obtain separations to powerful QBF calculi.
WhatsApp, Doc? A First Look at WhatsApp Public Group Data
Venue: arXiv cs.SI 2018
Year: 2018

In this dataset paper we describe our work on the collection and analysis of public WhatsApp group data. Our primary goal is to explore the feasibility of collecting and using WhatsApp data for social science research. We therefore present a generalisable data collection methodology, and a publicly available dataset for use by other researchers. To provide context, we perform statistical exploration to allow researchers to understand what public WhatsApp group data can be collected and how this data can be used. Given the widespread use of WhatsApp, our techniques to obtain public data and potential applications are important for the community.