OpenRaiser/Intern-Atlas huggingface dataset:
Integration of the Static Analysis Results Interchange Format in CogniCrypt
Venue: arXiv cs.PL 2019
Year: 2019

Background - Software companies increasingly rely on static analysis tools to detect potential bugs and security vulnerabilities in their software products. In the past decade, more and more commercial and open-source static analysis tools have been developed and are maintained. Each tool comes with its own reporting format, preventing an easy integration of multiple analysis tools in a single interface, such as the Static Analysis Server Protocol (SASP). In 2017, a collaborative effort in industry, including Microsoft and GrammaTech, has proposed the Static Analysis Results Interchange Format (SARIF) to address this issue. SARIF is a standardized format in which static analysis warnings can be encoded, to allow the import and export of analysis reports between different tools. Purpose - This paper explains the SARIF format through examples and presents a proof of concept of the connector that allows the static analysis tool CogniCrypt to generate and export its results in SARIF format. Design/Approach - We conduct a cross-sectional study between the SARIF format and CogniCrypt's output format before detailing the implementation of the connector. The study aims to find the components of interest in CogniCrypt that the SARIF export module can complete. Originality/Value - The integration of SARIF into CogniCrypt described in this paper can be reused to integrate SARIF into other static analysis tools. Conclusion - After detailing the SARIF format, we present an initial implementation to integrate SARIF into CogniCrypt. After taking advantage of all the features provided by SARIF, CogniCrypt will be able to support SASP.
Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous
Venue: arXiv cs.FL 2019
Year: 2019

We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called Synchronized Dynamic Pushdown Networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is unfortunately undecidable. Therefore, we tackle this problem by introducing an abstraction framework based on Kleene algebras in order to compute an abstraction of the execution paths between two regular sets of configurations. We combine an automata theoretic saturation procedure with constraint solving in a finite domain. We then apply this framework to an iterative abstraction refinement scheme, using multiple abstractions of increasing complexity and precision.
From LCF to Isabelle/HOL
Venue: arXiv cs.LO 2019
Year: 2019

Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing techniques from the world of first order theorem proving, but also the automatic search for counterexamples. They include a highly readable structured language of proofs and a unique interactive development environment for editing live proof documents. Everything rests on the foundation conceived by Robin Milner for Edinburgh LCF: a proof kernel, using abstract types to ensure soundness and eliminate the need to store proofs. Compared with the research prototypes of the 1970s, Isabelle is a practical and versatile tool. It is used by system designers, mathematicians and many others.
NeuType: A Simple and Effective Neural Network Approach for Predicting Missing Entity Type Information in Knowledge Bases
Venue: arXiv cs.IR 2019
Year: 2019

Knowledge bases store information about the semantic types of entities, which can be utilized in a range of information access tasks. This information, however, is often incomplete, due to new entities emerging on a daily basis. We address the task of automatically assigning types to entities in a knowledge base from a type taxonomy. Specifically, we present two neural network architectures, which take short entity descriptions and, optionally, information about related entities as input. Using the DBpedia knowledge base for experimental evaluation, we demonstrate that these simple architectures yield significant improvements over the current state of the art.
Gaussian Processes for Analyzing Positioned Trajectories in Sports
Venue: arXiv cs.LG 2019
Year: 2019

Kernel-based machine learning approaches are gaining increasing interest for exploring and modeling large dataset in recent years. Gaussian process (GP) is one example of such kernel-based approaches, which can provide very good performance for nonlinear modeling problems. In this work, we first propose a grey-box modeling approach to analyze the forces in cross country skiing races. To be more precise, a disciplined set of kinetic motion model formulae is combined with data-driven Gaussian process regression model, which accounts for everything unknown in the system. Then, a modeling approach is proposed to analyze the kinetic flow of both individual and clusters of skiers. The proposed approaches can be generally applied to use cases where positioned trajectories and kinetic measurements are available. The proposed approaches are evaluated using data collected from the Falun Nordic World Ski Championships 2015, in particular the Men's cross country $4\times10$ km relay. Forces during the cross country skiing races are analyzed and compared. Velocity models for skiers at different competition stages are also evaluated. Finally, the comparisons between the grey-box and black-box approach are carried out, where the grey-box approach can reduce the predictive uncertainty by $30\%$ to $40\%$.
Oblivious Location-Based Service Query
Venue: arXiv cs.CR 2019
Year: 2019

