OpenRaiser/Intern-Atlas huggingface dataset:
Encoding Monomorphic and Polymorphic Types
Venue: arXiv cs.LO 2016
Year: 2016

Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.
Psychologically Motivated Text Mining
Venue: arXiv cs.CL 2016
Year: 2016

Natural language processing techniques are increasingly applied to identify social trends and predict behavior based on large text collections. Existing methods typically rely on surface lexical and syntactic information. Yet, research in psychology shows that patterns of human conceptualisation, such as metaphorical framing, are reliable predictors of human expectations and decisions. In this paper, we present a method to learn patterns of metaphorical framing from large text collections, using statistical techniques. We apply the method to data in three different languages and evaluate the identified patterns, demonstrating their psychological validity.
Global asymptotic stability of a PID control system with Coulomb friction
Venue: arXiv cs.SY 2016
Year: 2016

We propose a model for representing a point mass subject to Coulomb friction in feedback with a PID controller, based on a differential inclusion comprising all the possible magnitudes of static friction during the stick phase. For this model we study the set of all equilibria and we establish its global asymptotic stability using a discontinuous Lyapunov-like function, and a suitable LaSalle's invariance principle. We finally use well-posedness of the proposed model to establish useful robustness results, including an ISS property from a suitable input in a perturbed context. Simulation results are also given to illustrate our statements.
On private information retrieval array codes
Venue: arXiv cs.IT 2016
Year: 2016

Given a database, the private information retrieval (PIR) protocol allows a user to make queries to several servers and retrieve a certain item of the database via the feedbacks, without revealing the privacy of the specific item to any single server. Classical models of PIR protocols require that each server stores a whole copy of the database. Recently new PIR models are proposed with coding techniques arising from distributed storage system. In these new models each server only stores a fraction $1/s$ of the whole database, where $s>1$ is a given rational number. PIR array codes are recently proposed by Fazeli, Vardy and Yaakobi to characterize the new models. Consider a PIR array code with $m$ servers and the $k$-PIR property (which indicates that these $m$ servers may emulate any efficient $k$-PIR protocol). The central problem is to design PIR array codes with optimal rate $k/m$. Our contribution to this problem is three-fold. First, for the case $1<s\le 2$, although PIR array codes with optimal rate have been constructed recently by Blackburn and Etzion, the number of servers in their construction is impractically large. We determine the minimum number of servers admitting the existence of a PIR array code with optimal rate for a certain range of parameters. Second, for the case $s>2$, we derive a new upper bound on the rate of a PIR array code. Finally, for the case $s>2$, we analyze a new construction by Blackburn and Etzion and show that its rate is better than all the other existing constructions.
Time/memory/data trade-off attack to a psuedo-random generator
Venue: arXiv cs.CR 2016
Year: 2016

Time, data and memory trade off attack is one of the most important threats against pseudo- random generators and resisting against it, is considered as a main criteria of designing such generators. In this research, the pseudo-random GMGK generator will be addressed and analyzed in details. Having indicated various weaknesses of this generator, we performed three different versions of structural attack on this generator and showed that proposed TMDTO attacks to this generator can discover blocks of plaintext with lower complexity than exhaustive search of space of key generator. Results indicated that the mentioned generator is lack of the security claimed by authors.
ICE: Information Credibility Evaluation on Social Media via Representation Learning
Venue: arXiv cs.SI 2016
Year: 2016

With the rapid growth of social media, rumors are also spreading widely on social media and bring harm to people's daily life. Nowadays, information credibility evaluation has drawn attention from academic and industrial communities. Current methods mainly focus on feature engineering and achieve some success. However, feature engineering based methods require a lot of labor and cannot fully reveal the underlying relations among data. In our viewpoint, the key elements of user behaviors for evaluating credibility are concluded as "who", "what", "when", and "how". These existing methods cannot model the correlation among different key elements during the spreading of microblogs. In this paper, we propose a novel representation learning method, Information Credibility Evaluation (ICE), to learn representations of information credibility on social media. In ICE, latent representations are learnt for modeling user credibility, behavior types, temporal properties, and comment attitudes. The aggregation of these factors in the microblog spreading process yields the representation of a user's behavior, and the aggregation of these dynamic representations generates the credibility representation of an event spreading on social media. Moreover, a pairwise learning method is applied to maximize the credibility difference between rumors and non-rumors. To evaluate the performance of ICE, we conduct experiments on a Sina Weibo data set, and the experimental results show that our ICE model outperforms the state-of-the-art methods.
Modelling depth for nonparametric foreground segmentation using RGBD devices
Venue: arXiv cs.CV 2016
Year: 2016

