OpenRaiser/Intern-Atlas huggingface dataset:
Asynchronous COMID: the theoretic basis for transmitted data sparsification tricks on Parameter Server
Venue: arXiv cs.DC 2017
Year: 2017

Asynchronous FTRL-proximal and L2 norm done at server are two widely used tricks in Parameters Server which is an implement of delayed SGD. Their commonness is leaving parts of updating computation on server which reduces the burden of network via making transmitted data sparse. But above tricks' convergences are not well-proved. In this paper, based on above commonness, we propose a more general algorithm named as asynchronous COMID and prove its convergence. We prove that asynchronous FTRL-proximal and L2 norm done at server are applications of asynchronous COMID, which demonstrates the convergences of above two tricks. Then, we conduct experiments to verify theoretical results. Experimental results show that compared with delayed SGD on Parameters Server, asynchronous COMID reduces the burden of the network without any harm on the mathematical convergence speed and final output.
Probabilistic Analysis Based On Symbolic Game Semantics and Model Counting
Venue: arXiv cs.PL 2017
Year: 2017

Probabilistic program analysis aims to quantify the probability that a given program satisfies a required property. It has many potential applications, from program understanding and debugging to computing program reliability, compiler optimizations and quantitative information flow analysis for security. In these situations, it is usually more relevant to quantify the probability of satisfying/violating a given property than to just assess the possibility of such events to occur. In this work, we introduce an approach for probabilistic analysis of open programs (i.e. programs with undefined identifiers) based on game semantics and model counting. We use a symbolic representation of algorithmic game semantics to collect the symbolic constraints on the input data (context) that lead to the occurrence of the target events (e.g. satisfaction/violation of a given property). The constraints are then analyzed to quantify how likely is an input to satisfy them. We use model counting techniques to count the number of solutions (from a bounded integer domain) that satisfy given constraints. These counts are then used to assign probabilities to program executions and to assess the probability for the target event to occur at the desired level of confidence. Finally, we present the results of applying our approach to several interesting examples and illustrate the benefits they may offer.
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
Venue: arXiv cs.GT 2017
Year: 2017

Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewriting each of these outcomes with either of two basic outcomes, namely that Player 1 wins or that Player 2 wins. If all ways of deriving such a win/lose game lead to a game where one player has a winning strategy, the original game also has a Nash equilibrium. This article makes three other contributions: first, while the original proof invoked linear extension of strict partial orders, here we avoid it by generalizing the relevant definition. Second, we notice that the theorem also implies the existence of a secure equilibrium, a stronger version of NE that was introduced for model checking. Third, we also notice that the constructive proof of the theorem computes secure equilibria for non-zero-sum priority games (generalizing parity games) in quasi-polynomial time.
A Parallel Linear Temporal Logic Tableau
Venue: arXiv cs.LO 2017
Year: 2017

For many applications, we are unable to take full advantage of the potential massive parallelisation offered by supercomputers or cloud computing because it is too hard to work out how to divide up the computation task between processors in such a way to minimise the need for communication. However, a recently developed branch-independent tableaux for the common LTL temporal logic should intuitively be easy to parallelise as each branch can be developed independently. Here we describe a simple technique for partitioning such a tableau such that each partition can be processed independently without need for interprocess communication. We investigate the extent to which this technique improves the performance of the LTL tableau on standard benchmarks and random formulas.
FingerNet: An Unified Deep Network for Fingerprint Minutiae Extraction
Venue: arXiv cs.CV 2017
Year: 2017

