OpenRaiser/Intern-Atlas huggingface dataset:
On the Formalization of Importance Measures using HOL Theorem Proving
Venue: arXiv cs.FL 2019
Year: 2019

Importance measures provide a systematic approach to scrutinize critical system components, which are extremely beneficial in making important decisions, such as prioritizing reliability improvement activities, identifying weak-links and effective usage of given resources. The importance measures are then in turn used to obtain a criticality value for each system component and to rank the components in descending manner. Simulations tools are generally used to perform importance measure based analysis, but they require expensive computations and thus they are not suitable for large systems. A more scalable approach is to utilize the importance measures to obtain all the necessary conditions by proving a generic relationship describing the relative importance between any pair of components in a system. In this paper, we propose to use higher-order-logic (HOL) theorem proving to verify such relationships and thus making sure that all the essential conditions are accompanied by the proven property. In particular, we formalize the commonly used importance measures, such as Birnbaum and Fussell-Vesely, and conduct a formal importance measure analysis of a railway signaling system at a Moroccan level crossing as an application for illustration purpose.
Hammering Mizar by Learning Clause Guidance
Venue: arXiv cs.AI 2019
Year: 2019

We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.
Out of Site: Empowering a New Approach to Online Boycotts
Venue: arXiv cs.HC 2019
Year: 2019

GrabYourWallet, #boycottNRA and other online boycott campaigns have attracted substantial public interest in recent months. However, a number of significant challenges are preventing online boycotts from reaching their potential. In particular, complex webs of brands and subsidiaries can make it difficult for participants to conform to the goals of a boycott. Similarly, participants and organizers have limited visibility into a boycott's progress. This affects their ability to use sociotechnical innovations from social computing to incentivize participation. To address these challenges, this paper makes a system contribution: a new boycott tool called Out of Site. Out of Site uses lightweight automation to remove obstacles to successful online boycotts. We describe the design challenges associated with Out of Site and report results from two phases of deployment with the GrabYourWallet and Stop Animal Testing boycott communities. Our findings highlight the potential of boycott-assisting technologies and inform the design of this new class of technologies. Finally, like is the case for many systems in social computing, while we designed Out of Site for pro-social uses, there are a number of easily predictable ways in which the system can be leveraged for anti-social purposes (e.g. exacerbating filter bubble issues, empowering boycotts of businesses owned by racial, ethnic, and religious minorities). As such, we developed for this project a new, very straightforward design approach that treats preventing these anti-social uses as a top-tier design concern. This approach stands in contrast to the status quo of ignoring potential anti-social uses and/or considering them to be a secondary design priority. We discuss how our simple approach may help other research projects reduce their potential negative impacts with minimal burden.
The Tower of Babel Meets Web 2.0: User-Generated Content and its Applications in a Multilingual Context
Venue: arXiv cs.CL 2019
Year: 2019

This study explores language's fragmenting effect on user-generated content by examining the diversity of knowledge representations across 25 different Wikipedia language editions. This diversity is measured at two levels: the concepts that are included in each edition and the ways in which these concepts are described. We demonstrate that the diversity present is greater than has been presumed in the literature and has a significant influence on applications that use Wikipedia as a source of world knowledge. We close by explicating how knowledge diversity can be beneficially leveraged to create "culturally-aware applications" and "hyperlingual applications".
VRGym: A Virtual Testbed for Physical and Interactive AI
Venue: arXiv cs.HC 2019
Year: 2019

We propose VRGym, a virtual reality testbed for realistic human-robot interaction. Different from existing toolkits and virtual reality environments, the VRGym emphasizes on building and training both physical and interactive agents for robotics, machine learning, and cognitive science. VRGym leverages mechanisms that can generate diverse 3D scenes with high realism through physics-based simulation. We demonstrate that VRGym is able to (i) collect human interactions and fine manipulations, (ii) accommodate various robots with a ROS bridge, (iii) support experiments for human-robot interaction, and (iv) provide toolkits for training the state-of-the-art machine learning algorithms. We hope VRGym can help to advance general-purpose robotics and machine learning agents, as well as assisting human studies in the field of cognitive science.
Explainable Text Classification in Legal Document Review A Case Study of Explainable Predictive Coding
Venue: arXiv cs.IR 2019
Year: 2019

