OpenRaiser/Intern-Atlas huggingface dataset:
Soft Contract Verification for Higher-Order Stateful Programs
Venue: arXiv cs.PL 2017
Year: 2017

Software contracts allow programmers to state rich program properties using the full expressive power of an object language. However, since they are enforced at runtime, monitoring contracts imposes significant overhead and delays error discovery. So contract verification aims to guarantee all or most of these properties ahead of time, enabling valuable optimizations and yielding a more general assurance of correctness. Existing methods for static contract verification satisfy the needs of more restricted target languages, but fail to address the challenges unique to those conjoining untyped, dynamic programming, higher-order functions, modularity, and statefulness. Our approach tackles all these features at once, in the context of the full Racket system---a mature environment for stateful, higher-order, multi-paradigm programming with or without types. Evaluating our method using a set of both pure and stateful benchmarks, we are able to verify 99.94% of checks statically (all but 28 of 49, 861). Stateful, higher-order functions pose significant challenges for static contract verification in particular. In the presence of these features, a modular analysis must permit code from the current module to escape permanently to an opaque context (unspecified code from outside the current module) that may be stateful and therefore store a reference to the escaped closure. Also, contracts themselves, being predicates wri en in unrestricted Racket, may exhibit stateful behavior; a sound approach must be robust to contracts which are arbitrarily expressive and interwoven with the code they monitor. In this paper, we present and evaluate our solution based on higher-order symbolic execution, explain the techniques we used to address such thorny issues, formalize a notion of behavioral approximation, and use it to provide a mechanized proof of soundness.
Unsupervised Learning of Geometry with Edge-aware Depth-Normal Consistency
Venue: arXiv cs.CV 2017
Year: 2017

Learning to reconstruct depths in a single image by watching unlabeled videos via deep convolutional network (DCN) is attracting significant attention in recent years. In this paper, we introduce a surface normal representation for unsupervised depth estimation framework. Our estimated depths are constrained to be compatible with predicted normals, yielding more robust geometry results. Specifically, we formulate an edge-aware depth-normal consistency term, and solve it by constructing a depth-to-normal layer and a normal-to-depth layer inside of the DCN. The depth-to-normal layer takes estimated depths as input, and computes normal directions using cross production based on neighboring pixels. Then given the estimated normals, the normal-to-depth layer outputs a regularized depth map through local planar smoothness. Both layers are computed with awareness of edges inside the image to help address the issue of depth/normal discontinuity and preserve sharp edges. Finally, to train the network, we apply the photometric error and gradient smoothness for both depth and normal predictions. We conducted experiments on both outdoor (KITTI) and indoor (NYUv2) datasets, and show that our algorithm vastly outperforms state of the art, which demonstrates the benefits from our approach.
Breast density classification with deep convolutional neural networks
Venue: arXiv cs.CV 2017
Year: 2017

Breast density classification is an essential part of breast cancer screening. Although a lot of prior work considered this problem as a task for learning algorithms, to our knowledge, all of them used small and not clinically realistic data both for training and evaluation of their models. In this work, we explore the limits of this task with a data set coming from over 200,000 breast cancer screening exams. We use this data to train and evaluate a strong convolutional neural network classifier. In a reader study, we find that our model can perform this task comparably to a human expert.
Communicative Capital for Prosthetic Agents
Venue: arXiv cs.AI 2017
Year: 2017

This work presents an overarching perspective on the role that machine intelligence can play in enhancing human abilities, especially those that have been diminished due to injury or illness. As a primary contribution, we develop the hypothesis that assistive devices, and specifically artificial arms and hands, can and should be viewed as agents in order for us to most effectively improve their collaboration with their human users. We believe that increased agency will enable more powerful interactions between human users and next generation prosthetic devices, especially when the sensorimotor space of the prosthetic technology greatly exceeds the conventional control and communication channels available to a prosthetic user. To more concretely examine an agency-based view on prosthetic devices, we propose a new schema for interpreting the capacity of a human-machine collaboration as a function of both the human's and machine's degrees of agency. We then introduce the idea of communicative capital as a way of thinking about the communication resources developed by a human and a machine during their ongoing interaction. Using this schema of agency and capacity, we examine the benefits and disadvantages of increasing the agency of a prosthetic limb. To do so, we present an analysis of examples from the literature where building communicative capital has enabled a progression of fruitful, task-directed interactions between prostheses and their human users. We then describe further work that is needed to concretely evaluate the hypothesis that prostheses are best thought of as agents. The agent-based viewpoint developed in this article significantly extends current thinking on how best to support the natural, functional use of increasingly complex prosthetic enhancements, and opens the door for more powerful interactions between humans and their assistive technologies.
Reinforcement Learning of Speech Recognition System Based on Policy Gradient and Hypothesis Selection
Venue: arXiv cs.CL 2017
Year: 2017