Minutiae extraction is of critical importance in automated fingerprint recognition. Previous works on rolled/slap fingerprints failed on latent fingerprints due to noisy ridge patterns and complex background noises. In this paper, we propose a new way to design deep convolutional network combining domain knowledge and the representation ability of deep learning. In terms of orientation estimation, segmentation, enhancement and minutiae extraction, several typical traditional methods performed well on rolled/slap fingerprints are transformed into convolutional manners and integrated as an unified plain network. We demonstrate that this pipeline is equivalent to a shallow network with fixed weights. The network is then expanded to enhance its representation ability and the weights are released to learn complex background variance from data, while preserving end-to-end differentiability. Experimental results on NIST SD27 latent database and FVC 2004 slap database demonstrate that the proposed algorithm outperforms the state-of-the-art minutiae extraction algorithms. Code is made publicly available at: https://github.com/felixTY/FingerNet.
On the detectability by novices, radiologists, and computer algorithms of smallest increases in local single dot size in random-dot images
Venue: arXiv cs.CY 2017
Year: 2017

Time-series of images may reveal important information about changes in medical or environmental conditions, depending on context. Visual inspection of images by humans (experts or laymen) may fail in detecting very small differences between images, yet, small but visually undetectable differences may carry important significance. Computer algorithms may help overcome this problem, and the use of computer driven image analysis in medical practice or for the tracking of small but critical changes in natural environments attracts a lot of interest. In many contexts relevant to society, the preprocessing of large sets of image series will soon no longer be the exclusive realm of a few scientists. Here we show that a metric obtained from self-organizing map analysis (SOM) of image contents in time series of images of one and the same object or environment reliably signals potentially critical local changes in images that may not be detectable visually by a layman or even an expert.
A Tight Lower Bound for Counting Hamiltonian Cycles via Matrix Rank
Venue: arXiv cs.DS 2017
Year: 2017

For even $k$, the matchings connectivity matrix $\mathbf{M}_k$ encodes which pairs of perfect matchings on $k$ vertices form a single cycle. Cygan et al. (STOC 2013) showed that the rank of $\mathbf{M}_k$ over $\mathbb{Z}_2$ is $Θ(\sqrt 2^k)$ and used this to give an $O^*((2+\sqrt{2})^{\mathsf{pw}})$ time algorithm for counting Hamiltonian cycles modulo $2$ on graphs of pathwidth $\mathsf{pw}$. The same authors complemented their algorithm by an essentially tight lower bound under the Strong Exponential Time Hypothesis (SETH). This bound crucially relied on a large permutation submatrix within $\mathbf{M}_k$, which enabled a "pattern propagation" commonly used in previous related lower bounds, as initiated by Lokshtanov et al. (SODA 2011). We present a new technique for a similar pattern propagation when only a black-box lower bound on the asymptotic rank of $\mathbf{M}_k$ is given; no stronger structural insights such as the existence of large permutation submatrices in $\mathbf{M}_k$ are needed. Given appropriate rank bounds, our technique yields lower bounds for counting Hamiltonian cycles (also modulo fixed primes $p$) parameterized by pathwidth. To apply this technique, we prove that the rank of $\mathbf{M}_k$ over the rationals is $4^k / \mathrm{poly}(k)$. We also show that the rank of $\mathbf{M}_k$ over $\mathbb{Z}_p$ is $Ω(1.97^k)$ for any prime $p\neq 2$ and even $Ω(2.15^k)$ for some primes. As a consequence, we obtain that Hamiltonian cycles cannot be counted in time $O^*((6-ε)^{\mathsf{pw}})$ for any $ε>0$ unless SETH fails. This bound is tight due to a $O^*(6^{\mathsf{pw}})$ time algorithm by Bodlaender et al. (ICALP 2013). Under SETH, we also obtain that Hamiltonian cycles cannot be counted modulo primes $p\neq 2$ in time $O^*(3.97^\mathsf{pw})$, indicating that the modulus can affect the complexity in intricate ways.
How Does Knowledge of the AUC Constrain the Set of Possible Ground-truth Labelings?
Venue: arXiv cs.LG 2017
Year: 2017

