OpenRaiser/Intern-Atlas huggingface dataset:
On the reducibility of geometric constraint graphs
Venue: arXiv cs.CG 2018
Year: 2018

Geometric modeling by constraints, whose applications are of interest to communities from various fields such as mechanical engineering, computer aided design, symbolic computation or molecular chemistry, is now integrated into standard modeling tools. In this discipline, a geometric form is specified by the relations that the components of this form must verify instead of explicitly specifying these components. The purpose of the resolution is to deduce the form satisfying all these constraints. Various methods have been proposed to solve this problem. We will focus on the so-called graph-based or graph-based methods with application to the two-dimensional space.
Invariant Synthesis for Incomplete Verification Engines
Venue: arXiv cs.PL 2018
Year: 2018

We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.
Avoiding Echo-Responses in a Retrieval-Based Conversation System
Venue: arXiv cs.CL 2018
Year: 2018

Retrieval-based conversation systems generally tend to highly rank responses that are semantically similar or even identical to the given conversation context. While the system's goal is to find the most appropriate response, rather than the most semantically similar one, this tendency results in low-quality responses. We refer to this challenge as the echoing problem. To mitigate this problem, we utilize a hard negative mining approach at the training stage. The evaluation shows that the resulting model reduces echoing and achieves better results in terms of Average Precision and Recall@N metrics, compared to the models trained without the proposed approach.
A Heuristic Proof Procedure for First-Order Logic
Venue: arXiv cs.LO 2018
Year: 2018

Inspired by the efficient proof procedures discussed in {\em Computability logic} \cite{Jap03,Japic,Japfin}, we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system and has the following features: (a)~ it views sequents as games between the machine and the environment, and (b)~ it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness. We also discuss LKg', a variant of LKg with some optimizations added.
Timely-Throughput Optimal Scheduling with Prediction
Venue: arXiv cs.NI 2018
Year: 2018

Motivated by the increasing importance of providing delay-guaranteed services in general computing and communication systems, and the recent wide adoption of learning and prediction in network control, in this work, we consider a general stochastic single-server multi-user system and investigate the fundamental benefit of predictive scheduling in improving timely-throughput, being the rate of packets that are delivered to destinations before their deadlines. By adopting an error rate-based prediction model, we first derive a Markov decision process (MDP) solution to optimize the timely-throughput objective subject to an average resource consumption constraint. Based on a packet-level decomposition of the MDP, we explicitly characterize the optimal scheduling policy and rigorously quantify the timely-throughput improvement due to predictive-service, which scales as $Θ(p\left[C_{1}\frac{(a-a_{\max}q)}{p-q}ρ^τ+C_{2}(1-\frac{1}{p})\right](1-ρ^{D}))$, where $a, a_{\max}, ρ\in(0, 1), C_1>0, C_2\ge0$ are constants, $p$ is the true-positive rate in prediction, $q$ is the false-negative rate, $τ$ is the packet deadline and $D$ is the prediction window size. We also conduct extensive simulations to validate our theoretical findings. Our results provide novel insights into how prediction and system parameters impact performance and provide useful guidelines for designing predictive low-latency control algorithms.
On W[1]-Hardness as Evidence for Intractability
Venue: arXiv cs.CC 2018
Year: 2018

The central conjecture of parameterized complexity states that FPT is not equal to W[1], and is generally regarded as the parameterized counterpart to P != NP. We revisit the issue of the plausibility of FPT != W[1], focusing on two aspects: the difficulty of proving the conjecture (assuming it holds), and how the relation between the two classes might differ from the one between P and NP. Regarding the first aspect, we give new evidence that separating FPT from W[1] would be considerably harder than doing the same for P and NP. Our main result regarding the relation between FPT and W[1] states that the closure of W[1] under relativization with FPT-oracles is precisely the class W[P], implying that either FPT is not low for W[1], or the W-Hierarchy collapses. This theorem also has consequences for the A-Hierarchy (a parameterized version of the Polynomial Hierarchy), namely that unless W[P] is a subset of some level A[t], there are structural differences between the A-Hierarchy and the Polynomial Hierarchy. We also prove that under the unlikely assumption that W[P] collapses to W[1] in a specific way, the collapse of any two consecutive levels of the A-Hierarchy implies the collapse of the entire hierarchy to a finite level; this extends a result of Chen, Flum, and Grohe (2005). Finally, we give weak (oracle-based) evidence that the inclusion of W[t] in A[t] is strict for t>1, and that the W-Hierarchy is proper. The latter result answers a question of Downey and Fellows (1993).
Bubble-Flip -- A New Generation Algorithm for Prefix Normal Words
Venue: arXiv cs.DS 2018
Year: 2018

We present a new recursive generation algorithm for prefix normal words. These are binary strings with the property that no substring has more 1s than the prefix of the same length. The new algorithm uses two operations on binary strings, which exploit certain properties of prefix normal words in a smart way. We introduce infinite prefix normal words and show that one of the operations used by the algorithm, if applied repeatedly to extend the string, produces an ultimately periodic infinite word, which is prefix normal. Moreover, based on the original finite word, we can predict both the length and the density of an ultimate period of this infinite word.
Toward Secure Edge Networks Taming Device to Device (D2D) Communication in IoT
Venue: arXiv cs.CR 2018
Year: 2018

The growing popularity of Internet-of-Things (IoT) has created the need for network-based traffic anomaly detection systems that could identify misbehaving devices. In this work, we propose a lightweight technique, IoT-guard, for identifying malicious traffic flows. IoT-guard uses semi-supervised learning to distinguish between malicious and benign device behaviours using the network traffic generated by devices. In order to achieve this, we extracted 39 features from network logs and discard any features containing redundant information. After feature selection, fuzzy C-Mean (FCM) algorithm was trained to obtain clusters discriminating benign traffic from malicious traffic. We studied the feature scores in these clusters and use this information to predict the type of new traffic flows. IoT-guard was evaluated using a real-world testbed with more than 30 devices. The results show that IoTguard achieves high accuracy (98%), in differentiating various types of malicious and benign traffic, with low false positive rates. Furthermore, it has low resource footprint and can operate on OpenWRT enabled access points and COTS computing boards.
An ILP Solver for Multi-label MRFs with Connectivity Constraints
Venue: arXiv cs.CV 2018
Year: 2018

Integer Linear Programming (ILP) formulations of Markov random fields (MRFs) models with global connectivity priors were investigated previously in computer vision, e.g., \cite{globalinter,globalconn}. In these works, only Linear Programing (LP) relaxations \cite{globalinter,globalconn} or simplified versions \cite{graphcutbase} of the problem were solved. This paper investigates the ILP of multi-label MRF with exact connectivity priors via a branch-and-cut method, which provably finds globally optimal solutions. The method enforces connectivity priors iteratively by a cutting plane method, and provides feasible solutions with a guarantee on sub-optimality even if we terminate it earlier. The proposed ILP can be applied as a post-processing method on top of any existing multi-label segmentation approach. As it provides globally optimal solution, it can be used off-line to generate ground-truth labeling, which serves as quality check for any fast on-line algorithm. Furthermore, it can be used to generate ground-truth proposals for weakly supervised segmentation. We demonstrate the power and usefulness of our model by several experiments on the BSDS500 and PASCAL image dataset, as well as on medical images with trained probability maps.
A Survey on Multi-View Clustering
Venue: arXiv cs.LG 2018
Year: 2018

With advances in information acquisition technologies, multi-view data become ubiquitous. Multi-view learning has thus become more and more popular in machine learning and data mining fields. Multi-view unsupervised or semi-supervised learning, such as co-training, co-regularization has gained considerable attention. Although recently, multi-view clustering (MVC) methods have been developed rapidly, there has not been a survey to summarize and analyze the current progress. Therefore, this paper reviews the common strategies for combining multiple views of data and based on this summary we propose a novel taxonomy of the MVC approaches. We further discuss the relationships between MVC and multi-view representation, ensemble clustering, multi-task clustering, multi-view supervised and semi-supervised learning. Several representative real-world applications are elaborated. To promote future development of MVC, we envision several open problems that may require further investigation and thorough examination.
LSTM Pose Machines
Venue: arXiv cs.CV 2018
Year: 2018

We observed that recent state-of-the-art results on single image human pose estimation were achieved by multi-stage Convolution Neural Networks (CNN). Notwithstanding the superior performance on static images, the application of these models on videos is not only computationally intensive, it also suffers from performance degeneration and flicking. Such suboptimal results are mainly attributed to the inability of imposing sequential geometric consistency, handling severe image quality degradation (e.g. motion blur and occlusion) as well as the inability of capturing the temporal correlation among video frames. In this paper, we proposed a novel recurrent network to tackle these problems. We showed that if we were to impose the weight sharing scheme to the multi-stage CNN, it could be re-written as a Recurrent Neural Network (RNN). This property decouples the relationship among multiple network stages and results in significantly faster speed in invoking the network for videos. It also enables the adoption of Long Short-Term Memory (LSTM) units between video frames. We found such memory augmented RNN is very effective in imposing geometric consistency among frames. It also well handles input quality degradation in videos while successfully stabilizes the sequential outputs. The experiments showed that our approach significantly outperformed current state-of-the-art methods on two large-scale video pose estimation benchmarks. We also explored the memory cells inside the LSTM and provided insights on why such mechanism would benefit the prediction for video-based pose estimations.
'Indifference' methods for managing agent rewards
Venue: arXiv cs.AI 2018
Year: 2018