Speech recognition systems have achieved high recognition performance for several tasks. However, the performance of such systems is dependent on the tremendously costly development work of preparing vast amounts of task-matched transcribed speech data for supervised training. The key problem here is the cost of transcribing speech data. The cost is repeatedly required to support new languages and new tasks. Assuming broad network services for transcribing speech data for many users, a system would become more self-sufficient and more useful if it possessed the ability to learn from very light feedback from the users without annoying them. In this paper, we propose a general reinforcement learning framework for speech recognition systems based on the policy gradient method. As a particular instance of the framework, we also propose a hypothesis selection-based reinforcement learning method. The proposed framework provides a new view for several existing training and adaptation methods. The experimental results show that the proposed method improves the recognition performance compared to unsupervised adaptation.
Saliency Prediction for Mobile User Interfaces
Venue: arXiv cs.CV 2017
Year: 2017

We introduce models for saliency prediction for mobile user interfaces. A mobile interface may include elements like buttons, text, etc. in addition to natural images which enable performing a variety of tasks. Saliency in natural images is a well studied area. However, given the difference in what constitutes a mobile interface, and the usage context of these devices, we postulate that saliency prediction for mobile interface images requires a fresh approach. Mobile interface design involves operating on elements, the building blocks of the interface. We first collected eye-gaze data from mobile devices for free viewing task. Using this data, we develop a novel autoencoder based multi-scale deep learning model that provides saliency prediction at the mobile interface element level. Compared to saliency prediction approaches developed for natural images, we show that our approach performs significantly better on a range of established metrics.
Logics for modelling collective attitudes
Venue: arXiv cs.LO 2017
Year: 2017

We introduce a number of logics to reason about collective propositional attitudes that are defined by means of the majority rule. It is well known that majoritarian aggregation is subject to irrationality, as the results in social choice theory and judgment aggregation show. The proposed logics for modelling collective attitudes are based on a substructural propositional logic that allows for circumventing inconsistent outcomes. Individual and collective propositional attitudes, such as beliefs, desires, obligations, are then modelled by means of minimal modalities to ensure a number of basic principles. In this way, a viable consistent modelling of collective attitudes is obtained.
Lattice embeddings between types of fuzzy sets. Closed-valued fuzzy sets
Venue: arXiv cs.AI 2017
Year: 2017

In this paper we deal with the problem of extending Zadeh's operators on fuzzy sets (FSs) to interval-valued (IVFSs), set-valued (SVFSs) and type-2 (T2FSs) fuzzy sets. Namely, it is known that seeing FSs as SVFSs, or T2FSs, whose membership degrees are singletons is not order-preserving. We then describe a family of lattice embeddings from FSs to SVFSs. Alternatively, if the former singleton viewpoint is required, we reformulate the intersection on hesitant fuzzy sets and introduce what we have called closed-valued fuzzy sets. This new type of fuzzy sets extends standard union and intersection on FSs. In addition, it allows handling together membership degrees of different nature as, for instance, closed intervals and finite sets. Finally, all these constructions are viewed as T2FSs forming a chain of lattices.
Robotic Tactile Perception of Object Properties: A Review
Venue: arXiv cs.RO 2017
Year: 2017

Touch sensing can help robots understand their sur- rounding environment, and in particular the objects they interact with. To this end, roboticists have, in the last few decades, developed several tactile sensing solutions, extensively reported in the literature. Research into interpreting the conveyed tactile information has also started to attract increasing attention in recent years. However, a comprehensive study on this topic is yet to be reported. In an effort to collect and summarize the major scientific achievements in the area, this survey extensively reviews current trends in robot tactile perception of object properties. Available tactile sensing technologies are briefly presented before an extensive review on tactile recognition of object properties. The object properties that are targeted by this review are shape, surface material and object pose. The role of touch sensing in combination with other sensing sources is also discussed. In this review, open issues are identified and future directions for applying tactile sensing in different tasks are suggested.
LSTM Networks for Data-Aware Remaining Time Prediction of Business Process Instances
Venue: arXiv cs.LG 2017
Year: 2017

Predicting the completion time of business process instances would be a very helpful aid when managing processes under service level agreement constraints. The ability to know in advance the trend of running process instances would allow business managers to react in time, in order to prevent delays or undesirable situations. However, making such accurate forecasts is not easy: many factors may influence the required time to complete a process instance. In this paper, we propose an approach based on deep Recurrent Neural Networks (specifically LSTMs) that is able to exploit arbitrary information associated to single events, in order to produce an as-accurate-as-possible prediction of the completion time of running instances. Experiments on real-world datasets confirm the quality of our proposal.
Model Checking Markov Population Models by Stochastic Approximations
Venue: arXiv cs.LO 2017
Year: 2017

