OpenRaiser/Intern-Atlas huggingface dataset:
Towards the Automated Generation of Focused Proof Systems
Venue: arXiv cs.LO 2015
Year: 2015

This paper tackles the problem of formulating and proving the completeness of focused-like proof systems in an automated fashion. Focusing is a discipline on proofs which structures them into phases in order to reduce proof search non-determinism. We demonstrate that it is possible to construct a complete focused proof system from a given un-focused proof system if it satisfies some conditions. Our key idea is to generalize the completeness proof based on permutation lemmas given by Miller and Saurin for the focused linear logic proof system. This is done by building a graph from the rule permutation relation of a proof system, called permutation graph. We then show that from the permutation graph of a given proof system, it is possible to construct a complete focused proof system, and additionally infer for which formulas contraction is admissible. An implementation for building the permutation graph of a system is provided. We apply our technique to generate the focused proof systems MALLF, LJF and LKF for linear, intuitionistic and classical logics, respectively.
Standard methods for inexpensive pollen loads authentication by means of computer vision and machine learning
Venue: arXiv cs.CV 2015
Year: 2015

We present a complete methodology for authenticating local bee pollen against fraudulent samples using image processing and machine learning techniques. The proposed standard methods do not need expensive equipment such as advanced microscopes and can be used for a preliminary fast rejection of unknown pollen types. The system is able to rapidly reject the non-local pollen samples with inexpensive hardware and without the need to send the product to the laboratory. Methods are based on the color properties of bee pollen loads images and the use of one-class classifiers which are appropriate to reject unknown pollen samples when there is limited data about them. The validation of the method is carried out by authenticating Spanish bee pollen types. Experimentation shows that the proposed methods can obtain an overall authentication accuracy of 94%. We finally illustrate the user interaction with the software in some practical cases by showing the developed application prototype.
Large Scale Artificial Neural Network Training Using Multi-GPUs
Venue: arXiv cs.DC 2015
Year: 2015

This paper describes a method for accelerating large scale Artificial Neural Networks (ANN) training using multi-GPUs by reducing the forward and backward passes to matrix multiplication. We propose an out-of-core multi-GPU matrix multiplication and integrate the algorithm with the ANN training. The experiments demonstrate that our matrix multiplication algorithm achieves linear speedup on multiple inhomogeneous GPUs. The full paper of this project can be found at [1].
An Efficient Assignment of Drainage Direction Over Flat Surfaces in Raster Digital Elevation Models
Venue: arXiv cs.DS 2015
Year: 2015

In processing raster digital elevation models (DEMs) it is often necessary to assign drainage directions over flats---that is, over regions with no local elevation gradient. This paper presents an approach to drainage direction assignment which is not restricted by a flat's shape, number of outlets, or surrounding topography. Flow is modeled by superimposing a gradient away from higher terrain with a gradient towards lower terrain resulting in a drainage field exhibiting flow convergence, an improvement over methods which produce regions of parallel flow. This approach builds on previous work by Garbrecht and Martz (1997), but presents several important improvements. The improved algorithm guarantees that flats are only resolved if they have outlets. The algorithm does not require iterative application; a single pass is sufficient to resolve all flats. The algorithm presents a clear strategy for identifying flats and their boundaries. The algorithm is not susceptible to loss of floating-point precision. Furthermore, the algorithm is efficient, operating in O( N ) time whereas the older algorithm operates in O( N^(3/2) ) time. In testing, the improved algorithm ran 6.5 times faster than the old for a 100 x 100 cell flat and 69 times faster for a 700 x 700 cell flat. In tests on actual DEMs, the improved algorithm finished its processing 38--110 times sooner while running on a single processor than a parallel implementation of the old algorithm did while running on 16 processors. The improved algorithm is an optimal, accurate, easy-to-implement drop-in replacement for the original. Pseudocode is provided in the paper and working source code is provided in the Supplemental Materials.
The Ranking Problem of Alternatives as a Cooperative Game
Venue: arXiv cs.GT 2015
Year: 2015

