OpenRaiser/Intern-Atlas huggingface dataset:
Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)
Venue: arXiv cs.SE 2018
Year: 2018

With the advancement of software engineering in recent years, the model checking techniques are widely applied in various areas to do the verification for the system model. However, it is difficult to apply the model checking to verify requirements due to lacking the details of the design. Unlike other model checking tools, LTSA provides the structure diagram, which can bridge the gap between the requirements and the design. In this paper, we demonstrate the abilities of LTSA shipped with the classic case study of the steam boiler system. The structure diagram of LTSA can specify the interactions between the controller and the steam boiler, which can be derived from UML requirements model such as system sequence diagram of the steam boiler system. The start-up design model of LTSA can be generated from the structure diagram. Furthermore, we provide a variation law of the steam rate to avoid the issue of state space explosion and show how explicitly and implicitly model the time that reflects the difference between system modeling and the physical world. Finally, the derived model is verified against the required properties. Our work demonstrates the potential power of integrating UML with model checking tools in requirement elicitation, system design, and verification.
Distributed Random Number Generation for the Needs of Public Governance
Venue: arXiv cs.CR 2018
Year: 2018

We propose distributed protocol for generation of random numbers via computer systems. The protocol is specifically designed to fit the needs of random selection as it is performed in public sphere and is inspired by real problems, which are posing difficulties for Bulgarian judicial system. Random selection in public sphere is meant to be mechanism for increasing the transparency and reducing the possibilities of collusion between various government actors. Usage of computers reduces transparency and when done improperly, can lead to disastrous consequences concerning the public trust in the institutions of government. This protocol tries to provide technical solution to the transparency problem by allowing third parties to guarantee for the fairness of the random selection without giving these parties the ability to influence maliciously the result.
Imitation Learning with Concurrent Actions in 3D Games
Venue: arXiv cs.AI 2018
Year: 2018

In this work we describe a novel deep reinforcement learning architecture that allows multiple actions to be selected at every time-step in an efficient manner. Multi-action policies allow complex behaviours to be learnt that would otherwise be hard to achieve when using single action selection techniques. We use both imitation learning and temporal difference (TD) reinforcement learning (RL) to provide a 4x improvement in training time and 2.5x improvement in performance over single action selection TD RL. We demonstrate the capabilities of this network using a complex in-house 3D game. Mimicking the behavior of the expert teacher significantly improves world state exploration and allows the agents vision system to be trained more rapidly than TD RL alone. This initial training technique kick-starts TD learning and the agent quickly learns to surpass the capabilities of the expert.
Think you have Solved Question Answering? Try ARC, the AI2 Reasoning Challenge
Venue: arXiv cs.AI 2018
Year: 2018

We present a new question set, text corpus, and baselines assembled to encourage AI research in advanced question answering. Together, these constitute the AI2 Reasoning Challenge (ARC), which requires far more powerful knowledge and reasoning than previous challenges such as SQuAD or SNLI. The ARC question set is partitioned into a Challenge Set and an Easy Set, where the Challenge Set contains only questions answered incorrectly by both a retrieval-based algorithm and a word co-occurence algorithm. The dataset contains only natural, grade-school science questions (authored for human tests), and is the largest public-domain set of this kind (7,787 questions). We test several baselines on the Challenge Set, including leading neural models from the SQuAD and SNLI tasks, and find that none are able to significantly outperform a random baseline, reflecting the difficult nature of this task. We are also releasing the ARC Corpus, a corpus of 14M science sentences relevant to the task, and implementations of the three neural baseline models tested. Can your model perform better? We pose ARC as a challenge to the community.
Computer-aided diagnosis of lung carcinoma using deep learning - a pilot study
Venue: arXiv cs.CV 2018
Year: 2018