Recent work on privacy-preserving machine learning has considered how data-mining competitions such as Kaggle could potentially be "hacked", either intentionally or inadvertently, by using information from an oracle that reports a classifier's accuracy on the test set. For binary classification tasks in particular, one of the most common accuracy metrics is the Area Under the ROC Curve (AUC), and in this paper we explore the mathematical structure of how the AUC is computed from an n-vector of real-valued "guesses" with respect to the ground-truth labels. We show how knowledge of a classifier's AUC on the test set can constrain the set of possible ground-truth labelings, and we derive an algorithm both to compute the exact number of such labelings and to enumerate efficiently over them. Finally, we provide empirical evidence that, surprisingly, the number of compatible labelings can actually decrease as n grows, until a test set-dependent threshold is reached.
An Analysis of ISO 26262: Using Machine Learning Safely in Automotive Software
Venue: arXiv cs.AI 2017
Year: 2017

Machine learning (ML) plays an ever-increasing role in advanced automotive functionality for driver assistance and autonomous operation; however, its adequacy from the perspective of safety certification remains controversial. In this paper, we analyze the impacts that the use of ML as an implementation approach has on ISO 26262 safety lifecycle and ask what could be done to address them. We then provide a set of recommendations on how to adapt the standard to accommodate ML.
Network Vector: Distributed Representations of Networks with Global Context
Venue: arXiv cs.SI 2017
Year: 2017

We propose a neural embedding algorithm called Network Vector, which learns distributed representations of nodes and the entire networks simultaneously. By embedding networks in a low-dimensional space, the algorithm allows us to compare networks in terms of structural similarity and to solve outstanding predictive problems. Unlike alternative approaches that focus on node level features, we learn a continuous global vector that captures each node's global context by maximizing the predictive likelihood of random walk paths in the network. Our algorithm is scalable to real world graphs with many nodes. We evaluate our algorithm on datasets from diverse domains, and compare it with state-of-the-art techniques in node classification, role discovery and concept analogy tasks. The empirical results show the effectiveness and the efficiency of our algorithm.
Scalable Annotation of Fine-Grained Categories Without Experts
Venue: arXiv cs.HC 2017
Year: 2017

We present a crowdsourcing workflow to collect image annotations for visually similar synthetic categories without requiring experts. In animals, there is a direct link between taxonomy and visual similarity: e.g. a collie (type of dog) looks more similar to other collies (e.g. smooth collie) than a greyhound (another type of dog). However, in synthetic categories such as cars, objects with similar taxonomy can have very different appearance: e.g. a 2011 Ford F-150 Supercrew-HD looks the same as a 2011 Ford F-150 Supercrew-LL but very different from a 2011 Ford F-150 Supercrew-SVT. We introduce a graph based crowdsourcing algorithm to automatically group visually indistinguishable objects together. Using our workflow, we label 712,430 images by ~1,000 Amazon Mechanical Turk workers; resulting in the largest fine-grained visual dataset reported to date with 2,657 categories of cars annotated at 1/20th the cost of hiring experts.
Decentralized Robust Transceiver Designs for MISO SWIPT Interference Channel
Venue: arXiv cs.IT 2017
Year: 2017

This paper considers a $K$-user multiple-input single-output (MISO) interference channels for simultaneous wireless information and power transfer (SWIPT), where each multi-antenna transmitter serves a single-antenna receiver per user pair. All receivers perform simultaneously information processing and energy harvesting (EH) based on the receive power-splitting (PS) architectures. Assuming imperfect channel state information (CSI) at the transmitters, we develop an optimal robust transceiver design scheme that minimizes the total transmission power under the worst-case signal-to-interference-plus-noise ratio (SINR) and energy harvesting (EH) constraints at the receivers, by jointly optimizing transmit beamforming and receive PS ratio per receiver. When the CSI uncertainties are bounded by ellipsoidal regions, it is shown that the worst-case SINR and EH constraints per receiver can be recast into quadratic matrix inequality forms. Leveraging semidefinite relaxation technique, the intended robust beamforming and PS (BFPS) problem can be relaxed as a tractable (centralized) semidefinite program (SDP). More importantly, relying on the state-of-the-art alternating direction method of multipliers (ADMM) in convex optimization, we propose a {\em decentralized} algorithm capable of computing the optimal robust BFPS scheme with local CSI and limited information exchange among the transmitters. It is shown the proposed decentralized algorithm is guaranteed to converge to the optimal centralized solution. Numerical results are provided to demonstrate the merits of the proposed approaches.
FreeGuard: A Faster Secure Heap Allocator
Venue: arXiv cs.OS 2017
Year: 2017