Privacy-preserving location-base services (LBS) have been proposed to protect users' location privacy. However, there are still some problems in existing schemes: (1) a semi-trusted third party (TTP) is required; or (2) both the computation cost and communication cost to generate a query are linear in the size of the queried area. In this paper, to improve query efficiency, an oblivious location-based service query (OLBSQ) scheme is proposed. Our scheme captures the following features: (1) a semi-trusted TTP is not required; (2) a user can query services from a service provider without revealing her exact location; (3) the service provider can only know the size of a query made by a user; and (4) both the computation cost and the communication cost to generate a query is constant, instead of linear in the size of the queried area. We formalise the definition and security model of OLBSQ schemes. The security of our scheme is reduced to well-known complexity assumptions. The novelty is to reduce the computation cost and communication cost of making a query and enable the service provider to obliviously and incrementally generate decrypt keys for queried services. This contributes to the growing work of formalising privacy-preserving LBS schemes and improving query efficiency.
Exploiting Out-of-Domain Parallel Data through Multilingual Transfer Learning for Low-Resource Neural Machine Translation
Venue: arXiv cs.CL 2019
Year: 2019

This paper proposes a novel multilingual multistage fine-tuning approach for low-resource neural machine translation (NMT), taking a challenging Japanese--Russian pair for benchmarking. Although there are many solutions for low-resource scenarios, such as multilingual NMT and back-translation, we have empirically confirmed their limited success when restricted to in-domain data. We therefore propose to exploit out-of-domain data through transfer learning, by using it to first train a multilingual NMT model followed by multistage fine-tuning on in-domain parallel and back-translated pseudo-parallel data. Our approach, which combines domain adaptation, multilingualism, and back-translation, helps improve the translation quality by more than 3.7 BLEU points, over a strong baseline, for this extremely low-resource scenario.
Adaptive Neuro-Surrogate-Based Optimisation Method for Wave Energy Converters Placement Optimisation
Venue: arXiv cs.NE 2019
Year: 2019

The installed amount of renewable energy has expanded massively in recent years. Wave energy, with its high capacity factors has great potential to complement established sources of solar and wind energy. This study explores the problem of optimising the layout of advanced, three-tether wave energy converters in a size-constrained farm in a numerically modelled ocean environment. Simulating and computing the complicated hydrodynamic interactions in wave farms can be computationally costly, which limits optimisation methods to have just a few thousand evaluations. For dealing with this expensive optimisation problem, an adaptive neuro-surrogate optimisation (ANSO) method is proposed that consists of a surrogate Recurrent Neural Network (RNN) model trained with a very limited number of observations. This model is coupled with a fast meta-heuristic optimiser for adjusting the model's hyper-parameters. The trained model is applied using a greedy local search with a backtracking optimisation strategy. For evaluating the performance of the proposed approach, some of the more popular and successful Evolutionary Algorithms (EAs) are compared in four real wave scenarios (Sydney, Perth, Adelaide and Tasmania). Experimental results show that the adaptive neuro model is competitive with other optimisation methods in terms of total harnessed power output and faster in terms of total computational costs.
Generative Counterfactual Introspection for Explainable Deep Learning
Venue: arXiv cs.LG 2019
Year: 2019

In this work, we propose an introspection technique for deep neural networks that relies on a generative model to instigate salient editing of the input image for model interpretation. Such modification provides the fundamental interventional operation that allows us to obtain answers to counterfactual inquiries, i.e., what meaningful change can be made to the input image in order to alter the prediction. We demonstrate how to reveal interesting properties of the given classifiers by utilizing the proposed introspection approach on both the MNIST and the CelebA dataset.
Constraint-Based Type-Directed Program Synthesis
Venue: arXiv cs.PL 2019
Year: 2019

We explore an approach to type-directed program synthesis rooted in constraint-based type inference techniques. By doing this, we aim to more efficiently synthesize polymorphic code while also tackling advanced typing features such as GADTs that build upon polymorphism. Along the way, we also present an implementation of these techniques in Scythe, a prototype live, type-directed programming tool for the Haskell programming language and reflect on our initial experience with the tool.
Constant-Factor Approximation Algorithms for Parity-Constrained Facility Location Problems
Venue: arXiv cs.DS 2019
Year: 2019

