OpenRaiser/Intern-Atlas huggingface dataset:
PSC: A Pattern-Based Temporal and Spatial Crowdsourcing Platform to Improve Performance, Reliability, and Privacy
Venue: arXiv cs.SI 2015
Year: 2015

In this paper, we study a novel spatial crowdsourcing system where the workers' time availabilities and their spatial locations are known a priori. Consequently, the tasks assignment to workers is performed not only based on the current location of the human workers and the tasks available in the region, but also based on the availability of the workers during the specific times that a given task should be accepted, processed, and completed. Having the system determine the daily pattern of the workers (either by predefined questionnaires when the workers register, or by archiving data from the worker's mobile devices, or by on the road and real-time entered status data) eliminates many unsuccessful task assignments and therefore significantly increases the efficiency of the system. In the original Spatial Crowdsourcing (SC) framework, the SC-server optimizes the task assignment locally at every instance of time and whenever a new task, or a new worker, enters the system. Our new framework (PSC), on the other hand, allows the users to enter their daily routine, and temporal, spatial, and availability patterns a priori. This makes the system much more stable and pattern-opportunistic. The PSC servers can focus on receiving and archiving new entries (e.g., workers, tasks, and their criteria) during busy times (e.g., when there are many new entries in the system), and can focus on optimization and computations during quiet times (e.g., when there are fewer new entries in the system). Having the task optimization process happen during quiet times, and when there are few changes to the system, makes the performance more stable and reliable. It also allows the PSC system to have a global view of the system and and perform global optimizations to improve the performance.
A framework for proof certificates in finite state exploration
Venue: arXiv cs.LO 2015
Year: 2015

Model checkers use automated state exploration in order to prove various properties such as reachability, non-reachability, and bisimulation over state transition systems. While model checkers have proved valuable for locating errors in computer models and specifications, they can also be used to prove properties that might be consumed by other computational logic systems, such as theorem provers. In such a situation, a prover must be able to trust that the model checker is correct. Instead of attempting to prove the correctness of a model checker, we ask that it outputs its "proof evidence" as a formally defined document--a proof certificate--and that this document is checked by a trusted proof checker. We describe a framework for defining and checking proof certificates for a range of model checking problems. The core of this framework is a (focused) proof system that is augmented with premises that involve "clerk and expert" predicates. This framework is designed so that soundness can be guaranteed independently of any concerns for the correctness of the clerk and expert specifications. To illustrate the flexibility of this framework, we define and formally check proof certificates for reachability and non-reachability in graphs, as well as bisimulation and non-bisimulation for labeled transition systems. Finally, we describe briefly a reference checker that we have implemented for this framework.
Translating HOL to Dedukti
Venue: arXiv cs.LO 2015
Year: 2015

Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate the proofs of a family of HOL proof assistants to Dedukti. The translation preserves binding, typing, and reduction. We implemented this translation in an automated tool and used it to successfully translate the OpenTheory standard library.
An Optimal Algorithm for Bandit and Zero-Order Convex Optimization with Two-Point Feedback
Venue: arXiv cs.LG 2015
Year: 2015

We consider the closely related problems of bandit convex optimization with two-point feedback, and zero-order stochastic convex optimization with two function evaluations per round. We provide a simple algorithm and analysis which is optimal for convex Lipschitz functions. This improves on \cite{dujww13}, which only provides an optimal result for smooth functions; Moreover, the algorithm and analysis are simpler, and readily extend to non-Euclidean problems. The algorithm is based on a small but surprisingly powerful modification of the gradient estimator.
Multimodal Multipart Learning for Action Recognition in Depth Videos
Venue: arXiv cs.CV 2015
Year: 2015

The articulated and complex nature of human actions makes the task of action recognition difficult. One approach to handle this complexity is dividing it to the kinetics of body parts and analyzing the actions based on these partial descriptors. We propose a joint sparse regression based learning method which utilizes the structured sparsity to model each action as a combination of multimodal features from a sparse set of body parts. To represent dynamics and appearance of parts, we employ a heterogeneous set of depth and skeleton based features. The proper structure of multimodal multipart features are formulated into the learning framework via the proposed hierarchical mixed norm, to regularize the structured features of each part and to apply sparsity between them, in favor of a group feature selection. Our experimental results expose the effectiveness of the proposed learning method in which it outperforms other methods in all three tested datasets while saturating one of them by achieving perfect accuracy.
Fast Stochastic Algorithms for SVD and PCA: Convergence Properties and Convexity
Venue: arXiv cs.LG 2015
Year: 2015

