OpenRaiser/Intern-Atlas huggingface dataset:
Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors
Venue: arXiv cs.SE 2022
Year: 2022

Bounded model checking (BMC) is vital for finding program property violations. For unsafe programs, BMC can quickly find an execution path from an initial state to the violated state that refutes a given safety property. However, BMC techniques struggle to falsify programs that contain loops. BMC needs to incrementally unfold the program loops up to the bound $k$, exposing the property violation, which can thus lead to exploring a considerable state space. Here, we describe and evaluate the first verification method based on interval methods via contractors to reduce the domains of variables representing the search space. This reduction is based on the specified property modeled as functions representing the contractor constraints. In particular, we exploit interval methods via contractors to incrementally analyze the program loop variables and contract the domain where the property is guaranteed to hold to prune the search exploration, thus reducing resource consumption aggressively. Experimental results demonstrate the efficiency and efficacy of our proposed approach over a large set of benchmarks, including $7044$ verification tasks, compared with state-of-the-art BMC tools. Our proposed method can reduce memory usage up to $75$\% while verifying $1$\% more verification tasks.
Flexible, Non-parametric Modeling Using Regularized Neural Networks
Venue: arXiv cs.LG 2022
Year: 2022

Non-parametric, additive models are able to capture complex data dependencies in a flexible, yet interpretable way. However, choosing the format of the additive components often requires non-trivial data exploration. Here, as an alternative, we propose PrAda-net, a one-hidden-layer neural network, trained with proximal gradient descent and adaptive lasso. PrAda-net automatically adjusts the size and architecture of the neural network to reflect the complexity and structure of the data. The compact network obtained by PrAda-net can be translated to additive model components, making it suitable for non-parametric statistical modelling with automatic model selection. We demonstrate PrAda-net on simulated data, where wecompare the test error performance, variable importance and variable subset identification properties of PrAda-net to other lasso-based regularization approaches for neural networks. We also apply PrAda-net to the massive U.K. black smoke data set, to demonstrate how PrAda-net can be used to model complex and heterogeneous data with spatial and temporal components. In contrast to classical, statistical non-parametric approaches, PrAda-net requires no preliminary modeling to select the functional forms of the additive components, yet still results in an interpretable model representation.
Warping of Radar Data into Camera Image for Cross-Modal Supervision in Automotive Applications
Venue: arXiv cs.CV 2022
Year: 2022

We present an approach to automatically generate semantic labels for real recordings of automotive range-Doppler (RD) radar spectra. Such labels are required when training a neural network for object recognition from radar data. The automatic labeling approach rests on the simultaneous recording of camera and lidar data in addition to the radar spectrum. By warping radar spectra into the camera image, state-of-the-art object recognition algorithms can be applied to label relevant objects, such as cars, in the camera image. The warping operation is designed to be fully differentiable, which allows backpropagating the gradient computed on the camera image through the warping operation to the neural network operating on the radar data. As the warping operation relies on accurate scene flow estimation, we further propose a novel scene flow estimation algorithm which exploits information from camera, lidar and radar sensors. The proposed scene flow estimation approach is compared against a state-of-the-art scene flow algorithm, and it outperforms it by approximately 30% w.r.t. mean average error. The feasibility of the overall framework for automatic label generation for RD spectra is verified by evaluating the performance of neural networks trained with the proposed framework for Direction-of-Arrival estimation.
Adversarial Momentum-Contrastive Pre-Training
Venue: arXiv cs.CV 2022
Year: 2022

Recently proposed adversarial self-supervised learning methods usually require big batches and long training epochs to extract robust features, which will bring heavy computational overhead on platforms with limited resources. In order to help the network learn more powerful feature representations in smaller batches and fewer epochs, this paper proposes a novel adversarial momentum contrastive learning method, which introduces two memory banks corresponding to clean samples and adversarial samples, respectively. These memory banks can be dynamically incorporated into the training process to track invariant features among historical mini-batches. Compared with the previous adversarial pre-training model, our method achieves superior performance with smaller batch size and less training epochs. In addition, the model outperforms some state-of-the-art supervised defensive methods on multiple benchmark datasets after being fine-tuned on downstream classification tasks.
The Age of Incorrect Information: an Enabler of Semantics-Empowered Communication
Venue: arXiv cs.IT 2022
Year: 2022