This paper considers the ranking problem of candidates for a certain position based on ballot papers filled by voters. We suggest a ranking procedure of alternatives using cooperative game theory methods. For this, it is necessary to construct a characteristic function via the filled ballot paper profile of voters. The Shapley value serves as the ranking method. The winner is the candidate having the maximum Shapley value. And finally, we explore the properties of the designed ranking procedure.
Mathematical model stabilization control of a robot due to the delay of the control signal
Venue: arXiv cs.SY 2015
Year: 2015

Consider the question of building a system of commands remotely controlled robot that can perform motion stabilization in the presence of a constant delay of the control signal.
Priority-Flood: An Optimal Depression-Filling and Watershed-Labeling Algorithm for Digital Elevation Models
Venue: arXiv cs.DS 2015
Year: 2015

Depressions (or pits) are low areas within a digital elevation model that are surrounded by higher terrain, with no outlet to lower areas. Filling them so they are level, as fluid would fill them if the terrain were impermeable, is often necessary in preprocessing DEMs. The depression-filling algorithm presented here---called Priority-Flood---unifies and improves on the work of a number of previous authors who have published similar algorithms. The algorithm operates by flooding DEMs inwards from their edges using a priority queue to determine the next cell to be flooded. The resultant DEM has no depressions or digital dams: every cell is guaranteed to drain. The algorithm is optimal for both integer and floating-point data, working in O(n) and O(n lg n) time, respectively. It is shown that by using a plain queue to fill depressions once they have been found, an O(m lg m) time-complexity can be achieved, where m does not exceed the number of cells n. This is the lowest time complexity of any known floating-point depression-filling algorithm. In testing, this improved variation of the algorithm performed up to 37% faster than the original. Additionally, a parallel version of an older, but widely-used depression-filling algorithm required six parallel processors to achieve a run-time on par with what the newer algorithm's improved variation took on a single processor. The Priority-Flood Algorithm is simple to understand and implement: the included pseudocode is only 20 lines and the included C++ reference implementation is under a hundred lines. The algorithm can work on irregular meshes as well as 4-, 6-, 8-, and n-connected grids. It can also be adapted to label watersheds and determine flow directions through either incremental elevation changes or depression carving. In the case of incremental elevation changes, the algorithm includes safety checks not present in prior works.
Solving Jigsaw Puzzles with Linear Programming
Venue: arXiv cs.CV 2015
Year: 2015

We propose a novel Linear Program (LP) based formula- tion for solving jigsaw puzzles. We formulate jigsaw solving as a set of successive global convex relaxations of the stan- dard NP-hard formulation, that can describe both jigsaws with pieces of unknown position and puzzles of unknown po- sition and orientation. The main contribution and strength of our approach comes from the LP assembly strategy. In contrast to existing greedy methods, our LP solver exploits all the pairwise matches simultaneously, and computes the position of each piece/component globally. The main ad- vantages of our LP approach include: (i) a reduced sensi- tivity to local minima compared to greedy approaches, since our successive approximations are global and convex and (ii) an increased robustness to the presence of mismatches in the pairwise matches due to the use of a weighted L1 penalty. To demonstrate the effectiveness of our approach, we test our algorithm on public jigsaw datasets and show that it outperforms state-of-the-art methods.
Multi-Clique-Width
Venue: arXiv cs.DM 2015
Year: 2015

Multi-clique-width is obtained by a simple modification in the definition of clique-width. It has the advantage of providing a natural extension of tree-width. Unlike clique-width, it does not explode exponentially compared to tree-width. Efficient algorithms based on multi-clique-width are still possible for interesting tasks like computing the independent set polynomial or testing $c$-colorability. In particular, $c$-colorability can be tested in time linear in $n$ and singly exponential in $c$ and the width $k$ of a given multi-$k$-expression. For these tasks, the running time as a function of the multi-clique-width is the same as the running time of the fastest known algorithm as a function of the clique-width. This results in an exponential speed-up for some graphs, if the corresponding graph generating expressions are given. The reason is that the multi-clique-width is never bigger, but is exponentially smaller than the clique-width for many graphs. This gap shows up when the tree-width is basically equal to the multi-clique width as well as when the tree-width is not bounded by any function of the clique-width.
Reversible Recursive Instance-level Object Segmentation
Venue: arXiv cs.CV 2015
Year: 2015

