OpenRaiser/Intern-Atlas huggingface dataset:
Faster Random $k$-CNF Satisfiability
Venue: arXiv cs.CC 2019
Year: 2019

We describe an algorithm to solve the problem of Boolean CNF-Satisfiability when the input formula is chosen randomly. We build upon the algorithms of Sch{ö}ning 1999 and Dantsin et al.~in 2002. The Sch{ö}ning algorithm works by trying many possible random assignments, and for each one searching systematically in the neighborhood of that assignment for a satisfying solution. Previous algorithms for this problem run in time $O(2^{n (1- Ω(1)/k)})$. Our improvement is simple: we count how many clauses are satisfied by each randomly sampled assignment, and only search in the neighborhoods of assignments with abnormally many satisfied clauses. We show that assignments like these are significantly more likely to be near a satisfying assignment. This improvement saves a factor of $2^{n Ω(\lg^2 k)/k}$, resulting in an overall runtime of $O(2^{n (1- Ω(\lg^2 k)/k)})$ for random $k$-SAT.
Restricting Control Flow During Speculative Execution with Venkman
Venue: arXiv cs.CR 2019
Year: 2019

Side-channel attacks such as Spectre that utilize speculative execution to steal application secrets pose a significant threat to modern computing systems. While program transformations can mitigate some Spectre attacks, more advanced attacks can divert control flow speculatively to bypass these protective instructions, rendering existing defenses useless. In this paper, we present Venkman: a system that employs program transformation to completely thwart Spectre attacks that poison entries in the Branch Target Buffer (BTB) and the Return Stack Buffer (RSB). Venkman transforms code so that all valid targets of a control-flow transfer have an identical alignment in the virtual address space; it further transforms all branches to ensure that all entries added to the BTB and RSB are properly aligned. By transforming all code this way, Venkman ensures that, in any program wanting Spectre defenses, all control-flow transfers, including speculative ones, do not skip over protective instructions Venkman adds to the code segment to mitigate Spectre attacks. Unlike existing defenses, Venkman does not reduce sharing of the BTB and RSB and does not flush these structures, allowing safe sharing and reuse among programs while maintaining strong protection against Spectre attacks. We built a prototype of Venkman on an IBM POWER8 machine. Our evaluation on the SPEC benchmarks and selected applications shows that Venkman increases execution time to 3.47$\times$ on average and increases code size to 1.94$\times$ on average when it is used to ensure that fences are executed to mitigate Spectre attacks. Our evaluation also shows that Spectre-resistant Software Fault Isolation (SFI) built using Venkman incurs a geometric mean of 2.42$\times$ space overhead and 1.68$\times$ performance overhead.
Robustness of Neural Networks to Parameter Quantization
Venue: arXiv cs.LG 2019
Year: 2019

Quantization, a commonly used technique to reduce the memory footprint of a neural network for edge computing, entails reducing the precision of the floating-point representation used for the parameters of the network. The impact of such rounding-off errors on the overall performance of the neural network is estimated using testing, which is not exhaustive and thus cannot be used to guarantee the safety of the model. We present a framework based on Satisfiability Modulo Theory (SMT) solvers to quantify the robustness of neural networks to parameter perturbation. To this end, we introduce notions of local and global robustness that capture the deviation in the confidence of class assignments due to parameter quantization. The robustness notions are then cast as instances of SMT problems and solved automatically using solvers, such as dReal. We demonstrate our framework on two simple Multi-Layer Perceptrons (MLP) that perform binary classification on a two-dimensional input. In addition to quantifying the robustness, we also show that Rectified Linear Unit activation results in higher robustness than linear activations for our MLPs.
Probabilistic Dense Reconstruction from a Moving Camera
Venue: arXiv cs.RO 2019
Year: 2019

This paper presents a probabilistic approach for online dense reconstruction using a single monocular camera moving through the environment. Compared to spatial stereo, depth estimation from motion stereo is challenging due to insufficient parallaxes, visual scale changes, pose errors, etc. We utilize both the spatial and temporal correlations of consecutive depth estimates to increase the robustness and accuracy of monocular depth estimation. An online, recursive, probabilistic scheme to compute depth estimates, with corresponding covariances and inlier probability expectations, is proposed in this work. We integrate the obtained depth hypotheses into dense 3D models in an uncertainty-aware way. We show the effectiveness and efficiency of our proposed approach by comparing it with state-of-the-art methods in the TUM RGB-D SLAM and ICL-NUIM dataset. Online indoor and outdoor experiments are also presented for performance demonstration.
On the tractability of the maximum clique problem
Venue: arXiv cs.DS 2019
Year: 2019

The maximum clique problem is a classical NP-complete problem in graph theory and has important applications in many domains. In this paper we show, in a partially non-constructive way, the existence of an exact polynomial-time algorithm for this problem. We outline the algorithm in pseudo-code style. Then we prove its exactness and efficiency by analysis.
Syntactic View of Sigma-Tau Generation of Permutations
Venue: arXiv cs.DS 2019
Year: 2019

