OpenRaiser/Intern-Atlas huggingface dataset:
Rank 3 Inhabitation of Intersection Types Revisited (Extended Version)
Venue: arXiv cs.LO 2017
Year: 2017

We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we strengthen the previous result by showing that intersection type inhabitation is undecidable for types of rank 3 and order 3, i.e. it is not necessary to introduce new functional dependencies (new instructions) during proof search. Second, we pinpoint the principles necessary to simulate Turing machine computation directly, whereas previous constructions used a highly parallel and non-deterministic computation model. Since our construction is more concise than existing approaches taking no detours, we believe that it is valuable for a better understanding of the expressiveness of intersection type inhabitation.
Applied Evaluative Informetrics: Part 1
Venue: arXiv cs.DL 2017
Year: 2017

This manuscript is a preprint version of Part 1 (General Introduction and Synopsis) of the book Applied Evaluative Informetrics, to be published by Springer in the summer of 2017. This book presents an introduction to the field of applied evaluative informetrics, and is written for interested scholars and students from all domains of science and scholarship. It sketches the field's history, recent achievements, and its potential and limits. It explains the notion of multi-dimensional research performance, and discusses the pros and cons of 28 citation-, patent-, reputation- and altmetrics-based indicators. In addition, it presents quantitative research assessment as an evaluation science, and focuses on the role of extra-informetric factors in the development of indicators, and on the policy context of their application. It also discusses the way forward, both for users and for developers of informetric tools.
DS++: A flexible, scalable and provably tight relaxation for matching problems
Venue: arXiv cs.GR 2017
Year: 2017

Correspondence problems are often modelled as quadratic optimization problems over permutations. Common scalable methods for approximating solutions of these NP-hard problems are the spectral relaxation for non-convex energies and the doubly stochastic (DS) relaxation for convex energies. Lately, it has been demonstrated that semidefinite programming relaxations can have considerably improved accuracy at the price of a much higher computational cost. We present a convex quadratic programming relaxation which is provably stronger than both DS and spectral relaxations, with the same scalability as the DS relaxation. The derivation of the relaxation also naturally suggests a projection method for achieving meaningful integer solutions which improves upon the standard closest-permutation projection. Our method can be easily extended to optimization over doubly stochastic matrices, partial or injective matching, and problems with additional linear constraints. We employ recent advances in optimization of linear-assignment type problems to achieve an efficient algorithm for solving the convex relaxation. We present experiments indicating that our method is more accurate than local minimization or competing relaxations for non-convex problems. We successfully apply our algorithm to shape matching and to the problem of ordering images in a grid, obtaining results which compare favorably with state of the art methods. We believe our results indicate that our method should be considered the method of choice for quadratic optimization over permutations.
An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution
Venue: arXiv cs.PL 2017
Year: 2017

There has been great progress recently in formally specifying the memory model of microprocessors like ARM and POWER. These specifications are, however, too complicated for reasoning about program behaviors, verifying compilers etc., because they involve microarchitectural details like the reorder buffer (ROB), partial and speculative execution, instruction replay on speculation failure, etc. In this paper we present a new Instantaneous Instruction Execution (I2E) framework which allows us to specify weak memory models in the same style as SC and TSO. Each instruction in I2E is executed instantaneously and in-order such that the state of the processor is always correct. The effect of instruction reordering is captured by the way data is moved between the processors and the memory non-deterministically, using three conceptual devices: invalidation buffers, timestamps and dynamic store buffers. We prove that I2E models capture the behaviors of modern microarchitectures and cache-coherent memory systems accurately, thus eliminating the need to think about microarchitectural details.
Data Access for LIGO on the OSG
Venue: arXiv cs.DC 2017
Year: 2017

During 2015 and 2016, the Laser Interferometer Gravitational-Wave Observatory (LIGO) conducted a three-month observing campaign. These observations delivered the first direct detection of gravitational waves from binary black hole mergers. To search for these signals, the LIGO Scientific Collaboration uses the PyCBC search pipeline. To deliver science results in a timely manner, LIGO collaborated with the Open Science Grid (OSG) to distribute the required computation across a series of dedicated, opportunistic, and allocated resources. To deliver the petabytes necessary for such a large-scale computation, our team deployed a distributed data access infrastructure based on the XRootD server suite and the CernVM File System (CVMFS). This data access strategy grew from simply accessing remote storage to a POSIX-based interface underpinned by distributed, secure caches across the OSG.
Transfer Learning for Named-Entity Recognition with Neural Networks
Venue: arXiv cs.CL 2017
Year: 2017

