OpenRaiser/Intern-Atlas huggingface dataset:
Denotational semantics for guarded dependent type theory
Venue: arXiv cs.LO 2020
Year: 2020

We present a new model of Guarded Dependent Type Theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with, and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion, and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann-Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.
Towards Generic Deobfuscation of Windows API Calls
Venue: arXiv cs.CR 2020
Year: 2020

A common way to get insight into a malicious program's functionality is to look at which API functions it calls. To complicate the reverse engineering of their programs, malware authors deploy API obfuscation techniques, hiding them from analysts' eyes and anti-malware scanners. This problem can be partially addressed by using dynamic analysis; that is, by executing a malware sample in a controlled environment and logging the API calls. However, malware that is aware of virtual machines and sandboxes might terminate without showing any signs of malicious behavior. In this paper, we introduce a static analysis technique allowing generic deobfuscation of Windows API calls. The technique utilizes symbolic execution and hidden Markov models to predict API names from the arguments passed to the API functions. Our best prediction model can correctly identify API names with 87.60% accuracy.
First-order queries on classes of structures with bounded expansion
Venue: arXiv cs.DB 2020
Year: 2020

We consider the evaluation of first-order queries over classes of databases with bounded expansion. The notion of bounded expansion is fairly broad and generalizes bounded degree, bounded treewidth and exclusion of at least one minor. It was known that over a class of databases with bounded expansion, first-order sentences could be evaluated in time linear in the size of the database. We give a different proof of this result. Moreover, we show that answers to first-order queries can be enumerated with constant delay after a linear time preprocessing. We also show that counting the number of answers to a query can be done in time linear in the size of the database.
A Short Survey on Sense-Annotated Corpora
Venue: arXiv cs.CL 2020
Year: 2020

Large sense-annotated datasets are increasingly necessary for training deep supervised systems in Word Sense Disambiguation. However, gathering high-quality sense-annotated data for as many instances as possible is a laborious and expensive task. This has led to the proliferation of automatic and semi-automatic methods for overcoming the so-called knowledge-acquisition bottleneck. In this short survey we present an overview of sense-annotated corpora, annotated either manually- or (semi)automatically, that are currently available for different languages and featuring distinct lexical resources as inventory of senses, i.e. WordNet, Wikipedia, BabelNet. Furthermore, we provide the reader with general statistics of each dataset and an analysis of their specific features.
Assigning times to minimise reachability in temporal graphs
Venue: arXiv cs.CC 2020
Year: 2020

Temporal graphs (in which edges are active at specified times) are of particular relevance for spreading processes on graphs, e.g.~the spread of disease or dissemination of information. Motivated by real-world applications, modification of static graphs to control this spread has proven a rich topic for previous research. Here, we introduce a new type of modification for temporal graphs: the number of active times for each edge is fixed, but we can change the relative order in which (sets of) edges are active. We investigate the problem of determining an ordering of edges that minimises the maximum number of vertices reachable from any single starting vertex; epidemiologically, this corresponds to the worst-case number of vertices infected in a single disease outbreak. We study two versions of this problem, both of which we show to be $\NP$-hard, and identify cases in which the problem can be solved or approximated efficiently.
Coconut: Threshold Issuance Selective Disclosure Credentials with Applications to Distributed Ledgers
Venue: arXiv cs.CR 2020
Year: 2020

Coconut is a novel selective disclosure credential scheme supporting distributed threshold issuance, public and private attributes, re-randomization, and multiple unlinkable selective attribute revelations. Coconut integrates with blockchains to ensure confidentiality, authenticity and availability even when a subset of credential issuing authorities are malicious or offline. We implement and evaluate a generic Coconut smart contract library for Chainspace and Ethereum; and present three applications related to anonymous payments, electronic petitions, and distribution of proxies for censorship resistance. Coconut uses short and computationally efficient credentials, and our evaluation shows that most Coconut cryptographic primitives take just a few milliseconds on average, with verification taking the longest time (10 milliseconds).
Third-Party Data Providers Ruin Simple Mechanisms
Venue: arXiv cs.GT 2020
Year: 2020

Motivated by the growing prominence of third-party data providers in online marketplaces, this paper studies the impact of the presence of third-party data providers on mechanism design. When no data provider is present, it has been shown that simple mechanisms are "good enough" -- they can achieve a constant fraction of the revenue of optimal mechanisms. The results in this paper demonstrate that this is no longer true in the presence of a third-party data provider who can provide the bidder with a signal that is correlated with the item type. Specifically, even with a single seller, a single bidder, and a single item of uncertain type for sale, the strategies of pricing each item-type separately (the analog of item pricing for multi-item auctions) and bundling all item-types under a single price (the analog of grand bundling) can both simultaneously be a logarithmic factor worse than the optimal revenue. Further, in the presence of a data provider, item-type partitioning mechanisms---a more general class of mechanisms which divide item-types into disjoint groups and offer prices for each group---still cannot achieve within a $\log \log$ factor of the optimal revenue. Thus, our results highlight that the presence of a data-provider forces the use of more complicated mechanisms in order to achieve a constant fraction of the optimal revenue.
WQO dichotomy for 3-graphs
Venue: arXiv cs.LO 2020
Year: 2020

