OpenRaiser/Intern-Atlas huggingface dataset:
What Do We Elect Committees For? A Voting Committee Model for Multi-Winner Rules
Venue: arXiv cs.MA 2016
Year: 2016

We present a new model that describes the process of electing a group of representatives (e.g., a parliament) for a group of voters. In this model, called the voting committee model, the elected group of representatives runs a number of ballots to make final decisions regarding various issues. The satisfaction of voters comes from the final decisions made by the elected committee. Our results suggest that depending on a decision system used by the committee to make these final decisions, different multi-winner election rules are most suitable for electing the committee. Furthermore, we show that if we allow not only a committee, but also an election rule used to make final decisions, to depend on the voters' preferences, we can obtain an even better representation of the voters.
High-Frequency Modeling and Simulation of a Single-Phase Three-Winding Transformer Including Taps in Regulating Winding
Venue: arXiv cs.CE 2016
Year: 2016

Transformer terminal equivalents obtained via admittance measurements are suitable for simulating high-frequency transient interaction between the transformer and the network. This paper augments the terminal equivalent approach with a measurement-based voltage transfer function model which permits calculation of voltages at internal points in the regulating winding. The approach is demonstrated for a single-phase three-winding transformer in tap position Nom+ with inclusion of three internal points in the regulating winding that represent the mid-point and the two extreme ends. The terminal equivalent modeling makes use of additional common-mode measurements to avoid error magnifications to result from the ungrounded tertiary winding. The final model is used in a time domain simulation where ground-fault initiation results in a resonant voltage build-up in the winding. It is shown that that the peak value of the resonant overvoltage can be higher than during the lightning impulse test, with unfavorable network conditions. Additional measurements show that the selected tap position affects the terminal behavior of the transformer, changing the frequency and peak value of the lower resonance point in the voltage transfer between windings.
A Data Structure for Nearest Common Ancestors with Linking
Venue: arXiv cs.DS 2016
Year: 2016

Consider a forest that evolves via $link$ operations that make the root of one tree the child of a node in another tree. Intermixed with $link$ operations are $nca$ operations, which return the nearest common ancestor of two given nodes when such exists. This paper shows that a sequence of $m$ such $nca$ and $link$ operations on a forest of $n$ nodes can be processed on-line in time $O(mα(m,n)+n)$. This was previously known only for a restricted type of $link$ operation. The special case where a $link$ only extends a tree by adding a new leaf occurs in Edmonds' algorithm for finding a maximum weight matching on a general graph. Incorporating our algorithm into the implementation of Edmonds' algorithm in \cite{G17} achieves time $O(n(m + n\log n))$ for weighted matching, an arguably optimum asymptotic bound ($n$ and $m$ are the number of vertices and edges, respectively).
Two statements of the Duggan-Schwartz theorem
Venue: arXiv cs.GT 2016
Year: 2016

The Duggan-Schwartz theorem (Duggan and Schwartz, 1992) is a famous result concerning strategy-proof social choice correspondences, often stated as "A social choice correspondence that can be manipulated by neither an optimist nor a pessimist has a weak dictator". However, this formulation is actually due to Taylor (2002), and the original theorem, at face value, looks rather different. In this note we show that the two are in fact equivalent.
A Simple Power Analysis Attack on the Twofish Key Schedule
Venue: arXiv cs.CR 2016
Year: 2016

This paper introduces an SPA power attack on the 8-bit implementation of the Twofish block cipher. The attack is able to unequivocally recover the secret key even under substantial amounts of error. An initial algorithm is described using exhaustive search on error free data. An error resistant algorithm is later described. It employs several threshold preprocessing stages followed by a combined approach of least mean squares and an optimized Hamming mask search. Further analysis of 32 and 64-bit Twofish implementations reveals that they are similarly vulnerable to the described SPA attack.
Development of an EKF-based localization algorithm using compass sensor and LRF
Venue: arXiv cs.RO 2016
Year: 2016

This paper presents the implementation of a perceptual system for a mobile robot. The system is designed and installed with modern sensors and multi-point communication channels. The goal is to equip the robot with a high level of perception to support a wide range of navigating applications including Internet-based telecontrol, semi-autonomy, and autonomy. Due to uncertainties of acquiring data, a sensor fusion model is developed, in which heterogeneous measured data including odometry, compass heading and laser range is combined to get an optimal estimate in a statistical sense. The combination is carried out by an extended Kalman filter. Experimental results indicate that based on the system, the robot localization is enhanced and sufficient for navigation tasks.
Cascaded Neural Networks with Selective Classifiers and its evaluation using Lung X-ray CT Images
Venue: arXiv cs.CV 2016
Year: 2016

