OpenRaiser/Intern-Atlas huggingface dataset:
Gyroscope-aided Relative Pose Estimation for Rolling Shutter Cameras
Venue: arXiv cs.CV 2019
Year: 2019

The rolling shutter camera has received great attention due to its low cost imaging capability, however, the estimation of relative pose between rolling shutter cameras still remains a difficult problem owing to its line-by-line image capturing characteristics. To alleviate this problem, we exploit gyroscope measurements, angular velocity, along with image measurement to compute the relative pose between rolling shutter cameras. The gyroscope measurements provide the information about instantaneous motion that causes the rolling shutter distortion. Having gyroscope measurements in one hand, we simplify the relative pose estimation problem and find a minimal solution for the problem based on the Grobner basis polynomial solver. The proposed method requires only five points to compute relative pose between rolling shutter cameras, whereas previous methods require 20 or 44 corresponding points for linear and uniform rolling shutter geometry models, respectively. Experimental results on synthetic and real data verify the superiority of the proposed method over existing relative pose estimation methods.
Curious iLQR: Resolving Uncertainty in Model-based RL
Venue: arXiv cs.RO 2019
Year: 2019

Curiosity as a means to explore during reinforcement learning problems has recently become very popular. However, very little progress has been made in utilizing curiosity for learning control. In this work, we propose a model-based reinforcement learning (MBRL) framework that combines Bayesian modeling of the system dynamics with curious iLQR, an iterative LQR approach that considers model uncertainty. During trajectory optimization the curious iLQR attempts to minimize both the task-dependent cost and the uncertainty in the dynamics model. We demonstrate the approach on reaching tasks with 7-DoF manipulators in simulation and on a real robot. Our experiments show that MBRL with curious iLQR reaches desired end-effector targets more reliably and with less system rollouts when learning a new task from scratch, and that the learned model generalizes better to new reaching tasks.
Permutation codes over finite fields
Venue: arXiv cs.IT 2019
Year: 2019

In this paper we describe a class of codes called {\it permutation codes}. This class of codes is a generalization of cyclic codes and quasi-cyclic codes. We also give some examples of optimal permutation codes over binary, ternary, and $5$-ary. Then, we describe its structure as submodules over a polynomial ring.
Computing a Minimum-Width Cubic and Hypercubic Shell
Venue: arXiv cs.CG 2019
Year: 2019

In this paper, we study the problem of computing a minimum-width axis-aligned cubic shell that encloses a given set of $n$ points in a three-dimensional space. A cubic shell is a closed volume between two concentric and face-parallel cubes. Prior to this work, there was no known algorithm for this problem in the literature. We present the first nontrivial algorithm whose running time is $O(n \log^2 n)$. Our approach easily extends to higher dimension, resulting in an $O(n^{\lfloor d/2 \rfloor} \log^{d-1} n)$-time algorithm for the hypercubic shell problem in $d\geq 3$ dimension.
Robust Visual Tracking Revisited: From Correlation Filter to Template Matching
Venue: arXiv cs.CV 2019
Year: 2019

In this paper, we propose a novel matching based tracker by investigating the relationship between template matching and the recent popular correlation filter based trackers (CFTs). Compared to the correlation operation in CFTs, a sophisticated similarity metric termed "mutual buddies similarity" (MBS) is proposed to exploit the relationship of multiple reciprocal nearest neighbors for target matching. By doing so, our tracker obtains powerful discriminative ability on distinguishing target and background as demonstrated by both empirical and theoretical analyses. Besides, instead of utilizing single template with the improper updating scheme in CFTs, we design a novel online template updating strategy named "memory filtering" (MF), which aims to select a certain amount of representative and reliable tracking results in history to construct the current stable and expressive template set. This scheme is beneficial for the proposed tracker to comprehensively "understand" the target appearance variations, "recall" some stable results. Both qualitative and quantitative evaluations on two benchmarks suggest that the proposed tracking method performs favorably against some recently developed CFTs and other competitive trackers.
On the Lambek Calculus with an Exchange Modality
Venue: arXiv cs.LO 2019
Year: 2019

In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.
Measuring the influence of mere exposure effect of TV commercial adverts on purchase behavior based on machine learning prediction models
Venue: arXiv cs.IR 2019
Year: 2019