In this work, we propose a novel Reversible Recursive Instance-level Object Segmentation (R2-IOS) framework to address the challenging instance-level object segmentation task. R2-IOS consists of a reversible proposal refinement sub-network that predicts bounding box offsets for refining the object proposal locations, and an instance-level segmentation sub-network that generates the foreground mask of the dominant object instance in each proposal. By being recursive, R2-IOS iteratively optimizes the two sub-networks during joint training, in which the refined object proposals and improved segmentation predictions are alternately fed into each other to progressively increase the network capabilities. By being reversible, the proposal refinement sub-network adaptively determines an optimal number of refinement iterations required for each proposal during both training and testing. Furthermore, to handle multiple overlapped instances within a proposal, an instance-aware denoising autoencoder is introduced into the segmentation sub-network to distinguish the dominant object from other distracting instances. Extensive experiments on the challenging PASCAL VOC 2012 benchmark well demonstrate the superiority of R2-IOS over other state-of-the-art methods. In particular, the $\text{AP}^r$ over $20$ classes at $0.5$ IoU achieves $66.7\%$, which significantly outperforms the results of $58.7\%$ by PFN~\cite{PFN} and $46.3\%$ by~\cite{liu2015multi}.
On the Computational Complexity of Optimal Simple Mechanisms
Venue: arXiv cs.GT 2015
Year: 2015

We consider a monopolist seller facing a single buyer with additive valuations over n heterogeneous, independent items. It is known that in this important setting optimal mechanisms may require randomization [HR12], use menus of infinite size [DDT15], and may be computationally intractable [DDT14]. This has sparked recent interest in finding simple mechanisms that obtain reasonable approximations to the optimal revenue [HN12, LY13, BILW14]. In this work we attempt to find the optimal simple mechanism. There are many ways to define simple mechanisms. Here we restrict our search to partition mechanisms, where the seller partitions the items into disjoint bundles and posts a price for each bundle; the buyer is allowed to buy any number of bundles. We give a PTAS for the problem of finding a revenue-maximizing partition mechanism, and prove that the problem is strongly NP-hard. En route, we prove structural properties of near-optimal partition mechanisms which may be of independent interest: for example, there always exists a near-optimal partition mechanism that uses only a constant number of non-trivial bundles (i.e. bundles with more than one item).
Job-related discourse on social media
Venue: arXiv cs.SI 2015
Year: 2015

Working adults spend nearly one third of their daily time at their jobs. In this paper, we study job-related social media discourse from a community of users. We use both crowdsourcing and local expertise to train a classifier to detect job-related messages on Twitter. Additionally, we analyze the linguistic differences in a job-related corpus of tweets between individual users vs. commercial accounts. The volumes of job-related tweets from individual users indicate that people use Twitter with distinct monthly, daily, and hourly patterns. We further show that the moods associated with jobs, positive and negative, have unique diurnal rhythms.
Budget Online Multiple Kernel Learning
Venue: arXiv cs.LG 2015
Year: 2015

Online learning with multiple kernels has gained increasing interests in recent years and found many applications. For classification tasks, Online Multiple Kernel Classification (OMKC), which learns a kernel based classifier by seeking the optimal linear combination of a pool of single kernel classifiers in an online fashion, achieves superior accuracy and enjoys great flexibility compared with traditional single-kernel classifiers. Despite being studied extensively, existing OMKC algorithms suffer from high computational cost due to their unbounded numbers of support vectors. To overcome this drawback, we present a novel framework of Budget Online Multiple Kernel Learning (BOMKL) and propose a new Sparse Passive Aggressive learning to perform effective budget online learning. Specifically, we adopt a simple yet effective Bernoulli sampling to decide if an incoming instance should be added to the current set of support vectors. By limiting the number of support vectors, our method can significantly accelerate OMKC while maintaining satisfactory accuracy that is comparable to that of the existing OMKC algorithms. We theoretically prove that our new method achieves an optimal regret bound in expectation, and empirically found that the proposed algorithm outperforms various OMKC algorithms and can easily scale up to large-scale datasets.
Optimum Transmission Through the Multiple-Antenna Gaussian Multiple Access Channel
Venue: arXiv cs.IT 2015
Year: 2015

