OpenRaiser/Intern-Atlas huggingface dataset:
A Constructor-Based Reachability Logic for Rewrite Theories
Venue: arXiv cs.PL 2017
Year: 2017

Reachability logic has been applied to $\mathbb{K}$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic's automation is increased by means of constructor-based semantic unification, matching, and satisfiability procedures. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.
Data-driven Job Search Engine Using Skills and Company Attribute Filters
Venue: arXiv cs.IR 2017
Year: 2017

According to a report online, more than 200 million unique users search for jobs online every month. This incredibly large and fast growing demand has enticed software giants such as Google and Facebook to enter this space, which was previously dominated by companies such as LinkedIn, Indeed and CareerBuilder. Recently, Google released their "AI-powered Jobs Search Engine", "Google For Jobs" while Facebook released "Facebook Jobs" within their platform. These current job search engines and platforms allow users to search for jobs based on general narrow filters such as job title, date posted, experience level, company and salary. However, they have severely limited filters relating to skill sets such as C++, Python, and Java and company related attributes such as employee size, revenue, technographics and micro-industries. These specialized filters can help applicants and companies connect at a very personalized, relevant and deeper level. In this paper we present a framework that provides an end-to-end "Data-driven Jobs Search Engine". In addition, users can also receive potential contacts of recruiters and senior positions for connection and networking opportunities. The high level implementation of the framework is described as follows: 1) Collect job postings data in the United States, 2) Extract meaningful tokens from the postings data using ETL pipelines, 3) Normalize the data set to link company names to their specific company websites, 4) Extract and ranking the skill sets, 5) Link the company names and websites to their respective company level attributes with the EVERSTRING Company API, 6) Run user-specific search queries on the database to identify relevant job postings and 7) Rank the job search results. This framework offers a highly customizable and highly targeted search experience for end users.
Accelerating SGD for Distributed Deep-Learning Using Approximated Hessian Matrix
Venue: arXiv cs.LG 2017
Year: 2017

We introduce a novel method to compute a rank $m$ approximation of the inverse of the Hessian matrix in the distributed regime. By leveraging the differences in gradients and parameters of multiple Workers, we are able to efficiently implement a distributed approximation of the Newton-Raphson method. We also present preliminary results which underline advantages and challenges of second-order methods for large stochastic optimization problems. In particular, our work suggests that novel strategies for combining gradients provide further information on the loss surface.
Unsupervised Aspect Term Extraction with B-LSTM & CRF using Automatically Labelled Datasets
Venue: arXiv cs.CL 2017
Year: 2017

Aspect Term Extraction (ATE) identifies opinionated aspect terms in texts and is one of the tasks in the SemEval Aspect Based Sentiment Analysis (ABSA) contest. The small amount of available datasets for supervised ATE and the costly human annotation for aspect term labelling give rise to the need for unsupervised ATE. In this paper, we introduce an architecture that achieves top-ranking performance for supervised ATE. Moreover, it can be used efficiently as feature extractor and classifier for unsupervised ATE. Our second contribution is a method to automatically construct datasets for ATE. We train a classifier on our automatically labelled datasets and evaluate it on the human annotated SemEval ABSA test sets. Compared to a strong rule-based baseline, we obtain a dramatically higher F-score and attain precision values above 80%. Our unsupervised method beats the supervised ABSA baseline from SemEval, while preserving high precision scores.
Distributed Random Process for a Large-Scale Peer-to-Peer Lottery
Venue: arXiv cs.DC 2017
Year: 2017

Most online lotteries today fail to ensure the verifiability of the random process and rely on a trusted third party. This issue has received little attention since the emergence of distributed protocols like Bitcoin that demonstrated the potential of protocols with no trusted third party. We argue that the security requirements of online lotteries are similar to those of online voting, and propose a novel distributed online lottery protocol that applies techniques developed for voting applications to an existing lottery protocol. As a result, the protocol is scalable, provides efficient verification of the random process and does not rely on a trusted third party nor on assumptions of bounded computational resources. An early prototype confirms the feasibility of our approach.
Optimal Base Station Design with Limited Fronthaul: Massive Bandwidth or Massive MIMO?
Venue: arXiv cs.IT 2017
Year: 2017

To reach a cost-efficient 5G architecture, the use of remote radio heads connected through a fronthaul to baseband controllers is a promising solution. However, the fronthaul links must support high bit rates as 5G networks are projected to use wide bandwidths and many antennas. Upgrading all of the existing fronthaul connections would be cumbersome, while replacing the remote radio head and upgrading the software in the baseband controllers is relatively simple. In this paper, we consider the uplink and seek the answer to the question: If we have a fixed fronthaul capacity and can deploy any technology in the remote radio head, what is the optimal technology? In particular, we optimize the number of antennas, quantization bits and bandwidth to maximize the sum rate under a fronthaul capacity constraint. The analytical results suggest that operating with many antennas equipped with low-resolution analog-to-digital converters, while the interplay between number of antennas and bandwidth depends on various parameters. The numerical analysis provides further insights into the design of communication systems with limited fronthaul capacity.
LSTM Fully Convolutional Networks for Time Series Classification
Venue: arXiv cs.LG 2017
Year: 2017

