OpenRaiser/Intern-Atlas huggingface dataset:
Schematic Polymorphism in the Abella Proof Assistant
Venue: arXiv cs.LO 2018
Year: 2018

The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism both in the core logic of Abella and in the executable specification logic that it embeds.
Energy Efficient Tri-State CNFET Ternary Logic Gates
Venue: arXiv cs.ET 2018
Year: 2018

Traditional silicon binary circuits continue to face challenges such as high leakage power dissipation and large area of interconnections. Multiple-Valued Logic (MVL) and nano devices are two feasible solutions to overcome these problems. In this paper, a novel method is presented to design ternary logic circuits based on Carbon Nanotube Field Effect Transistors (CNFETs). The proposed designs use the unique properties of CNFETs, for example, adjusting the Carbon Nanontube (CNT) diameters to have the desired threshold voltage and have the same mobility of P-FET and N-FET transistors. Each of our designed logic circuits implements a logic function and its complementary via a control signal. Also, these circuits have a high impedance state which saves power while the circuits are not in use. In an effort to show a more detailed application of our approach, we design a 2-digit adder-subtractor circuit. We simulate the proposed ternary circuits using HSPICE via standard 32nm CNFET technology. The simulation results indicate the correct operation of the designs under different process, voltage and temperature (PVT) variations. Moreover, a power efficient ternary logic ALU has been design based on the proposed gates.
User's Privacy in Recommendation Systems Applying Online Social Network Data, A Survey and Taxonomy
Venue: arXiv cs.CR 2018
Year: 2018

Recommender systems have become an integral part of many social networks and extract knowledge from a user's personal and sensitive data both explicitly, with the user's knowledge, and implicitly. This trend has created major privacy concerns as users are mostly unaware of what data and how much data is being used and how securely it is used. In this context, several works have been done to address privacy concerns for usage in online social network data and by recommender systems. This paper surveys the main privacy concerns, measurements and privacy-preserving techniques used in large-scale online social networks and recommender systems. It is based on historical works on security, privacy-preserving, statistical modeling, and datasets to provide an overview of the technical difficulties and problems associated with privacy preserving in online social networks.
Optimization Matrix Factorization Recommendation Algorithm Based on Rating Centrality
Venue: arXiv cs.IR 2018
Year: 2018

Matrix factorization (MF) is extensively used to mine the user preference from explicit ratings in recommender systems. However, the reliability of explicit ratings is not always consistent, because many factors may affect the user's final evaluation on an item, including commercial advertising and a friend's recommendation. Therefore, mining the reliable ratings of user is critical to further improve the performance of the recommender system. In this work, we analyze the deviation degree of each rating in overall rating distribution of user and item, and propose the notion of user-based rating centrality and item-based rating centrality, respectively. Moreover, based on the rating centrality, we measure the reliability of each user rating and provide an optimized matrix factorization recommendation algorithm. Experimental results on two popular recommendation datasets reveal that our method gets better performance compared with other matrix factorization recommendation algorithms, especially on sparse datasets.
Word Tagging with Foundational Ontology Classes: Extending the WordNet-DOLCE Mapping to Verbs
Venue: arXiv cs.CL 2018
Year: 2018

Semantic annotation is fundamental to deal with large-scale lexical information, mapping the information to an enumerable set of categories over which rules and algorithms can be applied, and foundational ontology classes can be used as a formal set of categories for such tasks. A previous alignment between WordNet noun synsets and DOLCE provided a starting point for ontology-based annotation, but in NLP tasks verbs are also of substantial importance. This work presents an extension to the WordNet-DOLCE noun mapping, aligning verbs according to their links to nouns denoting perdurants, transferring to the verb the DOLCE class assigned to the noun that best represents that verb's occurrence. To evaluate the usefulness of this resource, we implemented a foundational ontology-based semantic annotation framework, that assigns a high-level foundational category to each word or phrase in a text, and compared it to a similar annotation tool, obtaining an increase of 9.05% in accuracy.
Formal Specification & Analysis of Autonomous Systems in PrCCSL/Simulink Design Verifier
Venue: arXiv cs.SE 2018
Year: 2018