Aim: Early detection and correct diagnosis of lung cancer are the most important steps in improving patient outcome. This study aims to assess which deep learning models perform best in lung cancer diagnosis. Methods: Non-small cell lung carcinoma and small cell lung carcinoma biopsy specimens were consecutively obtained and stained. The specimen slides were diagnosed by two experienced pathologists (over 20 years). Several deep learning models were trained to discriminate cancer and non-cancer biopsies. Result: Deep learning models give reasonable AUC from 0.8810 to 0.9119. Conclusion: The deep learning analysis could help to speed up the detection process for the whole-slide image (WSI) and keep the comparable detection rate with human observer.
Improving Object Counting with Heatmap Regulation
Venue: arXiv cs.CV 2018
Year: 2018

In this paper, we propose a simple and effective way to improve one-look regression models for object counting from images. We use class activation map visualizations to illustrate the drawbacks of learning a pure one-look regression model for a counting task. Based on these insights, we enhance one-look regression counting models by regulating activation maps from the final convolution layer of the network with coarse ground-truth activation maps generated from simple dot annotations. We call this strategy heatmap regulation (HR). We show that this simple enhancement effectively suppresses false detections generated by the corresponding one-look baseline model and also improves the performance in terms of false negatives. Evaluations are performed on four different counting datasets --- two for car counting (CARPK, PUCPR+), one for crowd counting (WorldExpo) and another for biological cell counting (VGG-Cells). Adding HR to a simple VGG front-end improves performance on all these benchmarks compared to a simple one-look baseline model and results in state-of-the-art performance for car counting.
Evaluation of Dense 3D Reconstruction from 2D Face Images in the Wild
Venue: arXiv cs.CV 2018
Year: 2018

This paper investigates the evaluation of dense 3D face reconstruction from a single 2D image in the wild. To this end, we organise a competition that provides a new benchmark dataset that contains 2000 2D facial images of 135 subjects as well as their 3D ground truth face scans. In contrast to previous competitions or challenges, the aim of this new benchmark dataset is to evaluate the accuracy of a 3D dense face reconstruction algorithm using real, accurate and high-resolution 3D ground truth face scans. In addition to the dataset, we provide a standard protocol as well as a Python script for the evaluation. Last, we report the results obtained by three state-of-the-art 3D face reconstruction systems on the new benchmark dataset. The competition is organised along with the 2018 13th IEEE Conference on Automatic Face & Gesture Recognition.
Cross-Layer Designs for Body-to-Body Networks: Adaptive CSMA/CA with Distributed Routing
Venue: arXiv cs.NI 2018
Year: 2018

In this paper, we propose a novel adaptive carrier sense multiple access scheme with collision avoidance (CSMA/CA) to perform efficient and reliable data transfer with increased throughput across multiple coexisting wireless body area networks (BANs) in a tiered architecture. We investigate the proposed scheme using two distributed cross-layer optimized dynamic routing techniques, i.e., shortest path routing (SPR) and cooperative multi-path routing (CMR). The channel state information from the physical layer is passed on to the network layer using an adaptive cross-layer carrier sensing mechanism between the physical and MAC layer, which adjusts the carrier sense threshold (e.g., RSSI) periodically based on the slowly-varying channel condition. An open-access experimental dataset of 'everyday' mixed-activities is used for analyzing the cross-layer optimization. Our proposed optimization using adaptive carrier sensing performs better than static carrier sensing with CSMA/CA as it reduces the continuous back-off duration and latency as well as significantly increases the throughput (in successful packets/s) by more than 50%. Adaptive CSMA/CA also shows 20% and 6% improvement over a coordinated TDMA approach with higher duty cycle for throughput and spectral efficiency, respectively, and provides acceptable packet delivery ratio and outage probability with respect to SINR.
Modelling and Analysing the Landing Gear System: a Solution with Event-B/Rodin
Venue: arXiv cs.SE 2018
Year: 2018

This paper presents a solution to the landing gear system case study using Event-B and Rodin. We study the whole system (both the digital part and the controlled part). We use feature augmentation to build an abstract model of the whole system and structural refinement to detail more specifically the digital part. The required safety properties are formalised and proved. We propose a specific approach to deal with a family of reachability properties. The experimentations conducted during the study are supported by the Rodin tools. We show that the presented solution is systematic and it can be applied to similar case studies.
Relaxed Locally Correctable Codes in Computationally Bounded Channels
Venue: arXiv cs.DS 2018
Year: 2018