Fully convolutional neural networks (FCN) have been shown to achieve state-of-the-art performance on the task of classifying time series sequences. We propose the augmentation of fully convolutional networks with long short term memory recurrent neural network (LSTM RNN) sub-modules for time series classification. Our proposed models significantly enhance the performance of fully convolutional networks with a nominal increase in model size and require minimal preprocessing of the dataset. The proposed Long Short Term Memory Fully Convolutional Network (LSTM-FCN) achieves state-of-the-art performance compared to others. We also explore the usage of attention mechanism to improve time series classification with the Attention Long Short Term Memory Fully Convolutional Network (ALSTM-FCN). Utilization of the attention mechanism allows one to visualize the decision process of the LSTM cell. Furthermore, we propose fine-tuning as a method to enhance the performance of trained models. An overall analysis of the performance of our model is provided and compared to other techniques.
3D Placement of an Unmanned Aerial Vehicle Base Station for Maximum Coverage of Users with Different QoS Requirements
Venue: arXiv cs.IT 2017
Year: 2017

The need for a rapid-to-deploy solution for providing wireless cellular services can be realized by unmanned aerial vehicle base stations (UAV-BSs). To the best of our knowledge, this letter is the first in literature that studies a novel 3D UAV-BS placement that maximizes the number of covered users with different Quality-of-Service requirements. We model the placement problem as a multiple circles placement problem and propose an optimal placement algorithm that utilizes an exhaustive search (ES) over a one-dimensional parameter in a closed region. We also propose a low-complexity algorithm, namely, maximal weighted area (MWA) algorithm to tackle the placement problem. Numerical simulations are presented showing that the MWA algorithm performs very close to the ES algorithm with a significant complexity reduction.
Cooperative Motion Planning for Non-Holonomic Agents with Value Iteration Networks
Venue: arXiv cs.RO 2017
Year: 2017

Cooperative motion planning is still a challenging task for robots. Recently, Value Iteration Networks (VINs) were proposed to model motion planning tasks as Neural Networks. In this work, we extend VINs to solve cooperative planning tasks under non-holonomic constraints. For this, we interconnect multiple VINs to pay respect to each other's outputs. Policies for cooperation are generated via iterative gradient descend. Validation in simulation shows that the resulting networks can resolve non-holonomic motion planning problems that require cooperation.
Algorithms and Architecture for Real-time Recommendations at News UK
Venue: arXiv cs.IR 2017
Year: 2017

Recommendation systems are recognised as being hugely important in industry, and the area is now well understood. At News UK, there is a requirement to be able to quickly generate recommendations for users on news items as they are published. However, little has been published about systems that can generate recommendations in response to changes in recommendable items and user behaviour in a very short space of time. In this paper we describe a new algorithm for updating collaborative filtering models incrementally, and demonstrate its effectiveness on clickstream data from The Times. We also describe the architecture that allows recommendations to be generated on the fly, and how we have made each component scalable. The system is currently being used in production at News UK.
Forensics Analysis of Android Mobile VoIP Apps
Venue: arXiv cs.CR 2017
Year: 2017

Voice over Internet Protocol (VoIP) applications (apps) provide convenient and low cost means for users to communicate and share information with each other in real-time. Day by day, the popularity of such apps is increasing, and people produce and share a huge amount of data, including their personal and sensitive information. This might lead to several privacy issues, such as revealing user contacts, private messages or personal photos. Therefore, having an up-to-date forensic understanding of these apps is necessary. This chapter presents analysis of forensically valuable remnants of three popular Mobile VoIP (mVoIP) apps on Google Play store, namely: Viber, Skype, and WhatsApp Messenger, in order to figure out to what extent these apps reveal forensically valuable information about the users activities. We performed a thorough investigative study of these three mVoIP apps on smartphone devices. Our experimental results show that several artefacts, such as messages, contact details, phone numbers, images, and video files, are recoverable from the smartphone device that is equipped with these mVoIP apps.
A Two-Phase Power Allocation Scheme for CRNs Employing NOMA
Venue: arXiv cs.IT 2017
Year: 2017

