OpenRaiser/Intern-Atlas huggingface dataset:
The HoTT Library: A formalization of homotopy type theory in Coq
Venue: arXiv cs.LO 2016
Year: 2016

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
Code Definition Analysis for Call Graph Generation
Venue: arXiv cs.SE 2016
Year: 2016

Enterprise level software is implemented using multi-layer architecture. These layers are often implemented using de-coupled solutions with millions of lines of code. Programmers often have to track and debug a function call from user interface layer to the data access layer while troubleshooting an issue. They have to inspect the code based on search results or use design documents to construct the call graph. This process is time consuming and laborious. The development environment tools are insufficient or confined to analyzing only the code in the loaded solution. This paper proposes a method to construct a call graph of the call across several layers of the code residing in different code bases to help programmers better understand the design and architecture of the software. The signatures of class, methods, and properties were evaluated and then matched against the code files. A graph of matching functions was created. The recursive search stopped when there were no matches or the data layer code was detected. The method resulted in 78.26% accuracy when compared with manual search.
Road Curb Extraction from Mobile LiDAR Point Clouds
Venue: arXiv cs.CV 2016
Year: 2016

Automatic extraction of road curbs from uneven, unorganized, noisy and massive 3D point clouds is a challenging task. Existing methods often project 3D point clouds onto 2D planes to extract curbs. However, the projection causes loss of 3D information which degrades the performance of the detection. This paper presents a robust, accurate and efficient method to extract road curbs from 3D mobile LiDAR point clouds. Our method consists of two steps: 1) extracting the candidate points of curbs based on the proposed novel energy function and 2) refining the candidate points using the proposed least cost path model. We evaluated our method on a large-scale of residential area (16.7GB, 300 million points) and an urban area (1.07GB, 20 million points) mobile LiDAR point clouds. Results indicate that the proposed method is superior to the state-of-the-art methods in terms of robustness, accuracy and efficiency. The proposed curb extraction method achieved a completeness of 78.62% and a correctness of 83.29%. These experiments demonstrate that the proposed method is a promising solution to extract road curbs from mobile LiDAR point clouds.
Non-negative matrix factorization-based subband decomposition for acoustic source localization
Venue: arXiv cs.SD 2016
Year: 2016

A novel non-negative matrix factorization (NMF) based subband decomposition in frequency spatial domain for acoustic source localization using a microphone array is introduced. The proposed method decomposes source and noise subband and emphasises source dominant frequency bins for more accurate source representation. By employing NMF, delay basis vectors and their subband information in frequency spatial domain for each frame is extracted. The proposed algorithm is evaluated in both simulated noise and real noise with a speech corpus database. Experimental results clearly indicate that the algorithm performs more accurately than other conventional algorithms under both reverberant and noisy acoustic environments.
Prioritized Garbage Collection: Explicit GC Support for Software Caches
Venue: arXiv cs.PL 2016
Year: 2016

Programmers routinely trade space for time to increase performance, often in the form of caching or memoization. In managed languages like Java or JavaScript, however, this space-time tradeoff is complex. Using more space translates into higher garbage collection costs, especially at the limit of available memory. Existing runtime systems provide limited support for space-sensitive algorithms, forcing programmers into difficult and often brittle choices about provisioning. This paper presents prioritized garbage collection, a cooperative programming language and runtime solution to this problem. Prioritized GC provides an interface similar to soft references, called priority references, which identify objects that the collector can reclaim eagerly if necessary. The key difference is an API for defining the policy that governs when priority references are cleared and in what order. Application code specifies a priority value for each reference and a target memory bound. The collector reclaims references, lowest priority first, until the total memory footprint of the cache fits within the bound. We use this API to implement a space-aware least-recently-used (LRU) cache, called a Sache, that is a drop-in replacement for existing caches, such as Google's Guava library. The garbage collector automatically grows and shrinks the Sache in response to available memory and workload with minimal provisioning information from the programmer. Using a Sache, it is almost impossible for an application to experience a memory leak, memory pressure, or an out-of-memory crash caused by software caching.
Sample Efficient Optimization for Learning Controllers for Bipedal Locomotion
Venue: arXiv cs.RO 2016
Year: 2016