In spite of years of improvements to software security, heap-related attacks still remain a severe threat. One reason is that many existing memory allocators fall short in a variety of aspects. For instance, performance-oriented allocators are designed with very limited countermeasures against attacks, but secure allocators generally suffer from significant performance overhead, e.g., running up to 10x slower. This paper, therefore, introduces FreeGuard, a secure memory allocator that prevents or reduces a wide range of heap-related attacks, such as heap overflows, heap over-reads, use-after-frees, as well as double and invalid frees. FreeGuard has similar performance to the default Linux allocator, with less than 2% overhead on average, but provides significant improvement to security guarantees. FreeGuard also addresses multiple implementation issues of existing secure allocators, such as the issue of scalability. Experimental results demonstrate that FreeGuard is very effective in defending against a variety of heap-related attacks.
A cost-effective rumor-containing strategy
Venue: arXiv cs.SI 2017
Year: 2017

This paper addresses the issue of suppressing a rumor using the truth in a cost-effective way. First, an individual-level dynamical model capturing the rumor-truth mixed spreading processes is proposed. On this basis, the cost-effective rumor-containing problem is modeled as an optimization problem. Extensive experiments show that finding a cost-effective rumor-containing strategy boils down to enhancing the first truth-spreading rate until the cost effectiveness of the rumor-containing strategy reaches the first turning point. This finding greatly reduces the time spent for solving the optimization problem. The influences of different factors on the optimal cost effectiveness of a rumor-containing strategy are examined through computer simulations. We believe our findings help suppress rumors in a cost-effective way. To our knowledge, this is the first time the rumor-containing problem is treated this way.
A Statistical Comparison of Some Theories of NP Word Order
Venue: arXiv cs.CL 2017
Year: 2017

A frequent object of study in linguistic typology is the order of elements {demonstrative, adjective, numeral, noun} in the noun phrase. The goal is to predict the relative frequencies of these orders across languages. Here we use Poisson regression to statistically compare some prominent accounts of this variation. We compare feature systems derived from Cinque (2005) to feature systems given in Cysouw (2010) and Dryer (in prep). In this setting, we do not find clear reasons to prefer the model of Cinque (2005) or Dryer (in prep), but we find both of these models have substantially better fit to the typological data than the model from Cysouw (2010).
On the exact relationship between the denoising function and the data distribution
Venue: arXiv cs.NE 2017
Year: 2017

We prove an exact relationship between the optimal denoising function and the data distribution in the case of additive Gaussian noise, showing that denoising implicitly models the structure of data allowing it to be exploited in the unsupervised learning of representations. This result generalizes a known relationship [2], which is valid only in the limit of small corruption noise.
GOOWE: Geometrically Optimum and Online-Weighted Ensemble Classifier for Evolving Data Streams
Venue: arXiv cs.LG 2017
Year: 2017

Designing adaptive classifiers for an evolving data stream is a challenging task due to the data size and its dynamically changing nature. Combining individual classifiers in an online setting, the ensemble approach, is a well-known solution. It is possible that a subset of classifiers in the ensemble outperforms others in a time-varying fashion. However, optimum weight assignment for component classifiers is a problem which is not yet fully addressed in online evolving environments. We propose a novel data stream ensemble classifier, called Geometrically Optimum and Online-Weighted Ensemble (GOOWE), which assigns optimum weights to the component classifiers using a sliding window containing the most recent data instances. We map vote scores of individual classifiers and true class labels into a spatial environment. Based on the Euclidean distance between vote scores and ideal-points, and using the linear least squares (LSQ) solution, we present a novel, dynamic, and online weighting approach. While LSQ is used for batch mode ensemble classifiers, it is the first time that we adapt and use it for online environments by providing a spatial modeling of online ensembles. In order to show the robustness of the proposed algorithm, we use real-world datasets and synthetic data generators using the MOA libraries. First, we analyze the impact of our weighting system on prediction accuracy through two scenarios. Second, we compare GOOWE with 8 state-of-the-art ensemble classifiers in a comprehensive experimental environment. Our experiments show that GOOWE provides improved reactions to different types of concept drift compared to our baselines. The statistical tests indicate a significant improvement in accuracy, with conservative time and memory requirements.
Advanced Page Rank Algorithm with Semantics, In Links, Out Links and Google Analytics
Venue: arXiv cs.SI 2017
Year: 2017

