OpenRaiser/Intern-Atlas huggingface dataset:
The Delta-calculus: syntax and types
Venue: arXiv cs.LO 2019
Year: 2019

We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Salle', the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection type systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems a` la Curry and the corresponding intersection type systems a` la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.
Characterizing a Meta-CDN
Venue: arXiv cs.NI 2019
Year: 2019

CDNs have reshaped the Internet architecture at large. They operate (globally) distributed networks of servers to reduce latencies as well as to increase availability for content and to handle large traffic bursts. Traditionally, content providers were mostly limited to a single CDN operator. However, in recent years, more and more content providers employ multiple CDNs to serve the same content and provide the same services. Thus, switching between CDNs, which can be beneficial to reduce costs or to select CDNs by optimal performance in different geographic regions or to overcome CDN-specific outages, becomes an important task. Services that tackle this task emerged, also known as CDN broker, Multi-CDN selectors, or Meta-CDNs. Despite their existence, little is known about Meta-CDN operation in the wild. In this paper, we thus shed light on this topic by dissecting a major Meta-CDN. Our analysis provides insights into its infrastructure, its operation in practice, and its usage by Internet sites. We leverage PlanetLab and Ripe Atlas as distributed infrastructures to study how a Meta-CDN impacts the web latency.
Authentication schemes for Smart Mobile Devices: Threat Models, Countermeasures, and Open Research Issues
Venue: arXiv cs.CR 2019
Year: 2019

This paper presents a comprehensive investigation of authentication schemes for smart mobile devices. We start by providing an overview of existing survey articles published in the recent years that deal with security for mobile devices. Then, we describe and give a classification of threat models in smart mobile devices in five categories, including, identity-based attacks, eavesdropping-based attacks, combined eavesdropping and identity-based attacks, manipulation-based attacks, and service-based attacks. We also provide a classification of countermeasures into four types of categories, including, cryptographic functions, personal identification, classification algorithms, and channel characteristics. According to these, we categorize authentication schemes for smart mobile devices in four categories, namely, 1) biometric-based authentication schemes, 2) channel-based authentication schemes, 3) factor-based authentication schemes, and 4) ID-based authentication schemes. In addition, we provide a taxonomy and comparison of authentication schemes for smart mobile devices in the form of tables. Finally, we identify open challenges and future research directions.
Learning Deep Representations with Probabilistic Knowledge Transfer
Venue: arXiv cs.LG 2019
Year: 2019

Knowledge Transfer (KT) techniques tackle the problem of transferring the knowledge from a large and complex neural network into a smaller and faster one. However, existing KT methods are tailored towards classification tasks and they cannot be used efficiently for other representation learning tasks. In this paper a novel knowledge transfer technique, that is capable of training a student model that maintains the same amount of mutual information between the learned representation and a set of (possible unknown) labels as the teacher model, is proposed. Apart from outperforming existing KT techniques, the proposed method allows for overcoming several limitations of existing methods providing new insight into KT as well as novel KT applications, ranging from knowledge transfer from handcrafted feature extractors to {cross-modal} KT from the textual modality into the representation extracted from the visual modality of the data.
Error Analysis and Improving the Accuracy of Winograd Convolution for Deep Neural Networks
Venue: arXiv cs.NA 2019
Year: 2019

Popular deep neural networks (DNNs) spend the majority of their execution time computing convolutions. The Winograd family of algorithms can greatly reduce the number of arithmetic operations required and is present in many DNN software frameworks. However, the performance gain is at the expense of a reduction in floating point (FP) numerical accuracy. In this paper, we analyse the worst case FP error and prove the estimation of norm and conditioning of the algorithm. We show that the bound grows exponentially with the size of the convolution, but the error bound of the \textit{modified} algorithm is smaller than the original one. We propose several methods for reducing FP error. We propose a canonical evaluation ordering based on Huffman coding that reduces summation error. We study the selection of sampling "points" experimentally and find empirically good points for the most important sizes. We identify the main factors associated with good points. In addition, we explore other methods to reduce FP error, including mixed-precision convolution, and pairwise summation across DNN channels. Using our methods we can significantly reduce FP error for a given block size, which allows larger block sizes and reduced computation.
Learning to Navigate in Cities Without a Map
Venue: arXiv cs.AI 2019
Year: 2019