In this paper, we introduce the Age of Incorrect Information (AoII) as an enabler for semantics-empowered communication, a newly advocated communication paradigm centered around data's role and its usefulness to the communication's goal. First, we shed light on how the traditional communication paradigm, with its role-blind approach to data, is vulnerable to performance bottlenecks. Next, we highlight the shortcomings of several proposed performance measures destined to deal with the traditional communication paradigm's limitations, namely the Age of Information (AoI) and the error-based metrics. We also show how the AoII addresses these shortcomings and captures more meaningfully the purpose of data. Afterward, we consider the problem of minimizing the average AoII in a transmitter-receiver pair scenario. We prove that the optimal transmission strategy is a randomized threshold policy, and we propose an algorithm that finds the optimal parameters. Furthermore, we provide a theoretical comparison between the AoII framework and the standard error-based metrics counterpart. Interestingly, we show that the AoII-optimal policy is also error-optimal for the adopted information source model. Concurrently, the converse is not necessarily true. Finally, we implement our policy in various applications, and we showcase its performance advantages compared to both the error-optimal and the AoI-optimal policies.
A Tutorial on Sparse Gaussian Processes and Variational Inference
Venue: arXiv cs.LG 2022
Year: 2022

Gaussian processes (GPs) provide a framework for Bayesian inference that can offer principled uncertainty estimates for a large range of problems. For example, if we consider regression problems with Gaussian likelihoods, a GP model enjoys a posterior in closed form. However, identifying the posterior GP scales cubically with the number of training examples and requires to store all examples in memory. In order to overcome these obstacles, sparse GPs have been proposed that approximate the true posterior GP with pseudo-training examples. Importantly, the number of pseudo-training examples is user-defined and enables control over computational and memory complexity. In the general case, sparse GPs do not enjoy closed-form solutions and one has to resort to approximate inference. In this context, a convenient choice for approximate inference is variational inference (VI), where the problem of Bayesian inference is cast as an optimization problem -- namely, to maximize a lower bound of the log marginal likelihood. This paves the way for a powerful and versatile framework, where pseudo-training examples are treated as optimization arguments of the approximate posterior that are jointly identified together with hyperparameters of the generative model (i.e. prior and likelihood). The framework can naturally handle a wide scope of supervised learning problems, ranging from regression with heteroscedastic and non-Gaussian likelihoods to classification problems with discrete labels, but also problems with multidimensional labels. The purpose of this tutorial is to provide access to the basic matter for readers without prior knowledge in both GPs and VI. A proper exposition to the subject enables also access to more recent advances (like importance-weighted VI as well as interdomain, multioutput and deep GPs) that can serve as an inspiration for new research ideas.
SPINS: Structure Priors aided Inertial Navigation System
Venue: arXiv cs.RO 2022
Year: 2022

Although Simultaneous Localization and Mapping (SLAM) has been an active research topic for decades, current state-of-the-art methods still suffer from instability or inaccuracy due to feature insufficiency or its inherent estimation drift, in many civilian environments. To resolve these issues, we propose a navigation system combing the SLAM and prior-map-based localization. Specifically, we consider additional integration of line and plane features, which are ubiquitous and more structurally salient in civilian environments, into the SLAM to ensure feature sufficiency and localization robustness. More importantly, we incorporate general prior map information into the SLAM to restrain its drift and improve the accuracy. To avoid rigorous association between prior information and local observations, we parameterize the prior knowledge as low dimensional structural priors defined as relative distances/angles between different geometric primitives. The localization is formulated as a graph-based optimization problem that contains sliding-window-based variables and factors, including IMU, heterogeneous features, and structure priors. We also derive the analytical expressions of Jacobians of different factors to avoid the automatic differentiation overhead. To further alleviate the computation burden of incorporating structural prior factors, a selection mechanism is adopted based on the so-called information gain to incorporate only the most effective structure priors in the graph optimization. Finally, the proposed framework is extensively tested on synthetic data, public datasets, and, more importantly, on the real UAV flight data obtained from a building inspection task. The results show that the proposed scheme can effectively improve the accuracy and robustness of localization for autonomous robots in civilian applications.
Discovering the Ethereum2 P2P Network
Venue: arXiv cs.CR 2022
Year: 2022

Achieving the equilibrium between scalability, sustainability, and security while keeping decentralization has prevailed as the target solution for decentralized blockchain applications over the last years. Several approaches have been proposed by multiple blockchain teams to achieve it, Ethereum being among them. Ethereum is on the path of a major protocol improvement called Ethereum 2.0 (Eth2), implementing Sharding and introducing the Proof-of-Stake (PoS). As the change of consensus mechanism is a delicate matter, this improvement will be achieved through different phases, the first of which is the implementation of the Beacon Chain. As Ethereum1, Eth2 relies on a decentralized peer-to-peer (p2p) network for the message distribution. Up to date, we estimate that there are around 5.000 nodes in the Eth2 main net geographically distributed. However, the topology of this one still prevails unknown. In this paper, we present the results obtained from the analysis we performed on the Eth2 p2p network. Describing the topology of the network, as possible hazards that this one implies.
Adaptive Graph Diffusion Networks
Venue: arXiv cs.LG 2022
Year: 2022