In this paper we have modified the existing page ranking mechanism as an advanced Page Rank Algorithm based on Semantics Inlinks Outlinks and Google Analytics. We have used Semantics page ranking to rank pages according to the word searched and match it with the metadata of the website and provide a value of rank according to the highest priority.We have also used Google analytics to store the number of hits of a website in a particular variable and add the required percentage amount to the ranking procedure.The proposed algorithm is used to find more relevant information according to users query.So this concept is very useful to display most valuable pages on the top of the result list on the basis of user browsing behaviour which reduce the search space to a large scale.
Insertion Sort with Self-reproducing Comparator P System
Venue: arXiv cs.ET 2017
Year: 2017

We present in this paper a self-reproducing comparator P~system that simulates insertion sort. The comparator $Π_c$ is a degree-2 membrane and structured as $μ= [_{h_0} [_{h_1}]_{h_1} [_{h_2}]_{h_2} ]_{h_0}$. A maximizing $Π_c$ compares two multisets $a$ and $b$ where $\min(|a|,|b|)$ is stored in compartment $h_1$ while $\max(|a|,|b|)$ is stored in compartment $h_2$. A conditional reproduction rule triggers $Π_c$ to clone itself out via compartment division followed by endocytosis of the cloned compartment. We present the process of sorting as a collection of transactions implemented in hierarchical levels where each level has different concurrent or serialized steps.
Urban morphology meets deep learning: Exploring urban forms in one million cities, town and villages across the planet
Venue: arXiv cs.CV 2017
Year: 2017

Study of urban form is an important area of research in urban planning/design that contributes to our understanding of how cities function and evolve. However, classical approaches are based on very limited observations and inconsistent methods. As an alternative, availability of massive urban data collections such as Open Street Map from the one hand and the recent advancements in machine learning methods such as deep learning techniques on the other have opened up new possibilities to automatically investigate urban forms at the global scale. In this work for the first time, by collecting a large data set of street networks in more than one million cities, towns and villages all over the world, we trained a deep convolutional auto-encoder, that automatically learns the hierarchical structures of urban forms and represents them via dense and comparable vectors. We showed how the learned urban vectors could be used for different investigations. Using the learned urban vectors, one is able to easily find and compare similar urban forms all over the world, considering their overall spatial structure and other factors such as orientation, graphical structure, and density and partial deformations. Further cluster analysis reveals the distribution of the main patterns of urban forms all over the planet.
Spectral and Energy Efficiency of Cell-Free Massive MIMO Systems with Hardware Impairments
Venue: arXiv cs.IT 2017
Year: 2017

Cell-free massive multiple-input multiple-output (MIMO), with a large number of distributed access points (APs) that jointly serve the user equipments (UEs), is a promising network architecture for future wireless communications. To reduce the cost and power consumption of such systems, it is important to utilize low-quality transceiver hardware at the APs. However, the impact of hardware impairments on cell-free massive MIMO has thus far not been studied. In this paper, we take a first look at this important topic by utilizing well-established models of hardware distortion and deriving new closed-form expressions for the spectral and energy efficiency. These expressions provide important insights into the practical impact of hardware impairments and also how to efficiently deploy cell-free systems. Furthermore, a novel hardware-quality scaling law is presented. It proves that the impact of hardware impairments at the APs vanish as the number of APs grows. Numerical results validate that cell-free massive MIMO systems are inherently resilient to hardware impairments.