Navigating through unstructured environments is a basic capability of intelligent creatures, and thus is of fundamental interest in the study and development of artificial intelligence. Long-range navigation is a complex cognitive task that relies on developing an internal representation of space, grounded by recognisable landmarks and robust visual processing, that can simultaneously support continuous self-localisation ("I am here") and a representation of the goal ("I am going there"). Building upon recent research that applies deep reinforcement learning to maze navigation problems, we present an end-to-end deep reinforcement learning approach that can be applied on a city scale. Recognising that successful navigation relies on integration of general policies with locale-specific knowledge, we propose a dual pathway architecture that allows locale-specific features to be encapsulated, while still enabling transfer to multiple cities. We present an interactive navigation environment that uses Google StreetView for its photographic content and worldwide coverage, and demonstrate that our learning method allows agents to learn to navigate multiple cities and to traverse to target destinations that may be kilometres away. The project webpage http://streetlearn.cc contains a video summarising our research and showing the trained agent in diverse city environments and on the transfer task, the form to request the StreetLearn dataset and links to further resources. The StreetLearn environment code is available at https://github.com/deepmind/streetlearn
CodeSLAM - Learning a Compact, Optimisable Representation for Dense Visual SLAM
Venue: arXiv cs.CV 2019
Year: 2019

The representation of geometry in real-time 3D perception systems continues to be a critical research issue. Dense maps capture complete surface shape and can be augmented with semantic labels, but their high dimensionality makes them computationally costly to store and process, and unsuitable for rigorous probabilistic inference. Sparse feature-based representations avoid these problems, but capture only partial scene information and are mainly useful for localisation only. We present a new compact but dense representation of scene geometry which is conditioned on the intensity data from a single image and generated from a code consisting of a small number of parameters. We are inspired by work both on learned depth from images, and auto-encoders. Our approach is suitable for use in a keyframe-based monocular dense SLAM system: While each keyframe with a code can produce a depth map, the code can be optimised efficiently jointly with pose variables and together with the codes of overlapping keyframes to attain global consistency. Conditioning the depth map on the image allows the code to only represent aspects of the local geometry which cannot directly be predicted from the image. We explain how to learn our code representation, and demonstrate its advantageous properties in monocular SLAM.
Packet Duplication in Dual Connectivity Enabled 5G Wireless Networks: Overview and Challenges
Venue: arXiv cs.NI 2019
Year: 2019

Enabling ultra-reliable low latency communications (uRLLC) over 5G wireless networks creates challenging design requirements, particularly on the air-interface. The stringent latency and reliability targets require enhancements at different layers of the protocol stack. On the other hand, the parallel redundancy protocol (PRP), wherein each data packet is duplicated and transmitted concurrently over two independent networks, provides a simple solution for improving reliability and reducing latency in wireless networks. PRP can be realized in cellular networks through the dual connectivity (DC) solution. Recently, 3GPP has introduced packet duplication functionality in 5G wireless networks. To this end, this paper provides an overview of the packet duplication functionality in 5G, in light of recent developments within 3GPP, and also highlights the related technical challenges.
Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
Venue: arXiv cs.LO 2019
Year: 2019

We employ tools from the fields of symbolic computation and satisfiability checking---namely, computer algebra systems and SAT solvers---to study the Williamson conjecture from combinatorial design theory and increase the bounds to which Williamson matrices have been enumerated. In particular, we completely enumerate all Williamson matrices of even order up to and including 70 which gives us deeper insight into the behaviour and distribution of Williamson matrices. We find that, in contrast to the case when the order is odd, Williamson matrices of even order are quite plentiful and exist in every even order up to and including 70. As a consequence of this and a new construction for 8-Williamson matrices we construct 8-Williamson matrices in all odd orders up to and including 35. We additionally enumerate all Williamson matrices whose orders are divisible by 3 and less than 70, finding one previously unknown set of Williamson matrices of order 63.
When Hypermutations and Ageing Enable Artificial Immune Systems to Outperform Evolutionary Algorithms
Venue: arXiv cs.NE 2019
Year: 2019

We present a time complexity analysis of the Opt-IA artificial immune system (AIS). We first highlight the power and limitations of its distinguishing operators (i.e., hypermutations with mutation potential and ageing) by analysing them in isolation. Recent work has shown that ageing combined with local mutations can help escape local optima on a dynamic optimisation benchmark function. We generalise this result by rigorously proving that, compared to evolutionary algorithms (EAs), ageing leads to impressive speed-ups on the standard Cliff benchmark function both when using local and global mutations. Unless the stop at first constructive mutation (FCM) mechanism is applied, we show that hypermutations require exponential expected runtime to optimise any function with a polynomial number of optima. If instead FCM is used, the expected runtime is at most a linear factor larger than the upper bound achieved for any random local search algorithm using the artificial fitness levels method. Nevertheless, we prove that algorithms using hypermutations can be considerably faster than EAs at escaping local optima. An analysis of the complete Opt-IA reveals that it is efficient on the previously considered functions and highlights problems where the use of the full algorithm is crucial. We complete the picture by presenting a class of functions for which Opt-IA fails with overwhelming probability while standard EAs are efficient.
Minimal series-parallel network realizations of bicubic impedances
Venue: arXiv cs.SY 2019
Year: 2019

