OpenRaiser/Intern-Atlas huggingface dataset:
Approximating Multistage Matching Problems
Venue: arXiv cs.DS 2021
Year: 2021

In multistage perfect matching problems we are given a sequence of graphs on the same vertex set and asked to find a sequence of perfect matchings, corresponding to the sequence of graphs, such that consecutive matchings are as similar as possible. More precisely, we aim to maximize the intersections, or minimize the unions between consecutive matchings. We show that these problems are NP-hard even in very restricted scenarios. We propose new approximation algorithms and present methods to transfer results between different problem variants without loosing approximation guarantees.
In Search for an Optimal Authenticated Byzantine Agreement
Venue: arXiv cs.DC 2021
Year: 2021

In this paper, we challenge the conventional approach of state machine replication systems to design deterministic agreement protocols in the eventually synchronous communication model. We first prove that no such protocol can guarantee bounded communication cost before the global stabilization time and propose a different approach that hopes for the best (synchrony) but prepares for the worst (asynchrony). Accordingly, we design an optimistic byzantine agreement protocol that first tries an efficient deterministic algorithm that relies on synchrony for termination only, and then, only if an agreement was not reached due to asynchrony, the protocol uses a randomized asynchronous protocol for fallback that guarantees termination with probability 1. We formally prove that our protocol achieves optimal communication complexity under all network conditions and failure scenarios. We first prove a lower bound of $Ω(ft+ t)$ for synchronous deterministic byzantine agreement protocols, where $t$ is the failure threshold, and $f$ is the actual number of failures. Then, we present a tight upper bound and use it for the synchronous part of the optimistic protocol. Finally, for the asynchronous fallback, we use a variant of the (optimal) VABA protocol, which we reconstruct to safely combine it with the synchronous part. We believe that our adaptive to failures synchronous byzantine agreement protocol has an independent interest since it is the first protocol we are aware of which communication complexity optimally depends on the actual number of failures.
The upper density of an automatic set is rational
Venue: arXiv cs.FL 2021
Year: 2021

Given a natural number $k\ge 2$ and a $k$-automatic set $S$ of natural numbers, we show that the lower density and upper density of $S$ are recursively computable rational numbers and we provide an algorithm for computing these quantities. In addition, we show that for every natural number $k\ge 2$ and every pair of rational numbers $(α,β)$ with $0<α<β<1$ or with $(α,β)\in \{(0,0),(1,1)\}$ there is a $k$-automatic subset of the natural numbers whose lower density and upper density are $α$ and $β$ respectively, and we show that these are precisely the values that can occur as the lower and upper densities of an automatic set.
Langevin DQN
Venue: arXiv cs.LG 2021
Year: 2021

Algorithms that tackle deep exploration -- an important challenge in reinforcement learning -- have relied on epistemic uncertainty representation through ensembles or other hypermodels, exploration bonuses, or visitation count distributions. An open question is whether deep exploration can be achieved by an incremental reinforcement learning algorithm that tracks a single point estimate, without additional complexity required to account for epistemic uncertainty. We answer this question in the affirmative. In particular, we develop Langevin DQN, a variation of DQN that differs only in perturbing parameter updates with Gaussian noise and demonstrate through a computational study that the presented algorithm achieves deep exploration. We also offer some intuition to how Langevin DQN achieves deep exploration. In addition, we present a modification of the Langevin DQN algorithm to improve the computational efficiency.
The power of adaptivity in source identification with time queries on the path
Venue: arXiv cs.DS 2021
Year: 2021

We study the problem of identifying the source of a stochastic diffusion process spreading on a graph based on the arrival times of the diffusion at a few queried nodes. In a graph $G=(V,E)$, an unknown source node $v^* \in V$ is drawn uniformly at random, and unknown edge weights $w(e)$ for $e\in E$, representing the propagation delays along the edges, are drawn independently from a Gaussian distribution of mean $1$ and variance $σ^2$. An algorithm then attempts to identify $v^*$ by querying nodes $q \in V$ and being told the length of the shortest path between $q$ and $v^*$ in graph $G$ weighted by $w$. We consider two settings: non-adaptive, in which all query nodes must be decided in advance, and adaptive, in which each query can depend on the results of the previous ones. Both settings are motivated by an application of the problem to epidemic processes (where the source is called patient zero), which we discuss in detail. We characterize the query complexity when $G$ is an $n$-node path. In the non-adaptive setting, $Θ(nσ^2)$ queries are needed for $σ^2 \leq 1$, and $Θ(n)$ for $σ^2 \geq 1$. In the adaptive setting, somewhat surprisingly, only $Θ(\log\log_{1/σ}n)$ are needed when $σ^2 \leq 1/2$, and $Θ(\log \log n)+O_σ(1)$ when $σ^2 \geq 1/2$. This is the first mathematical study of source identification with time queries in a non-deterministic diffusion process.
Structural Invariants for the Verification of Systems with Parameterized Architectures
Venue: arXiv cs.DC 2021
Year: 2021

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology of the system (e.g.\ pipeline, ring). The logic can be easily embedded in monadic second order logic of finitely many successors, and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.
A Possibility in Algorithmic Fairness: Can Calibration and Equal Error Rates Be Reconciled?
Venue: arXiv cs.LG 2021
Year: 2021