Recent approaches based on artificial neural networks (ANNs) have shown promising results for named-entity recognition (NER). In order to achieve high performances, ANNs need to be trained on a large labeled dataset. However, labels might be difficult to obtain for the dataset on which the user wants to perform NER: label scarcity is particularly pronounced for patient note de-identification, which is an instance of NER. In this work, we analyze to what extent transfer learning may address this issue. In particular, we demonstrate that transferring an ANN model trained on a large labeled dataset to another dataset with a limited number of labels improves upon the state-of-the-art results on two different datasets for patient note de-identification.
Supervised Machine Learning for Signals Having RRC Shaped Pulses
Venue: arXiv cs.IT 2017
Year: 2017

Classification performances of the supervised machine learning techniques such as support vector machines, neural networks and logistic regression are compared for modulation recognition purposes. The simple and robust features are used to distinguish continuous-phase FSK from QAM-PSK signals. Signals having root-raised-cosine shaped pulses are simulated in extreme noisy conditions having joint impurities of block fading, lack of symbol and sampling synchronization, carrier offset, and additive white Gaussian noise. The features are based on sample mean and sample variance of the imaginary part of the product of two consecutive complex signal values.
Matching Logic
Venue: arXiv cs.LO 2017
Year: 2017

This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, modal logic, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning with equality remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have an operational semantics, but it is not limited to this.
Plane Formation by Synchronous Mobile Robots without Chirality
Venue: arXiv cs.DC 2017
Year: 2017

We consider a distributed system consisting of autonomous mobile computing entities, called robots, moving in a specified space. The robots are anonymous, oblivious, and have neither any access to the global coordinate system nor any explicit communication medium. Each robot observes the positions of other robots and moves in terms of its local coordinate system. To investigate the self-organization power of robot systems, formation problems in the two dimensional space (2D-space) have been extensively studied. Yamauchi et al. (DISC 2015) introduced robot systems in the three dimensional space (3D-space). While existing results for 3D-space assume that the robots agree on the handedness of their local coordinate systems, we remove the assumption and consider the robots without chirality. One of the most fundamental agreement problems in 3D-space is the plane formation problem that requires the robots to land on a common plane, that is not predefined. It has been shown that the solvability of the plane formation problem by robots with chirality is determined by the rotation symmetry of their initial local coordinate systems because the robots cannot break it. We show that when the robots lack chirality, the combination of rotation symmetry and reflection symmetry determines the solvability of the plane formation problem because a set of symmetric local coordinate systems without chirality is obtained by rotations and reflections. This richer symmetry results in the increase of unsolvable instances compared with robots with chirality and a flaw of existing plane formation algorithm. In this paper, we give a characterization of initial configurations from which the robots without chirality can form a plane and a new plane formation algorithm for solvable instances.
Analysis of the effectiveness of the truth-spreading strategy for inhibiting rumors
Venue: arXiv cs.SI 2017
Year: 2017

Spreading truths is recognized as a feasible strategy for inhibiting rumors. This paper is devoted to assessing the effectiveness of the truth-spreading strategy. An individual-level rumor-truth spreading model (the generic URTU model) is derived. Under the model, two criteria for the termination of a rumor are presented. These criteria capture the influence of the network structures on the effectiveness of the truth-spreading strategy. Extensive simulations show that, when the rumor or the truth terminates, the dynamics of a simplified URTU model (the linear URTU model) fits well with the actual rumor-truth interplay process. Therefore, the generic URTU model forms a theoretical basis for assessing the effectiveness of the truth-spreading strategy for restraining rumors.
Sensor Array Design Through Submodular Optimization
Venue: arXiv cs.IT 2017
Year: 2017