Graph Neural Networks (GNNs) have received much attention in the graph deep learning domain. However, recent research empirically and theoretically shows that deep GNNs suffer from over-fitting and over-smoothing problems. The usual solutions either cannot solve extensive runtime of deep GNNs or restrict graph convolution in the same feature space. We propose the Adaptive Graph Diffusion Networks (AGDNs) which perform multi-layer generalized graph diffusion in different feature spaces with moderate complexity and runtime. Standard graph diffusion methods combine large and dense powers of the transition matrix with predefined weighting coefficients. Instead, AGDNs combine smaller multi-hop node representations with learnable and generalized weighting coefficients. We propose two scalable mechanisms of weighting coefficients to capture multi-hop information: Hop-wise Attention (HA) and Hop-wise Convolution (HC). We evaluate AGDNs on diverse, challenging Open Graph Benchmark (OGB) datasets with semi-supervised node classification and link prediction tasks. Until the date of submission (Aug 26, 2022), AGDNs achieve top-1 performance on the ogbn-arxiv, ogbn-proteins and ogbl-ddi datasets and top-3 performance on the ogbl-citation2 dataset. On the similar Tesla V100 GPU cards, AGDNs outperform Reversible GNNs (RevGNNs) with 13% complexity and 1% training runtime of RevGNNs on the ogbn-proteins dataset. AGDNs also achieve comparable performance to SEAL with 36% training and 0.2% inference runtime of SEAL on the ogbl-citation2 dataset.
Test Score Algorithms for Budgeted Stochastic Utility Maximization
Venue: arXiv cs.DS 2022
Year: 2022

Motivated by recent developments in designing algorithms based on individual item scores for solving utility maximization problems, we study the framework of using test scores, defined as a statistic of observed individual item performance data, for solving the budgeted stochastic utility maximization problem. We extend an existing scoring mechanism, namely the replication test scores, to incorporate heterogeneous item costs as well as item values. We show that a natural greedy algorithm that selects items solely based on their replication test scores outputs solutions within a constant factor of the optimum for a broad class of utility functions. Our algorithms and approximation guarantees assume that test scores are noisy estimates of certain expected values with respect to marginal distributions of individual item values, thus making our algorithms practical and extending previous work that assumes noiseless estimates. Moreover, we show how our algorithm can be adapted to the setting where items arrive in a streaming fashion while maintaining the same approximation guarantee. We present numerical results, using synthetic data and data sets from the Academia.StackExchange Q&A forum, which show that our test score algorithm can achieve competitiveness, and in some cases better performance than a benchmark algorithm that requires access to a value oracle to evaluate function values.
Crossover-SGD: A gossip-based communication in distributed deep learning for alleviating large mini-batch problem and enhancing scalability
Venue: arXiv cs.LG 2022
Year: 2022

Distributed deep learning is an effective way to reduce the training time of deep learning for large datasets as well as complex models. However, the limited scalability caused by network overheads makes it difficult to synchronize the parameters of all workers. To resolve this problem, gossip-based methods that demonstrates stable scalability regardless of the number of workers have been proposed. However, to use gossip-based methods in general cases, the validation accuracy for a large mini-batch needs to be verified. To verify this, we first empirically study the characteristics of gossip methods in a large mini-batch problem and observe that the gossip methods preserve higher validation accuracy than AllReduce-SGD(Stochastic Gradient Descent) when the number of batch sizes is increased and the number of workers is fixed. However, the delayed parameter propagation of the gossip-based models decreases validation accuracy in large node scales. To cope with this problem, we propose Crossover-SGD that alleviates the delay propagation of weight parameters via segment-wise communication and load balancing random network topology. We also adapt hierarchical communication to limit the number of workers in gossip-based communication methods. To validate the effectiveness of our proposed method, we conduct empirical experiments and observe that our Crossover-SGD shows higher node scalability than SGP(Stochastic Gradient Push).
The jsRealB Text Realizer: Organization and Use Cases -- Revised version
Venue: arXiv cs.CL 2022
Year: 2022

This paper describes the design principles behind jsRealB (Version 4.0), a surface realizer written JavaScript for English or French sentences from a specification inspired by the constituent syntax formalism but for which a dependency-based input notation is also available. jsRealB can be used either within a web page or as a node.js module. We show that the seemingly simple process of text realization involves many interesting implementation challenges in order to take into account the specifics of each language. jsRealB has a large coverage of English and French and has been used to develop realistic data-to-text applications and to reproduce existing literary texts and sentences from Universal Dependency annotations. Its source code and that of its applications are available on GitHub. The port of this approach to Python (pyrealb) is also presented.
Maximum-Likelihood Quantum State Tomography by Soft-Bayes
Venue: arXiv cs.LG 2022
Year: 2022