This paper studies the optimal points in the capacity region of Gaussian multiple access channels (GMACs) with constant fading, multiple antennas and various power constraints. The points of interest maximize general rate objectives that arise in practical communication scenarios. Achieving these points constitutes the task of jointly optimizing the time-sharing parameters, the input covariance matrices and the order of decoding used by the successive interference cancellation receiver. To approach this problem, Carathéodory's theorem is invoked to represent time-sharing and decoding orders jointly as a finite-dimensional matrix variable. This variable enables us to use variational inequalities to extend results pertaining to problems with linear rate objectives to more general, potentially nonconvex, problems, and to obtain a necessary and sufficient condition for the optimality of the transmission parameters in a wide range of problems. Using the insights gained from this condition, we develop and analyze the convergence of an algorithm for solving, otherwise daunting, GMAC-based optimization problems.
A Polynomial Lower Bound for Testing Monotonicity
Venue: arXiv cs.CC 2015
Year: 2015

We show that every algorithm for testing $n$-variate Boolean functions for monotonicity must have query complexity $\tildeΩ(n^{1/4})$. All previous lower bounds for this problem were designed for non-adaptive algorithms and, as a result, the best previous lower bound for general (possibly adaptive) monotonicity testers was only $Ω(\log n)$. Combined with the query complexity of the non-adaptive monotonicity tester of Khot, Minzer, and Safra (FOCS 2015), our lower bound shows that adaptivity can result in at most a quadratic reduction in the query complexity for testing monotonicity. By contrast, we show that there is an exponential gap between the query complexity of adaptive and non-adaptive algorithms for testing regular linear threshold functions (LTFs) for monotonicity. Chen, De, Servedio, and Tan (STOC 2015) recently showed that non-adaptive algorithms require almost $Ω(n^{1/2})$ queries for this task. We introduce a new adaptive monotonicity testing algorithm which has query complexity $O(\log n)$ when the input is a regular LTF.
Minimum Eccentricity Shortest Paths in some Structured Graph Classes
Venue: arXiv cs.DM 2015
Year: 2015

We investigate the Minimum Eccentricity Shortest Path problem in some structured graph classes. It asks for a given graph to find a shortest path with minimum eccentricity. Although it is NP-hard in general graphs, we demonstrate that a minimum eccentricity shortest path can be found in linear time for distance-hereditary graphs (generalizing the previous result for trees) and give a generalised approach which allows to solve the problem in polynomial time for other graph classes. This includes chordal graphs, dually chordal graphs, graphs with bounded tree-length, and graphs with bounded hyperbolicity. Additionally, we give a simple algorithm to compute an additive approximation for graphs with bounded tree-length and graphs with bounded hyperbolicity.
Completeness of Randomized Kinodynamic Planners with State-based Steering
Venue: arXiv cs.RO 2015
Year: 2015

Probabilistic completeness is an important property in motion planning. Although it has been established with clear assumptions for geometric planners, the panorama of completeness results for kinodynamic planners is still incomplete, as most existing proofs rely on strong assumptions that are difficult, if not impossible, to verify on practical systems. In this paper, we focus on an important class of kinodynamic planners, namely those that interpolate trajectories in the state space. We provide a proof of probabilistic completeness for these planners under assumptions that can be readily verified from the system's equations of motion and the user-defined interpolation function. Our proof relies crucially on a property of interpolated trajectories, termed second-order continuity (SOC), which we show is tightly related to the ability of a planner to benefit from denser sampling. We analyze the impact of this property in simulations on a low-torque pendulum. Our results show that a simple RRT using a second-order continuous interpolation swiftly finds solution, while it is impossible for the same planner using standard Bezier curves (which are not SOC) to find any solution.
Classifying and Segmenting Microscopy Images Using Convolutional Multiple Instance Learning
Venue: arXiv cs.CV 2015
Year: 2015