Decision makers increasingly rely on algorithmic risk scores to determine access to binary treatments including bail, loans, and medical interventions. In these settings, we reconcile two fairness criteria that were previously shown to be in conflict: calibration and error rate equality. In particular, we derive necessary and sufficient conditions for the existence of calibrated scores that yield classifications achieving equal error rates at any given group-blind threshold. We then present an algorithm that searches for the most accurate score subject to both calibration and minimal error rate disparity. Applied to the COMPAS criminal risk assessment tool, we show that our method can eliminate error disparities while maintaining calibration. In a separate application to credit lending, we compare our procedure to the omission of sensitive features and show that it raises both profit and the probability that creditworthy individuals receive loans.
Sampling in Software Engineering Research: A Critical Review and Guidelines
Venue: arXiv cs.SE 2021
Year: 2021

Representative sampling appears rare in empirical software engineering research. Not all studies need representative samples, but a general lack of representative sampling undermines a scientific field. This article therefore reports a critical review of the state of sampling in recent, high-quality software engineering research. The key findings are: (1) random sampling is rare; (2) sophisticated sampling strategies are very rare; (3) sampling, representativeness and randomness often appear misunderstood. These findings suggest that software engineering research has a generalizability crisis. To address these problems, this paper synthesizes existing knowledge of sampling into a succinct primer and proposes extensive guidelines for improving the conduct, presentation and evaluation of sampling in software engineering research. It is further recommended that while researchers should strive for more representative samples, disparaging non-probability sampling is generally capricious and particularly misguided for predominately qualitative research.
Dissecting Neural ODEs
Venue: arXiv cs.LG 2021
Year: 2021

Continuous deep learning architectures have recently re-emerged as Neural Ordinary Differential Equations (Neural ODEs). This infinite-depth approach theoretically bridges the gap between deep learning and dynamical systems, offering a novel perspective. However, deciphering the inner working of these models is still an open challenge, as most applications apply them as generic black-box modules. In this work we "open the box", further developing the continuous-depth formulation with the aim of clarifying the influence of several design choices on the underlying dynamics.
Constructing Higher Inductive Types as Groupoid Quotients
Venue: arXiv cs.LO 2021
Year: 2021

In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.
Interface Modeling for Quality and Resource Management
Venue: arXiv cs.LO 2021
Year: 2021

We develop an interface-modeling framework for quality and resource management that captures configurable working points of hardware and software components in terms of functionality, resource usage and provision, and quality indicators such as performance and energy consumption. We base these aspects on partially-ordered sets to capture quality levels, budget sizes, and functional compatibility. This makes the framework widely applicable and domain independent (although we aim for embedded and cyber-physical systems). The framework paves the way for dynamic (re-)configuration and multi-objective optimization of component-based systems for quality- and resource-management purposes.
Improvements of Algebraic Attacks for solving the Rank Decoding and MinRank problems
Venue: arXiv cs.CR 2021
Year: 2021