Quantum state tomography (QST), the task of estimating an unknown quantum state given measurement outcomes, is essential to building reliable quantum computing devices. Whereas computing the maximum-likelihood (ML) estimate corresponds to solving a finite-sum convex optimization problem, the objective function is not smooth nor Lipschitz, so most existing convex optimization methods lack sample complexity guarantees; moreover, both the sample size and dimension grow exponentially with the number of qubits in a QST experiment, so a desired algorithm should be highly scalable with respect to the dimension and sample size, just like stochastic gradient descent. In this paper, we propose a stochastic first-order algorithm that computes an $\varepsilon$-approximate ML estimate in $O( ( D \log D ) / \varepsilon ^ 2 )$ iterations with $O( D^3 )$ per-iteration time complexity, where $D$ denotes the dimension of the unknown quantum state and $\varepsilon$ denotes the optimization error. Our algorithm is an extension of Soft-Bayes to the quantum setup.
Chunk List: Concurrent Data Structures
Venue: arXiv cs.DS 2022
Year: 2022

Chunking data is obviously no new concept; however, I had never found any data structures that used chunking as the basis of their implementation. I figured that by using chunking alongside concurrency, I could create an extremely fast run-time in regards to particular methods as searching and/or sorting. By using chunking and concurrency to my advantage, I came up with the chunk list - a dynamic list-based data structure that would separate large amounts of data into specifically sized chunks, each of which should be able to be searched at the exact same time by searching each chunk on a separate thread. As a result of implementing this concept into its own class, I was able to create something that almost consistently gives around 20x-300x faster results than a regular ArrayList. However, should speed be a particular issue even after implementation, users can modify the size of the chunks and benchmark the speed of using smaller or larger chunks, depending on the amount of data being stored.
Domain Adaptation for the Segmentation of Confidential Medical Images
Venue: arXiv cs.CV 2022
Year: 2022

Convolutional neural networks (CNNs) have led to significant improvements in the semantic segmentation of images. When source and target datasets come from different modalities, CNN performance suffers due to domain shift. In such cases data annotation in the target domain becomes necessary to maintain model performance. To circumvent the re-annotation process, unsupervised domain adaptation (UDA) is proposed to adapt a model to new modalities using solely unlabeled target data. Common UDA algorithms require access to source domain data during adaptation, which may not be feasible in medical imaging due to data sharing restrictions. In this work, we develop an algorithm for UDA where the source domain data is inaccessible during target adaptation. Our approach is based on encoding the source domain information into an internal distribution that is used to guide adaptation in the absence of source samples. We demonstrate the effectiveness of our algorithm by comparing it to state-of-the-art medical image semantic segmentation approaches on two medical image semantic segmentation datasets.
Automorphisms and isogeny graphs of abelian varieties, with applications to the superspecial Richelot isogeny graph
Venue: arXiv cs.CR 2022
Year: 2022

We investigate special structures due to automorphisms in isogeny graphs of principally polarized abelian varieties, and abelian surfaces in particular. We give theoretical and experimental results on the spectral and statistical properties of (2, 2)-isogeny graphs of superspecial abelian surfaces, including stationary distributions for random walks, bounds on eigenvalues and diameters, and a proof of the connectivity of the Jacobian subgraph of the (2, 2)-isogeny graph. Our results improve our understanding of the performance and security of some recently-proposed cryptosystems, and are also a concrete step towards a better understanding of general superspecial isogeny graphs in arbitrary dimension.
A polynomial-time construction of a hitting set for read-once branching programs of width 3
Venue: arXiv cs.CC 2022
Year: 2022

Recently, an interest in constructing pseudorandom or hitting set generators for restricted branching programs has increased, which is motivated by the fundamental issue of derandomizing space-bounded computations. Such constructions have been known only in the case of width 2 and in very restricted cases of bounded width. In this paper, we characterize the hitting sets for read-once branching programs of width 3 by a so-called richness condition. Namely, we show that such sets hit the class of read-once conjunctions of DNF and CNF (i.e. the weak richness). Moreover, we prove that any rich set extended with all strings within Hamming distance of 3 is a hitting set for read-once branching programs of width 3. Then, we show that any almost $O(\log n)$-wise independent set satisfies the richness condition. By using such a set due to Alon et al. (1992) our result provides an explicit polynomial-time construction of a hitting set for read-once branching programs of width 3 with acceptance probability $\varepsilon>5/6$. We announced this result at conferences more than ten years ago, including only proof sketches, which motivated a number of subsequent results on pseudorandom generators for restricted read-once branching programs. This paper contains our original detailed proof that has not been published yet.