In this paper, we consider the power allocation (PA) problem in cognitive radio networks (CRNs) employing nonorthogonal multiple access (NOMA) technique. Specifically, we aim to maximize the number of admitted secondary users (SUs) and their throughput, without violating the interference tolerance threshold of the primary users (PUs). This problem is divided into a two-phase PA process: a) maximizing the number of admitted SUs; b) maximizing the minimum throughput among the admitted SUs. To address the first phase, we apply a sequential and iterative PA algorithm, which fully exploits the characteristics of the NOMA-based system. Following this, the second phase is shown to be quasiconvex and is optimally solved via the bisection method. Furthermore, we prove the existence of a unique solution for the second phase and propose another PA algorithm, which is also optimal and significantly reduces the complexity in contrast with the bisection method. Simulation results verify the effectiveness of the proposed two-phase PA scheme.
String Attractors
Venue: arXiv cs.DS 2017
Year: 2017

Let $S$ be a string of length $n$. In this paper we introduce the notion of \emph{string attractor}: a subset of the string's positions $[1,n]$ such that every distinct substring of $S$ has an occurrence crossing one of the attractor's elements. We first show that the minimum attractor's size yields upper-bounds to the string's repetitiveness as measured by its linguistic complexity and by the length of its longest repeated substring. We then prove that all known compressors for repetitive strings induce a string attractor whose size is bounded by their associated repetitiveness measure, and can therefore be considered as approximations of the smallest one. Using further reductions, we derive the approximation ratios of these compressors with respect to the smallest attractor and solve several open problems related to the asymptotic relations between repetitiveness measures (in particular, between the the sizes of the Lempel-Ziv factorization, the run-length Burrows-Wheeler transform, the smallest grammar, and the smallest macro scheme). These reductions directly provide approximation algorithms for the smallest string attractor. We then apply string attractors to solve efficiently a fundamental problem in the field of compressed computation: we present a universal compressed data structure for text extraction that improves existing strategies simultaneously for \emph{all} known dictionary compressors and that, by recent lower bounds, almost matches the optimal running time within the resulting space. To conclude, we consider generalizations of string attractors to labeled graphs, show that the attractor problem is NP-complete on trees, and provide a logarithmic approximation computable in polynomial time.
LoIDE: a web-based IDE for Logic Programming - Preliminary Technical Report
Venue: arXiv cs.SE 2017
Year: 2017

Logic-based paradigms are nowadays widely used in many different fields, also thank to the availability of robust tools and systems that allow the development of real-world and industrial applications. In this work we present LoIDE, an advanced and modular web-editor for logic-based languages that also integrates with state-of-the-art solvers.
Synthesizing Coupling Proofs of Differential Privacy
Venue: arXiv cs.PL 2017
Year: 2017

Differential privacy has emerged as a promising probabilistic formulation of privacy, generating intense interest within academia and industry. We present a push-button, automated technique for verifying $\varepsilon$-differential privacy of sophisticated randomized algorithms. We make several conceptual, algorithmic, and practical contributions: (i) Inspired by the recent advances on approximate couplings and randomness alignment, we present a new proof technique called coupling strategies, which casts differential privacy proofs as a winning strategy in a game where we have finite privacy resources to expend. (ii) To discover a winning strategy, we present a constraint-based formulation of the problem as a set of Horn modulo couplings (HMC) constraints, a novel combination of first-order Horn clauses and probabilistic constraints. (iii) We present a technique for solving HMC constraints by transforming probabilistic constraints into logical constraints with uninterpreted functions. (iv) Finally, we implement our technique in the FairSquare verifier and provide the first automated privacy proofs for a number of challenging algorithms from the differential privacy literature, including Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism.
Tortoise: Interactive System Configuration Repair
Venue: arXiv cs.SE 2017
Year: 2017

System configuration languages provide powerful abstractions that simplify managing large-scale, networked systems. Thousands of organizations now use configuration languages, such as Puppet. However, specifications written in configuration languages can have bugs and the shell remains the simplest way to debug a misconfigured system. Unfortunately, it is unsafe to use the shell to fix problems when a system configuration language is in use: a fix applied from the shell may cause the system to drift from the state specified by the configuration language. Thus, despite their advantages, configuration languages force system administrators to give up the simplicity and familiarity of the shell. This paper presents a synthesis-based technique that allows administrators to use configuration languages and the shell in harmony. Administrators can fix errors using the shell and the technique automatically repairs the higher-level specification written in the configuration language. The approach (1) produces repairs that are consistent with the fix made using the shell; (2) produces repairs that are maintainable by minimizing edits made to the original specification; (3) ranks and presents multiple repairs when relevant; and (4) supports all shells the administrator may wish to use. We implement our technique for Puppet, a widely used system configuration language, and evaluate it on a suite of benchmarks under 42 repair scenarios. The top-ranked repair is selected by humans 76% of the time and the human-equivalent repair is ranked 1.31 on average.
A Rule-Based Approach to Analyzing Database Schema Objects with Datalog
Venue: arXiv cs.PL 2017
Year: 2017