We give a syntactic view of the Sawada-Williams $(σ,τ)$-generation of permutations. The corresponding sequence of $σ-τ$-operations, of length $n!-1$ is shown to be highly compressible: it has $O(n^2\log n)$ bit description. Using this compact description we design fast algorithms for ranking and unranking permutations.
Domain Representation for Knowledge Graph Embedding
Venue: arXiv cs.AI 2019
Year: 2019

Embedding entities and relations into a continuous multi-dimensional vector space have become the dominant method for knowledge graph embedding in representation learning. However, most existing models ignore to represent hierarchical knowledge, such as the similarities and dissimilarities of entities in one domain. We proposed to learn a Domain Representations over existing knowledge graph embedding models, such that entities that have similar attributes are organized into the same domain. Such hierarchical knowledge of domains can give further evidence in link prediction. Experimental results show that domain embeddings give a significant improvement over the most recent state-of-art baseline knowledge graph embedding models.
Interoperability and machine-to-machine translation model with mappings to machine learning tasks
Venue: arXiv cs.LG 2019
Year: 2019

Modern large-scale automation systems integrate thousands to hundreds of thousands of physical sensors and actuators. Demands for more flexible reconfiguration of production systems and optimization across different information models, standards and legacy systems challenge current system interoperability concepts. Automatic semantic translation across information models and standards is an increasingly important problem that needs to be addressed to fulfill these demands in a cost-efficient manner under constraints of human capacity and resources in relation to timing requirements and system complexity. Here we define a translator-based operational interoperability model for interacting cyber-physical systems in mathematical terms, which includes system identification and ontology-based translation as special cases. We present alternative mathematical definitions of the translator learning task and mappings to similar machine learning tasks and solutions based on recent developments in machine learning. Possibilities to learn translators between artefacts without a common physical context, for example in simulations of digital twins and across layers of the automation pyramid are briefly discussed.
Partitioning a Symmetric Rational Relation into Two Asymmetric Rational Relations
Venue: arXiv cs.FL 2019
Year: 2019

We consider the problem of partitioning effectively a given symmetric (and irreflexive) rational relation R into two asymmetric rational relations. This problem is motivated by a recent method of embedding an R-independent language into one that is maximal R-independent, where the method requires to use an asymmetric partition of R. We solve the problem when R is realized by a zero-avoiding transducer (with some bound k): if the absolute value of the input-output length discrepancy of a computation exceeds k then the length discrepancy of the computation cannot become zero. This class of relations properly contains all recognizable, all left synchronous, and all right synchronous relations. We leave the asymmetric partition problem open when R is not realized by a zero-avoiding transducer. We also show examples of total wordorderings for which there is a relation R that cannot be partitioned into two asymmetric rational relations such that one of them is decreasing with respect to the given word-ordering.
Loopy Cuts: Surface-Field Aware Block Decomposition for Hex-Meshing
Venue: arXiv cs.GR 2019
Year: 2019

We present a new fully automatic block-decomposition hexahedral meshing algorithm capable of producing high quality meshes that strictly preserve feature curve networks on the input surface and align with an input surface cross-field. We produce all-hex meshes on the vast majority of inputs, and introduce localized non-hex elements only when the surface feature network necessitates those. The input to our framework is a closed surface with a collection of geometric or user-demarcated feature curves and a feature-aligned surface cross-field. Its output is a compact set of blocks whose edges interpolate these features and are loosely aligned with this cross-field. We obtain this block decomposition by cutting the input model using a collection of simple cutting surfaces bounded by closed surface loops. The set of cutting loops spans the input feature curves, ensuring feature preservation, and is obtained using a field-space sampling process. The computed loops are uniformly distributed across the surface, cross orthogonally, and are loosely aligned with the cross-field directions, inducing the desired block decomposition. We validate our method by applying it to a large range of complex inputs and comparing our results to those produced by state-of-the-art alternatives. Contrary to prior approaches, our framework consistently produces high-quality field aligned meshes while strictly preserving geometric or user-specified surface features.
Existential Ontology and Thinging Modeling in Software Engineering
Venue: arXiv cs.SE 2019
Year: 2019