Lung nodule detection is a class imbalanced problem because nodules are found with much lower frequency than non-nodules. In the class imbalanced problem, conventional classifiers tend to be overwhelmed by the majority class and ignore the minority class. We therefore propose cascaded convolutional neural networks to cope with the class imbalanced problem. In the proposed approach, cascaded convolutional neural networks that perform as selective classifiers filter out obvious non-nodules. Successively, a convolutional neural network trained with a balanced data set calculates nodule probabilities. The proposed method achieved the detection sensitivity of 85.3% and 90.7% at 1 and 4 false positives per scan in FROC curve, respectively.
Active learning with version spaces for object detection
Venue: arXiv cs.CV 2016
Year: 2016

Given an image, we would like to learn to detect objects belonging to particular object categories. Common object detection methods train on large annotated datasets which are annotated in terms of bounding boxes that contain the object of interest. Previous works on object detection model the problem as a structured regression problem which ranks the correct bounding boxes more than the background ones. In this paper we develop algorithms which actively obtain annotations from human annotators for a small set of images, instead of all images, thereby reducing the annotation effort. Towards this goal, we make the following contributions: 1. We develop a principled version space based active learning method that solves for object detection as a structured prediction problem in a weakly supervised setting 2. We also propose two variants of the margin sampling strategy 3. We analyse the results on standard object detection benchmarks that show that with only 20% of the data we can obtain more than 95% of the localization accuracy of full supervision. Our methods outperform random sampling and the classical uncertainty-based active learning algorithms like entropy
A Metric for Performance Portability
Venue: arXiv cs.PF 2016
Year: 2016

The term "performance portability" has been informally used in computing to refer to a variety of notions which generally include: 1) the ability to run one application across multiple hardware platforms; and 2) achieving some notional level of performance on these platforms. However, there has been a noticeable lack of consensus on the precise meaning of the term, and authors' conclusions regarding their success (or failure) to achieve performance portability have thus been subjective. Comparing one approach to performance portability with another has generally been marked with vague claims and verbose, qualitative explanation of the comparison. This paper presents a concise definition for performance portability, along with a simple metric that accurately captures the performance and portability of an application across different platforms. The utility of this metric is then demonstrated with a retroactive application to previous work.
Achieving non-discrimination in data release
Venue: arXiv cs.LG 2016
Year: 2016

Discrimination discovery and prevention/removal are increasingly important tasks in data mining. Discrimination discovery aims to unveil discriminatory practices on the protected attribute (e.g., gender) by analyzing the dataset of historical decision records, and discrimination prevention aims to remove discrimination by modifying the biased data before conducting predictive analysis. In this paper, we show that the key to discrimination discovery and prevention is to find the meaningful partitions that can be used to provide quantitative evidences for the judgment of discrimination. With the support of the causal graph, we present a graphical condition for identifying a meaningful partition. Based on that, we develop a simple criterion for the claim of non-discrimination, and propose discrimination removal algorithms which accurately remove discrimination while retaining good data utility. Experiments using real datasets show the effectiveness of our approaches.
F-Index of Four Operations on Graphs
Venue: arXiv cs.DM 2016
Year: 2016

The F-index of a graph is defined as the sum of cubes of the vertex degrees of the graph which was introduced in 1972, in the same paper where the first and second Zagreb indices were introduced. In this paper we study the F-index of four operations on graphs which were introduced by Eliasi and Taeri [M. Eliasi, B. Taeri, Four new sums of graphs and their Wiener indices, \textit{Discrete Appl. Math.}\textbf{157}(2009) 794--803.].
Self-learning Scene-specific Pedestrian Detectors using a Progressive Latent Model
Venue: arXiv cs.CV 2016
Year: 2016

In this paper, a self-learning approach is proposed towards solving scene-specific pedestrian detection problem without any human' annotation involved. The self-learning approach is deployed as progressive steps of object discovery, object enforcement, and label propagation. In the learning procedure, object locations in each frame are treated as latent variables that are solved with a progressive latent model (PLM). Compared with conventional latent models, the proposed PLM incorporates a spatial regularization term to reduce ambiguities in object proposals and to enforce object localization, and also a graph-based label propagation to discover harder instances in adjacent frames. With the difference of convex (DC) objective functions, PLM can be efficiently optimized with a concave-convex programming and thus guaranteeing the stability of self-learning. Extensive experiments demonstrate that even without annotation the proposed self-learning approach outperforms weakly supervised learning approaches, while achieving comparable performance with transfer learning and fully supervised approaches.
Mutable WadlerFest DOT
Venue: arXiv cs.PL 2016
Year: 2016