We study the convergence properties of the VR-PCA algorithm introduced by \cite{shamir2015stochastic} for fast computation of leading singular vectors. We prove several new results, including a formal analysis of a block version of the algorithm, and convergence from random initialization. We also make a few observations of independent interest, such as how pre-initializing with just a single exact power iteration can significantly improve the runtime of stochastic methods, and what are the convexity and non-convexity properties of the underlying optimization problem.
A control theoretic approach to achieve proportional fairness in 802.11e EDCA WLANs
Venue: arXiv cs.NI 2015
Year: 2015

This paper considers proportional fairness amongst ACs in an EDCA WLAN for provision of distinct QoS requirements and priority parameters. A detailed theoretical analysis is provided to derive the optimal station attempt probability which leads to a proportional fair allocation of station throughputs. The desirable fairness can be achieved using a centralised adaptive control approach. This approach is based on multivariable statespace control theory and uses the Linear Quadratic Integral (LQI) controller to periodically update CWmin till the optimal fair point of operation. Performance evaluation demonstrates that the control approach has high accuracy performance and fast convergence speed for general network scenarios. To our knowledge this might be the first time that a closed-loop control system is designed for EDCA WLANs to achieve proportional fairness.
Achieving proportional fairness with a control theoretic approach in error-prone 802.11e WLANs
Venue: arXiv cs.NI 2015
Year: 2015

This letter proposes a control theoretic approach to achieve proportional fairness amongst access categories (ACs) in an error-prone EDCA WLAN for provision of distinct QoS requirements and priority parameters. The approach adaptively adjusts the minimum contention window of each AC to derive the station attempt probability to its optimum which leads to a proportional fair allocation of station throughputs. Evaluation results demonstrate that the proposed control approach has high accuracy performance and fast convergence speed for general network scenarios.
Efficient and robust calibration of the Heston option pricing model for American options using an improved Cuckoo Search Algorithm
Venue: arXiv cs.NE 2015
Year: 2015

In this paper an improved Cuckoo Search Algorithm is developed to allow for an efficient and robust calibration of the Heston option pricing model for American options. Calibration of stochastic volatility models like the Heston is significantly harder than classical option pricing models as more parameters have to be estimated. The difficult task of calibrating one of these models to American Put options data is the main objective of this paper. Numerical results are shown to substantiate the suitability of the chosen method to tackle this problem.
Artificial Neural Networks Applied to Taxi Destination Prediction
Venue: arXiv cs.LG 2015
Year: 2015

We describe our first-place solution to the ECML/PKDD discovery challenge on taxi destination prediction. The task consisted in predicting the destination of a taxi based on the beginning of its trajectory, represented as a variable-length sequence of GPS points, and diverse associated meta-information, such as the departure time, the driver id and client information. Contrary to most published competitor approaches, we used an almost fully automated approach based on neural networks and we ranked first out of 381 teams. The architectures we tried use multi-layer perceptrons, bidirectional recurrent neural networks and models inspired from recently introduced memory networks. Our approach could easily be adapted to other applications in which the goal is to predict a fixed-length output from a variable-length sequence.
An Analysis of Device-Free and Device-Based WiFi-Localization Systems
Venue: arXiv cs.NI 2015
Year: 2015

WiFi-based localization became one of the main indoor localization techniques due to the ubiquity of WiFi connectivity. However, indoor environments exhibit complex wireless propagation characteristics. Typically, these characteristics are captured by constructing a fingerprint map for the different locations in the area of interest. This fingerprint requires significant overhead in manual construction, and thus has been one of the major drawbacks of WiFi-based localization. In this paper, we present an automated tool for fingerprint constructions and leverage it to study novel scenarios for device-based and device-free WiFi-based localization that are difficult to evaluate in a real environment. In a particular, we examine the effect of changing the access points (AP) mounting location, AP technology upgrade, crowd effect on calibration and operation, among others; on the accuracy of the localization system. We present the analysis for the two classes of WiFi-based localization: device-based and device-free. Our analysis highlights factors affecting the localization system accuracy, how to tune it for better localization, and provides insights for both researchers and practitioners.
Mixed Logical and Probabilistic Reasoning for Planning and Explanation Generation in Robotics
Venue: arXiv cs.RO 2015
Year: 2015