This study is a sequel to a previous study entitled Thinging for Software Engineers, which showed that the notion of thing, in contrast to objectification, has some beneficial orientations in modeling. The incorporation of thinging in conceptual modeling is required to explain the roots of Heidegger s conception of things. This requires an understanding of Heidegger s existential ontology to identify any relationship to thinging. This paper is an exploration of existential ontology in search of further clarification of the concept of thinging. We start by reviewing the thinging machine (TM) introduced in Thinging for Software Engineers and provide a full example of its utilization in modeling an ordering system. We follow this with a discussion of the being (existence) of things in the word and Heidegger s interpretation of time as a possible horizon for any understanding whatsoever of being. We emphasize that the TM is not related directly to the Heideggerian notion of existence and its elaborate analysis of Dasein. However, there may be some benefit to studying non-Dasein things to provide a philosophical foundation to thinging, as utilized in TM modeling. Interestingly, the TM can be utilized to model existential ontology, thus increasing the level of understanding about them.
Generalized Feedback Loop for Joint Hand-Object Pose Estimation
Venue: arXiv cs.CV 2019
Year: 2019

We propose an approach to estimating the 3D pose of a hand, possibly handling an object, given a depth image. We show that we can correct the mistakes made by a Convolutional Neural Network trained to predict an estimate of the 3D pose by using a feedback loop. The components of this feedback loop are also Deep Networks, optimized using training data. This approach can be generalized to a hand interacting with an object. Therefore, we jointly estimate the 3D pose of the hand and the 3D pose of the object. Our approach performs en-par with state-of-the-art methods for 3D hand pose estimation, and outperforms state-of-the-art methods for joint hand-object pose estimation when using depth images only. Also, our approach is efficient as our implementation runs in real-time on a single GPU.
Learning Quadrangulated Patches For 3D Shape Processing
Venue: arXiv cs.CV 2019
Year: 2019

We propose a system for surface completion and inpainting of 3D shapes using generative models, learnt on local patches. Our method uses a novel encoding of height map based local patches parameterized using 3D mesh quadrangulation of the low resolution input shape. This provides us sufficient amount of local 3D patches to learn a generative model for the task of repairing moderate sized holes. Following the ideas from the recent progress in 2D inpainting, we investigated both linear dictionary based model and convolutional denoising autoencoders based model for the task for inpainting, and show our results to be better than the previous geometry based method of surface inpainting. We validate our method on both synthetic shapes and real world scans.
Exploring Confidence Measures for Word Spotting in Heterogeneous Datasets
Venue: arXiv cs.CV 2019
Year: 2019

In recent years, convolutional neural networks (CNNs) took over the field of document analysis and they became the predominant model for word spotting. Especially attribute CNNs, which learn the mapping between a word image and an attribute representation, showed exceptional performances. The drawback of this approach is the overconfidence of neural networks when used out of their training distribution. In this paper, we explore different metrics for quantifying the confidence of a CNN in its predictions, specifically on the retrieval problem of word spotting. With these confidence measures, we limit the inability of a retrieval list to reject certain candidates. We investigate four different approaches that are either based on the network's attribute estimations or make use of a surrogate model. Our approach also aims at answering the question for which part of a dataset the retrieval system gives reliable results. We further show that there exists a direct relation between the proposed confidence measures and the quality of an estimated attribute representation.
Towards Resilient 5G: Lessons Learned from Experimental Evaluations of LTE Uplink Jamming
Venue: arXiv cs.NI 2019
Year: 2019

Energy, water, health, transportation and emergency services act as backbones for our society. Aiming at high degrees of efficiency, these systems are increasingly automated, depending on communication systems. However, this makes these Critical Infrastructures (CI) prone to cyber attacks, resulting in data leaks, reduced performance or even total system failure. Beyond a survey of existing vulnerabilities, we provide an experimental evaluation of targeted uplink jamming against LTE's air interface. Primarily, our implementations of smart attacks on the LTE Physical Uplink Control Channel (PUCCH), the Physical Uplink Shared Channel (PUSCH) as well as on the radio access procedure are outlined and tested. In exploiting the unencrypted resource assignment process, these attacks are able to target and jam specific UE resources, effectively denying uplink access. Evaluation results reveal the criticality of such attacks, severely destabilizing CI, while minimizing attacker exposure. Finally we derive possible mitigations and recommendations for 5G stakeholders, which serve to improve the robustness of mission critical communications and enable the design of resilient next generation mobile networks.
On the Influence of Bias-Correction on Distributed Stochastic Optimization
Venue: arXiv cs.LG 2019
Year: 2019

Various bias-correction methods such as EXTRA, gradient tracking methods, and exact diffusion have been proposed recently to solve distributed {\em deterministic} optimization problems. These methods employ constant step-sizes and converge linearly to the {\em exact} solution under proper conditions. However, their performance under stochastic and adaptive settings is less explored. It is still unknown {\em whether}, {\em when} and {\em why} these bias-correction methods can outperform their traditional counterparts (such as consensus and diffusion) with noisy gradient and constant step-sizes. This work studies the performance of exact diffusion under the stochastic and adaptive setting, and provides conditions under which exact diffusion has superior steady-state mean-square deviation (MSD) performance than traditional algorithms without bias-correction. In particular, it is proven that this superiority is more evident over sparsely-connected network topologies such as lines, cycles, or grids. Conditions are also provided under which exact diffusion method match or may even degrade the performance of traditional methods. Simulations are provided to validate the theoretical findings.
Apache Hive: From MapReduce to Enterprise-grade Big Data Warehousing
Venue: arXiv cs.DB 2019
Year: 2019