The Dependent Object Types (DOT) calculus aims to model the essence of Scala, with a focus on abstract type members, path-dependent types, and subtyping. Other Scala features could be defined by translation to DOT. Mutation is a fundamental feature of Scala currently missing in DOT. Mutation in DOT is needed not only to model effectful computation and mutation in Scala programs, but even to precisely specify how Scala initializes immutable variables and fields (vals). We present an extension to DOT that adds typed mutable reference cells. We have proven the extension sound with a mechanized proof in Coq. We present the key features of our extended calculus and its soundness proof, and discuss the challenges that we encountered in our search for a sound design and the alternative solutions that we considered.
Leveraging Parallel Data Processing Frameworks with Verified Lifting
Venue: arXiv cs.PL 2016
Year: 2016

Many parallel data frameworks have been proposed in recent years that let sequential programs access parallel processing. To capitalize on the benefits of such frameworks, existing code must often be rewritten to the domain-specific languages that each framework supports. This rewriting-tedious and error-prone-also requires developers to choose the framework that best optimizes performance given a specific workload. This paper describes Casper, a novel compiler that automatically retargets sequential Java code for execution on Hadoop, a parallel data processing framework that implements the MapReduce paradigm. Given a sequential code fragment, Casper uses verified lifting to infer a high-level summary expressed in our program specification language that is then compiled for execution on Hadoop. We demonstrate that Casper automatically translates Java benchmarks into Hadoop. The translated results execute on average 3.3x faster than the sequential implementations and scale better, as well, to larger datasets.
Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned
Venue: arXiv cs.SE 2016
Year: 2016

We summarise our experience developing and using Termite, the first reactive synthesis tool intended for use by software development practitioners. We identify the main barriers to making reactive synthesis accessible to software developers and describe the key features of Termite designed to overcome these barriers, including an imperative C-like specification language, an interactive source-level debugger, and a user-guided code generator. Based on our experience applying Termite to synthesising real-world reactive software, we identify several caveats of the practical use of the reactive synthesis technology. We hope that these findings will help define the agenda for future research on practical reactive synthesis.
SyGuS-Comp 2016: Results and Analysis
Venue: arXiv cs.SE 2016
Year: 2016

Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $φ$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition we added a new track devoted to programming by examples. This track consisted of two categories, one using the theory of bit-vectors and one using the theory of strings. This paper presents and analyses the results of SyGuS-Comp'16.
Mechanism Design for Multi-Type Housing Markets
Venue: arXiv cs.GT 2016
Year: 2016

We study multi-type housing markets, where there are $p\ge 2$ types of items, each agent is initially endowed one item of each type, and the goal is to design mechanisms without monetary transfer to (re)allocate items to the agents based on their preferences over bundles of items, such that each agent gets one item of each type. In sharp contrast to classical housing markets, previous studies in multi-type housing markets have been hindered by the lack of natural solution concepts, because the strict core might be empty. We break the barrier in the literature by leveraging AI techniques and making natural assumptions on agents' preferences. We show that when agents' preferences are lexicographic, even with different importance orders, the classical top-trading-cycles mechanism can be extended while preserving most of its nice properties. We also investigate computational complexity of checking whether an allocation is in the strict core and checking whether the strict core is empty. Our results convey an encouragingly positive message: it is possible to design good mechanisms for multi-type housing markets under natural assumptions on preferences.
On the Design and Optimization of an Autonomous Microgravity Enabling Aerial Robot
Venue: arXiv cs.RO 2016
Year: 2016

This paper describes the process and challenges behind the design and development of a micro-gravity enabling aerial robot. The vehicle, designed to provide at minimum 4 seconds of micro-gravity at an accuracy of .001 g's, is designed with suggestions and constraints from both academia and industry as well a regulatory agency. The feasibility of the flight mission is validated using a simulation environment, where models obtained from system identification of existing hardware are implemented to increase the fidelity of the simulation. The current development of a physical test bed is described. The vehicle employs both control and autonomy logic, which is developed in the Simulink environment and executed in a Pixhawk flight control board.
'Part'ly first among equals: Semantic part-based benchmarking for state-of-the-art object recognition systems
Venue: arXiv cs.CV 2016
Year: 2016