Convolutional neural networks (CNN) have achieved state of the art performance on both classification and segmentation tasks. Applying CNNs to microscopy images is challenging due to the lack of datasets labeled at the single cell level. We extend the application of CNNs to microscopy image classification and segmentation using multiple instance learning (MIL). We present the adaptive Noisy-AND MIL pooling function, a new MIL operator that is robust to outliers. Combining CNNs with MIL enables training CNNs using full resolution microscopy images with global labels. We base our approach on the similarity between the aggregation function used in MIL and pooling layers used in CNNs. We show that training MIL CNNs end-to-end outperforms several previous methods on both mammalian and yeast microscopy images without requiring any segmentation steps.
Research of the Correlation between the H1N1 Morbidity Data and Google Trends in Egypt
Venue: arXiv cs.SI 2015
Year: 2015

The search engine based on influenza monitoring system has been widely applied in many European and American countries. However, there are not any correlative researches reported for African developing countries. Especially, the countries Egypt has not designed an influenza monitoring system on the basis of the Internet search data. This study aims at analyzing the correlation between the Google search data and the H1N1 morbidity data of Egypt, and examining the feasibility of Google Flu Model in predicting the H1N1 influenza trend.
Accelerating Random Kaczmarz Algorithm Based on Clustering Information
Venue: arXiv cs.NA 2015
Year: 2015

Kaczmarz algorithm is an efficient iterative algorithm to solve overdetermined consistent system of linear equations. During each updating step, Kaczmarz chooses a hyperplane based on an individual equation and projects the current estimate for the exact solution onto that space to get a new estimate. Many vairants of Kaczmarz algorithms are proposed on how to choose better hyperplanes. Using the property of randomly sampled data in high-dimensional space, we propose an accelerated algorithm based on clustering information to improve block Kaczmarz and Kaczmarz via Johnson-Lindenstrauss lemma. Additionally, we theoretically demonstrate convergence improvement on block Kaczmarz algorithm.
On the Existence of Tree Backbones that Realize the Chromatic Number on a Backbone Coloring
Venue: arXiv cs.DM 2015
Year: 2015

A proper $k$-coloring of a graph $G=(V,E)$ is a function $c: V(G)\to \{1,\ldots,k\}$ such that $c(u)\neq c(v)$, for every $uv\in E(G)$. The chromatic number $χ(G)$ is the minimum $k$ such that there exists a proper $k$-coloring of $G$. Given a spanning subgraph $H$ of $G$, a $q$-backbone $k$-coloring of $(G,H)$ is a proper $k$-coloring $c$ of $V(G)$ such that $\lvert c(u)-c(v)\rvert \ge q$, for every edge $uv\in E(H)$. The $q$-backbone chromatic number $BBC_q(G,H)$ is the smallest $k$ for which there exists a $q$-backbone $k$-coloring of $(G,H)$. In this work, we show that every connected graph $G$ has a generating tree $T$ such that $BBC_q(G,T) = \max\{χ(G),\left\lceil\frac{χ(G)}{2}\right\rceil+q\}$, and that this value is the best possible. As a direct consequence, we get that every connected graph $G$ has a spanning tree $T$ for which $BBC_2(G,T)=χ(G)$, if $χ(G)\ge 4$, or $BBC_2(G,T)=χ(G)+1$, otherwise. Thus, by applying the Four Color Theorem, we have that every connected nonbipartite planar graph $G$ has a spanning tree $T$ such that $BBC_2(G,T)=4$. This settles a question by Wang, Bu, Montassier and Raspaud (2012), and generalizes a number of previous partial results to their question.
PPV modelling of memristor-based oscillator
Venue: arXiv cs.ET 2015
Year: 2015

In this letter, we propose for the first time a method of abstracting the PPV (Perturbation Projection Vector) characteristic of the up-to-date memristor-based oscillators. Inspired from biological oscillators and its characteristic named PRC (Phase Response Curve), we build a bridge between PRC and PPV. This relationship is verified rigorously using the transistor level simulation of Colpitts and ring oscillators, i.e., comparing the PPV converted from PRC and the PPV obtained from accurate PSS+PXF simulation. Then we apply this method to the PPV calculation of the memristor-based oscillator. By keeping the phase dynamics of the oscillator and dropping the details of voltage/current amplitude, the PPV modelling is highly efficient to describe the phase dynamics due to the oscillator coupling, and will be very suitable for the fast simulation of large scale oscillatory neural networks.