Robots assisting humans in complex domains have to represent knowledge and reason at both the sensorimotor level and the social level. The architecture described in this paper couples the non-monotonic logical reasoning capabilities of a declarative language with probabilistic belief revision, enabling robots to represent and reason with qualitative and quantitative descriptions of knowledge and degrees of belief. Specifically, incomplete domain knowledge, including information that holds in all but a few exceptional situations, is represented as a Answer Set Prolog (ASP) program. The answer set obtained by solving this program is used for inference, planning, and for jointly explaining (a) unexpected action outcomes due to exogenous actions and (b) partial scene descriptions extracted from sensor input. For any given task, each action in the plan contained in the answer set is executed probabilistically. The subset of the domain relevant to the action is identified automatically, and observations extracted from sensor inputs perform incremental Bayesian updates to a belief distribution defined over this domain subset, with highly probable beliefs being committed to the ASP program. The architecture's capabilities are illustrated in simulation and on a mobile robot in the context of a robot waiter operating in the dining room of a restaurant.
A New Property of Hamilton Graphs
Venue: arXiv cs.DM 2015
Year: 2015

A Hamilton cycle is a cycle containing every vertex of a graph. A graph is called Hamiltonian if it contains a Hamilton cycle. The Hamilton cycle problem is to find the sufficient and necessary condition that a graph is Hamiltonian. In this paper, we give out some new kind of definitions of the subgraphs and determine the Hamiltoncity of edges according to the existence of the subgraphs in a graph, and then obtain a new property of Hamilton graphs as being a necessary and sufficient condition characterized in the connectivity of the subgraph that induced from the cycle structure of a given graph.
Turnover Prediction Of Shares using Data Mining techniques : A Case Study
Venue: arXiv cs.LG 2015
Year: 2015

Predicting the turnover of a company in the ever fluctuating Stock market has always proved to be a precarious situation and most certainly a difficult task in hand. Data mining is a well-known sphere of Computer Science that aims on extracting meaningful information from large databases. However, despite the existence of many algorithms for the purpose of predicting the future trends, their efficiency is questionable as their predictions suffer from a high error rate. The objective of this paper is to investigate various classification algorithms to predict the turnover of different companies based on the Stock price. The authorized dataset for predicting the turnover was taken from www.bsc.com and included the stock market values of various companies over the past 10 years. The algorithms were investigated using the "R" tool. The feature selection algorithm, Boruta, was run on this dataset to extract the important and influential features for classification. With these extracted features, the Total Turnover of the company was predicted using various classification algorithms like Random Forest, Decision Tree, SVM and Multinomial Regression. This prediction mechanism was implemented to predict the turnover of a company on an everyday basis and hence could help navigate through dubious stock market trades. An accuracy rate of 95% was achieved by the above prediction process. Moreover, the importance of stock market attributes was established as well.
Land Use Classification in Remote Sensing Images by Convolutional Neural Networks
Venue: arXiv cs.CV 2015
Year: 2015

We explore the use of convolutional neural networks for the semantic classification of remote sensing scenes. Two recently proposed architectures, CaffeNet and GoogLeNet, are adopted, with three different learning modalities. Besides conventional training from scratch, we resort to pre-trained networks that are only fine-tuned on the target data, so as to avoid overfitting problems and reduce design time. Experiments on two remote sensing datasets, with markedly different characteristics, testify on the effectiveness and wide applicability of the proposed solution, which guarantees a significant performance improvement over all state-of-the-art references.
Online Contention Resolution Schemes
Venue: arXiv cs.DS 2015
Year: 2015

We introduce a new rounding technique designed for online optimization problems, which is related to contention resolution schemes, a technique initially introduced in the context of submodular function maximization. Our rounding technique, which we call online contention resolution schemes (OCRSs), is applicable to many online selection problems, including Bayesian online selection, oblivious posted pricing mechanisms, and stochastic probing models. It allows for handling a wide set of constraints, and shares many strong properties of offline contention resolution schemes. In particular, OCRSs for different constraint families can be combined to obtain an OCRS for their intersection. Moreover, we can approximately maximize submodular functions in the online settings we consider. We, thus, get a broadly applicable framework for several online selection problems, which improves on previous approaches in terms of the types of constraints that can be handled, the objective functions that can be dealt with, and the assumptions on the strength of the adversary. Furthermore, we resolve two open problems from the literature; namely, we present the first constant-factor constrained oblivious posted price mechanism for matroid constraints, and the first constant-factor algorithm for weighted stochastic probing with deadlines.
Procedural Content Generation for GDL Descriptions of Simplified Boardgames
Venue: arXiv cs.AI 2015
Year: 2015

We present initial research towards procedural generation of Simplified Boardgames and translating them into an efficient GDL code. This is a step towards establishing Simplified Boardgames as a comparison class for General Game Playing agents. To generate playable, human readable, and balanced chess-like games we use an adaptive evolutionary algorithm with the fitness function based on simulated playouts. In future, we plan to use the proposed method to diversify and extend the set of GGP tournament games by those with fully automatically generated rules.
Toward a Robust Sparse Data Representation for Wireless Sensor Networks
Venue: arXiv cs.NI 2015
Year: 2015