Facility location is a prominent optimization problem that has inspired a large quantity of both theoretical and practical studies in combinatorial optimization. Although the problem has been investigated under various settings reflecting typical structures within the optimization problems of practical interest, little is known on how the problem behaves in conjunction with parity constraints. This shortfall of understanding was rather disturbing when we consider the central role of parity in the field of combinatorics. In this paper, we present the first constant-factor approximation algorithm for the facility location problem with parity constraints. We are given as the input a metric on a set of facilities and clients, the opening cost of each facility, and the parity requirement--odd, even, or unconstrained--of every facility in this problem. The objective is to open a subset of facilities and assign every client to an open facility so as to minimize the sum of the total opening costs and the assignment distances, but subject to the condition that the number of clients assigned to each open facility must have the same parity as its requirement. Although the unconstrained facility location problem as a relaxation for this parity-constrained generalization has unbounded gap, we demonstrate that it yields a structured solution whose parity violation can be corrected at small cost. This correction is prescribed by a T-join on an auxiliary graph constructed by the algorithm. This graph does not satisfy the triangle inequality, but we show that a carefully chosen set of shortcutting operations leads to a cheap and sparse T-join. Finally, we bound the correction cost by exhibiting a combinatorial multi-step construction of an upper bound. We also present the first constant-factor approximation algorithm for the parity-constrained k-center problem, the bottleneck optimization variant.
AutoCompress: An Automatic DNN Structured Pruning Framework for Ultra-High Compression Rates
Venue: arXiv cs.LG 2019
Year: 2019

Structured weight pruning is a representative model compression technique of DNNs to reduce the storage and computation requirements and accelerate inference. An automatic hyperparameter determination process is necessary due to the large number of flexible hyperparameters. This work proposes AutoCompress, an automatic structured pruning framework with the following key performance improvements: (i) effectively incorporate the combination of structured pruning schemes in the automatic process; (ii) adopt the state-of-art ADMM-based structured weight pruning as the core algorithm, and propose an innovative additional purification step for further weight reduction without accuracy loss; and (iii) develop effective heuristic search method enhanced by experience-based guided search, replacing the prior deep reinforcement learning technique which has underlying incompatibility with the target pruning problem. Extensive experiments on CIFAR-10 and ImageNet datasets demonstrate that AutoCompress is the key to achieve ultra-high pruning rates on the number of weights and FLOPs that cannot be achieved before. As an example, AutoCompress outperforms the prior work on automatic model compression by up to 33x in pruning rate (120x reduction in the actual parameter count) under the same accuracy. Significant inference speedup has been observed from the AutoCompress framework on actual measurements on smartphone. We release all models of this work at anonymous link: http://bit.ly/2VZ63dS.
Intelligent Systems Design for Malware Classification Under Adversarial Conditions
Venue: arXiv cs.LG 2019
Year: 2019

The use of machine learning and intelligent systems has become an established practice in the realm of malware detection and cyber threat prevention. In an environment characterized by widespread accessibility and big data, the feasibility of malware classification without the use of artificial intelligence-based techniques has been diminished exponentially. Also characteristic of the contemporary realm of automated, intelligent malware detection is the threat of adversarial machine learning. Adversaries are looking to target the underlying data and/or algorithm responsible for the functionality of malware classification to map its behavior or corrupt its functionality. The ends of such adversaries are bypassing the cyber security measures and increasing malware effectiveness. The focus of this research is the design of an intelligent systems approach using machine learning that can accurately and robustly classify malware under adversarial conditions. Such an outcome ultimately relies on increased flexibility and adaptability to build a model robust enough to identify attacks on the underlying algorithm.
Unsupervised cycle-consistent deformation for shape matching
Venue: arXiv cs.CV 2019
Year: 2019

We propose a self-supervised approach to deep surface deformation. Given a pair of shapes, our algorithm directly predicts a parametric transformation from one shape to the other respecting correspondences. Our insight is to use cycle-consistency to define a notion of good correspondences in groups of objects and use it as a supervisory signal to train our network. Our method does not rely on a template, assume near isometric deformations or rely on point-correspondence supervision. We demonstrate the efficacy of our approach by using it to transfer segmentation across shapes. We show, on Shapenet, that our approach is competitive with comparable state-of-the-art methods when annotated training data is readily available, but outperforms them by a large margin in the few-shot segmentation scenario.
Exploring difference in public perceptions on HPV vaccine between gender groups from Twitter using deep learning
Venue: arXiv cs.CL 2019
Year: 2019

In this study, we proposed a convolutional neural network model for gender prediction using English Twitter text as input. Ensemble of proposed model achieved an accuracy at 0.8237 on gender prediction and compared favorably with the state-of-the-art performance in a recent author profiling task. We further leveraged the trained models to predict the gender labels from an HPV vaccine related corpus and identified gender difference in public perceptions regarding HPV vaccine. The findings are largely consistent with previous survey-based studies.
I Am Not What I Write: Privacy Preserving Text Representation Learning
Venue: arXiv cs.CR 2019
Year: 2019