Learning policies for bipedal locomotion can be difficult, as experiments are expensive and simulation does not usually transfer well to hardware. To counter this, we need al- gorithms that are sample efficient and inherently safe. Bayesian Optimization is a powerful sample-efficient tool for optimizing non-convex black-box functions. However, its performance can degrade in higher dimensions. We develop a distance metric for bipedal locomotion that enhances the sample-efficiency of Bayesian Optimization and use it to train a 16 dimensional neuromuscular model for planar walking. This distance metric reflects some basic gait features of healthy walking and helps us quickly eliminate a majority of unstable controllers. With our approach we can learn policies for walking in less than 100 trials for a range of challenging settings. In simulation, we show results on two different costs and on various terrains including rough ground and ramps, sloping upwards and downwards. We also perturb our models with unknown inertial disturbances analogous with differences between simulation and hardware. These results are promising, as they indicate that this method can potentially be used to learn control policies on hardware.
Trees That Grow
Venue: arXiv cs.PL 2016
Year: 2016

We study the notion of extensibility in functional data types, as a new approach to the problem of decorating abstract syntax trees with additional sets of information. We observed the need for such extensibility while redesigning the data types representing Haskell abstract syntax inside GHC. Specifically, we describe our approach to the tree-decoration problem using a novel syntactic machinery in Haskell for expressing extensible data types. We show that the syntactic machinery is complete in that it can express all the syntactically possible forms of extensions to algebraic data type declarations. Then, we describe an encoding of the syntactic machinery based on the existing features in Glasgow Haskell Compiler(GHC).
RGBD-based Parameter Extraction for Door Opening Tasks with Human Assists in Nuclear Rescue
Venue: arXiv cs.RO 2016
Year: 2016

The ability to open a door is essential for robots to perform home-serving and rescuing tasks. A substantial problem is to obtain the necessary parameters such as the width of the door and the length of the handle. Many researchers utilize computer vision techniques to extract the parameters automatically which lead to fine but not very stable results because of the complexity of the environment. We propose a method that utilizes an RGBD sensor and a GUI for users to 'point' at the target region with a mouse to acquire 3D information. Algorithms that can extract important parameters from the selected points are designed. To avoid large internal force induced by the misalignment of the robot orientation and the normal of the door plane, we design a module that can compute the normal of the plane by pointing at three non-collinear points and then drive the robot to the desired orientation. We carried out experiments on real robot. The result shows that the designed GUI and algorithms can help find the necessary parameters stably and get the robot prepared for further operations.
Location Sensitive Deep Convolutional Neural Networks for Segmentation of White Matter Hyperintensities
Venue: arXiv cs.CV 2016
Year: 2016

The anatomical location of imaging features is of crucial importance for accurate diagnosis in many medical tasks. Convolutional neural networks (CNN) have had huge successes in computer vision, but they lack the natural ability to incorporate the anatomical location in their decision making process, hindering success in some medical image analysis tasks. In this paper, to integrate the anatomical location information into the network, we propose several deep CNN architectures that consider multi-scale patches or take explicit location features while training. We apply and compare the proposed architectures for segmentation of white matter hyperintensities in brain MR images on a large dataset. As a result, we observe that the CNNs that incorporate location information substantially outperform a conventional segmentation method with hand-crafted features as well as CNNs that do not integrate location information. On a test set of 46 scans, the best configuration of our networks obtained a Dice score of 0.791, compared to 0.797 for an independent human observer. Performance levels of the machine and the independent human observer were not statistically significantly different (p-value=0.17).
Translation Quality Estimation using Recurrent Neural Network
Venue: arXiv cs.CL 2016
Year: 2016

This paper describes our submission to the shared task on word/phrase level Quality Estimation (QE) in the First Conference on Statistical Machine Translation (WMT16). The objective of the shared task was to predict if the given word/phrase is a correct/incorrect (OK/BAD) translation in the given sentence. In this paper, we propose a novel approach for word level Quality Estimation using Recurrent Neural Network Language Model (RNN-LM) architecture. RNN-LMs have been found very effective in different Natural Language Processing (NLP) applications. RNN-LM is mainly used for vector space language modeling for different NLP problems. For this task, we modify the architecture of RNN-LM. The modified system predicts a label (OK/BAD) in the slot rather than predicting the word. The input to the system is a word sequence, similar to the standard RNN-LM. The approach is language independent and requires only the translated text for QE. To estimate the phrase level quality, we use the output of the word level QE system.
Fault Detection Engine in Intelligent Predictive Analytics Platform for DCIM
Venue: arXiv cs.AI 2016
Year: 2016