Error-correcting codes that admit local decoding and correcting algorithms have been the focus of much recent research due to their numerous theoretical and practical applications. An important goal is to obtain the best possible tradeoffs between the number of queries the algorithm makes to its oracle (the locality of the task), and the amount of redundancy in the encoding (the information rate). In Hamming's classical adversarial channel model, the current tradeoffs are dramatic, allowing either small locality, but superpolynomial blocklength, or small blocklength, but high locality. However, in the computationally bounded, adversarial channel model, proposed by Lipton (STACS 1994), constructions of locally decodable codes suddenly exhibit small locality and small blocklength, but these constructions require strong trusted setup assumptions e.g., Ostrovsky, Pandey and Sahai (ICALP 2007) construct private locally decodable codes in the setting where the sender and receiver already share a symmetric key. We study variants of locally decodable and locally correctable codes in computationally bounded, adversarial channels, in a setting with no public-key or private-key cryptographic setup. The only setup assumption we require is the selection of the public parameters (seed) for a collision-resistant hash function. Specifically, we provide constructions of relaxed locally correctable and relaxed locally decodable codes over the binary alphabet, with constant information rate, and poly-logarithmic locality. Our constructions, which compare favorably with their classical analogues in the computationally unbounded Hamming channel, crucially employ collision-resistant hash functions and local expander graphs, extending ideas from recent cryptographic constructions of memory-hard functions.
Mm-wave specific challenges in designing 5G transceiver architectures and air-interfaces
Venue: arXiv cs.IT 2018
Year: 2018

The mm-wave spectrum will be of significant importance to 5G mobile systems. There are multiple challenges in designing transceiver architectures and air interfaces in this spectrum. This paper is an attempt to explain some of these challenges and their interactions as means of enabling robust system design in near future.
A Study of Recent Contributions on Information Extraction
Venue: arXiv cs.IR 2018
Year: 2018

This paper reports on modern approaches in Information Extraction (IE) and its two main sub-tasks of Named Entity Recognition (NER) and Relation Extraction (RE). Basic concepts and the most recent approaches in this area are reviewed, which mainly include Machine Learning (ML) based approaches and the more recent trend to Deep Learning (DL) based methods.
Minimizing Crossings in Constrained Two-Sided Circular Graph Layouts
Venue: arXiv cs.CG 2018
Year: 2018

Circular layouts are a popular graph drawing style, where vertices are placed on a circle and edges are drawn as straight chords. Crossing minimization in circular layouts is \NP-hard. One way to allow for fewer crossings in practice are two-sided layouts that draw some edges as curves in the exterior of the circle. In fact, one- and two-sided circular layouts are equivalent to one-page and two-page book drawings, i.e., graph layouts with all vertices placed on a line (the spine) and edges drawn in one or two distinct half-planes (the pages) bounded by the spine. In this paper we study the problem of minimizing the crossings for a fixed cyclic vertex order by computing an optimal $k$-plane set of exteriorly drawn edges for $k \ge 1$, extending the previously studied case $k=0$. We show that this relates to finding bounded-degree maximum-weight induced subgraphs of circle graphs, which is a graph-theoretic problem of independent interest. We show \NP-hardness for arbitrary $k$, present an efficient algorithm for $k=1$, and generalize it to an explicit \XP-time algorithm for any fixed $k$. For the practically interesting case $k=1$ we implemented our algorithm and present experimental results that confirm the applicability of our algorithm.
Exploring Linear Relationship in Feature Map Subspace for ConvNets Compression
Venue: arXiv cs.CV 2018
Year: 2018