Database schema elements such as tables, views, triggers and functions are typically defined with many interrelationships. In order to support database users in understanding a given schema, a rule-based approach for analyzing the respective dependencies is proposed using Datalog expressions. We show that many interesting properties of schema elements can be systematically determined this way. The expressiveness of the proposed analysis is exemplarily shown with the problem of computing induced functional dependencies for derived relations. The propagation of functional dependencies plays an important role in data integration and query optimization but represents an undecidable problem in general. And yet, our rule-based analysis covers all relational operators as well as linear recursive expressions in a systematic way showing the depth of analysis possible by our proposal. The analysis of functional dependencies is well-integrated in a uniform approach to analyzing dependencies between schema elements in general.
Dynamic Mobile Edge Caching with Location Differentiation
Venue: arXiv cs.NI 2017
Year: 2017

Mobile edge caching enables content delivery directly within the radio access network, which effectively alleviates the backhaul burden and reduces round-trip latency. To fully exploit the edge resources, the most popular contents should be identified and cached. Observing that content popularity varies greatly at different locations, to maximize local hit rate, this paper proposes an online learning algorithm that dynamically predicts content hit rate, and makes location-differentiated caching decisions. Specifically, a linear model is used to estimate the future hit rate. Considering the variations in user demand, a perturbation is added to the estimation to account for uncertainty. The proposed learning algorithm requires no training phase, and hence is adaptive to the time-varying content popularity profile. Theoretical analysis indicates that the proposed algorithm asymptotically approaches the optimal policy in the long term. Extensive simulations based on real world traces show that, the proposed algorithm achieves higher hit rate and better adaptiveness to content popularity fluctuation, compared with other schemes.
Road Friction Estimation for Connected Vehicles using Supervised Machine Learning
Venue: arXiv cs.LG 2017
Year: 2017

In this paper, the problem of road friction prediction from a fleet of connected vehicles is investigated. A framework is proposed to predict the road friction level using both historical friction data from the connected cars and data from weather stations, and comparative results from different methods are presented. The problem is formulated as a classification task where the available data is used to train three machine learning models including logistic regression, support vector machine, and neural networks to predict the friction class (slippery or non-slippery) in the future for specific road segments. In addition to the friction values, which are measured by moving vehicles, additional parameters such as humidity, temperature, and rainfall are used to obtain a set of descriptive feature vectors as input to the classification methods. The proposed prediction models are evaluated for different prediction horizons (0 to 120 minutes in the future) where the evaluation shows that the neural networks method leads to more stable results in different conditions.
Zero-Shot Learning to Manage a Large Number of Place-Specific Compressive Change Classifiers
Venue: arXiv cs.CV 2017
Year: 2017

With recent progress in large-scale map maintenance and long-term map learning, the task of change detection on a large-scale map from a visual image captured by a mobile robot has become a problem of increasing criticality. Previous approaches for change detection are typically based on image differencing and require the memorization of a prohibitively large number of mapped images in the above context. In contrast, this study follows the recent, efficient paradigm of change-classifier-learning and specifically employs a collection of place-specific change classifiers. Our change-classifier-learning algorithm is based on zero-shot learning (ZSL) and represents a place-specific change classifier by its training examples mined from an external knowledge base (EKB). The proposed algorithm exhibits several advantages. First, we are required to memorize only training examples (rather than the classifier itself), which can be further compressed in the form of bag-of-words (BoW). Secondly, we can incorporate the most recent map into the classifiers by straightforwardly adding or deleting a few training examples that correspond to these classifiers. Thirdly, we can share the BoW vocabulary with other related task scenarios (e.g., BoW-based self-localization), wherein the vocabulary is generally designed as a rich, continuously growing, and domain-adaptive knowledge base. In our contribution, the proposed algorithm is applied and evaluated on a practical long-term cross-season change detection system that consists of a large number of place-specific object-level change classifiers.
Commutativity and Commutative Pairs of Some Differential Equations
Venue: arXiv cs.SY 2017
Year: 2017

In this study, explicit differential equations representing commutative pairs of some well-known second-order linear time-varying systems have been derived. The commutativity of these systems are investigated by considering 30 second-order linear differential equations with variable coefficients. It is shown that the system modeled by each one of these equations has a commutative pair with (or without) some conditions or not. There appear special cases such that both, only one or neither of the original system and its commutative pair has explicit analytic solution. Some benefits of commutativity have already been mentioned in the literature but a new application for in cryptology for obscuring transmitted signals in telecommunication is illustrated in this paper.