In today's legal environment, lawsuits and regulatory investigations require companies to embark upon increasingly intensive data-focused engagements to identify, collect and analyze large quantities of data. When documents are staged for review the process can require companies to dedicate an extraordinary level of resources, both with respect to human resources, but also with respect to the use of technology-based techniques to intelligently sift through data. For several years, attorneys have been using a variety of tools to conduct this exercise, and most recently, they are accepting the use of machine learning techniques like text classification to efficiently cull massive volumes of data to identify responsive documents for use in these matters. In recent years, a group of AI and Machine Learning researchers have been actively researching Explainable AI. In an explainable AI system, actions or decisions are human understandable. In typical legal `document review' scenarios, a document can be identified as responsive, as long as one or more of the text snippets in a document are deemed responsive. In these scenarios, if predictive coding can be used to locate these responsive snippets, then attorneys could easily evaluate the model's document classification decision. When deployed with defined and explainable results, predictive coding can drastically enhance the overall quality and speed of the document review process by reducing the time it takes to review documents. The authors of this paper propose the concept of explainable predictive coding and simple explainable predictive coding methods to locate responsive snippets within responsive documents. We also report our preliminary experimental results using the data from an actual legal matter that entailed this type of document review.
An Empirical Study of the Application of Machine Learning and Keyword Terms Methodologies to Privilege-Document Review Projects in Legal Matters
Venue: arXiv cs.IR 2019
Year: 2019