An examination of object recognition challenge leaderboards (ILSVRC, PASCAL-VOC) reveals that the top-performing classifiers typically exhibit small differences amongst themselves in terms of error rate/mAP. To better differentiate the top performers, additional criteria are required. Moreover, the (test) images, on which the performance scores are based, predominantly contain fully visible objects. Therefore, `harder' test images, mimicking the challenging conditions (e.g. occlusion) in which humans routinely recognize objects, need to be utilized for benchmarking. To address the concerns mentioned above, we make two contributions. First, we systematically vary the level of local object-part content, global detail and spatial context in images from PASCAL VOC 2010 to create a new benchmarking dataset dubbed PPSS-12. Second, we propose an object-part based benchmarking procedure which quantifies classifiers' robustness to a range of visibility and contextual settings. The benchmarking procedure relies on a semantic similarity measure that naturally addresses potential semantic granularity differences between the category labels in training and test datasets, thus eliminating manual mapping. We use our procedure on the PPSS-12 dataset to benchmark top-performing classifiers trained on the ILSVRC-2012 dataset. Our results show that the proposed benchmarking procedure enables additional differentiation among state-of-the-art object classifiers in terms of their ability to handle missing content and insufficient object detail. Given this capability for additional differentiation, our approach can potentially supplement existing benchmarking procedures used in object recognition challenge leaderboards.
Infinite Variational Autoencoder for Semi-Supervised Learning
Venue: arXiv cs.LG 2016
Year: 2016

This paper presents an infinite variational autoencoder (VAE) whose capacity adapts to suit the input data. This is achieved using a mixture model where the mixing coefficients are modeled by a Dirichlet process, allowing us to integrate over the coefficients when performing inference. Critically, this then allows us to automatically vary the number of autoencoders in the mixture based on the data. Experiments show the flexibility of our method, particularly for semi-supervised learning, where only a small number of training samples are available.
ATR4S: Toolkit with State-of-the-art Automatic Terms Recognition Methods in Scala
Venue: arXiv cs.CL 2016
Year: 2016

Automatically recognized terminology is widely used for various domain-specific texts processing tasks, such as machine translation, information retrieval or sentiment analysis. However, there is still no agreement on which methods are best suited for particular settings and, moreover, there is no reliable comparison of already developed methods. We believe that one of the main reasons is the lack of state-of-the-art methods implementations, which are usually non-trivial to recreate. In order to address these issues, we present ATR4S, an open-source software written in Scala that comprises more than 15 methods for automatic terminology recognition (ATR) and implements the whole pipeline from text document preprocessing, to term candidates collection, term candidates scoring, and finally, term candidates ranking. It is highly scalable, modular and configurable tool with support of automatic caching. We also compare 10 state-of-the-art methods on 7 open datasets by average precision and processing time. Experimental comparison reveals that no single method demonstrates best average precision for all datasets and that other available tools for ATR do not contain the best methods.
The World of Fast Moving Objects
Venue: arXiv cs.CV 2016
Year: 2016

The notion of a Fast Moving Object (FMO), i.e. an object that moves over a distance exceeding its size within the exposure time, is introduced. FMOs may, and typically do, rotate with high angular speed. FMOs are very common in sports videos, but are not rare elsewhere. In a single frame, such objects are often barely visible and appear as semi-transparent streaks. A method for the detection and tracking of FMOs is proposed. The method consists of three distinct algorithms, which form an efficient localization pipeline that operates successfully in a broad range of conditions. We show that it is possible to recover the appearance of the object and its axis of rotation, despite its blurred appearance. The proposed method is evaluated on a new annotated dataset. The results show that existing trackers are inadequate for the problem of FMO localization and a new approach is required. Two applications of localization, temporal super-resolution and highlighting, are presented.
Map-aided Dead-reckoning --- A Study on Locational Privacy in Insurance Telematics
Venue: arXiv cs.CR 2016
Year: 2016

We present a particle-based framework for estimating the position of a vehicle using map information and measurements of speed. Two measurement functions are considered. The first is based on the assumption that the lateral force on the vehicle does not exceed critical limits derived from physical constraints. The second is based on the assumption that the driver approaches a target speed derived from the speed limits along the upcoming trajectory. Performance evaluations of the proposed method indicate that end destinations often can be estimated with an accuracy in the order of $100\,[m]$. These results expose the sensitivity and commercial value of data collected in many of today's insurance telematics programs, and thereby have privacy implications for millions of policyholders. We end by discussing the strengths and weaknesses of different methods for anonymization and privacy preservation in telematics programs.