We consider the problem of far-field sensing by means of a sensor array. Traditional array geometry design techniques are agnostic to prior information about the far-field scene. However, in many applications such priors are available and may be utilized to design more efficient array topologies. We formulate the problem of array geometry design with scene prior as one of finding a sampling configuration that enables efficient inference, which turns out to be a combinatorial optimization problem. While generic combinatorial optimization problems are NP-hard and resist efficient solvers, we show how for array design problems the theory of submodular optimization may be utilized to obtain efficient algorithms that are guaranteed to achieve solutions within a constant approximation factor from the optimum. We leverage the connection between array design problems and submodular optimization and port several results of interest. We demonstrate efficient methods for designing arrays with constraints on the sensing aperture, as well as arrays respecting combinatorial placement constraints. This novel connection between array design and submodularity suggests the possibility for utilizing other insights and techniques from the growing body of literature on submodular optimization in the field of array design.
Limited-Memory Matrix Adaptation for Large Scale Black-box Optimization
Venue: arXiv cs.NE 2017
Year: 2017

The Covariance Matrix Adaptation Evolution Strategy (CMA-ES) is a popular method to deal with nonconvex and/or stochastic optimization problems when the gradient information is not available. Being based on the CMA-ES, the recently proposed Matrix Adaptation Evolution Strategy (MA-ES) provides a rather surprising result that the covariance matrix and all associated operations (e.g., potentially unstable eigendecomposition) can be replaced in the CMA-ES by a updated transformation matrix without any loss of performance. In order to further simplify MA-ES and reduce its $\mathcal{O}\big(n^2\big)$ time and storage complexity to $\mathcal{O}\big(n\log(n)\big)$, we present the Limited-Memory Matrix Adaptation Evolution Strategy (LM-MA-ES) for efficient zeroth order large-scale optimization. The algorithm demonstrates state-of-the-art performance on a set of established large-scale benchmarks. We explore the algorithm on the problem of generating adversarial inputs for a (non-smooth) random forest classifier, demonstrating a surprising vulnerability of the classifier.
ADMM-Net: A Deep Learning Approach for Compressive Sensing MRI
Venue: arXiv cs.CV 2017
Year: 2017

Compressive sensing (CS) is an effective approach for fast Magnetic Resonance Imaging (MRI). It aims at reconstructing MR images from a small number of under-sampled data in k-space, and accelerating the data acquisition in MRI. To improve the current MRI system in reconstruction accuracy and speed, in this paper, we propose two novel deep architectures, dubbed ADMM-Nets in basic and generalized versions. ADMM-Nets are defined over data flow graphs, which are derived from the iterative procedures in Alternating Direction Method of Multipliers (ADMM) algorithm for optimizing a general CS-based MRI model. They take the sampled k-space data as inputs and output reconstructed MR images. Moreover, we extend our network to cope with complex-valued MR images. In the training phase, all parameters of the nets, e.g., transforms, shrinkage functions, etc., are discriminatively trained end-to-end. In the testing phase, they have computational overhead similar to ADMM algorithm but use optimized parameters learned from the data for CS-based reconstruction task. We investigate different configurations in network structures and conduct extensive experiments on MR image reconstruction under different sampling rates. Due to the combination of the advantages in model-based approach and deep learning approach, the ADMM-Nets achieve state-of-the-art reconstruction accuracies with fast computational speed.
Experimental Study on Low Power Wide Area Networks (LPWAN) for Mobile Internet of Things
Venue: arXiv cs.NI 2017
Year: 2017