An important open problem in the synthesis of passive controllers is to obtain a passive network that realizes an arbitrary given impedance function and contains the least possible number of elements. This problem has its origins in electric circuit theory, and is directly applicable to the cost-effective design of mechanical systems containing the inerter. Despite a rich history, the problem can only be considered solved for networks that contain at most two energy storage elements, and in a small number of other special cases. In this paper, we solve the minimal network realization problem for the class of impedances realized by series-parallel networks containing at most three energy storage elements. To accomplish this, we develop a novel continuity-based approach to eliminate redundant elements from a network.
A PTAS for subset TSP in minor-free graphs
Venue: arXiv cs.DS 2019
Year: 2019

We give the first PTAS for the subset Traveling Salesperson Problem (TSP) in $H$-minor-free graphs. This resolves a long standing open problem in a long line of work on designing PTASes for TSP in minor-closed families initiated by Grigni, Koutsoupias and Papadimitriou in FOCS'95. The main technical ingredient in our PTAS is a construction of a nearly light subset $(1+ε)$-spanner for any given edge-weighted $H$-minor-free graph. This construction is based on a necessary and sufficient condition given by \emph{sparse spanner oracles}: light subset spanners exist if and only if sparse spanner oracles exist. This relationship allows us to obtain two new results: _ An $(1+ε)$-spanner with lightness $O(ε^{-d+2})$ for any doubling metric of constant dimension $d$. This improves the earlier lightness bound $ε^{-O(d)}$ obtained by Borradaile, Le and Wulff-Nilsen. _ An $(1+ε)$-spanner with sublinear lightness for any metric of constant correlation dimension. Previously, no spanner with non-trivial lightness was known.
Detecting Multi-Oriented Text with Corner-based Region Proposals
Venue: arXiv cs.CV 2019
Year: 2019

Previous approaches for scene text detection usually rely on manually defined sliding windows. This work presents an intuitive two-stage region-based method to detect multi-oriented text without any prior knowledge regarding the textual shape. In the first stage, we estimate the possible locations of text instances by detecting and linking corners instead of shifting a set of default anchors. The quadrilateral proposals are geometry adaptive, which allows our method to cope with various text aspect ratios and orientations. In the second stage, we design a new pooling layer named Dual-RoI Pooling which embeds data augmentation inside the region-wise subnetwork for more robust classification and regression over these proposals. Experimental results on public benchmarks confirm that the proposed method is capable of achieving comparable performance with state-of-the-art methods. The code is publicly available at https://github.com/xhzdeng/crpn
Lazy Abstraction-Based Controller Synthesis
Venue: arXiv cs.SY 2019
Year: 2019

We present lazy abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against reach-avoid and safety specifications. State-of-the-art multi-layered ABCS pre-computes multiple finite-state abstractions of varying granularity and applies reactive synthesis to the coarsest abstraction whenever feasible, but adaptively considers finer abstractions when necessary. Lazy ABCS improves this technique by constructing abstractions on demand. Our insight is that the abstract transition relation only needs to be locally computed for a small set of frontier states at the precision currently required by the synthesis algorithm. We show that lazy ABCS can significantly outperform previous multi-layered ABCS algorithms: on standard benchmarks, lazy ABCS is more than 4 times faster.
3D Fluid Flow Estimation with Integrated Particle Reconstruction
Venue: arXiv cs.CV 2019
Year: 2019