We investigate data-enriched models, like Petri nets with data, where executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems in such models may depend on the structure of data domain. According to the WQO Dichotomy Conjecture, if a data domain is homogeneous then it either exhibits a well quasi-order (in which case decidability follows by standard arguments), or essentially all the decision problems are undecidable for Petri nets over that data domain. We confirm the conjecture for data domains being 3-graphs (graphs with 2-colored edges). On the technical level, this results is a significant step beyond known classification results for homogeneous structures.
Temporal Difference Models: Model-Free Deep RL for Model-Based Control
Venue: arXiv cs.LG 2020
Year: 2020

Model-free reinforcement learning (RL) is a powerful, general tool for learning complex behaviors. However, its sample efficiency is often impractically large for solving challenging real-world problems, even with off-policy algorithms such as Q-learning. A limiting factor in classic model-free RL is that the learning signal consists only of scalar rewards, ignoring much of the rich information contained in state transition tuples. Model-based RL uses this information, by training a predictive model, but often does not achieve the same asymptotic performance as model-free RL due to model bias. We introduce temporal difference models (TDMs), a family of goal-conditioned value functions that can be trained with model-free learning and used for model-based control. TDMs combine the benefits of model-free and model-based RL: they leverage the rich information in state transitions to learn very efficiently, while still attaining asymptotic performance that exceeds that of direct model-based RL methods. Our experimental results show that, on a range of continuous control tasks, TDMs provide a substantial improvement in efficiency compared to state-of-the-art model-based and model-free methods.
Surrogate Scoring Rules
Venue: arXiv cs.GT 2020
Year: 2020

Strictly proper scoring rules (SPSR) are incentive compatible for eliciting information about random variables from strategic agents when the principal can reward agents after the realization of the random variables. They also quantify the quality of elicited information, with more accurate predictions receiving higher scores in expectation. In this paper, we extend such scoring rules to settings where a principal elicits private probabilistic beliefs but only has access to agents' reports. We name our solution \emph{Surrogate Scoring Rules} (SSR). SSR build on a bias correction step and an error rate estimation procedure for a reference answer defined using agents' reports. We show that, with a single bit of information about the prior distribution of the random variables, SSR in a multi-task setting recover SPSR in expectation, as if having access to the ground truth. Therefore, a salient feature of SSR is that they quantify the quality of information despite the lack of ground truth, just as SPSR do for the setting \emph{with} ground truth. As a by-product, SSR induce \emph{dominant truthfulness} in reporting. Our method is verified both theoretically and empirically using data collected from real human forecasters.
O-Minimal Invariants for Discrete-Time Dynamical Systems
Venue: arXiv cs.CC 2020
Year: 2020

Termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of \emph{o-minimal invariants}, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory.
Continuity of Functional Transducers: A Profinite Study of Rational Functions
Venue: arXiv cs.FL 2020
Year: 2020

A word-to-word function is continuous for a class of languages~$\mathcal{V}$ if its inverse maps $\mathcal{V}$_languages to~$\mathcal{V}$. This notion provides a basis for an algebraic study of transducers, and was integral to the characterization of the sequential transducers computable in some circuit complexity classes. Here, we report on the decidability of continuity for functional transducers and some standard classes of regular languages. To this end, we develop a robust theory rooted in the standard profinite analysis of regular languages. Since previous algebraic studies of transducers have focused on the sole structure of the underlying input automaton, we also compare the two algebraic approaches. We focus on two questions: When are the automaton structure and the continuity properties related, and when does continuity propagate to superclasses?
Polyhedral Characterization of Reversible Hinged Dissections
Venue: arXiv cs.CG 2020
Year: 2020

We prove that two polygons $A$ and $B$ have a reversible hinged dissection (a chain hinged dissection that reverses inside and outside boundaries when folding between $A$ and $B$) if and only if $A$ and $B$ are two noncrossing nets of a common polyhedron. Furthermore, monotone reversible hinged dissections (where all hinges rotate in the same direction when changing from $A$ to $B$) correspond exactly to noncrossing nets of a common convex polyhedron. By envelope/parcel magic, it becomes easy to design many hinged dissections.
Robust Odometry using Sensor Consensus Analysis
Venue: arXiv cs.RO 2020
Year: 2020