Rank Decoding (RD) is the main underlying problem in rank-based cryptography. Based on this problem and quasi-cyclic versions of it, very efficient schemes have been proposed recently, such as those in the ROLLO and RQC submissions, which have reached the second round of the NIST Post-Quantum competition. Two main approaches have been studied to solve RD: combinatorial ones and algebraic ones. While the former has been studied extensively, a better understanding of the latter was recently obtained by Bardet et al. (EUROCRYPT20) where it appeared that algebraic attacks can often be more efficient than combinatorial ones for cryptographic parameters. This paper gives substantial improvements upon this attack in terms both of complexity and of the assumptions required by the cryptanalysis. We present attacks for ROLLO-I-128, 192, and 256 with bit complexity respectively in 70, 86, and 158, to be compared to 117, 144, and 197 for the aforementionned previous attack. Moreover, unlike this previous attack, ours does not need generic Gröbner basis algorithms since it only requires to solve a linear system. For a case called overdetermined, this modeling allows us to avoid Gröbner basis computations by going directly to solving a linear system. For the other case, called underdetermined, we also improve the results from the previous attack by combining the Ourivski-Johansson modeling together with a new modeling for a generic MinRank instance; the latter modeling allows us to refine the analysis of MinRank's complexity given in the paper by Verbel et al. (PQC19). Finally, since the proposed parameters of ROLLO and RQC are completely broken by our new attack, we give examples of new parameters for ROLLO and RQC that make them resistant to our attacks. These new parameters show that these systems remain attractive, with a loss of only about 50\% in terms of key size for ROLLO-I.
Scalable Constrained Bayesian Optimization
Venue: arXiv cs.LG 2021
Year: 2021

The global optimization of a high-dimensional black-box function under black-box constraints is a pervasive task in machine learning, control, and engineering. These problems are challenging since the feasible set is typically non-convex and hard to find, in addition to the curses of dimensionality and the heterogeneity of the underlying functions. In particular, these characteristics dramatically impact the performance of Bayesian optimization methods, that otherwise have become the de facto standard for sample-efficient optimization in unconstrained settings, leaving practitioners with evolutionary strategies or heuristics. We propose the scalable constrained Bayesian optimization (SCBO) algorithm that overcomes the above challenges and pushes the applicability of Bayesian optimization far beyond the state-of-the-art. A comprehensive experimental evaluation demonstrates that SCBO achieves excellent results on a variety of benchmarks. To this end, we propose two new control problems that we expect to be of independent value for the scientific community.
Byzantine-resilient Decentralized Stochastic Gradient Descent
Venue: arXiv cs.LG 2021
Year: 2021

Decentralized learning has gained great popularity to improve learning efficiency and preserve data privacy. Each computing node makes equal contribution to collaboratively learn a Deep Learning model. The elimination of centralized Parameter Servers (PS) can effectively address many issues such as privacy, performance bottleneck and single-point-failure. However, how to achieve Byzantine Fault Tolerance in decentralized learning systems is rarely explored, although this problem has been extensively studied in centralized systems. In this paper, we present an in-depth study towards the Byzantine resilience of decentralized learning systems with two contributions. First, from the adversarial perspective, we theoretically illustrate that Byzantine attacks are more dangerous and feasible in decentralized learning systems: even one malicious participant can arbitrarily alter the models of other participants by sending carefully crafted updates to its neighbors. Second, from the defense perspective, we propose UBAR, a novel algorithm to enhance decentralized learning with Byzantine Fault Tolerance. Specifically, UBAR provides a Uniform Byzantine-resilient Aggregation Rule for benign nodes to select the useful parameter updates and filter out the malicious ones in each training iteration. It guarantees that each benign node in a decentralized system can train a correct model under very strong Byzantine attacks with an arbitrary number of faulty nodes. We conduct extensive experiments on standard image classification tasks and the results indicate that UBAR can effectively defeat both simple and sophisticated Byzantine attacks with higher performance efficiency than existing solutions.
Encryption without Centralization: Distributing DNS Queries Across Recursive Resolvers
Venue: arXiv cs.NI 2021
Year: 2021

Emerging protocols such as DNS-over-HTTPS (DoH) and DNS-over-TLS (DoT) improve the privacy of DNS queries and responses. While this trend towards encryption is positive, deployment of these protocols has in some cases resulted in further centralization of the DNS, which introduces new challenges. In particular, centralization has consequences for performance, privacy, and availability; a potentially greater concern is that it has become more difficult to control the choice of DNS recursive resolver, particularly for IoT devices. Ultimately, the best strategy for selecting among one or more recursive resolvers may ultimately depend on circumstance, user, and even device. Accordingly, the DNS architecture must permit flexibility in allowing users, devices, and applications to specify these strategies. Towards this goal of increased de-centralization and improved flexibility, this paper presents the design and implementation of a refactored DNS resolver architecture that allows for de-centralized name resolution, preserving the benefits of encrypted DNS while satisfying other desirable properties, including performance and privacy.
Learning Precise 3D Manipulation from Multiple Uncalibrated Cameras
Venue: arXiv cs.RO 2021
Year: 2021