Modeling and analysis of timing constraints is crucial in automotive systems. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. In most cases, a bounded number of violations of timing constraints in systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). We have previously specified EAST-ADL timing constraints in Clock Constraint Specification Language (CCSL) and transformed timed behaviors in CCSL into formal models amenable to model checking. Previous work is extended in this paper by including support for probabilistic analysis of timing constraints in the context of WH: Probabilistic extension of CCSL, called PrCCSL, is defined and the EAST-ADL timing constraints with stochastic properties are specified in PrCCSL. The semantics of the extended constraints in PrCCSL is translated into Proof Objective Models that can be verified using SIMULINK DESIGN VERIFIER. Furthermore, a set of mapping rules is proposed to facilitate guarantee of translation. Our approach is demonstrated on an autonomous traffic sign recognition vehicle case study.
How to Maximize the Spread of Social Influence: A Survey
Venue: arXiv cs.SI 2018
Year: 2018

This survey presents the main results achieved for the influence maximization problem in social networks. This problem is well studied in the literature and, thanks to its recent applications, some of which currently deployed on the field, it is receiving more and more attention in the scientific community. The problem can be formulated as follows: given a graph, with each node having a certain probability of influencing its neighbors, select a subset of vertices so that the number of nodes in the network that are influenced is maximized. Starting from this model, we introduce the main theoretical developments and computational results that have been achieved, taking into account different diffusion models describing how the information spreads throughout the network, various ways in which the sources of information could be placed, and how to tackle the problem in the presence of uncertainties affecting the network. Finally, we present one of the main application that has been developed and deployed exploiting tools and techniques previously discussed.
Attitudes of Children with Autism towards Robots: An Exploratory Study
Venue: arXiv cs.HC 2018
Year: 2018

In this exploratory study we assessed how attitudes of children with autism spectrum disorder (ASD) towards robots together with children's autism-related social impairments are linked to indicators of children's preference of an interaction with a robot over an interaction with a person. We found that children with ASD have overall positive attitudes towards robots and that they often prefer interacting with a robot than with a person. Several of children's attitudes were linked to children's longer gazes towards a robot compared to a person. Autism-related social impairments were linked to more repetitive and stereotyped behaviors and to a shorter gaze duration in the interaction with the robot compared to the person. These preliminary results contribute to better understand factors that might help determine sub-groups of children with ASD for whom robots could be particularly useful.
Learning Neural Parsers with Deterministic Differentiable Imitation Learning
Venue: arXiv cs.LG 2018
Year: 2018

We explore the problem of learning to decompose spatial tasks into segments, as exemplified by the problem of a painting robot covering a large object. Inspired by the ability of classical decision tree algorithms to construct structured partitions of their input spaces, we formulate the problem of decomposing objects into segments as a parsing approach. We make the insight that the derivation of a parse-tree that decomposes the object into segments closely resembles a decision tree constructed by ID3, which can be done when the ground-truth available. We learn to imitate an expert parsing oracle, such that our neural parser can generalize to parse natural images without ground truth. We introduce a novel deterministic policy gradient update, DRAG (i.e., DeteRministically AGgrevate) in the form of a deterministic actor-critic variant of AggreVaTeD, to train our neural parser. From another perspective, our approach is a variant of the Deterministic Policy Gradient suitable for the imitation learning setting. The deterministic policy representation offered by training our neural parser with DRAG allows it to outperform state of the art imitation and reinforcement learning approaches.
Resource-Efficient Neural Architect
Venue: arXiv cs.NE 2018
Year: 2018

Neural Architecture Search (NAS) is a laborious process. Prior work on automated NAS targets mainly on improving accuracy, but lacks consideration of computational resource use. We propose the Resource-Efficient Neural Architect (RENA), an efficient resource-constrained NAS using reinforcement learning with network embedding. RENA uses a policy network to process the network embeddings to generate new configurations. We demonstrate RENA on image recognition and keyword spotting (KWS) problems. RENA can find novel architectures that achieve high performance even with tight resource constraints. For CIFAR10, it achieves 2.95% test error when compute intensity is greater than 100 FLOPs/byte, and 3.87% test error when model size is less than 3M parameters. For Google Speech Commands Dataset, RENA achieves the state-of-the-art accuracy without resource constraints, and it outperforms the optimized architectures with tight resource constraints.
Searching for a Single Community in a Graph
Venue: arXiv cs.SI 2018
Year: 2018