With the advancement of huge data generation and data handling capability, Machine Learning and Probabilistic modelling enables an immense opportunity to employ predictive analytics platform in high security critical industries namely data centers, electricity grids, utilities, airport etc. where downtime minimization is one of the primary objectives. This paper proposes a novel, complete architecture of an intelligent predictive analytics platform, Fault Engine, for huge device network connected with electrical/information flow. Three unique modules, here proposed, seamlessly integrate with available technology stack of data handling and connect with middleware to produce online intelligent prediction in critical failure scenarios. The Markov Failure module predicts the severity of a failure along with survival probability of a device at any given instances. The Root Cause Analysis model indicates probable devices as potential root cause employing Bayesian probability assignment and topological sort. Finally, a community detection algorithm produces correlated clusters of device in terms of failure probability which will further narrow down the search space of finding route cause. The whole Engine has been tested with different size of network with simulated failure environments and shows its potential to be scalable in real-time implementation.
Optimal Capacity Allocation for Sampled Networked Systems
Venue: arXiv cs.SY 2016
Year: 2016

We consider the problem of estimating the states of weakly coupled linear systems from sampled measurements. We assume that the total capacity available to the sensors to transmit their samples to a network manager in charge of the estimation is bounded above, and that each sample requires the same amount of communication. Our goal is then to find an optimal allocation of the capacity to the sensors so that the average estimation error is minimized. We show that when the total available channel capacity is large, this resource allocation problem can be recast as a strictly convex optimization problem, and hence there exists a unique optimal allocation of the capacity. We further investigate how this optimal allocation varies as the available capacity increases. In particular, we show that if the coupling among the subsystems is weak, then the sampling rate allocated to each sensor is nondecreasing in the total sampling rate, and is strictly increasing if and only if the total sampling rate exceeds a certain threshold.
ProvDB: A System for Lifecycle Management of Collaborative Analysis Workflows
Venue: arXiv cs.DB 2016
Year: 2016

As data-driven methods are becoming pervasive in a wide variety of disciplines, there is an urgent need to develop scalable and sustainable tools to simplify the process of data science, to make it easier to keep track of the analyses being performed and datasets being generated, and to enable introspection of the workflows. In this paper, we describe our vision of a unified provenance and metadata management system to support lifecycle management of complex collaborative data science workflows. We argue that a large amount of information about the analysis processes and data artifacts can, and should be, captured in a semi-passive manner; and we show that querying and analyzing this information can not only simplify bookkeeping and debugging tasks for data analysts but can also enable a rich new set of capabilities like identifying flaws in the data science process itself. It can also significantly reduce the time spent in fixing post-deployment problems through automated analysis and monitoring. We have implemented an initial prototype of our system, called ProvDB, on top of git (a version control system) and Neo4j (a graph database), and we describe its key features and capabilities.
Multiple Instance Fuzzy Inference Neural Networks
Venue: arXiv cs.NE 2016
Year: 2016

Fuzzy logic is a powerful tool to model knowledge uncertainty, measurements imprecision, and vagueness. However, there is another type of vagueness that arises when data have multiple forms of expression that fuzzy logic does not address quite well. This is the case for multiple instance learning problems (MIL). In MIL, an object is represented by a collection of instances, called a bag. A bag is labeled negative if all of its instances are negative, and positive if at least one of its instances is positive. Positive bags encode ambiguity since the instances themselves are not labeled. In this paper, we introduce fuzzy inference systems and neural networks designed to handle bags of instances as input and capable of learning from ambiguously labeled data. First, we introduce the Multiple Instance Sugeno style fuzzy inference (MI-Sugeno) that extends the standard Sugeno style inference to handle reasoning with multiple instances. Second, we use MI-Sugeno to define and develop Multiple Instance Adaptive Neuro Fuzzy Inference System (MI-ANFIS). We expand the architecture of the standard ANFIS to allow reasoning with bags and derive a learning algorithm using backpropagation to identify the premise and consequent parameters of the network. The proposed inference system is tested and validated using synthetic and benchmark datasets suitable for MIL problems. We also apply the proposed MI-ANFIS to fuse the output of multiple discrimination algorithms for the purpose of landmine detection using Ground Penetrating Radar.
Wind ramp event prediction with parallelized Gradient Boosted Regression Trees
Venue: arXiv cs.LG 2016
Year: 2016