`Indifference' refers to a class of methods used to control reward based agents. Indifference techniques aim to achieve one or more of three distinct goals: rewards dependent on certain events (without the agent being motivated to manipulate the probability of those events), effective disbelief (where agents behave as if particular events could never happen), and seamless transition from one reward function to another (with the agent acting as if this change is unanticipated). This paper presents several methods for achieving these goals in the POMDP setting, establishing their uses, strengths, and requirements. These methods of control work even when the implications of the agent's reward are otherwise not fully understood.
An Online Detection Framework for Cyber Attacks on Automatic Generation Control
Venue: arXiv cs.SY 2018
Year: 2018

We propose an online framework to detect cyber attacks on Automatic Generation Control (AGC). A cyber at- tack detection algorithm is designed based on the approach of Dynamic Watermarking. The detection algorithm provides a theoretical guarantee of detection of cyber attacks launched by sophisticated attackers possessing extensive knowledge of the physical and statistical models of targeted power systems. The proposed framework is practically implementable, as it needs no hardware update on generation units. The efficacy of the proposed framework is validated in both four-area system and 140-bus system.
Enabling Work-conserving Bandwidth Guarantees for Multi-tenant Datacenters via Dynamic Tenant-Queue Binding
Venue: arXiv cs.NI 2018
Year: 2018

Today's cloud networks are shared among many tenants. Bandwidth guarantees and work conservation are two key properties to ensure predictable performance for tenant applications and high network utilization for providers. Despite significant efforts, very little prior work can really achieve both properties simultaneously even some of them claimed so. In this paper, we present QShare, an in-network based solution to achieve bandwidth guarantees and work conservation simultaneously. QShare leverages weighted fair queuing on commodity switches to slice network bandwidth for tenants, and solves the challenge of queue scarcity through balanced tenant placement and dynamic tenant-queue binding. QShare is readily implementable with existing switching chips. We have implemented a QShare prototype and evaluated it via both testbed experiments and simulations. Our results show that QShare ensures bandwidth guarantees while driving network utilization to over 91% even under unpredictable traffic demands.
Learning Representations from Road Network for End-to-End Urban Growth Simulation
Venue: arXiv cs.AI 2018
Year: 2018

From our experiences in the past, we have seen that the growth of cities is very much dependent on the transportation networks. In mega cities, transportation networks determine to a significant extent as to where the people will move and houses will be built. Hence, transportation network data is crucial to an urban growth prediction system. Existing works have used manually derived distance based features based on the road networks to build models on urban growth. But due to the non-generic and laborious nature of the manual feature engineering process, we can shift to End-to-End systems which do not rely on manual feature engineering. In this paper, we propose a method to integrate road network data to an existing Rule based End-to-End framework without manual feature engineering. Our method employs recurrent neural networks to represent road networks in a structured way such that it can be plugged into the previously proposed End-to-End framework. The proposed approach enhances the performance in terms of Figure of Merit, Producer's accuracy, User's accuracy and Overall accuracy of the existing Rule based End-to-End framework.
Real-time deep hair matting on mobile devices
Venue: arXiv cs.CV 2018
Year: 2018

Augmented reality is an emerging technology in many application domains. Among them is the beauty industry, where live virtual try-on of beauty products is of great importance. In this paper, we address the problem of live hair color augmentation. To achieve this goal, hair needs to be segmented quickly and accurately. We show how a modified MobileNet CNN architecture can be used to segment the hair in real-time. Instead of training this network using large amounts of accurate segmentation data, which is difficult to obtain, we use crowd sourced hair segmentation data. While such data is much simpler to obtain, the segmentations there are noisy and coarse. Despite this, we show how our system can produce accurate and fine-detailed hair mattes, while running at over 30 fps on an iPad Pro tablet.
On the Relation of External and Internal Feature Interactions: A Case Study
Venue: arXiv cs.SE 2018
Year: 2018

Detecting feature interactions is imperative for accurately predicting performance of highly-configurable systems. State-of-the-art performance prediction techniques rely on supervised machine learning for detecting feature interactions, which, in turn, relies on time consuming performance measurements to obtain training data. By providing information about potentially interacting features, we can reduce the number of required performance measurements and make the overall performance prediction process more time efficient. We expect that the information about potentially interacting features can be obtained by statically analyzing the source code of a highly-configurable system, which is computationally cheaper than performing multiple performance measurements. To this end, we conducted a qualitative case study in which we explored the relation between control-flow feature interactions (detected through static program analysis) and performance feature interactions (detected by performance prediction techniques using performance measurements). We found that a relation exists, which can potentially be exploited to predict performance interactions.
In silico generation of novel, drug-like chemical matter using the LSTM neural network
Venue: arXiv cs.LG 2018
Year: 2018

The exploration of novel chemical spaces is one of the most important tasks of cheminformatics when supporting the drug discovery process. Properly designed and trained deep neural networks can provide a viable alternative to brute-force de novo approaches or various other machine-learning techniques for generating novel drug-like molecules. In this article we present a method to generate molecules using a long short-term memory (LSTM) neural network and provide an analysis of the results, including a virtual screening test. Using the network one million drug-like molecules were generated in 2 hours. The molecules are novel, diverse (contain numerous novel chemotypes), have good physicochemical properties and have good synthetic accessibility, even though these qualities were not specific constraints. Although novel, their structural features and functional groups remain closely within the drug-like space defined by the bioactive molecules from ChEMBL. Virtual screening using the profile QSAR approach confirms that the potential of these novel molecules to show bioactivity is comparable to the ChEMBL set from which they were derived. The molecule generator written in Python used in this study is available on request.
A Distributed Frank-Wolfe Framework for Learning Low-Rank Matrices with the Trace Norm
Venue: arXiv cs.DC 2018
Year: 2018

We consider the problem of learning a high-dimensional but low-rank matrix from a large-scale dataset distributed over several machines, where low-rankness is enforced by a convex trace norm constraint. We propose DFW-Trace, a distributed Frank-Wolfe algorithm which leverages the low-rank structure of its updates to achieve efficiency in time, memory and communication usage. The step at the heart of DFW-Trace is solved approximately using a distributed version of the power method. We provide a theoretical analysis of the convergence of DFW-Trace, showing that we can ensure sublinear convergence in expectation to an optimal solution with few power iterations per epoch. We implement DFW-Trace in the Apache Spark distributed programming framework and validate the usefulness of our approach on synthetic and real data, including the ImageNet dataset with high-dimensional features extracted from a deep neural network.
A Unified Asymptotic Analysis of Area Spectral Efficiency in Ultradense Cellular Networks
Venue: arXiv cs.IT 2018
Year: 2018

This paper studies the asymptotic properties of average area spectral efficiency (ASE) of a downlink cellular network in the limit of very dense base station (BS) and user densities. This asymptotic analysis relies on three assumptions: (1) interference is treated as noise; (2) the BS locations are drawn from a Poisson point process; (3) the path loss function is bounded above satisfying mild regularity conditions. We consider three possible definitions of the average ASE, all of which give units of bits per second per unit bandwidth per unit area. When there is no constraint on the minimum operational signal-to-interference-plus-noise ratio (SINR) and instantaneous full channel state information (CSI) is available at the transmitter, the average ASE is proven to saturate to a constant, which we derive in a closed form. For the other two ASE definitions, wherein either a minimum SINR is enforced or CSI is not available, the average ASE is instead shown to collapse to zero at high BS density. We provide several familiar case studies for the class of considered path loss models, and demonstrate that our results cover most previous models and results on ultradense networks as special cases.
Adjacency and Tensor Representation in General Hypergraphs Part 1: e-adjacency Tensor Uniformisation Using Homogeneous Polynomials
Venue: arXiv cs.DM 2018
Year: 2018

Adjacency between two vertices in graphs or hypergraphs is a pairwise relationship. It is redefined in this article as 2-adjacency. In general hypergraphs, hyperedges hold for $n$-adic relationship. To keep the $n$-adic relationship the concepts of $k$-adjacency and e-adjacency are defined. In graphs 2-adjacency and e-adjacency concepts match, just as $k$-adjacency and e-adjacency do for $k$-uniform hypergraphs. For general hypergraphs these concepts are different. This paper also contributes in a uniformization process of a general hypergraph to allow the definition of an e-adjacency tensor, viewed as a hypermatrix, reflecting the general hypergraph structure. This symmetric e-adjacency hypermatrix allows to capture not only the degree of the vertices and the cardinality of the hyperedges but also makes a full separation of the different layers of a hypergraph.