While the research on convolutional neural networks (CNNs) is progressing quickly, the real-world deployment of these models is often limited by computing resources and memory constraints. In this paper, we address this issue by proposing a novel filter pruning method to compress and accelerate CNNs. Our work is based on the linear relationship identified in different feature map subspaces via visualization of feature maps. Such linear relationship implies that the information in CNNs is redundant. Our method eliminates the redundancy in convolutional filters by applying subspace clustering to feature maps. In this way, most of the representative information in the network can be retained in each cluster. Therefore, our method provides an effective solution to filter pruning for which most existing methods directly remove filters based on simple heuristics. The proposed method is independent of the network structure, thus it can be adopted by any off-the-shelf deep learning libraries. Experiments on different networks and tasks show that our method outperforms existing techniques before fine-tuning, and achieves the state-of-the-art results after fine-tuning.
FDD Massive MIMO via UL/DL Channel Covariance Extrapolation and Active Channel Sparsification
Venue: arXiv cs.IT 2018
Year: 2018

We propose a novel method for massive Multiple-Input Multiple-Output (massive MIMO) in Frequency Division Duplexing (FDD) systems. Due to the large frequency separation between Uplink (UL) and Downlink (DL), in FDD systems channel reciprocity does not hold. Hence, in order to provide DL channel state information to the Base Station (BS), closed-loop DL channel probing and Channel State Information (CSI) feedback is needed. In massive MIMO this incurs typically a large training overhead. For example, in a typical configuration with M = 200 BS antennas and fading coherence block of T = 200 symbols, the resulting rate penalty factor due to the DL training overhead, given by max{0, 1 - M/T}, is close to 0. To reduce this overhead, we build upon the well-known fact that the Angular Scattering Function (ASF) of the user channels is invariant over frequency intervals whose size is small with respect to the carrier frequency (as in current FDD cellular standards). This allows to estimate the users' DL channel covariance matrix from UL pilots without additional overhead. Based on this covariance information, we propose a novel sparsifying precoder in order to maximize the rank of the effective sparsified channel matrix subject to the condition that each effective user channel has sparsity not larger than some desired DL pilot dimension T_{dl}, resulting in the DL training overhead factor max{0, 1 - T_{dl} / T} and CSI feedback cost of T_{dl} pilot measurements. The optimization of the sparsifying precoder is formulated as a Mixed Integer Linear Program, that can be efficiently solved. Extensive simulation results demonstrate the superiority of the proposed approach with respect to concurrent state-of-the-art schemes based on compressed sensing or UL/DL dictionary learning.
PAC-Reasoning in Relational Domains
Venue: arXiv cs.AI 2018
Year: 2018

We consider the problem of predicting plausible missing facts in relational data, given a set of imperfect logical rules. In particular, our aim is to provide bounds on the (expected) number of incorrect inferences that are made in this way. Since for classical inference it is in general impossible to bound this number in a non-trivial way, we consider two inference relations that weaken, but remain close in spirit to classical inference.
Sonifying stochastic walks on biomolecular energy landscapes
Venue: arXiv cs.HC 2018
Year: 2018

Translating the complex, multi-dimensional data from simulations of biomolecules to intuitive knowledge is a major challenge in computational chemistry and biology. The so-called "free energy landscape" is amongst the most fundamental concepts used by scientists to understand both static and dynamic properties of biomolecular systems. In this paper we use Markov models to design a strategy for mapping features of this landscape to sonic parameters, for use in conjunction with visual display techniques such as structural animations and free energy diagrams.
Theory and Algorithms for Forecasting Time Series
Venue: arXiv cs.LG 2018
Year: 2018

We present data-dependent learning bounds for the general scenario of non-stationary non-mixing stochastic processes. Our learning guarantees are expressed in terms of a data-dependent measure of sequential complexity and a discrepancy measure that can be estimated from data under some mild assumptions. We also also provide novel analysis of stable time series forecasting algorithm using this new notion of discrepancy that we introduce. We use our learning bounds to devise new algorithms for non-stationary time series forecasting for which we report some preliminary experimental results.
Enriching Frame Representations with Distributionally Induced Senses
Venue: arXiv cs.CL 2018
Year: 2018