Accurate prediction of wind ramp events is critical for ensuring the reliability and stability of the power systems with high penetration of wind energy. This paper proposes a classification based approach for estimating the future class of wind ramp event based on certain thresholds. A parallelized gradient boosted regression tree based technique has been proposed to accurately classify the normal as well as rare extreme wind power ramp events. The model has been validated using wind power data obtained from the National Renewable Energy Laboratory database. Performance comparison with several benchmark techniques indicates the superiority of the proposed technique in terms of superior classification accuracy.
Validation of community robustness
Venue: arXiv cs.SI 2016
Year: 2016

The large amount of work on community detection and its applications leaves unaddressed one important question: the statistical validation of the results. In this paper we present a methodology able to clearly detect if the community structure found by some algorithms is statistically significant or is a result of chance, merely due to edge positions in the network. Given a community detection method and a network of interest, our proposal examines the stability of the partition recovered against random perturbations of the original graph structure. To address this issue, we specify a perturbation strategy and a null model to build a set of procedures based on a special measure of clustering distance, namely Variation of Information, using tools set up for functional data analysis. The procedures determine whether the obtained clustering departs significantly from the null model. This strongly supports the robustness against perturbation of the algorithm used to identify the community structure. We show the results obtained with the proposed technique on simulated and real datasets.
Online Thevenin Equivalent Parameter Estimation using Nonlinear and Linear Recursive Least Square Algorithm
Venue: arXiv cs.SY 2016
Year: 2016

This paper proposes method for detection, estimation of Thevenin equivalent parameters to describe power system behavior. Thevenin equivalent estimation is a challenge due to variation in system states caused by power flow in the network. Thevenin equivalent calculation based on changes in system with multiple sources integrated with grid, isolated distributed generator system is analysed and nonlinear least square fit estimation technique for algorithm is adopted. Linear least square fit is used with a linearized model. Performance evaluation of proposed method is carried out through mathematical model, nonlinear and linear least square fit based algorithm technique and simulation through MATLAB/SIMULINK package. Accurate grid and source side impedance estimation technique is applicable for distributed generation sources interfaced with grid to improve dynamic response, stability, reliability when subjected to faults or any other disturbances in network. Algorithm can accurately estimate Thevenin equivalent of multiple sources connected in parallel simultaneously with voltage and current phasor measurements at point of common coupling. Mathematical analysis and simulation results validate the effectiveness of proposed method.
Spatio-temporal Co-Occurrence Characterizations for Human Action Classification
Venue: arXiv cs.CV 2016
Year: 2016

The human action classification task is a widely researched topic and is still an open problem. Many state-of-the-arts approaches involve the usage of bag-of-video-words with spatio-temporal local features to construct characterizations for human actions. In order to improve beyond this standard approach, we investigate the usage of co-occurrences between local features. We propose the usage of co-occurrences information to characterize human actions. A trade-off factor is used to define an optimal trade-off between vocabulary size and classification rate. Next, a spatio-temporal co-occurrence technique is applied to extract co-occurrence information between labeled local features. Novel characterizations for human actions are then constructed. These include a vector quantized correlogram-elements vector, a highly discriminative PCA (Principal Components Analysis) co-occurrence vector and a Haralick texture vector. Multi-channel kernel SVM (support vector machine) is utilized for classification. For evaluation, the well known KTH as well as the challenging UCF-Sports action datasets are used. We obtained state-of-the-arts classification performance. We also demonstrated that we are able to fully utilize co-occurrence information, and improve the standard bag-of-video-words approach.
Sensitivity of Complex Networks
Venue: arXiv cs.SY 2016
Year: 2016

The sensitivity (i.e. dynamic response) of complex networked systems has not been well understood, making difficult to predict whether new macroscopic dynamic behavior will emerge even if we know exactly how individual nodes behave and how they are coupled. Here we build a framework to quantify the sensitivity of complex networked system of coupled dynamic units. We characterize necessary and sufficient conditions for the emergence of new macroscopic dynamic behavior in the thermodynamic limit. We prove that these conditions are satisfied only for architectures with power-law degree distributions. Surprisingly, we find that highly connected nodes (i.e. hubs) only dominate the sensitivity of the network up to certain critical frequency.