The problem of detecting changes in a scene and segmenting the foreground from background is still challenging, despite previous work. Moreover, new RGBD capturing devices include depth cues, which could be incorporated to improve foreground segmentation. In this work, we present a new nonparametric approach where a unified model mixes the device multiple information cues. In order to unify all the device channel cues, a new probabilistic depth data model is also proposed where we show how handle the inaccurate data to improve foreground segmentation. A new RGBD video dataset is presented in order to introduce a new standard for comparison purposes of this kind of algorithms. Results show that the proposed approach can handle several practical situations and obtain good results in all cases.
Comprehensive Evaluation of OpenCL-based Convolutional Neural Network Accelerators in Xilinx and Altera FPGAs
Venue: arXiv cs.CV 2016
Year: 2016

Deep learning has significantly advanced the state of the art in artificial intelligence, gaining wide popularity from both industry and academia. Special interest is around Convolutional Neural Networks (CNN), which take inspiration from the hierarchical structure of the visual cortex, to form deep layers of convolutional operations, along with fully connected classifiers. Hardware implementations of these deep CNN architectures are challenged with memory bottlenecks that require many convolution and fully-connected layers demanding large amount of communication for parallel computation. Multi-core CPU based solutions have demonstrated their inadequacy for this problem due to the memory wall and low parallelism. Many-core GPU architectures show superior performance but they consume high power and also have memory constraints due to inconsistencies between cache and main memory. FPGA design solutions are also actively being explored, which allow implementing the memory hierarchy using embedded BlockRAM. This boosts the parallel use of shared memory elements between multiple processing units, avoiding data replicability and inconsistencies. This makes FPGAs potentially powerful solutions for real-time classification of CNNs. Both Altera and Xilinx have adopted OpenCL co-design framework from GPU for FPGA designs as a pseudo-automatic development solution. In this paper, a comprehensive evaluation and comparison of Altera and Xilinx OpenCL frameworks for a 5-layer deep CNN is presented. Hardware resources, temporal performance and the OpenCL architecture for CNNs are discussed. Xilinx demonstrates faster synthesis, better FPGA resource utilization and more compact boards. Altera provides multi-platforms tools, mature design community and better execution times.
A New Queue Discipline for Reducing Bufferbloat Effects in HetNet Concurrent Multipath Transfer
Venue: arXiv cs.NI 2016
Year: 2016

Heterogeneous wireless networks have evolved to reach application requirements for low latency and high throughput on Internet access. Recent studies have improved network performance employing the Multipath TCP, which aggregates flows from heterogeneous wireless interfaces in a single connection. Although existing proposals are powerful, coupled congestion control algorithms are currently limited because of the high variation in path delays, bandwidth and loss rate, typical from heterogeneous wireless networks, even more over concurrent multipath transmissions. These transmissions experience bufferbloat, i.e., high delays caused by long queues. Hence, to cope with the current limitations, this work presents CoDel-LIFO, a new active queue management (AQM) discipline to reduce the dropped packet ratio in the Multipath TCP congestion control mechanism. Differently from other approaches, CoDel-LIFO gives priority to the most recent packets, being then promising. This paper provides a detailed simulation analysis over congestion control algorithms by comparing CoDel-LIFO to CoDel and DropTail disciplines. Results indicate that CoDel-LIFO reduces queue drops, diminishing the impact on congestion control; improving substantially the goodput; and keeping RTT low.
Combining Belief Propagation and Successive Cancellation List Decoding of Polar Codes on a GPU Platform
Venue: arXiv cs.IT 2016
Year: 2016

The decoding performance of polar codes strongly depends on the decoding algorithm used, while also the decoder throughput and its latency mainly depend on the decoding algorithm. In this work, we implement the powerful successive cancellation list (SCL) decoder on a GPU and identify the bottlenecks of this algorithm with respect to parallel computing and its difficulties. The inherent serial decoding property of the SCL algorithm naturally limits the achievable speed-up gains on GPUs when compared to CPU implementations. In order to increase the decoding throughput, we use a hybrid decoding scheme based on the belief propagation (BP) decoder, which can be intra and inter-frame parallelized. The proposed scheme combines excellent decoding performance and high throughput within the signal-to-noise ratio (SNR) region of interest.
Design and Analysis of Deadline and Budget Constrained Autoscaling (DBCA) Algorithm for 5G Mobile Networks
Venue: arXiv cs.NI 2016
Year: 2016