Since its introduction, television has been the main channel of investment for advertisements in order to influence customers purchase behavior. Many have attributed the mere exposure effect as the source of influence in purchase intention and purchase decision; however, most of the studies of television advertisement effects are not only outdated, but their sample size is questionable and their environments do not reflect reality. With the advent of the internet, social media and new information technologies, many recent studies focus on the effects of online advertisement, meanwhile, the investment in television advertisement still has not declined. In response to this, we applied machine learning algorithms SVM and XGBoost, as well as Logistic Regression, to construct a number of prediction models based on at-home advertisement exposure time and demographic data, examining the predictability of Actual Purchase and Purchase Intention behaviors of 3000 customers across 36 different products during the span of 3 months. If models based on exposure time had unreliable predictability in contrast to models based on demographic data, doubts would surface about the effectiveness of the hard investment in television advertising. Based on our results, we found that models based on advert exposure time were consistently low in their predictability in comparison with models based on demographic data only, and with models based on both demographic data and exposure time data. We also found that there was not a statistically significant difference between these last two kinds of models. This suggests that advert exposure time has little to no effect in the short-term in increasing positive actual purchase behavior.
Improving interactive reinforcement learning: What makes a good teacher?
Venue: arXiv cs.AI 2019
Year: 2019

Interactive reinforcement learning has become an important apprenticeship approach to speed up convergence in classic reinforcement learning problems. In this regard, a variant of interactive reinforcement learning is policy shaping which uses a parent-like trainer to propose the next action to be performed and by doing so reduces the search space by advice. On some occasions, the trainer may be another artificial agent which in turn was trained using reinforcement learning methods to afterward becoming an advisor for other learner-agents. In this work, we analyze internal representations and characteristics of artificial agents to determine which agent may outperform others to become a better trainer-agent. Using a polymath agent, as compared to a specialist agent, an advisor leads to a larger reward and faster convergence of the reward signal and also to a more stable behavior in terms of the state visit frequency of the learner-agents. Moreover, we analyze system interaction parameters in order to determine how influential they are in the apprenticeship process, where the consistency of feedback is much more relevant when dealing with different learner obedience parameters.
Wireless Power Transfer with Information Asymmetry: A Public Goods Perspective
Venue: arXiv cs.NI 2019
Year: 2019

Wireless power transfer (WPT) technology enables a cost-effective and sustainable energy supply in wireless networks. However, the broadcast nature of wireless signals makes them non-excludable public goods, which leads to potential free-riders among energy receivers. In this study, we formulate the wireless power provision problem as a public goods provision problem, aiming to maximize the social welfare of a system of an energy transmitter (ET) and all the energy users (EUs), while considering their private information and self-interested behaviors. We propose a two-phase all-or-none scheme involving a low-complexity Power And Taxation (PAT) mechanism, which ensures voluntary participation, truthfulness, budget balance, and social optimality at every Nash equilibrium (NE). We propose a distributed PAT (D-PAT) algorithm to reach an NE, and prove its convergence by connecting the structure of NEs and that of the optimal solution to a related optimization problem. We further extend the analysis to a multi-channel system, which brings a further challenge due to the non-strict concavity of the agents' payoffs. We propose a Multi-Channel PAT (M-PAT) mechanism and a distributed M-PAT (D-MPAT) algorithm to address the challenge. Simulation results show that our design is most beneficial when there are more EUs with more homogeneous channel gains.
Synthesis of Admissible Shields
Venue: arXiv cs.LO 2019
Year: 2019

Shield synthesis is an approach to enforce a set of safety-critical properties of a reactive system at runtime. A shield monitors the system and corrects any erroneous output values instantaneously. The shield deviates from the given outputs as little as it can and recovers to hand back control to the system as soon as possible. This paper takes its inspiration from a case study on mission planning for unmanned aerial vehicles (UAVs) in which k-stabilizing shields, which guarantee recovery in a finite time, could not be constructed. We introduce the notion of admissible shields, which improves k-stabilizing shields in two ways: (1) whereas k-stabilizing shields take an adversarial view on the system, admissible shields take a collaborative view. That is, if there is no shield that guarantees recovery within k steps regardless of system behavior, the admissible shield will attempt to work with the system to recover as soon as possible. (2) Admissible shields can handle system failures during the recovery phase. In our experimental results we show that for UAVs, we can generate admissible shields, even when k-stabilizing shields do not exist.
Cooperation on the monte carlo rule Prison's dilemma game on the grid
Venue: arXiv cs.GT 2019
Year: 2019