Apache Hive is an open-source relational database system for analytic big-data workloads. In this paper we describe the key innovations on the journey from batch tool to fully fledged enterprise data warehousing system. We present a hybrid architecture that combines traditional MPP techniques with more recent big data and cloud concepts to achieve the scale and performance required by today's analytic applications. We explore the system by detailing enhancements along four main axis: Transactions, optimizer, runtime, and federation. We then provide experimental results to demonstrate the performance of the system for typical workloads and conclude with a look at the community roadmap.
On the Benefits of Populations on the Exploitation Speed of Standard Steady-State Genetic Algorithms
Venue: arXiv cs.NE 2019
Year: 2019

It is generally accepted that populations are useful for the global exploration of multi-modal optimisation problems. Indeed, several theoretical results are available showing such advantages over single-trajectory search heuristics. In this paper we provide evidence that evolving populations via crossover and mutation may also benefit the optimisation time for hillclimbing unimodal functions. In particular, we prove bounds on the expected runtime of the standard ($μ$+1)~GA for OneMax that are lower than its unary black box complexity and decrease in the leading constant with the population size up to $μ=O(\sqrt{\log n})$. Our analysis suggests that the optimal mutation strategy is to flip two bits most of the time. To achieve the results we provide two interesting contributions to the theory of randomised search heuristics: 1) A novel application of drift analysis which compares absorption times of different Markov chains without defining an explicit potential function. 2) The inversion of fundamental matrices to calculate the absorption times of the Markov chains. The latter strategy was previously proposed in the literature but to the best of our knowledge this is the first time is has been used to show non-trivial bounds on expected runtimes.
Explaining Deep Neural Networks with a Polynomial Time Algorithm for Shapley Values Approximation
Venue: arXiv cs.LG 2019
Year: 2019

The problem of explaining the behavior of deep neural networks has recently gained a lot of attention. While several attribution methods have been proposed, most come without strong theoretical foundations, which raises questions about their reliability. On the other hand, the literature on cooperative game theory suggests Shapley values as a unique way of assigning relevance scores such that certain desirable properties are satisfied. Unfortunately, the exact evaluation of Shapley values is prohibitively expensive, exponential in the number of input features. In this work, by leveraging recent results on uncertainty propagation, we propose a novel, polynomial-time approximation of Shapley values in deep neural networks. We show that our method produces significantly better approximations of Shapley values than existing state-of-the-art attribution methods.
Optimising the Input Image to Improve Visual Relationship Detection
Venue: arXiv cs.CV 2019
Year: 2019

Visual Relationship Detection is defined as, given an image composed of a subject and an object, the correct relation is predicted. To improve the visual part of this difficult problem, ten preprocessing methods were tested to determine whether the widely used Union method yields the optimal results. Therefore, focusing solely on predicate prediction, no object detection and linguistic knowledge were used to prevent them from affecting the comparison results. Once fine-tuned, the Visual Geometry Group models were evaluated using Recall@1, per-predicate recall, activation maximisations, class activation maps, and error analysis. From this research it was found that using preprocessing methods such as the Union-Without-Background-and-with-Binary-mask (Union-WB-and-B) method yields significantly better results than the widely used Union method since, as designed, it enables the Convolutional Neural Network to also identify the subject and object in the convolutional layers instead of solely in the fully-connected layers.
Formation control on Jordan curves based on noisy proximity measurements
Venue: arXiv cs.SY 2019
Year: 2019

The paradigmatic formation control problem of steering a multi-agent system towards a balanced circular formation has been the subject of extensive studies in the control engineering community. Indeed, this is due to the fact that it shares several features with relevant applications such as distributed environmental monitoring or fence-patrolling. However, these applications may also present some relevant differences from the ideal setting such as the curve on which the formation must be achieved not being a circle, or the measurements being neither ideal nor as a continuous information flow. In this work, we attempt to fill this gap between theory and applications by considering the problem of steering a multi-agent system towards a balanced formation on a generic closed curve and under very restrictive assumptions on the information flow amongst the agents. We tackle this problem through an estimation and control strategy that borrows tools from interval analysis to guarantee the robustness that is required in the considered scenario.
Tool Support of Formal Methods for Privacy by Design
Venue: arXiv cs.CR 2019
Year: 2019

Formal methods are, in principle, suited for supporting the recent paradigm of privacy by design, but no overview is available that summarizes which particular approaches have been investigated, for which application domains they are suited, and whether they are implemented and available as tools. Using the techniques of search-based literature review and snowballing this paper answers those questions for a selected set of research papers.