Compressive sensing has been successfully used for optimized operations in wireless sensor networks. However, raw data collected by sensors may be neither originally sparse nor easily transformed into a sparse data representation. This paper addresses the problem of transforming source data collected by sensor nodes into a sparse representation with a few nonzero elements. Our contributions that address three major issues include: 1) an effective method that extracts population sparsity of the data, 2) a sparsity ratio guarantee scheme, and 3) a customized learning algorithm of the sparsifying dictionary. We introduce an unsupervised neural network to extract an intrinsic sparse coding of the data. The sparse codes are generated at the activation of the hidden layer using a sparsity nomination constraint and a shrinking mechanism. Our analysis using real data samples shows that the proposed method outperforms conventional sparsity-inducing methods.
A Provably, Linear Time, In-place and Stable Merge Algorithm via the Perfect Shuffle
Venue: arXiv cs.DS 2015
Year: 2015

We reconsider a recently published algorithm (Dalkilic et al.) for merging lists by way of the perfect shuffle. The original publication gave only experimental results which, although consistent with linear execution time on the samples tested, provided no analysis. Here we prove that the time complexity, in the average case, is indeed linear, although there is an Omega(n^2) worst case. This is then the first provably linear time merge algorithm based on the use of the perfect shuffle. We provide a proof of correctness, extend the algorithm to the general case where the lists are of unequal length and show how it can be made stable, all aspects not included in the original presentation and we give a much more concise definition of the algorithm.
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study
Venue: arXiv cs.LO 2015
Year: 2015

This paper presents a case study of formalizing a normalization proof for Leivant's Predicative System F using the Equations package. Leivant's Predicative System F is a stratified version of System F, where type quantification is annotated with kinds representing universe levels. A weaker variant of this system was studied by Stump & Eades, employing the hereditary substitution method to show normalization. We improve on this result by showing normalization for Leivant's original system using hereditary substitutions and a novel multiset ordering on types. Our development is done in the Coq proof assistant using the Equations package, which provides an interface to define dependently-typed programs with well-founded recursion and full dependent pattern- matching. Equations allows us to define explicitly the hereditary substitution function, clarifying its algorithmic behavior in presence of term and type substitutions. From this definition, consistency can easily be derived. The algorithmic nature of our development is crucial to reflect languages with type quantification, enlarging the class of languages on which reflection methods can be used in the proof assistant.
Integral Action in Output Feedback for multi-input multi-output nonlinear systems
Venue: arXiv cs.SY 2015
Year: 2015

We address a particular problem of output regulation for multi-input multi-output nonlinear systems. Specifically, we are interested in making the stability of an equilibrium point and the regulation to zero of an output, robust to (small) unmodelled discrepancies between design model and actual system in particular those introducing an offset. We propose a novel procedure which is intended to be relevant to real life systems, as illustrated by a (non academic) example.
Dimension Reduction with Non-degrading Generalization
Venue: arXiv cs.LG 2015
Year: 2015

Visualizing high dimensional data by projecting them into two or three dimensional space is one of the most effective ways to intuitively understand the data's underlying characteristics, for example their class neighborhood structure. While data visualization in low dimensional space can be efficient for revealing the data's underlying characteristics, classifying a new sample in the reduced-dimensional space is not always beneficial because of the loss of information in expressing the data. It is possible to classify the data in the high dimensional space, while visualizing them in the low dimensional space, but in this case, the visualization is often meaningless because it fails to illustrate the underlying characteristics that are crucial for the classification process. In this paper, the performance-preserving property of the previously proposed Restricted Radial Basis Function Network in reducing the dimension of labeled data is explained. Here, it is argued through empirical experiments that the internal representation of the Restricted Radial Basis Function Network, which during the supervised learning process organizes a visualizable two dimensional map, does not only preserve the topographical structure of high dimensional data but also captures their class neighborhood structures that are important for classifying them. Hence, unlike many of the existing dimension reduction methods, the Restricted Radial Basis Function Network offers two dimensional visualization that is strongly correlated with the classification process.
Single and Multiple Illuminant Estimation Using Convolutional Neural Networks
Venue: arXiv cs.CV 2015
Year: 2015

In this paper we present a method for the estimation of the color of the illuminant in RAW images. The method includes a Convolutional Neural Network that has been specially designed to produce multiple local estimates. A multiple illuminant detector determines whether or not the local outputs of the network must be aggregated into a single estimate. We evaluated our method on standard datasets with single and multiple illuminants, obtaining lower estimation errors with respect to those obtained by other general purpose methods in the state of the art.