In cloud computing paradigm, virtual resource autoscaling approaches have been intensively studied recent years. Those approaches dynamically scale in/out virtual resources to adjust system performance for saving operation cost. However, designing the autoscaling algorithm for desired performance with limited budget, while considering the existing capacity of legacy network equipment, is not a trivial task. In this paper, we propose a Deadline and Budget Constrained Autoscaling (DBCA) algorithm for addressing the budget-performance tradeoff. We develop an analytical model to quantify the tradeoff and cross-validate the model by extensive simulations. The results show that the DBCA can significantly improve system performance given the budget upper-bound. In addition, the model provides a quick way to evaluate the budget-performance tradeoff and system design without wide deployment, saving on cost and time.
Reconstructing Vechicles from a Single Image: Shape Priors for Road Scene Understanding
Venue: arXiv cs.CV 2016
Year: 2016

We present an approach for reconstructing vehicles from a single (RGB) image, in the context of autonomous driving. Though the problem appears to be ill-posed, we demonstrate that prior knowledge about how 3D shapes of vehicles project to an image can be used to reason about the reverse process, i.e., how shapes (back-)project from 2D to 3D. We encode this knowledge in \emph{shape priors}, which are learnt over a small keypoint-annotated dataset. We then formulate a shape-aware adjustment problem that uses the learnt shape priors to recover the 3D pose and shape of a query object from an image. For shape representation and inference, we leverage recent successes of Convolutional Neural Networks (CNNs) for the task of object and keypoint localization, and train a novel cascaded fully-convolutional architecture to localize vehicle \emph{keypoints} in images. The shape-aware adjustment then robustly recovers shape (3D locations of the detected keypoints) while simultaneously filling in occluded keypoints. To tackle estimation errors incurred due to erroneously detected keypoints, we use an Iteratively Re-weighted Least Squares (IRLS) scheme for robust optimization, and as a by-product characterize noise models for each predicted keypoint. We evaluate our approach on autonomous driving benchmarks, and present superior results to existing monocular, as well as stereo approaches.
Multi-dimensional signal approximation with sparse structured priors using split Bregman iterations
Venue: arXiv cs.DS 2016
Year: 2016

This paper addresses the structurally-constrained sparse decomposition of multi-dimensional signals onto overcomplete families of vectors, called dictionaries. The contribution of the paper is threefold. Firstly, a generic spatio-temporal regularization term is designed and used together with the standard $\ell_1$ regularization term to enforce a sparse decomposition preserving the spatio-temporal structure of the signal. Secondly, an optimization algorithm based on the split Bregman approach is proposed to handle the associated optimization problem, and its convergence is analyzed. Our well-founded approach yields same accuracy as the other algorithms at the state-of-the-art, with significant gains in terms of convergence speed. Thirdly, the empirical validation of the approach on artificial and real-world problems demonstrates the generality and effectiveness of the method. On artificial problems, the proposed regularization subsumes the Total Variation minimization and recovers the expected decomposition. On the real-world problem of electro-encephalography brainwave decomposition, the approach outperforms similar approaches in terms of P300 evoked potentials detection, using structured spatial priors to guide the decomposition.
Asynchronous Multi-Task Learning
Venue: arXiv cs.LG 2016
Year: 2016

Many real-world machine learning applications involve several learning tasks which are inter-related. For example, in healthcare domain, we need to learn a predictive model of a certain disease for many hospitals. The models for each hospital may be different because of the inherent differences in the distributions of the patient populations. However, the models are also closely related because of the nature of the learning tasks modeling the same disease. By simultaneously learning all the tasks, multi-task learning (MTL) paradigm performs inductive knowledge transfer among tasks to improve the generalization performance. When datasets for the learning tasks are stored at different locations, it may not always be feasible to transfer the data to provide a data-centralized computing environment due to various practical issues such as high data volume and privacy. In this paper, we propose a principled MTL framework for distributed and asynchronous optimization to address the aforementioned challenges. In our framework, gradient update does not wait for collecting the gradient information from all the tasks. Therefore, the proposed method is very efficient when the communication delay is too high for some task nodes. We show that many regularized MTL formulations can benefit from this framework, including the low-rank MTL for shared subspace learning. Empirical studies on both synthetic and real-world datasets demonstrate the efficiency and effectiveness of the proposed framework.
The Role of Rating and Loan Characteristics in Online Microfunding Behaviors
Venue: arXiv cs.CY 2016
Year: 2016