The standard approach to densely reconstruct the motion in a volume of fluid is to inject high-contrast tracer particles and record their motion with multiple high-speed cameras. Almost all existing work processes the acquired multi-view video in two separate steps, utilizing either a pure Eulerian or pure Lagrangian approach. Eulerian methods perform a voxel-based reconstruction of particles per time step, followed by 3D motion estimation, with some form of dense matching between the precomputed voxel grids from different time steps. In this sequential procedure, the first step cannot use temporal consistency considerations to support the reconstruction, while the second step has no access to the original, high-resolution image data. Alternatively, Lagrangian methods reconstruct an explicit, sparse set of particles and track the individual particles over time. Physical constraints can only be incorporated in a post-processing step when interpolating the particle tracks to a dense motion field. We show, for the first time, how to jointly reconstruct both the individual tracer particles and a dense 3D fluid motion field from the image data, using an integrated energy minimization. Our hybrid Lagrangian/Eulerian model reconstructs individual particles, and at the same time recovers a dense 3D motion field in the entire domain. Making particles explicit greatly reduces the memory consumption and allows one to use the high-res input images for matching. Whereas the dense motion field makes it possible to include physical a-priori constraints and account for the incompressibility and viscosity of the fluid. The method exhibits greatly (~70%) improved results over our recently published baseline with two separate steps for 3D reconstruction and motion estimation. Our results with only two time steps are comparable to those of sota tracking-based methods that require much longer sequences.
Approximating Operator Norms via Generalized Krivine Rounding
Venue: arXiv cs.DS 2019
Year: 2019

We consider the $(\ell_p,\ell_r)$-Grothendieck problem, which seeks to maximize the bilinear form $y^T A x$ for an input matrix $A$ over vectors $x,y$ with $\|x\|_p=\|y\|_r=1$. The problem is equivalent to computing the $p \to r^*$ operator norm of $A$. The case $p=r=\infty$ corresponds to the classical Grothendieck problem. Our main result is an algorithm for arbitrary $p,r \ge 2$ with approximation ratio $(1+ε_0)/(\sinh^{-1}(1)\cdot γ_{p^*} \,γ_{r^*})$ for some fixed $ε_0 \le 0.00863$. Comparing this with Krivine's approximation ratio of $(π/2)/\sinh^{-1}(1)$ for the original Grothendieck problem, our guarantee is off from the best known hardness factor of $(γ_{p^*} γ_{r^*})^{-1}$ for the problem by a factor similar to Krivine's defect. Our approximation follows by bounding the value of the natural vector relaxation for the problem which is convex when $p,r \ge 2$. We give a generalization of random hyperplane rounding and relate the performance of this rounding to certain hypergeometric functions, which prescribe necessary transformations to the vector solution before the rounding is applied. Unlike Krivine's Rounding where the relevant hypergeometric function was $\arcsin$, we have to study a family of hypergeometric functions. The bulk of our technical work then involves methods from complex analysis to gain detailed information about the Taylor series coefficients of the inverses of these hypergeometric functions, which then dictate our approximation factor. Our result also implies improved bounds for "factorization through $\ell_{2}^{\,n}$" of operators from $\ell_{p}^{\,n}$ to $\ell_{q}^{\,m}$ (when $p\geq 2 \geq q$)--- such bounds are of significant interest in functional analysis and our work provides modest supplementary evidence for an intriguing parallel between factorizability, and constant-factor approximability.
Threshold Trapdoor Functions and Their Applications
Venue: arXiv cs.CR 2019
Year: 2019

We introduce a cryptographic primitive named threshold trapdoor functions (TTDFs), from which we give generic constructions of threshold and revocation encryptions under adaptive corruption model. Then, we show TTDF can be instantiated under the decisional Diffie-Hellman (DDH) assumption and the learning with errors (LWE) assumption. By combining the instantiations of TTDF with the generic constructions, we obtain threshold and revocation encryptions which compare favorably over existing schemes. The experimental results show that our proposed schemes are practical.
MaskReID: A Mask Based Deep Ranking Neural Network for Person Re-identification
Venue: arXiv cs.CV 2019
Year: 2019

Person retrieval faces many challenges including cluttered background, appearance variations (e.g., illumination, pose, occlusion) among different camera views and the similarity among different person's images. To address these issues, we put forward a novel mask based deep ranking neural network with a skipped fusing layer. Firstly, to alleviate the problem of cluttered background, masked images with only the foreground regions are incorporated as input in the proposed neural network. Secondly, to reduce the impact of the appearance variations, the multi-layer fusion scheme is developed to obtain more discriminative fine-grained information. Lastly, considering person retrieval is a special image retrieval task, we propose a novel ranking loss to optimize the whole network. The proposed ranking loss can further mitigate the interference problem of similar negative samples when producing ranking results. The extensive experiments validate the superiority of the proposed method compared with the state-of-the-art methods on many benchmark datasets.
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL
Venue: arXiv cs.LO 2019
Year: 2019

In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane.