OpenRaiser/Intern-Atlas huggingface dataset:
Tight Bounds on the Rényi Entropy via Majorization with Applications to Guessing and Compression
Venue: arXiv cs.IT 2018
Year: 2018

This paper provides tight bounds on the Rényi entropy of a function of a discrete random variable with a finite number of possible values, where the considered function is not one-to-one. To that end, a tight lower bound on the Rényi entropy of a discrete random variable with a finite support is derived as a function of the size of the support, and the ratio of the maximal to minimal probability masses. This work was inspired by the recently published paper by Cicalese et al., which is focused on the Shannon entropy, and it strengthens and generalizes the results of that paper to Rényi entropies of arbitrary positive orders. In view of these generalized bounds and the works by Arikan and Campbell, non-asymptotic bounds are derived for guessing moments and lossless data compression of discrete memoryless sources.
Engagement Estimation in Advertisement Videos with EEG
Venue: arXiv cs.HC 2018
Year: 2018

Engagement is a vital metric in the advertising industry and its automatic estimation has huge commercial implications. This work presents a basic and simple framework for engagement estimation using EEG (electroencephalography) data specifically recorded while watching advertisement videos, and is meant to be a first step in a promising line of research. The system combines recent advances in low cost commercial Brain-Computer Interfaces with modeling user engagement in response to advertisement videos. We achieve an F1 score of nearly 0.7 for a binary classification of high and low values of self-reported engagement from multiple users. This study illustrates the possibility of seamless engagement measurement in the wild when interacting with media using a non invasive and readily available commercial EEG device. Performing engagement measurement via implicit tagging in this manner with a direct feedback from physiological signals, thus requiring no additional human effort, demonstrates a novel and potentially commercially relevant application in the area of advertisement video analysis.
Unsupervised Learning of Monocular Depth Estimation with Bundle Adjustment, Super-Resolution and Clip Loss
Venue: arXiv cs.CV 2018
Year: 2018

We present a novel unsupervised learning framework for single view depth estimation using monocular videos. It is well known in 3D vision that enlarging the baseline can increase the depth estimation accuracy, and jointly optimizing a set of camera poses and landmarks is essential. In previous monocular unsupervised learning frameworks, only part of the photometric and geometric constraints within a sequence are used as supervisory signals. This may result in a short baseline and overfitting. Besides, previous works generally estimate a low resolution depth from a low resolution impute image. The low resolution depth is then interpolated to recover the original resolution. This strategy may generate large errors on object boundaries, as the depth of background and foreground are mixed to yield the high resolution depth. In this paper, we introduce a bundle adjustment framework and a super-resolution network to solve the above two problems. In bundle adjustment, depths and poses of an image sequence are jointly optimized, which increases the baseline by establishing the relationship between farther frames. The super resolution network learns to estimate a high resolution depth from a low resolution image. Additionally, we introduce the clip loss to deal with moving objects and occlusion. Experimental results on the KITTI dataset show that the proposed algorithm outperforms the state-of-the-art unsupervised methods using monocular sequences, and achieves comparable or even better result compared to unsupervised methods using stereo sequences.
A Multilevel Cybersecurity and Safety Monitor for Embedded Cyber-Physical Systems
Venue: arXiv cs.CR 2018
Year: 2018

Cyber-physical systems (CPS) are composed of various embedded subsystems and require specialized software, firmware, and hardware to coordinate with the rest of the system. These multiple levels of integration expose attack surfaces which can be susceptible to attack vectors that require novel architectural methods to effectively secure against. We present a multilevel hierarchical monitor architecture cybersecurity approach applied to a flight control system. However, the principles present in this paper apply to any CPS. Additionally, the real-time nature of these monitors allow for adaptable security, meaning that they mitigate against possible classes of attacks online. This results in an appealing bolt-on solution that is independent of different system designs. Consequently, employing such monitors leads to strengthened system resiliency and dependability of safety-critical CPS.
Area-preserving mapping of 3D ultrasound carotid artery images using density-equalizing reference map
Venue: arXiv cs.CG 2018
Year: 2018

Carotid atherosclerosis is a focal disease at the bifurcations of the carotid artery. To quantitatively monitor the local changes in the vessel-wall-plus-plaque thickness (VWT) and compare the VWT distributions for different patients or for the same patients at different ultrasound scanning sessions, a mapping technique is required to adjust for the geometric variability of different carotid artery models. In this work, we propose a novel method called density-equalizing reference map (DERM) for mapping 3D carotid surfaces to a standardized 2D carotid template, with an emphasis on preserving the local geometry of the carotid surface by minimizing the local area distortion. The initial map was generated by a previously described arc-length scaling (ALS) mapping method, which projects a 3D carotid surface onto a 2D non-convex L-shaped domain. A smooth and area-preserving flattened map was subsequently constructed by deforming the ALS map using the proposed algorithm that combines the density-equalizing map and the reference map techniques. This combination allows, for the first time, one-to-one mapping from a 3D surface to a standardized non-convex planar domain in an area-preserving manner. Evaluations using 20 carotid surface models show that the proposed method reduced the area distortion of the flattening maps by over 80% as compared to the ALS mapping method.
Virtual replicas of real places: Experimental investigations
Venue: arXiv cs.HC 2018
Year: 2018

The emergence of social virtual reality (VR) experiences, such as Facebook Spaces, Oculus Rooms, and Oculus Venues, will generate increased interest from users who want to share real places (both personal and public) with their fellow users in VR. At the same time, advances in scanning and reconstruction technology are making the realistic capture of real places more and more feasible. These complementary pressures mean that the representation of real places in virtual reality will be an increasingly common use case for VR. Despite this, there has been very little research into how users perceive such replicated spaces. This paper reports the results from a series of three user studies investigating this topic. Taken together, these results show that getting the scale of the space correct is the most important factor for generating a "feeling of reality", that it is important to avoid incoherent behaviors (such as floating objects), and that lighting makes little difference to perceptual similarity.
Speech-Gesture Mapping and Engagement Evaluation in Human Robot Interaction
Venue: arXiv cs.RO 2018
Year: 2018

A robot needs contextual awareness, effective speech production and complementing non-verbal gestures for successful communication in society. In this paper, we present our end-to-end system that tries to enhance the effectiveness of non-verbal gestures. For achieving this, we identified prominently used gestures in performances by TED speakers and mapped them to their corresponding speech context and modulated speech based upon the attention of the listener. The proposed method utilized Convolutional Pose Machine [4] to detect the human gesture. Dominant gestures of TED speakers were used for learning the gesture-to-speech mapping. The speeches by them were used for training the model. We also evaluated the engagement of the robot with people by conducting a social survey. The effectiveness of the performance was monitored by the robot and it self-improvised its speech pattern on the basis of the attention level of the audience, which was calculated using visual feedback from the camera. The effectiveness of interaction as well as the decisions made during improvisation was further evaluated based on the head-pose detection and interaction survey.
Joint Vertebrae Identification and Localization in Spinal CT Images by Combining Short- and Long-Range Contextual Information
Venue: arXiv cs.CV 2018
Year: 2018

Automatic vertebrae identification and localization from arbitrary CT images is challenging. Vertebrae usually share similar morphological appearance. Because of pathology and the arbitrary field-of-view of CT scans, one can hardly rely on the existence of some anchor vertebrae or parametric methods to model the appearance and shape. To solve the problem, we argue that one should make use of the short-range contextual information, such as the presence of some nearby organs (if any), to roughly estimate the target vertebrae; due to the unique anatomic structure of the spine column, vertebrae have fixed sequential order which provides the important long-range contextual information to further calibrate the results. We propose a robust and efficient vertebrae identification and localization system that can inherently learn to incorporate both the short-range and long-range contextual information in a supervised manner. To this end, we develop a multi-task 3D fully convolutional neural network (3D FCN) to effectively extract the short-range contextual information around the target vertebrae. For the long-range contextual information, we propose a multi-task bidirectional recurrent neural network (Bi-RNN) to encode the spatial and contextual information among the vertebrae of the visible spine column. We demonstrate the effectiveness of the proposed approach on a challenging dataset and the experimental results show that our approach outperforms the state-of-the-art methods by a significant margin.
Software Fault Tolerance for Cyber-Physical Systems via Full System Restart
Venue: arXiv cs.SY 2018
Year: 2018

The paper addresses the issue of reliability of complex embedded control systems in the safety-critical environment. In this paper, we propose a novel approach to design controller that (i) guarantees the safety of nonlinear physical systems, (ii) enables safe system restart during runtime, and (iii) allows the use of complex, unverified controllers (e.g., neural networks) that drive the physical systems towards complex specifications. We use abstraction-based controller synthesis approach to design a formally verified controller that provides application and system-level fault tolerance along with safety guarantee. Moreover, our approach is implementable using commercial-off-the-shelf (COTS) processing unit. To demonstrate the efficacy of our solution and to verify the safety of the system under various types of faults injected in applications and in the underlying real-time operating system (RTOS), we implemented the proposed controller for the inverted pendulum and three degree-of-freedom (3-DOF) helicopter.
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
Venue: arXiv cs.LO 2018
Year: 2018

We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of Quipper. Quipper is a new quantum programming language under active development and recently has gained much popularity among the quantum computing communities. Hybrid is a system that is designed to support the use of higher-order abstract syntax (HOAS) for representing and reasoning about formal systems implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic (SL) in order to reason about the linear type system of Quipper. To this end, we formalize the semantics of Proto-Quipper by encoding the typing and evaluation rules in the SL, and prove type soundness.
A context-based geoprocessing framework for optimizing meetup location of multiple moving objects along road networks
Venue: arXiv cs.AI 2018
Year: 2018

Given different types of constraints on human life, people must make decisions that satisfy social activity needs. Minimizing costs (i.e., distance, time, or money) associated with travel plays an important role in perceived and realized social quality of life. Identifying optimal interaction locations on road networks when there are multiple moving objects (MMO) with space-time constraints remains a challenge. In this research, we formalize the problem of finding dynamic ideal interaction locations for MMO as a spatial optimization model and introduce a context-based geoprocessing heuristic framework to address this problem. As a proof of concept, a case study involving identification of a meetup location for multiple people under traffic conditions is used to validate the proposed geoprocessing framework. Five heuristic methods with regard to efficient shortest-path search space have been tested. We find that the R* tree-based algorithm performs the best with high quality solutions and low computation time. This framework is implemented in a GIS environment to facilitate integration with external geographic contextual information, e.g., temporary road barriers, points of interest (POI), and real-time traffic information, when dynamically searching for ideal meetup sites. The proposed method can be applied in trip planning, carpooling services, collaborative interaction, and logistics management.
A Supervised-Learning Detector for Multihop Distributed Reception Systems
Venue: arXiv cs.IT 2018
Year: 2018

We consider a multihop distributed uplink reception system in which $K$ users transmit independent messages to one data center of $N_{\rm r} \geq K$ receive antennas, with the aid of multihop intermediate relays. In particular, each antenna of the data center is equipped with one-bit analog-to-digital converts (ADCs) for the sake of power-efficiency. In this system, it is extremely challenging to develop a low-complexity detector due to the non-linearity of an end-to-end channel transfer function (created by relays' operations and one-bit ADCs). Furthermore, there is no efficient way to estimate such complex function with a limited number of training data. Motivated by this, we propose a supervised-learning (SL) detector by introducing a novel Bernoulli-like model in which training data is directly used to design a detector rather than estimating a channel transfer function. It is shown that the proposed SL detector outperforms the existing SL detectors based on Gaussian model for one-bit quantized (binary observation) systems. Furthermore, we significantly reduce the complexity of the proposed SL detector using the fast kNN algorithm. Simulation results demonstrate that the proposed SL detector can yield an attractive performance with a significantly lower complexity.
Asynchronous Training of Word Embeddings for Large Text Corpora
Venue: arXiv cs.LG 2018
Year: 2018

Word embeddings are a powerful approach for analyzing language and have been widely popular in numerous tasks in information retrieval and text mining. Training embeddings over huge corpora is computationally expensive because the input is typically sequentially processed and parameters are synchronously updated. Distributed architectures for asynchronous training that have been proposed either focus on scaling vocabulary sizes and dimensionality or suffer from expensive synchronization latencies. In this paper, we propose a scalable approach to train word embeddings by partitioning the input space instead in order to scale to massive text corpora while not sacrificing the performance of the embeddings. Our training procedure does not involve any parameter synchronization except a final sub-model merge phase that typically executes in a few minutes. Our distributed training scales seamlessly to large corpus sizes and we get comparable and sometimes even up to 45% performance improvement in a variety of NLP benchmarks using models trained by our distributed procedure which requires $1/10$ of the time taken by the baseline approach. Finally we also show that we are robust to missing words in sub-models and are able to effectively reconstruct word representations.
Video Colorization using CNNs and Keyframes extraction: An application in saving bandwidth
Venue: arXiv cs.CV 2018
Year: 2018

In this paper, we tackle the problem of colorization of grayscale videos to reduce bandwidth usage. For this task, we use some colored keyframes as reference images from the colored version of the grayscale video. We propose a model that extracts keyframes from a colored video and trains a Convolutional Neural Network from scratch on these colored frames. Through the extracted keyframes we get a good knowledge of the colors that have been used in the video which helps us in colorizing the grayscale version of the video efficiently. An application of the technique that we propose in this paper, is in saving bandwidth while sending raw colored videos that haven't gone through any compression. A raw colored video takes up around three times more memory size than its grayscale version. We can exploit this fact and send a grayscale video along with out trained model instead of a colored video. Later on, in this paper we show how this technique can help to save bandwidth usage to upto three times while transmitting raw colored videos.
A decidability result for the halting problem of cellular automata in the pentagrid
Venue: arXiv cs.FL 2018
Year: 2018

In this paper, we investigate the halting problem for deterministic cellula automata in the pentagrid. We prove that the problem is decidable when the cellular automaton starts its computation from a finite configuration and when it has at most two states, one of them being a quiescent state.
A Computationally Efficient and Practically Feasible Two Microphones Blind Speech Separation Method
Venue: arXiv cs.SD 2018
Year: 2018

Traditionally, Blind Speech Separation techniques are computationally expensive as they update the demixing matrix at every time frame index, making them impractical to use in many Real-Time applications. In this paper, a robust data-driven two-microphone sound source localization method is used as a criterion to reduce the computational complexity of the Independent Vector Analysis (IVA) Blind Speech Separation (BSS) method. IVA is used to separate convolutedly mixed speech and noise sources. The practical feasibility of the proposed method is proved by implementing it on a smartphone device to separate speech and noise in Real-World scenarios for Hearing-Aid applications. The experimental results with objective and subjective tests reveal the practical usability of the developed method in many real-world applications.
The Effectiveness of Privacy Enhancing Technologies against Fingerprinting
Venue: arXiv cs.CR 2018
Year: 2018

We measure how effective Privacy Enhancing Technologies (PETs) are at protecting users from website fingerprinting. Our measurements use both experimental and observational methods. Experimental methods allow control, precision, and use on new PETs that currently lack a user base. Observational methods enable scale and drawing from the browsers currently in real-world use. By applying experimentally created models of a PET's behavior to an observational data set, our novel hybrid method offers the best of both worlds. We find the Tor Browser Bundle to be the most effective PET amongst the set we tested. We find that some PETs have inconsistent behaviors, which can do more harm than good.
A Metric for Linear Temporal Logic
Venue: arXiv cs.LO 2018
Year: 2018

We propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets. We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. An implementation for computing the measure of bounded LTL properties is provided and explained. This implementation leverages SAT model counting and effects independence checks on subexpressions to compute the measure and metric compositionally.
Building Ethically Bounded AI
Venue: arXiv cs.AI 2018
Year: 2018

The more AI agents are deployed in scenarios with possibly unexpected situations, the more they need to be flexible, adaptive, and creative in achieving the goal we have given them. Thus, a certain level of freedom to choose the best path to the goal is inherent in making AI robust and flexible enough. At the same time, however, the pervasive deployment of AI in our life, whether AI is autonomous or collaborating with humans, raises several ethical challenges. AI agents should be aware and follow appropriate ethical principles and should thus exhibit properties such as fairness or other virtues. These ethical principles should define the boundaries of AI's freedom and creativity. However, it is still a challenge to understand how to specify and reason with ethical boundaries in AI agents and how to combine them appropriately with subjective preferences and goal specifications. Some initial attempts employ either a data-driven example-based approach for both, or a symbolic rule-based approach for both. We envision a modular approach where any AI technique can be used for any of these essential ingredients in decision making or decision support systems, paired with a contextual approach to define their combination and relative weight. In a world where neither humans nor AI systems work in isolation, but are tightly interconnected, e.g., the Internet of Things, we also envision a compositional approach to building ethically bounded AI, where the ethical properties of each component can be fruitfully exploited to derive those of the overall system. In this paper we define and motivate the notion of ethically-bounded AI, we describe two concrete examples, and we outline some outstanding challenges.
SIMD-X: Programming and Processing of Graph Algorithms on GPUs
Venue: arXiv cs.DC 2018
Year: 2018

With high computation power and memory bandwidth, graphics processing units (GPUs) lend themselves to accelerate data-intensive analytics, especially when such applications fit the single instruction multiple data (SIMD) model. However, graph algorithms such as breadth-first search and k-core, often fail to take full advantage of GPUs, due to irregularity in memory access and control flow. To address this challenge, we have developed SIMD-X, for programming and processing of single instruction multiple, complex, data on GPUs. Specifically, the new Active-Compute-Combine (ACC) model not only provides ease of programming to programmers, but more importantly creates opportunities for system-level optimizations. To this end, SIMD-X utilizes just-in-time task management which filters out inactive vertices at runtime and intelligently maps various tasks to different amount of GPU cores in pursuit of workload balancing. In addition, SIMD-X leverages push-pull based kernel fusion that, with the help of a new deadlock-free global barrier, reduces a large number of computation kernels to very few. Using SIMD-X, a user can program a graph algorithm in tens of lines of code, while achieving 3?, 6?, 24?, 3? speedup over Gunrock, Galois, CuSha, and Ligra, respectively.