Many complex systems can be described by population models, in which a pool of agents interacts and produces complex collective behaviours. We consider the problem of verifying formal properties of the underlying mathematical representation of these models, which is a Continuous Time Markov Chain, often with a huge state space. To circumvent the state space explosion, we rely on stochastic approximation techniques, which replace the large model by a simpler one, guaranteed to be probabilistically consistent. We show how to efficiently and accurately verify properties of random individual agents, specified by Continuous Stochastic Logic extended with Timed Automata (CSL-TA), and how to lift these specifications to the collective level, approximating the number of agents satisfying them using second or higher order stochastic approximation techniques.
Towards the Use of Deep Reinforcement Learning with Global Policy For Query-based Extractive Summarisation
Venue: arXiv cs.CL 2017
Year: 2017

Supervised approaches for text summarisation suffer from the problem of mismatch between the target labels/scores of individual sentences and the evaluation score of the final summary. Reinforcement learning can solve this problem by providing a learning mechanism that uses the score of the final summary as a guide to determine the decisions made at the time of selection of each sentence. In this paper we present a proof-of-concept approach that applies a policy-gradient algorithm to learn a stochastic policy using an undiscounted reward. The method has been applied to a policy consisting of a simple neural network and simple features. The resulting deep reinforcement learning system is able to learn a global policy and obtain encouraging results.
Manipulative Elicitation -- A New Attack on Elections with Incomplete Preferences
Venue: arXiv cs.MA 2017
Year: 2017

Lu and Boutilier proposed a novel approach based on "minimax regret" to use classical score based voting rules in the setting where preferences can be any partial (instead of complete) orders over the set of alternatives. We show here that such an approach is vulnerable to a new kind of manipulation which was not present in the classical (where preferences are complete orders) world of voting. We call this attack "manipulative elicitation." More specifically, it may be possible to (partially) elicit the preferences of the agents in a way that makes some distinguished alternative win the election who may not be a winner if we elicit every preference completely. More alarmingly, we show that the related computational task is polynomial time solvable for a large class of voting rules which includes all scoring rules, maximin, Copeland$^α$ for every $α\in[0,1]$, simplified Bucklin voting rules, etc. We then show that introducing a parameter per pair of alternatives which specifies the minimum number of partial preferences where this pair of alternatives must be comparable makes the related computational task of manipulative elicitation \NPC for all common voting rules including a class of scoring rules which includes the plurality, $k$-approval, $k$-veto, veto, and Borda voting rules, maximin, Copeland$^α$ for every $α\in[0,1]$, and simplified Bucklin voting rules. Hence, in this work, we discover a fundamental vulnerability in using minimax regret based approach in partial preferential setting and propose a novel way to tackle it.
Multi-agent based IoT smart waste monitoring and collection architecture
Venue: arXiv cs.MA 2017
Year: 2017

Solid waste management is one of the existing challenges in urban areas and it is becoming a critical issue due to rapid increase in population. Appropriate solid waste management systems are important for improving the environment and the well being of residents. In this paper, an Internet of Things (IoT) architecture for real time waste monitoring and collection has been proposed; able to improve and optimize solid waste collection in a city. Netlogo Multiagent platform has been used to simulate real time monitoring and smart decisions on waste management. Waste filling level in bins and truck collection process are abstracted to a multiagent model and citizen are involved by paying the price for waste collection services. Furthermore, waste level data are updated and recorded continuously and are provided to decision algorithms to determine the vehicle optimal route for waste collection to the distributed bins in the city. Several simulation cases executed and results validated. The presented solution gives substantial benefits to all waste stakeholders by enabling the waste collection process to be more efficient.
Reuters Tracer: Toward Automated News Production Using Large Scale Social Media Data
Venue: arXiv cs.SI 2017
Year: 2017

To deal with the sheer volume of information and gain competitive advantage, the news industry has started to explore and invest in news automation. In this paper, we present Reuters Tracer, a system that automates end-to-end news production using Twitter data. It is capable of detecting, classifying, annotating, and disseminating news in real time for Reuters journalists without manual intervention. In contrast to other similar systems, Tracer is topic and domain agnostic. It has a bottom-up approach to news detection, and does not rely on a predefined set of sources or subjects. Instead, it identifies emerging conversations from 12+ million tweets per day and selects those that are news-like. Then, it contextualizes each story by adding a summary and a topic to it, estimating its newsworthiness, veracity, novelty, and scope, and geotags it. Designing algorithms to generate news that meets the standards of Reuters journalists in accuracy and timeliness is quite challenging. But Tracer is able to achieve competitive precision, recall, timeliness, and veracity on news detection and delivery. In this paper, we reveal our key algorithm designs and evaluations that helped us achieve this goal, and lessons learned along the way.
Towards Automated ICD Coding Using Deep Learning
Venue: arXiv cs.CL 2017
Year: 2017