We introduce a new lexical resource that enriches the Framester knowledge graph, which links Framnet, WordNet, VerbNet and other resources, with semantic features from text corpora. These features are extracted from distributionally induced sense inventories and subsequently linked to the manually-constructed frame representations to boost the performance of frame disambiguation in context. Since Framester is a frame-based knowledge graph, which enables full-fledged OWL querying and reasoning, our resource paves the way for the development of novel, deeper semantic-aware applications that could benefit from the combination of knowledge from text and complex symbolic representations of events and participants. Together with the resource we also provide the software we developed for the evaluation in the task of Word Frame Disambiguation (WFD).
GossipGraD: Scalable Deep Learning using Gossip Communication based Asynchronous Gradient Descent
Venue: arXiv cs.DC 2018
Year: 2018

In this paper, we present GossipGraD - a gossip communication protocol based Stochastic Gradient Descent (SGD) algorithm for scaling Deep Learning (DL) algorithms on large-scale systems. The salient features of GossipGraD are: 1) reduction in overall communication complexity from Θ(log(p)) for p compute nodes in well-studied SGD to O(1), 2) model diffusion such that compute nodes exchange their updates (gradients) indirectly after every log(p) steps, 3) rotation of communication partners for facilitating direct diffusion of gradients, 4) asynchronous distributed shuffle of samples during the feedforward phase in SGD to prevent over-fitting, 5) asynchronous communication of gradients for further reducing the communication cost of SGD and GossipGraD. We implement GossipGraD for GPU and CPU clusters and use NVIDIA GPUs (Pascal P100) connected with InfiniBand, and Intel Knights Landing (KNL) connected with Aries network. We evaluate GossipGraD using well-studied dataset ImageNet-1K (~250GB), and widely studied neural network topologies such as GoogLeNet and ResNet50 (current winner of ImageNet Large Scale Visualization Research Challenge (ILSVRC)). Our performance evaluation using both KNL and Pascal GPUs indicates that GossipGraD can achieve perfect efficiency for these datasets and their associated neural network topologies. Specifically, for ResNet50, GossipGraD is able to achieve ~100% compute efficiency using 128 NVIDIA Pascal P100 GPUs - while matching the top-1 classification accuracy published in literature.
Using Automatic Refactoring to Improve Energy Efficiency of Android Apps
Venue: arXiv cs.SE 2018
Year: 2018

The ever-growing popularity of mobile phones has brought additional challenges to the software development lifecycle. Mobile applications (apps, for short) ought to provide the same set of features as conventional software, with limited resources: such as, limited processing capabilities, storage, screen and, not less important, power source. Although energy efficiency is a valuable requirement, developers often lack knowledge of best practices. In this paper, we study whether or not automatic refactoring can aid developers ship energy efficient apps. We leverage a tool, Leafactor, with five energy code smells that tend to go unnoticed. We use Leafactor to analyze code smells in 140 free and open source apps. As a result, we detected and fixed code smells in 45 apps, from which 40% have successfully merged our changes into the official repository.
Toolflows for Mapping Convolutional Neural Networks on FPGAs: A Survey and Future Directions
Venue: arXiv cs.CV 2018
Year: 2018

In the past decade, Convolutional Neural Networks (CNNs) have demonstrated state-of-the-art performance in various Artificial Intelligence tasks. To accelerate the experimentation and development of CNNs, several software frameworks have been released, primarily targeting power-hungry CPUs and GPUs. In this context, reconfigurable hardware in the form of FPGAs constitutes a potential alternative platform that can be integrated in the existing deep learning ecosystem to provide a tunable balance between performance, power consumption and programmability. In this paper, a survey of the existing CNN-to-FPGA toolflows is presented, comprising a comparative study of their key characteristics which include the supported applications, architectural choices, design space exploration methods and achieved performance. Moreover, major challenges and objectives introduced by the latest trends in CNN algorithmic research are identified and presented. Finally, a uniform evaluation methodology is proposed, aiming at the comprehensive, complete and in-depth evaluation of CNN-to-FPGA toolflows.