Odometry forms an important component of many manned and autonomous systems. In the rail industry in particular, having precise and robust odometry is crucial for the correct operation of the Automatic Train Protection systems that ensure the safety of high-speed trains in operation around the world. Two problems commonly encountered in such odometry systems are miscalibration of the wheel encoders and slippage of the wheels under acceleration and braking, resulting in incorrect velocity estimates. This paper introduces an odometry system that addresses these problems. It comprises of an Extended Kalman Filter that tracks the calibration of the wheel encoders as state variables, and a measurement pre-processing stage called Sensor Consensus Analysis (SCA) that scales the uncertainty of a measurement based on how consistent it is with the measurements from the other sensors. SCA uses the statistical z-test to determine when an individual measurement is inconsistent with the other measurements, and scales the uncertainty until the z-test passes. This system is demonstrated on data from German Intercity-Express high-speed trains and it is shown to successfully deal with errors due to miscalibration and wheel slip.
Redundancy in Distributed Proofs
Venue: arXiv cs.DC 2020
Year: 2020

Distributed proofs are mechanisms enabling the nodes of a network to collectivity and efficiently check the correctness of Boolean predicates on the structure of the network, or on data-structures distributed over the nodes (e.g., spanning trees or routing tables). We consider mechanisms consisting of two components: a \emph{prover} assigning a \emph{certificate} to each node, and a distributed algorithm called \emph{verifier} that is in charge of verifying the distributed proof formed by the collection of all certificates. In this paper, we show that many network predicates have distributed proofs offering a high level of redundancy, explicitly or implicitly. We use this remarkable property of distributed proofs for establishing perfect tradeoffs between the \emph{size of the certificate} stored at every node, and the \emph{number of rounds} of the verification protocol. If we allow every node to communicate to distance at most $t$, one might expect that the certificate sizes can be reduced by a multiplicative factor of at least~$t$. In trees, cycles and grids, we show that such tradeoffs can be established for \emph{all} network predicates, i.e., it is always possible to linearly decrease the certificate size. In arbitrary graphs, we show that any part of the certificates common to all nodes can be evenly redistributed among these nodes, achieving even a better tradeoff: this common part of the certificate can be reduced by the size of a smallest ball of radius $t$ in the network. In addition to these general results, we establish several upper and lower bounds on the certificate sizes used for distributed proofs for spanning trees, minimum-weight spanning trees, diameter, additive and multiplicative spanners, and more, improving and generalizing previous results from the literature.
Improved Distributed $Δ$-Coloring
Venue: arXiv cs.DS 2020
Year: 2020

We present a randomized distributed algorithm that computes a $Δ$-coloring in any non-complete graph with maximum degree $Δ\geq 4$ in $O(\log Δ) + 2^{O(\sqrt{\log\log n})}$ rounds, as well as a randomized algorithm that computes a $Δ$-coloring in $O((\log \log n)^2)$ rounds when $Δ\in [3, O(1)]$. Both these algorithms improve on an $O(\log^3 n/\log Δ)$-round algorithm of Panconesi and Srinivasan~[STOC'1993], which has remained the state of the art for the past 25 years. Moreover, the latter algorithm gets (exponentially) closer to an $Ω(\log\log n)$ round lower bound of Brandt et al.~[STOC'16].
Concept2vec: Metrics for Evaluating Quality of Embeddings for Ontological Concepts
Venue: arXiv cs.CL 2020
Year: 2020

Although there is an emerging trend towards generating embeddings for primarily unstructured data and, recently, for structured data, no systematic suite for measuring the quality of embeddings has been proposed yet. This deficiency is further sensed with respect to embeddings generated for structured data because there are no concrete evaluation metrics measuring the quality of the encoded structure as well as semantic patterns in the embedding space. In this paper, we introduce a framework containing three distinct tasks concerned with the individual aspects of ontological concepts: (i) the categorization aspect, (ii) the hierarchical aspect, and (iii) the relational aspect. Then, in the scope of each task, a number of intrinsic metrics are proposed for evaluating the quality of the embeddings. Furthermore, w.r.t. this framework, multiple experimental studies were run to compare the quality of the available embedding models. Employing this framework in future research can reduce misjudgment and provide greater insight about quality comparisons of embeddings for ontological concepts. We positioned our sampled data and code at https://github.com/alshargi/Concept2vec under GNU General Public License v3.0.
Defending against Adversarial Attack towards Deep Neural Networks via Collaborative Multi-task Training
Venue: arXiv cs.LG 2020
Year: 2020