Online users generate tremendous amounts of textual information by participating in different activities, such as writing reviews and sharing tweets. This textual data provides opportunities for researchers and business partners to study and understand individuals. However, this user-generated textual data not only can reveal the identity of the user but also may contain individual's private information (e.g., age, location, gender). Hence, "you are what you write" as the saying goes. Publishing the textual data thus compromises the privacy of individuals who provided it. The need arises for data publishers to protect people's privacy by anonymizing the data before publishing it. It is challenging to design effective anonymization techniques for textual information which minimizes the chances of re-identification and does not contain users' sensitive information (high privacy) while retaining the semantic meaning of the data for given tasks (high utility). In this paper, we study this problem and propose a novel double privacy preserving text representation learning framework, DPText, which learns a textual representation that (1) is differentially private, (2) does not contain private information and (3) retains high utility for the given task. Evaluating on two natural language processing tasks, i.e., sentiment analysis and part of speech tagging, we show the effectiveness of this approach in terms of preserving both privacy and utility.
Oracle Separations Between Quantum and Non-interactive Zero-Knowledge Classes
Venue: arXiv cs.CC 2019
Year: 2019

We study the relationship between problems solvable by quantum algorithms in polynomial time and those for which zero-knowledge proofs exist. In prior work, Aaronson [arxiv:quant-ph/0111102] showed an oracle separation between BQP and SZK, i.e. an oracle $A$ such that $\mathrm{SZK}^A \not\subseteq \mathrm{BQP}^A$. In this paper we give a simple extension of Aaronson's result to non-interactive zero-knowledge proofs with perfect security. This class, NIPZK, is the most restrictive zero-knowledge class. We show that even for this class we can construct an $A$ with $\mathrm{NIPZK}^A \not\subseteq \mathrm{BQP}^A$.
Zero-Shot Open Entity Typing as Type-Compatible Grounding
Venue: arXiv cs.CL 2019
Year: 2019

The problem of entity-typing has been studied predominantly in supervised learning fashion, mostly with task-specific annotations (for coarse types) and sometimes with distant supervision (for fine types). While such approaches have strong performance within datasets, they often lack the flexibility to transfer across text genres and to generalize to new type taxonomies. In this work we propose a zero-shot entity typing approach that requires no annotated data and can flexibly identify newly defined types. Given a type taxonomy defined as Boolean functions of FREEBASE "types", we ground a given mention to a set of type-compatible Wikipedia entries and then infer the target mention's types using an inference algorithm that makes use of the types of these entries. We evaluate our system on a broad range of datasets, including standard fine-grained and coarse-grained entity typing datasets, and also a dataset in the biological domain. Our system is shown to be competitive with state-of-the-art supervised NER systems and outperforms them on out-of-domain datasets. We also show that our system significantly outperforms other zero-shot fine typing systems.
ASCNet: Adaptive-Scale Convolutional Neural Networks for Multi-Scale Feature Learning
Venue: arXiv cs.CV 2019
Year: 2019

Extracting multi-scale information is key to semantic segmentation. However, the classic convolutional neural networks (CNNs) encounter difficulties in achieving multi-scale information extraction: expanding convolutional kernel incurs the high computational cost and using maximum pooling sacrifices image information. The recently developed dilated convolution solves these problems, but with the limitation that the dilation rates are fixed and therefore the receptive field cannot fit for all objects with different sizes in the image. We propose an adaptivescale convolutional neural network (ASCNet), which introduces a 3-layer convolution structure in the end-to-end training, to adaptively learn an appropriate dilation rate for each pixel in the image. Such pixel-level dilation rates produce optimal receptive fields so that the information of objects with different sizes can be extracted at the corresponding scale. We compare the segmentation results using the classic CNN, the dilated CNN and the proposed ASCNet on two types of medical images (The Herlev dataset and SCD RBC dataset). The experimental results show that ASCNet achieves the highest accuracy. Moreover, the automatically generated dilation rates are positively correlated to the sizes of the objects, confirming the effectiveness of the proposed method.
Resource-Efficient Computing in Wearable Systems
Venue: arXiv cs.LG 2019
Year: 2019

We propose two optimization techniques to minimize memory usage and computation while meeting system timing constraints for real-time classification in wearable systems. Our method derives a hierarchical classifier structure for Support Vector Machine (SVM) in order to reduce the amount of computations, based on the probability distribution of output classes occurrences. Also, we propose a memory optimization technique based on SVM parameters, which results in storing fewer support vectors and as a result requiring less memory. To demonstrate the efficiency of our proposed techniques, we performed an activity recognition experiment and were able to save up to 35% and 56% in memory storage when classifying 14 and 6 different activities, respectively. In addition, we demonstrated that there is a trade-off between accuracy of classification and memory savings, which can be controlled based on application requirements.