In this work, we present an effective multi-view approach to closed-loop end-to-end learning of precise manipulation tasks that are 3D in nature. Our method learns to accomplish these tasks using multiple statically placed but uncalibrated RGB camera views without building an explicit 3D representation such as a pointcloud or voxel grid. This multi-camera approach achieves superior task performance on difficult stacking and insertion tasks compared to single-view baselines. Single view robotic agents struggle from occlusion and challenges in estimating relative poses between points of interest. While full 3D scene representations (voxels or pointclouds) are obtainable from registered output of multiple depth sensors, several challenges complicate operating off such explicit 3D representations. These challenges include imperfect camera calibration, poor depth maps due to object properties such as reflective surfaces, and slower inference speeds over 3D representations compared to 2D images. Our use of static but uncalibrated cameras does not require camera-robot or camera-camera calibration making the proposed approach easy to setup and our use of \textit{sensor dropout} during training makes it resilient to the loss of camera-views after deployment.
Homotopy Type Theory in Isabelle
Venue: arXiv cs.LO 2021
Year: 2021

This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing logical framework infrastructure to implement essential automation, such as type checking and term elaboration, that is usually handled on the source code level of dependently typed systems. I also integrate the propositions-as-types paradigm with the declarative Isar proof language, providing an alternative to the tactic-based proofs of Coq and the proof terms of Agda. The infrastructure developed is then used to formalize foundational results from the Homotopy Type Theory book.
A Toolkit for Generating Code Knowledge Graphs
Venue: arXiv cs.DB 2021
Year: 2021

Knowledge graphs have been proven extremely useful in powering diverse applications in semantic search and natural language understanding. In this paper, we present GraphGen4Code, a toolkit to build code knowledge graphs that can similarly power various applications such as program search, code understanding, bug detection, and code automation. GraphGen4Code uses generic techniques to capture code semantics with the key nodes in the graph representing classes, functions, and methods. Edges indicate function usage (e.g., how data flows through function calls, as derived from program analysis of real code), and documentation about functions (e.g., code documentation, usage documentation, or forum discussions such as StackOverflow). Our toolkit uses named graphs in RDF to model graphs per program, or can output graphs as JSON. We show the scalability of the toolkit by applying it to 1.3 million Python files drawn from GitHub, 2,300 Python modules, and 47 million forum posts. This results in an integrated code graph with over 2 billion triples. We make the toolkit to build such graphs as well as the sample extraction of the 2 billion triples graph publicly available to the community for use.
RobustPeriod: Time-Frequency Mining for Robust Multiple Periodicity Detection
Venue: arXiv cs.LG 2021
Year: 2021

Periodicity detection is a crucial step in time series tasks, including monitoring and forecasting of metrics in many areas, such as IoT applications and self-driving database management system. In many of these applications, multiple periodic components exist and are often interlaced with each other. Such dynamic and complicated periodic patterns make the accurate periodicity detection difficult. In addition, other components in the time series, such as trend, outliers and noises, also pose additional challenges for accurate periodicity detection. In this paper, we propose a robust and general framework for multiple periodicity detection. Our algorithm applies maximal overlap discrete wavelet transform to transform the time series into multiple temporal-frequency scales such that different periodic components can be isolated. We rank them by wavelet variance, and then at each scale detect single periodicity by our proposed Huber-periodogram and Huber-ACF robustly. We rigorously prove the theoretical properties of Huber-periodogram and justify the use of Fisher's test on Huber-periodogram for periodicity detection. To further refine the detected periods, we compute unbiased autocorrelation function based on Wiener-Khinchin theorem from Huber-periodogram for improved robustness and efficiency. Experiments on synthetic and real-world datasets show that our algorithm outperforms other popular ones for both single and multiple periodicity detection.
Conceptual Game Expansion
Venue: arXiv cs.AI 2021
Year: 2021

Automated game design is the problem of automatically producing games through computational processes. Traditionally, these methods have relied on the authoring of search spaces by a designer, defining the space of all possible games for the system to author. In this paper, we instead learn representations of existing games from gameplay video and use these to approximate a search space of novel games. In a human subject study we demonstrate that these novel games are indistinguishable from human games in terms of challenge, and that one of the novel games was equivalent to one of the human games in terms of fun, frustration, and likeability.