In this paper, we investigate the prison's dilemma game with monte carlo rule in the view of the idea of the classic Monte Carlo method on the grid. Monte carlo rule is an organic combination of the current dynamic rules of individual policy adjustment, which not only makes full use of information but also reflects the individual's bounded rational behavior and the ambivalence between the pursuit of high returns and high risks. In addition, it also reflects the individual's behavioral execution preferences. The implementation of monte carlo rule brings an extremely good result, higher cooperation level and stronger robustness are achieved by comparing with the unconditional imitation rule, replicator dynamics rule and fermi rule. When analyse the equilibrium density of cooperators as a function of the temptation to defect, it appears a smooth transition between the mixed state of coexistence of cooperators and defectors and the pure state of defectors when enhancing the temptation, which can be perfectly characterized by the trigonometric behavior instead of the power-law behavior discovered in the pioneer's work. When discuss the relationship between the temptation to defect and the average returns of cooperators and defectors, it is found that cooperators' average returns is almost a constant throughout the whole temptation parameter ranges while defectors' decreases as the growth of temptation. Additionally, the insensitivity of cooperation level to the initial density of cooperators and the sensitivity to the social population have been both demonstrated.
LeanResNet: A Low-cost Yet Effective Convolutional Residual Networks
Venue: arXiv cs.LG 2019
Year: 2019

Convolutional Neural Networks (CNNs) filter the input data using spatial convolution operators with compact stencils. Commonly, the convolution operators couple features from all channels, which leads to immense computational cost in the training of and prediction with CNNs. To improve the efficiency of CNNs, we introduce lean convolution operators that reduce the number of parameters and computational complexity, and can be used in a wide range of existing CNNs. Here, we exemplify their use in residual networks (ResNets), which have been very reliable for a few years now and analyzed intensively. In our experiments on three image classification problems, the proposed LeanResNet yields results that are comparable to other recently proposed reduced architectures using similar number of parameters.
SyGuS-Comp 2018: Results and Analysis
Venue: arXiv cs.PL 2019
Year: 2019

Syntax-guided synthesis (SyGuS) is the computational problem of finding an implementation $f$ that meets both a semantic constraint given by a logical formula $ϕ$ in a background theory $\mathbb{T}$, and a syntactic constraint given by a grammar $G$, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in the SyGuS input format (SyGuS-IF), a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In the 5th SyGuS-Comp, five solvers competed on over 1600 benchmarks across various tracks. This paper presents and analyses the results of this year's (2018) SyGuS competition.
Efficient Search and Elimination of Harmful Objects in Optimized QC SC-LDPC Codes
Venue: arXiv cs.IT 2019
Year: 2019

The error correction performance of low-density parity-check (LDPC) codes under iterative message-passing decoding is degraded by the presence of certain harmful objects existing in their Tanner graph representation. Depending on the context, such harmful objects are known as stopping sets, trapping sets, absorbing sets, or pseudocodewords. In this paper, we propose a general procedure based on edge spreading that enables the design of quasi-cyclic (QC) spatially coupled low-density parity-check codes (SC-LDPCCs) that are derived from QC-LDPC block codes and possess a significantly reduced multiplicity of harmful objects with respect to the original QC-LDPC block code. This procedure relies on a novel algorithm that greedily spans the search space of potential candidates to reduce the multiplicity of the target harmful object(s) in the Tanner graph. The effectiveness of the method we propose is validated via examples and numerical computer simulations.
A Discussion on Solving Partial Differential Equations using Neural Networks
Venue: arXiv cs.LG 2019
Year: 2019

Can neural networks learn to solve partial differential equations (PDEs)? We investigate this question for two (systems of) PDEs, namely, the Poisson equation and the steady Navier--Stokes equations. The contributions of this paper are five-fold. (1) Numerical experiments show that small neural networks (< 500 learnable parameters) are able to accurately learn complex solutions for systems of partial differential equations. (2) It investigates the influence of random weight initialization on the quality of the neural network approximate solution and demonstrates how one can take advantage of this non-determinism using ensemble learning. (3) It investigates the suitability of the loss function used in this work. (4) It studies the benefits and drawbacks of solving (systems of) PDEs with neural networks compared to classical numerical methods. (5) It proposes an exhaustive list of possible directions of future work.
Attention-Passing Models for Robust and Data-Efficient End-to-End Speech Translation
Venue: arXiv cs.CL 2019
Year: 2019