Deep neural networks (DNNs) are known to be vulnerable to adversarial examples which contain human-imperceptible perturbations. A series of defending methods, either proactive defence or reactive defence, have been proposed in the recent years. However, most of the methods can only handle specific attacks. For example, proactive defending methods are invalid against grey-box or white-box attacks, while reactive defending methods are challenged by low-distortion adversarial examples or transferring adversarial examples. This becomes a critical problem since a defender usually does not have the type of the attack as a priori knowledge. Moreover, existing two-pronged defences (e.g., MagNet), which take advantages of both proactive and reactive methods, have been reported as broken under transferring attacks. To address this problem, this paper proposed a novel defensive framework based on collaborative multi-task training, aiming at providing defence for different types of attacks. The proposed defence first encodes training labels into label pairs and counters black-box attacks leveraging adversarial training supervised by the encoded label pairs. The defence further constructs a detector to identify and reject high-confidence adversarial examples that bypass the black-box defence. In addition, the proposed collaborative architecture can prevent adversaries from finding valid adversarial examples when the defence strategy is exposed. In the experiments, we evaluated our defence against four state-of-the-art attacks on $MNIST$ and $CIFAR10$ datasets. The results showed that our defending method achieved up to $96.3\%$ classification accuracy on black-box adversarial examples, and detected up to $98.7\%$ of the high confidence adversarial examples. It only decreased the model accuracy on benign example classification by $2.1\%$ for the $CIFAR10$ dataset.
Fully Automated HTML and Javascript Rewriting for Constructing a Self-healing Web Proxy
Venue: arXiv cs.SE 2020
Year: 2020

Over the last few years, the complexity of web applications has increased to provide more dynamic web applications to users. The drawback of this complexity is the growing number of errors in the front-end applications. In this paper, we present an approach to provide self-healing for the web. We implemented this approach in two different tools: 1) BikiniProxy, an HTTP repair proxy, and 2) BugBlock, a browser extension. They use five self-healing strategies to rewrite the buggy HTML and Javascript code to handle errors in web pages. We evaluate BikiniProxy and BugBlock with a new benchmark of 555 reproducible Javascript errors of which 31.76% can be automatically self-healed by BikiniProxy and 15.67% by BugBlock.
Blockclique: scaling blockchains through transaction sharding in a multithreaded block graph
Venue: arXiv cs.CR 2020
Year: 2020

Decentralized crypto-currencies based on the blockchain architecture under-utilize available network bandwidth, making them unable to scale to thousands of transactions per second. We define the Blockclique architecture, that addresses this limitation by sharding transactions in a block graph with a fixed number of threads. The architecture allows the creation of intrinsically compatible blocks in parallel, where each block references one previous block of each thread. The consistency of the Blockclique protocol is formally established in presence of attackers. An experimental evaluation of the architecture's performance in large realistic networks demonstrates an efficient use of available bandwidth and a throughput of thousands of transactions per second.
Tight Query Complexity Lower Bounds for PCA via Finite Sample Deformed Wigner Law
Venue: arXiv cs.LG 2020
Year: 2020

We prove a \emph{query complexity} lower bound for approximating the top $r$ dimensional eigenspace of a matrix. We consider an oracle model where, given a symmetric matrix $\mathbf{M} \in \mathbb{R}^{d \times d}$, an algorithm $\mathsf{Alg}$ is allowed to make $\mathsf{T}$ exact queries of the form $\mathsf{w}^{(i)} = \mathbf{M} \mathsf{v}^{(i)}$ for $i$ in $\{1,...,\mathsf{T}\}$, where $\mathsf{v}^{(i)}$ is drawn from a distribution which depends arbitrarily on the past queries and measurements $\{\mathsf{v}^{(j)},\mathsf{w}^{(i)}\}_{1 \le j \le i-1}$. We show that for every $\mathtt{gap} \in (0,1/2]$, there exists a distribution over matrices $\mathbf{M}$ for which 1) $\mathrm{gap}_r(\mathbf{M}) = Ω(\mathtt{gap})$ (where $\mathrm{gap}_r(\mathbf{M})$ is the normalized gap between the $r$ and $r+1$-st largest-magnitude eigenvector of $\mathbf{M}$), and 2) any algorithm $\mathsf{Alg}$ which takes fewer than $\mathrm{const} \times \frac{r \log d}{\sqrt{\mathtt{gap}}}$ queries fails (with overwhelming probability) to identity a matrix $\widehat{\mathsf{V}} \in \mathbb{R}^{d \times r}$ with orthonormal columns for which $\langle \widehat{\mathsf{V}}, \mathbf{M} \widehat{\mathsf{V}}\rangle \ge (1 - \mathrm{const} \times \mathtt{gap})\sum_{i=1}^r λ_i(\mathbf{M})$. Our bound requires only that $d$ is a small polynomial in $1/\mathtt{gap}$ and $r$, and matches the upper bounds of Musco and Musco '15. Moreover, it establishes a strict separation between convex optimization and \emph{randomized}, "strict-saddle" non-convex optimization of which PCA is a canonical example: in the former, first-order methods can have dimension-free iteration complexity, whereas in PCA, the iteration complexity of gradient-based methods must necessarily grow with the dimension.