International Classification of Diseases(ICD) is an authoritative health care classification system of different diseases and conditions for clinical and management purposes. Considering the complicated and dedicated process to assign correct codes to each patient admission based on overall diagnosis, we propose a hierarchical deep learning model with attention mechanism which can automatically assign ICD diagnostic codes given written diagnosis. We utilize character-aware neural language models to generate hidden representations of written diagnosis descriptions and ICD codes, and design an attention mechanism to address the mismatch between the numbers of descriptions and corresponding codes. Our experimental results show the strong potential of automated ICD coding from diagnosis descriptions. Our best model achieves 0.53 and 0.90 of F1 score and area under curve of receiver operating characteristic respectively. The result outperforms those achieved using character-unaware encoding method or without attention mechanism. It indicates that our proposed deep learning model can code automatically in a reasonable way and provide a framework for computer-auxiliary ICD coding.
Mobile Sensing of Two-Dimensional Bandlimited Fields on Random Paths
Venue: arXiv cs.IT 2017
Year: 2017

Mobile sensing has been recently proposed for sampling spatial fields, where mobile sensors record the field along various paths for reconstruction. Classical and contemporary sampling typically assumes that the sampling locations are approximately known. This work explores multiple sampling strategies along random paths to sample and reconstruct a two dimensional bandlimited field. Extensive simulations are carried out, with insights from sensing matrices and their properties, to evaluate the sampling strategies. Their performance is measured by evaluating the stability of field reconstruction from field samples. The effect of location unawareness on some sampling strategies is also evaluated by simulations.
STWalk: Learning Trajectory Representations in Temporal Graphs
Venue: arXiv cs.SI 2017
Year: 2017

Analyzing the temporal behavior of nodes in time-varying graphs is useful for many applications such as targeted advertising, community evolution and outlier detection. In this paper, we present a novel approach, STWalk, for learning trajectory representations of nodes in temporal graphs. The proposed framework makes use of structural properties of graphs at current and previous time-steps to learn effective node trajectory representations. STWalk performs random walks on a graph at a given time step (called space-walk) as well as on graphs from past time-steps (called time-walk) to capture the spatio-temporal behavior of nodes. We propose two variants of STWalk to learn trajectory representations. In one algorithm, we perform space-walk and time-walk as part of a single step. In the other variant, we perform space-walk and time-walk separately and combine the learned representations to get the final trajectory embedding. Extensive experiments on three real-world temporal graph datasets validate the effectiveness of the learned representations when compared to three baseline methods. We also show the goodness of the learned trajectory embeddings for change point detection, as well as demonstrate that arithmetic operations on these trajectory representations yield interesting and interpretable results.
An efficient algorithm computing composition factors of $T(V)^{\otimes n}$
Venue: arXiv cs.DS 2017
Year: 2017

We present an algorithm that computes the composition factors of the n-th tensor power of the free associative algebra on a vector space. The composition factors admit a description in terms of certain coefficients $c_{λμ}$ determining their irreducible structure. By reinterpreting these coefficients as counting the number of ways to solve certain `decomposition-puzzles' we are able to design an efficient algorithm extending the range of computation by a factor of over 750. Furthermore, by visualising the data appropriately, we gain insights into the nature of the coefficients leading to the development of a new representation theoretic framework called PD-modules.
Longest Alignment with Edits in Data Streams
Venue: arXiv cs.DS 2017
Year: 2017

Analyzing patterns in data streams generated by network traffic, sensor networks, or satellite feeds is a challenge for systems in which the available storage is limited. In addition, real data is noisy, which makes designing data stream algorithms even more challenging. Motivated by such challenges, we study algorithms for detecting the similarity of two data streams that can be read in sync. Two strings $S, T\in Σ^n$ form a $d$-near-alignment if the distance between them in some given metric is at most $d$. We study the problem of identifying a longest substring of $S$ and $T$ that forms a $d$-near-alignment under the edit distance, in the simultaneous streaming model. In this model, symbols of strings $S$ and $T$ are streamed at the same time, and the amount of available processing space is sublinear in the length of the strings. We give several algorithms, including an exact one-pass algorithm that uses $\mathcal{O}(d^2+d\log n)$ bits of space. We couple these results with comparable lower bounds.