We propose an in-depth study of lending behaviors in Kiva using a mix of quantitative and large-scale data mining techniques. Kiva is a non-profit organization that offers an online platform to connect lenders with borrowers. Their site, kiva.org, allows citizens to microlend small amounts of money to entrepreneurs (borrowers) from different countries. The borrowers are always affiliated with a Field Partner (FP) which can be a microfinance institution (MFI) or other type of local organization that has partnered with Kiva. Field partners give loans to selected businesses based on their local knowledge regarding the country, the business sector including agriculture, health or manufacture among others, and the borrower.Our objective is to understand the relationship between lending activity and various features offered by the online platform. Specifically, we focus on two research questions: (i) the role that MFI ratings play in driving lending activity and (ii) the role that various loan features have in the lending behavior. The first question analyzes whether there exists a relationship between the MFI ratings - that lenders can explore online - and their lending volumes. The second research question attempts to understand if certain loan features - available online at Kiva - such as the type of small business, the gender of the borrower, or the loan's country information might affect the way lenders lend.
Referential Uncertainty and Word Learning in High-dimensional, Continuous Meaning Spaces
Venue: arXiv cs.CL 2016
Year: 2016

This paper discusses lexicon word learning in high-dimensional meaning spaces from the viewpoint of referential uncertainty. We investigate various state-of-the-art Machine Learning algorithms and discuss the impact of scaling, representation and meaning space structure. We demonstrate that current Machine Learning techniques successfully deal with high-dimensional meaning spaces. In particular, we show that exponentially increasing dimensions linearly impact learner performance and that referential uncertainty from word sensitivity has no impact.
A Comprehensive Analysis of 5G Heterogeneous Cellular Systems operating over $κ$-$μ$ Shadowed Fading Channels
Venue: arXiv cs.IT 2016
Year: 2016

Emerging cellular technologies such as those proposed for use in 5G communications will accommodate a wide range of usage scenarios with diverse link requirements. This will include the necessity to operate over a versatile set of wireless channels ranging from indoor to outdoor, from line-of-sight (LOS) to non-LOS, and from circularly symmetric scattering to environments which promote the clustering of scattered multipath waves. Unfortunately, many of the conventional fading models adopted in the literature to develop network models lack the flexibility to account for such disparate signal propagation mechanisms. To bridge the gap between theory and practical channels, we consider $κ$-$μ$ shadowed fading, which contains as special cases, the majority of the linear fading models proposed in the open literature, including Rayleigh, Rician, Nakagami-m, Nakagami-q, One-sided Gaussian, $κ$-$μ$, $η$-$μ$, and Rician shadowed to name but a few. In particular, we apply an orthogonal expansion to represent the $κ$-$μ$ shadowed fading distribution as a simplified series expression. Then using the series expressions with stochastic geometry, we propose an analytic framework to evaluate the average of an arbitrary function of the SINR over $κ$-$μ$ shadowed fading channels. Using the proposed method, we evaluate the spectral efficiency, moments of the SINR, bit error probability and outage probability of a $K$-tier HetNet with $K$ classes of BSs, differing in terms of the transmit power, BS density, shadowing characteristics and small-scale fading. Building upon these results, we provide important new insights into the network performance of these emerging wireless applications while considering a diverse range of fading conditions and link qualities.
Skin Normal Force Calibration Using Vacuum Bags
Venue: arXiv cs.RO 2016
Year: 2016

The paper presents a proof of concept to calibrate iCub's skin using vacuum bags. The method's main idea consists in inserting the skin in a vacuum bag, and then decreasing the pressure in the bag to create a uniform pressure distribution on the skin surface. Acquisition and data processing of the bag pressure and sensors' measured capacitance allow us to characterize the relationship between the pressure and the measured capacitance of each sensor. After calibration, integration of the pressure distribution over the skin geometry provides us with the net normal force applied to the skin. Experiments are conducted using the forearm skin of the iCub humanoid robot, and validation results indicate acceptable average errors in force prediction.
Characterization of experts in crowdsourcing platforms
Venue: arXiv cs.AI 2016
Year: 2016

Crowdsourcing platforms enable to propose simple human intelligence tasks to a large number of participants who realise these tasks. The workers often receive a small amount of money or the platforms include some other incentive mechanisms, for example they can increase the workers reputation score, if they complete the tasks correctly. We address the problem of identifying experts among participants, that is, workers, who tend to answer the questions correctly. Knowing who are the reliable workers could improve the quality of knowledge one can extract from responses. As opposed to other works in the literature, we assume that participants can give partial or incomplete responses, in case they are not sure that their answers are correct. We model such partial or incomplete responses with the help of belief functions, and we derive a measure that characterizes the expertise level of each participant. This measure is based on precise and exactitude degrees that represent two parts of the expertise level. The precision degree reflects the reliability level of the participants and the exactitude degree reflects the knowledge level of the participants. We also analyze our model through simulation and demonstrate that our richer model can lead to more reliable identification of experts.