In standard graph clustering/community detection, one is interested in partitioning the graph into more densely connected subsets of nodes. In contrast, the "search" problem of this paper aims to only find the nodes in a "single" such community, the target, out of the many communities that may exist. To do so , we are given suitable side information about the target; for example, a very small number of nodes from the target are labeled as such. We consider a general yet simple notion of side information: all nodes are assumed to have random weights, with nodes in the target having higher weights on average. Given these weights and the graph, we develop a variant of the method of moments that identifies nodes in the target more reliably, and with lower computation, than generic community detection methods that do not use side information and partition the entire graph. Our empirical results show significant gains in runtime, and also gains in accuracy over other graph clustering algorithms.
The Corpus Replication Task
Venue: arXiv cs.LG 2018
Year: 2018

In the field of Natural Language Processing (NLP), we revisit the well-known word embedding algorithm word2vec. Word embeddings identify words by vectors such that the words' distributional similarity is captured. Unexpectedly, besides semantic similarity even relational similarity has been shown to be captured in word embeddings generated by word2vec, whence two questions arise. Firstly, which kind of relations are representable in continuous space and secondly, how are relations built. In order to tackle these questions we propose a bottom-up point of view. We call generating input text for which word2vec outputs target relations solving the Corpus Replication Task. Deeming generalizations of this approach to any set of relations possible, we expect solving of the Corpus Replication Task to provide partial answers to the questions.
A Hierarchical Deep Architecture and Mini-Batch Selection Method For Joint Traffic Sign and Light Detection
Venue: arXiv cs.CV 2018
Year: 2018

Traffic light and sign detectors on autonomous cars are integral for road scene perception. The literature is abundant with deep learning networks that detect either lights or signs, not both, which makes them unsuitable for real-life deployment due to the limited graphics processing unit (GPU) memory and power available on embedded systems. The root cause of this issue is that no public dataset contains both traffic light and sign labels, which leads to difficulties in developing a joint detection framework. We present a deep hierarchical architecture in conjunction with a mini-batch proposal selection mechanism that allows a network to detect both traffic lights and signs from training on separate traffic light and sign datasets. Our method solves the overlapping issue where instances from one dataset are not labelled in the other dataset. We are the first to present a network that performs joint detection on traffic lights and signs. We measure our network on the Tsinghua-Tencent 100K benchmark for traffic sign detection and the Bosch Small Traffic Lights benchmark for traffic light detection and show it outperforms the existing Bosch Small Traffic light state-of-the-art method. We focus on autonomous car deployment and show our network is more suitable than others because of its low memory footprint and real-time image processing time. Qualitative results can be viewed at https://youtu.be/_YmogPzBXOw
A Supervised Approach To The Interpretation Of Imperative To-Do Lists
Venue: arXiv cs.CL 2018
Year: 2018

To-do lists are a popular medium for personal information management. As to-do tasks are increasingly tracked in electronic form with mobile and desktop organizers, so does the potential for software support for the corresponding tasks by means of intelligent agents. While there has been work in the area of personal assistants for to-do tasks, no work has focused on classifying user intention and information extraction as we do. We show that our methods perform well across two corpora that span sub-domains, one of which we released.
Physical-Layer Security in Cache-Enabled Cooperative Small Cell Networks Against Randomly Distributed Eavesdroppers
Venue: arXiv cs.IT 2018
Year: 2018

This paper explores the physical-layer security in a small cell network (SCN) with cooperative cache-enabled small base stations (SBSs) in the presence of randomly distributed eavesdroppers. We propose a joint design on the caching placement and the physical-layer transmission to improve the secure content delivery probability (SCDP). We first put forward a hybrid caching placement strategy in which a proportion of the cache unit in each SBS is assigned to store the most popular files (MPFs), while the remaining is used to cache the disjoint subfiles (DSFs) of the less popular files in different SBSs as a means to enhance transmission secrecy and content diversity. We then introduce two coordinated multi-point (CoMP) techniques, namely, joint transmission (JT) and orthogonal transmission (OT), to deliver the MPFs and DSFs, respectively. We derive analytical expressions for the SCDP in each transmission scheme, considering both non-colluding and colluding eavesdropping scenarios. Based on the obtained analytical results, we jointly design the optimal transmission rates and the optimal caching assignment for maximizing the overall SCDP. Various insights into the optimal transmission and caching designs are further provided. Numerical results are also presented to verify our theoretical findings and to demonstrate the superiority of the proposed caching and transmission strategies.
An empirical study on the names of points of interest and their changes with geographic distance
Venue: arXiv cs.CL 2018
Year: 2018