Protecting privileged communications and data from disclosure is paramount for legal teams. Unrestricted legal advice, such as attorney-client communications or litigation strategy. are vital to the legal process and are exempt from disclosure in litigations or regulatory events. To protect this information from being disclosed, companies and outside counsel must review vast amounts of documents to determine those that contain privileged material. This process is extremely costly and time consuming. As data volumes increase, legal counsel employ methods to reduce the number of documents requiring review while balancing the need to ensure the protection of privileged information. Keyword searching is relied upon as a method to target privileged information and reduce document review populations. Keyword searches are effective at casting a wide net but return over inclusive results -- most of which do not contain privileged information -- and without detailed knowledge of the data, keyword lists cannot be crafted to find all privilege material. Overly-inclusive keyword searching can also be problematic, because even while it drives up costs, it also can cast `too far of a net' and thus produce unreliable results.To overcome these weaknesses of keyword searching, legal teams are using a new method to target privileged information called predictive modeling. Predictive modeling can successfully identify privileged material but little research has been published to confirm its effectiveness when compared to keyword searching. This paper summarizes a study of the effectiveness of keyword searching and predictive modeling when applied to real-world data. With this study, this group of collaborators wanted to examine and understand the benefits and weaknesses of both approaches to legal teams with identifying privilege material in document populations.
Evaluation of the Spatio-Temporal features and GAN for Micro-expression Recognition System
Venue: arXiv cs.CV 2019
Year: 2019

Owing to the development and advancement of artificial intelligence, numerous works were established in the human facial expression recognition system. Meanwhile, the detection and classification of micro-expressions are attracting attentions from various research communities in the recent few years. In this paper, we first review the processes of a conventional optical-flow-based recognition system, which comprised of facial landmarks annotations, optical flow guided images computation, features extraction and emotion class categorization. Secondly, a few approaches have been proposed to improve the feature extraction part, such as exploiting GAN to generate more image samples. Particularly, several variations of optical flow are computed in order to generate optimal images to lead to high recognition accuracy. Next, GAN, a combination of Generator and Discriminator, is utilized to generate new "fake" images to increase the sample size. Thirdly, a modified state-of-the-art Convolutional neural networks is proposed. To verify the effectiveness of the the proposed method, the results are evaluated on spontaneous micro-expression databases, namely SMIC, CASME II and SAMM. Both the F1-score and accuracy performance metrics are reported in this paper.
MAVNet: an Effective Semantic Segmentation Micro-Network for MAV-based Tasks
Venue: arXiv cs.CV 2019
Year: 2019

Real-time semantic image segmentation on platforms subject to size, weight and power (SWaP) constraints is a key area of interest for air surveillance and inspection. In this work, we propose MAVNet: a small, light-weight, deep neural network for real-time semantic segmentation on micro Aerial Vehicles (MAVs). MAVNet, inspired by ERFNet, features 400 times fewer parameters and achieves comparable performance with some reference models in empirical experiments. Our model achieves a trade-off between speed and accuracy, achieving up to 48 FPS on an NVIDIA 1080Ti and 9 FPS on the NVIDIA Jetson Xavier when processing high resolution imagery. Additionally, we provide two novel datasets that represent challenges in semantic segmentation for real-time MAV tracking and infrastructure inspection tasks and verify MAVNet on these datasets. Our algorithm and datasets are made publicly available.
Bayesian Approach with Extended Support Estimation for Sparse Regression
Venue: arXiv cs.IT 2019
Year: 2019

A greedy algorithm called Bayesian multiple matching pursuit (BMMP) is proposed to estimate a sparse signal vector and its support given $m$ linear measurements. Unlike the maximum a posteriori (MAP) support detection, which was proposed by Lee to estimate the support by selecting an index with the maximum likelihood ratio of the correlation given by a normalized version of the orthogonal matching pursuit (OMP), the proposed method uses the correlation given by the matching pursuit proposed by Davies and Eldar. BMMP exploits the diversity gain to estimate the support by considering multiple support candidates, each of which is obtained by iteratively selecting an index set with a size different for each candidate. In particular, BMMP considers an extended support estimate whose maximal size is $m$ in the process to obtain each of the support candidates. It is observed that BMMP outperforms other state-of-the-art methods and approaches the ideal limit of the signal sparsity in our simulation setting.
affinity: A System for Latent User Similarity Comparison on Texting Data
Venue: arXiv cs.SI 2019
Year: 2019

In the field of social networking services, finding similar users based on profile data is common practice. Smartphones harbor sensor and personal context data that can be used for user profiling. Yet, one vast source of personal data, that is text messaging data, has hardly been studied for user profiling. We see three reasons for this: First, private text messaging data is not shared due to their intimate character. Second, the definition of an appropriate privacy-preserving similarity measure is non-trivial. Third, assessing the quality of a similarity measure on text messaging data representing a potentially infinite set of topics is non-trivial. In order to overcome these obstacles we propose affinity, a system that assesses the similarity between text messaging histories of users reliably and efficiently in a privacy-preserving manner. Private texting data stays on user devices and data for comparison is compared in a latent format that neither allows to reconstruct the comparison words nor any original private plain text. We evaluate our approach by calculating similarities between Twitter histories of 60 US senators. The resulting similarity network reaches an average 85.0% accuracy on a political party classification task.
Super accurate low latency object detection on a surveillance UAV
Venue: arXiv cs.CV 2019
Year: 2019

Drones have proven to be useful in many industry segments such as security and surveillance, where e.g. on-board real-time object tracking is a necessity for autonomous flying guards. Tracking and following suspicious objects is therefore required in real-time on limited hardware. With an object detector in the loop, low latency becomes extremely important. In this paper, we propose a solution to make object detection for UAVs both fast and super accurate. We propose a multi-dataset learning strategy yielding top eye-sky object detection accuracy. Our model generalizes well on unseen data and can cope with different flying heights, optically zoomed-in shots and different viewing angles. We apply optimization steps such that we achieve minimal latency on embedded on-board hardware by fusing layers, quantizing calculations to 16-bit floats and 8-bit integers, with negligible loss in accuracy. We validate on NVIDIA's Jetson TX2 and Jetson Xavier platforms where we achieve a speed-wise performance boost of more than 10x.
Interpreting Adversarial Examples by Activation Promotion and Suppression
Venue: arXiv cs.CV 2019
Year: 2019

It is widely known that convolutional neural networks (CNNs) are vulnerable to adversarial examples: images with imperceptible perturbations crafted to fool classifiers. However, interpretability of these perturbations is less explored in the literature. This work aims to better understand the roles of adversarial perturbations and provide visual explanations from pixel, image and network perspectives. We show that adversaries have a promotion-suppression effect (PSE) on neurons' activations and can be primarily categorized into three types: i) suppression-dominated perturbations that mainly reduce the classification score of the true label, ii) promotion-dominated perturbations that focus on boosting the confidence of the target label, and iii) balanced perturbations that play a dual role in suppression and promotion. We also provide image-level interpretability of adversarial examples. This links PSE of pixel-level perturbations to class-specific discriminative image regions localized by class activation mapping (Zhou et al. 2016). Further, we examine the adversarial effect through network dissection (Bau et al. 2017), which offers concept-level interpretability of hidden units. We show that there exists a tight connection between the units' sensitivity to adversarial attacks and their interpretability on semantic concepts. Lastly, we provide some new insights from our interpretation to improve the adversarial robustness of networks.
A queueing approach to the latency of decoupled UL/DL with flexible TDD and asymmetric services
Venue: arXiv cs.IT 2019
Year: 2019

One of the main novelties in 5G is the flexible Time Division Duplex (TDD) frame, which allows adaptation to the latency requirements. However, this flexibility is not sufficient to support heterogeneous latency requirements, in which different traffic instances have different switching requirements between Uplink (UL) and Downlink (DL). This is visible in a traffic mix of enhanced mobile broadband (eMBB) and ultra-reliable low-latency communications (URLLC). In this paper we address this problem through the use of a decoupled UL/DL access, where the UL and the DL of a device are not necessarily served by the same base station. The latency gain over coupled access is quantified in the form of queueing sojourn time in a Rayleigh channel, as well as an upper bound for critical traffic.
Graph based Nearest Neighbor Search: Promises and Failures
Venue: arXiv cs.IR 2019
Year: 2019

Recently, graph based nearest neighbor search gets more and more popular on large-scale retrieval tasks. The attractiveness of this type of approaches lies in its superior performance over most of the known nearest neighbor search approaches as well as its genericness to various metrics. In this paper, the role of two strategies, namely hierarchical structure and graph diversification that are adopted as the key steps in the graph based approaches, is investigated. We find the hierarchical structure could not achieve "much better logarithmic complexity scaling" as it was claimed in the original paper, particularly on high dimensional cases. Moreover, we find that similar high search speed efficiency as the one with hierarchical structure could be achieved with the support of flat k-NN graph after graph diversification. Finally, we point out the difficulty, that is faced by most of the graph based search approaches, is directly linked to "curse of dimensionality".
Agent-based Vs Agent-less Sandbox for Dynamic Behavioral Analysis
Venue: arXiv cs.CR 2019
Year: 2019

Malicious software is detected and classified by either static analysis or dynamic analysis. In static analysis, malware samples are reverse engineered and analyzed so that signatures of malware can be constructed. These techniques can be easily thwarted through polymorphic, metamorphic malware, obfuscation and packing techniques, whereas in dynamic analysis malware samples are executed in a controlled environment using the sandboxing technique, in order to model the behavior of malware. In this paper, we have analyzed Petya, Spyeye, VolatileCedar, PAFISH etc. through Agent-based and Agentless dynamic sandbox systems in order to investigate and benchmark their efficiency in advanced malware detection.
Multidimensional Capacitive Sensing for Robot-Assisted Dressing and Bathing
Venue: arXiv cs.RO 2019
Year: 2019

Robotic assistance presents an opportunity to benefit the lives of many people with physical disabilities, yet accurately sensing the human body and tracking human motion remain difficult for robots. We present a multidimensional capacitive sensing technique that estimates the local pose of a human limb in real time. A key benefit of this sensing method is that it can sense the limb through opaque materials, including fabrics and wet cloth. Our method uses a multielectrode capacitive sensor mounted to a robot's end effector. A neural network model estimates the position of the closest point on a person's limb and the orientation of the limb's central axis relative to the sensor's frame of reference. These pose estimates enable the robot to move its end effector with respect to the limb using feedback control. We demonstrate that a PR2 robot can use this approach with a custom six electrode capacitive sensor to assist with two activities of daily living-dressing and bathing. The robot pulled the sleeve of a hospital gown onto able-bodied participants' right arms, while tracking human motion. When assisting with bathing, the robot moved a soft wet washcloth to follow the contours of able-bodied participants' limbs, cleaning their surfaces. Overall, we found that multidimensional capacitive sensing presents a promising approach for robots to sense and track the human body during assistive tasks that require physical human-robot interaction.
A Recoverable Mutex Algorithm with Sub-logarithmic RMR on Both CC and DSM
Venue: arXiv cs.DC 2019
Year: 2019

In light of recent advances in non-volatile main memory technology, Golab and Ramaraju reformulated the traditional mutex problem into the novel {\em Recoverable Mutual Exclusion} (RME) problem. In the best known solution for RME, due to Golab and Hendler from PODC 2017, a process incurs at most $O(\frac{\log n}{\log \log n})$ remote memory references (RMRs) per passage, where a passage is an interval from when a process enters the Try section to when it subsequently returns to Remainder. Their algorithm, however, guarantees this bound only for cache-coherent (CC) multiprocessors, leaving open the question of whether a similar bound is possible for distributed shared memory (DSM) multiprocessors. We answer this question affirmatively by designing an algorithm that satisfies the same complexity bound as Golab and Hendler's for both CC and DSM multiprocessors. Our algorithm has some additional advantages over Golab and Hendler's: (i) its Exit section is wait-free, (ii) it uses only the Fetch-and-Store instruction, and (iii) on a CC machine our algorithm needs each process to have a cache of only $O(1)$ words, while their algorithm needs $O(n)$ words.
Private Information Retrieval from Heterogeneous Uncoded Storage Constrained Databases with Reduced Sub-Messages
Venue: arXiv cs.IT 2019
Year: 2019

We propose capacity-achieving schemes for private information retrieval (PIR) from uncoded databases (DBs) with both homogeneous and heterogeneous storage constraints. In the PIR setting, a user queries a set of DBs to privately download a message, where privacy implies that no one DB can infer which message the user desires. In general, a PIR scheme is comprised of storage placement and delivery designs. Previous works have derived the capacity, or infimum download cost, of PIR with uncoded storage placement and also sufficient conditions of a storage placement design to meet capacity. However, the currently proposed storage placement designs require splitting each message into an exponential number of sub-messages with respect to the number of DBs. In this work, when DBs have the same storage constraint, we propose two simple storage placement designs that satisfy the capacity conditions. Then, for more general heterogeneous storage constraints, we translate the storage placement design process into a "filling problem". We design an iterative algorithm to solve the filling problem where, in each iteration, messages are partitioned into sub-messages and stored at subsets of DBs. All of our proposed storage placement designs require a number of sub-messages per message at most equal to the number of DBs.