In the past decade, we have witnessed explosive growth in the number of low-power embedded and Internet-connected devices, reinforcing the new paradigm, Internet of Things (IoT). The low power wide area network (LPWAN), due to its long-range, low-power and low-cost communication capability, is actively considered by academia and industry as the future wireless communication standard for IoT. However, despite the increasing popularity of `mobile IoT', little is known about the suitability of LPWAN for those mobile IoT applications in which nodes have varying degrees of mobility. To fill this knowledge gap, in this paper, we conduct an experimental study to evaluate, analyze, and characterize LPWAN in both indoor and outdoor mobile environments. Our experimental results indicate that the performance of LPWAN is surprisingly susceptible to mobility, even to minor human mobility, and the effect of mobility significantly escalates as the distance to the gateway increases. These results call for development of new mobility-aware LPWAN protocols to support mobile IoT.
Voltage-Driven Domain-Wall Motion based Neuro-Synaptic Devices for Dynamic On-line Learning
Venue: arXiv cs.ET 2017
Year: 2017

Conventional von-Neumann computing models have achieved remarkable feats for the past few decades. However, they fail to deliver the required efficiency for certain basic tasks like image and speech recognition when compared to biological systems. As such, taking cues from biological systems, novel computing paradigms are being explored for efficient hardware implementations of recognition/classification tasks. The basic building blocks of such neuromorphic systems are neurons and synapses. Towards that end, we propose a leaky-integrate-fire (LIF) neuron and a programmable non-volatile synapse using domain wall motion induced by magneto-electric effect. Due to a strong elastic pinning between the ferro-magnetic domain wall (FM-DW) and the underlying ferro-electric domain wall (FE-DW), the FM-DW gets dragged by the FE-DW on application of a voltage pulse. The fact that FE materials are insulators allows for pure voltage-driven FM-DW motion, which in turn can be used to mimic the behaviors of biological spiking neurons and synapses. The voltage driven nature of the proposed devices allows energy-efficient operation. A detailed device to system level simulation framework based on micromagnetic simulations has been developed to analyze the feasibility of the proposed neuro-synaptic devices. We also demonstrate that the energy-efficient voltage-controlled behavior of the proposed devices make them suitable for dynamic on-line and lifelong learning in spiking neural networks (SNNs).
Technical Report - MillimeterWave Communication in Vehicular Networks: Coverage and Connectivity Analysis
Venue: arXiv cs.NI 2017
Year: 2017

In this technical report (TR), we describe the mathematical model we developed to carry out a preliminary coverage and connectivity analysis in an automotive communication scenario based on mmWave links. The purpose is to exemplify some of the complex and interesting tradeoffs that have to be considered when designing solutions for mmWave automotive scenarios.
LinkedIn Salary: A System for Secure Collection and Presentation of Structured Compensation Insights to Job Seekers
Venue: arXiv cs.SI 2017
Year: 2017

Online professional social networks such as LinkedIn have enhanced the ability of job seekers to discover and assess career opportunities, and the ability of job providers to discover and assess potential candidates. For most job seekers, salary (or broadly compensation) is a crucial consideration in choosing a new job. At the same time, job seekers face challenges in learning the compensation associated with different jobs, given the sensitive nature of compensation data and the dearth of reliable sources containing compensation data. Towards the goal of helping the world's professionals optimize their earning potential through salary transparency, we present LinkedIn Salary, a system for collecting compensation information from LinkedIn members and providing compensation insights to job seekers. We present the overall design and architecture, and describe the key components needed for the secure collection, de-identification, and processing of compensation data, focusing on the unique challenges associated with privacy and security. We perform an experimental study with more than one year of compensation submission history data collected from over 1.5 million LinkedIn members, thereby demonstrating the tradeoffs between privacy and modeling needs. We also highlight the lessons learned from the production deployment of this system at LinkedIn.
A Lightweight Regression Method to Infer Psycholinguistic Properties for Brazilian Portuguese
Venue: arXiv cs.CL 2017
Year: 2017

Psycholinguistic properties of words have been used in various approaches to Natural Language Processing tasks, such as text simplification and readability assessment. Most of these properties are subjective, involving costly and time-consuming surveys to be gathered. Recent approaches use the limited datasets of psycholinguistic properties to extend them automatically to large lexicons. However, some of the resources used by such approaches are not available to most languages. This study presents a method to infer psycholinguistic properties for Brazilian Portuguese (BP) using regressors built with a light set of features usually available for less resourced languages: word length, frequency lists, lexical databases composed of school dictionaries and word embedding models. The correlations between the properties inferred are close to those obtained by related works. The resulting resource contains 26,874 words in BP annotated with concreteness, age of acquisition, imageability and subjective frequency.
Fundamental mode exact schemes for unsteady problems
Venue: arXiv cs.NA 2017
Year: 2017

The problem of increasing the accuracy of an approximate solution is considered for boundary value problems for parabolic equations. For ordinary differential equations (ODEs), nonstandard finite difference schemes are in common use for this problem. They are based on a modification of standard discretizations of time derivatives and, in some cases, allow to obtain the exact solution of problems. For multidimensional problems, we can consider the problem of increasing the accuracy only for the most important components of the approximate solution. In the present work, new unconditionally stable schemes for parabolic problems are constructed, which are exact for the fundamental mode. Such two-level schemes are designed via a modification of standard schemes with weights using Padé approximations. Numerical results obtained for a model problem demonstrate advantages of the proposed fundamental mode exact schemes.