While Points Of Interest (POIs), such as restaurants, hotels, and barber shops, are part of urban areas irrespective of their specific locations, the names of these POIs often reveal valuable information related to local culture, landmarks, influential families, figures, events, and so on. Place names have long been studied by geographers, e.g., to understand their origins and relations to family names. However, there is a lack of large-scale empirical studies that examine the localness of place names and their changes with geographic distance. In addition to enhancing our understanding of the coherence of geographic regions, such empirical studies are also significant for geographic information retrieval where they can inform computational models and improve the accuracy of place name disambiguation. In this work, we conduct an empirical study based on 112,071 POIs in seven US metropolitan areas extracted from an open Yelp dataset. We propose to adopt term frequency and inverse document frequency in geographic contexts to identify local terms used in POI names and to analyze their usages across different POI types. Our results show an uneven usage of local terms across POI types, which is highly consistent among different geographic regions. We also examine the decaying effect of POI name similarity with the increase of distance among POIs. While our analysis focuses on urban POI names, the presented methods can be generalized to other place types as well, such as mountain peaks and streets.
On the Robustness of Interpretability Methods
Venue: arXiv cs.LG 2018
Year: 2018

We argue that robustness of explanations---i.e., that similar inputs should give rise to similar explanations---is a key desideratum for interpretability. We introduce metrics to quantify robustness and demonstrate that current methods do not perform well according to these metrics. Finally, we propose ways that robustness can be enforced on existing interpretability approaches.
GrCAN: Gradient Boost Convolutional Autoencoder with Neural Decision Forest
Venue: arXiv cs.LG 2018
Year: 2018

Random forest and deep neural network are two schools of effective classification methods in machine learning. While the random forest is robust irrespective of the data domain, the deep neural network has advantages in handling high dimensional data. In view that a differentiable neural decision forest can be added to the neural network to fully exploit the benefits of both models, in our work, we further combine convolutional autoencoder with neural decision forest, where autoencoder has its advantages in finding the hidden representations of the input data. We develop a gradient boost module and embed it into the proposed convolutional autoencoder with neural decision forest to improve the performance. The idea of gradient boost is to learn and use the residual in the prediction. In addition, we design a structure to learn the parameters of the neural decision forest and gradient boost module at contiguous steps. The extensive experiments on several public datasets demonstrate that our proposed model achieves good efficiency and prediction performance compared with a series of baseline methods.
Inference of Quantized Neural Networks on Heterogeneous All-Programmable Devices
Venue: arXiv cs.NE 2018
Year: 2018

Neural networks have established as a generic and powerful means to approach challenging problems such as image classification, object detection or decision making. Their successful employment foots on an enormous demand of compute. The quantization of network parameters and the processed data has proven a valuable measure to reduce the challenges of network inference so effectively that the feasible scope of applications is expanded even into the embedded domain. This paper describes the making of a real-time object detection in a live video stream processed on an embedded all-programmable device. The presented case illustrates how the required processing is tamed and parallelized across both the CPU cores and the programmable logic and how the most suitable resources and powerful extensions, such as NEON vectorization, are leveraged for the individual processing steps. The crafted result is an extended Darknet framework implementing a fully integrated, end-to-end solution from video capture over object annotation to video output applying neural network inference at different quantization levels running at 16~frames per second on an embedded Zynq UltraScale+ (XCZU3EG) platform.
Detecting Cyberattacks in Industrial Control Systems Using Convolutional Neural Networks
Venue: arXiv cs.CR 2018
Year: 2018

This paper presents a study on detecting cyberattacks on industrial control systems (ICS) using unsupervised deep neural networks, specifically, convolutional neural networks. The study was performed on a SecureWater Treatment testbed (SWaT) dataset, which represents a scaled-down version of a real-world industrial water treatment plant. e suggest a method for anomaly detection based on measuring the statistical deviation of the predicted value from the observed value.We applied the proposed method by using a variety of deep neural networks architectures including different variants of convolutional and recurrent networks. The test dataset from SWaT included 36 different cyberattacks. The proposed method successfully detects the vast majority of the attacks with a low false positive rate thus improving on previous works based on this data set. The results of the study show that 1D convolutional networks can be successfully applied to anomaly detection in industrial control systems and outperform more complex recurrent networks while being much smaller and faster to train.