Speech translation has traditionally been approached through cascaded models consisting of a speech recognizer trained on a corpus of transcribed speech, and a machine translation system trained on parallel texts. Several recent works have shown the feasibility of collapsing the cascade into a single, direct model that can be trained in an end-to-end fashion on a corpus of translated speech. However, experiments are inconclusive on whether the cascade or the direct model is stronger, and have only been conducted under the unrealistic assumption that both are trained on equal amounts of data, ignoring other available speech recognition and machine translation corpora. In this paper, we demonstrate that direct speech translation models require more data to perform well than cascaded models, and while they allow including auxiliary data through multi-task training, they are poor at exploiting such data, putting them at a severe disadvantage. As a remedy, we propose the use of end-to-end trainable models with two attention mechanisms, the first establishing source speech to source text alignments, the second modeling source to target text alignment. We show that such models naturally decompose into multi-task-trainable recognition and translation tasks and propose an attention-passing technique that alleviates error propagation issues in a previous formulation of a model with two attention stages. Our proposed model outperforms all examined baselines and is able to exploit auxiliary training data much more effectively than direct attentional models.
Estimation of Linear Motion in Dense Crowd Videos using Langevin Model
Venue: arXiv cs.CV 2019
Year: 2019

Crowd gatherings at social and cultural events are increasing in leaps and bounds with the increase in population. Surveillance through computer vision and expert decision making systems can help to understand the crowd phenomena at large gatherings. Understanding crowd phenomena can be helpful in early identification of unwanted incidents and their prevention. Motion flow is one of the important crowd phenomena that can be instrumental in describing the crowd behavior. Flows can be useful in understanding instabilities in the crowd. However, extracting motion flows is a challenging task due to randomness in crowd movement and limitations of the sensing device. Moreover, low-level features such as optical flow can be misleading if the randomness is high. In this paper, we propose a new model based on Langevin equation to analyze the linear dominant flows in videos of densely crowded scenarios. We assume a force model with three components, namely external force, confinement/drift force, and disturbance force. These forces are found to be sufficient to describe the linear or near-linear motion in dense crowd videos. The method is significantly faster as compared to existing popular crowd segmentation methods. The evaluation of the proposed model has been carried out on publicly available datasets as well as using our dataset. It has been observed that the proposed method is able to estimate and segment the linear flows in the dense crowd with better accuracy as compared to state-of-the-art techniques with substantial decrease in the computational overhead.
ct-fuzz: Fuzzing for Timing Leaks
Venue: arXiv cs.SE 2019
Year: 2019

Testing-based methodologies like fuzzing are able to analyze complex software which is not amenable to traditional formal approaches like verification, model checking, and abstract interpretation. Despite enormous success at exposing countless security vulnerabilities in many popular software projects, applications of testing-based approaches have mainly targeted checking traditional safety properties like memory safety. While unquestionably important, this class of properties does not precisely characterize other important security aspects such as information leakage, e.g., through side channels. In this work we extend testing-based software analysis methodologies to two-safety properties, which enables the precise discovery of information leaks in complex software. In particular, we present the ct-fuzz tool, which lends coverage-guided greybox fuzzers the ability to detect two-safety property violations. Our approach is capable of exposing violations to any two-safety property expressed as equality between two program traces. Empirically, we demonstrate that ct-fuzz swiftly reveals timing leaks in popular cryptographic implementations.
A Path To DOT: Formalizing Fully Path-Dependent Types
Venue: arXiv cs.PL 2019
Year: 2019

The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types $-$ types such as $x.a_1\dots a_n.T$ that depend on the runtime value of a path $x.a_1\dots a_n$ to an object. Unfortunately, existing formulations of DOT can model only types of the form $x.A$ which depend on variables rather than general paths. This restriction makes it impossible to model nested module dependencies. Nesting small components inside larger ones is a necessary ingredient of a modular, scalable language. DOT's variable restriction thus undermines its ability to fully formalize a variety of programming-language features including Scala's module system, family polymorphism, and covariant specialization. This paper presents the pDOT calculus, which generalizes DOT to support types that depend on paths of arbitrary length, as well as singleton types to track path equality. We show that naive approaches to add paths to DOT make it inherently unsound, and present necessary conditions for such a calculus to be sound. We discuss the key changes necessary to adapt the techniques of the DOT soundness proofs so that they can be applied to pDOT. Our paper comes with a Coq-mechanized type-safety proof of pDOT. With support for paths of arbitrary length, pDOT can realize DOT's full potential for formalizing Scala-like calculi.