OpenRaiser/Intern-Atlas huggingface dataset:
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Venue: arXiv cs.LO 2022
Year: 2022

Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work shows the design of a small, memory- and thread-safe kernel that efficiently checks proofs both concurrently and non-concurrently. This design is implemented in a new proof checker called Kontroli for the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. Kontroli is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers. Furthermore, Kontroli reduces the time of the most time-consuming part of proof checking using eight threads by up to 6.6x.
Differential Privacy for Government Agencies -- Are We There Yet?
Venue: arXiv cs.CR 2022
Year: 2022

Government agencies typically need to take potential risks of disclosure into account whenever they publish statistics based on their data or give external researchers access to collected data. In this context, the promise of formal privacy guarantees offered by concepts such as differential privacy seems to be the panacea enabling the agencies to quantify and control the privacy loss incurred by any data release exactly. Nevertheless, despite the excitement in academia and industry, most agencies -- with the prominent exception of the U.S. Census Bureau -- have been reluctant to even consider the concept for their data release strategy. This paper discusses potential reasons for this. We argue that the requirements for implementing differential privacy approaches at government agencies are often fundamentally different from the requirements in industry. This raises many challenges and questions that still need to be addressed before the concept can be used as an overarching principle when sharing data with the public. The paper does not offer any solutions to these challenges. Instead, we hope to stimulate some collaborative research efforts, as we believe that many of the problems can only be addressed by interdisciplinary collaborations.
Online $k$-means Clustering on Arbitrary Data Streams
Venue: arXiv cs.LG 2022
Year: 2022

We consider online $k$-means clustering where each new point is assigned to the nearest cluster center, after which the algorithm may update its centers. The loss incurred is the sum of squared distances from new points to their assigned cluster centers. The goal over a data stream $X$ is to achieve loss that is a constant factor of $L(X, OPT_k)$, the best possible loss using $k$ fixed points in hindsight. We propose a data parameter, $Λ(X)$, such that for any algorithm maintaining $O(k\text{poly}(\log n))$ centers at time $n$, there exists a data stream $X$ for which a loss of $Ω(Λ(X))$ is inevitable. We then give a randomized algorithm that achieves clustering loss $O(Λ(X) + L(X, OPT_k))$. Our algorithm uses $O(k\text{poly}(\log n))$ memory and maintains $O(k\text{poly}(\log n))$ cluster centers. Our algorithm also enjoys a running time of $O(k\text{poly}(\log n))$ and is the first algorithm to achieve polynomial space and time complexity in this setting. It also is the first to have provable guarantees without making any assumptions on the input data.
Learning Continuous Exponential Families Beyond Gaussian
Venue: arXiv cs.LG 2022
Year: 2022

We address the problem of learning of continuous exponential family distributions with unbounded support. While a lot of progress has been made on learning of Gaussian graphical models, we still lack scalable algorithms for reconstructing general continuous exponential families modeling higher-order moments of the data beyond the mean and the covariance. Here, we introduce a computationally efficient method for learning continuous graphical models based on the Interaction Screening approach. Through a series of numerical experiments, we show that our estimator maintains similar requirements in terms of accuracy and sample complexity scalings compared to alternative approaches such as maximization of conditional likelihood, while considerably improving upon the algorithm's run-time.
Strongly Connected Topology Model and Confirmation-based Propagation Method for Cross-chain Interaction
Venue: arXiv cs.DC 2022
Year: 2022

Cross-chain interaction is among different blockchains. When the number of blockchains increases, it is difficult for blockchains to form a single star topology or a fully connected topology. Meanwhile, different from legacy networks, the propagation method is required to keep the data validity. Thus, the blockchain topology and associated propagation methods are two key issues, which should be ensured during the propagation. In this paper, we first propose the confirmation-based propagation method to keep the validity of the cross-chain data. The confirmation method is to seal the cross-chain transaction synchronized from other blockchains. Second, we point out that a valid topology requires blockchains to be strongly connected. With this requirement, we propose several topologies, which match different connection scenarios. The simulation results show that the proposed methods can securely propagate the cross-chain data and the connection way is flexible.
Projection Filtering with Observed State Increments with Applications in Continuous-Time Circular Filtering
Venue: arXiv cs.RO 2022
Year: 2022

Angular path integration is the ability of a system to estimate its own heading direction from potentially noisy angular velocity (or increment) observations. Non-probabilistic algorithms for angular path integration, which rely on a summation of these noisy increments, do not appropriately take into account the reliability of such observations, which is essential for appropriately weighing one's current heading direction estimate against incoming information. In a probabilistic setting, angular path integration can be formulated as a continuous-time nonlinear filtering problem (circular filtering) with observed state increments. The circular symmetry of heading direction makes this inference task inherently nonlinear, thereby precluding the use of popular inference algorithms such as Kalman filters, rendering the problem analytically inaccessible. Here, we derive an approximate solution to circular continuous-time filtering, which integrates state increment observations while maintaining a fixed representation through both state propagation and observational updates. Specifically, we extend the established projection-filtering method to account for observed state increments and apply this framework to the circular filtering problem. We further propose a generative model for continuous-time angular-valued direct observations of the hidden state, which we integrate seamlessly into the projection filter. Applying the resulting scheme to a model of probabilistic angular path integration, we derive an algorithm for circular filtering, which we term the circular Kalman filter. Importantly, this algorithm is analytically accessible, interpretable, and outperforms an alternative filter based on a Gaussian approximation.
On the Similarity between von Neumann Graph Entropy and Structural Information: Interpretation, Computation, and Applications
Venue: arXiv cs.SI 2022
Year: 2022

The von Neumann graph entropy is a measure of graph complexity based on the Laplacian spectrum. It has recently found applications in various learning tasks driven by networked data. However, it is computational demanding and hard to interpret using simple structural patterns. Due to the close relation between Lapalcian spectrum and degree sequence, we conjecture that the structural information, defined as the Shannon entropy of the normalized degree sequence, might be a good approximation of the von Neumann graph entropy that is both scalable and interpretable. In this work, we thereby study the difference between the structural information and von Neumann graph entropy named as {\em entropy gap}. Based on the knowledge that the degree sequence is majorized by the Laplacian spectrum, we for the first time prove the entropy gap is between $0$ and $\log_2 e$ in any undirected unweighted graphs. Consequently we certify that the structural information is a good approximation of the von Neumann graph entropy that achieves provable accuracy, scalability, and interpretability simultaneously. This approximation is further applied to two entropy-related tasks: network design and graph similarity measure, where novel graph similarity measure and fast algorithms are proposed. Our experimental results on graphs of various scales and types show that the very small entropy gap readily applies to a wide range of graphs and weighted graphs. As an approximation of the von Neumann graph entropy, the structural information is the only one that achieves both high efficiency and high accuracy among the prominent methods. It is at least two orders of magnitude faster than SLaQ with comparable accuracy. Our structural information based methods also exhibit superior performance in two entropy-related tasks.
Linear Classifiers in Product Space Forms
Venue: arXiv cs.LG 2022
Year: 2022

Embedding methods for product spaces are powerful techniques for low-distortion and low-dimensional representation of complex data structures. Here, we address the new problem of linear classification in product space forms -- products of Euclidean, spherical, and hyperbolic spaces. First, we describe novel formulations for linear classifiers on a Riemannian manifold using geodesics and Riemannian metrics which generalize straight lines and inner products in vector spaces. Second, we prove that linear classifiers in $d$-dimensional space forms of any curvature have the same expressive power, i.e., they can shatter exactly $d+1$ points. Third, we formalize linear classifiers in product space forms, describe the first known perceptron and support vector machine classifiers for such spaces and establish rigorous convergence results for perceptrons. Moreover, we prove that the Vapnik-Chervonenkis dimension of linear classifiers in a product space form of dimension $d$ is \emph{at least} $d+1$. We support our theoretical findings with simulations on several datasets, including synthetic data, image data, and single-cell RNA sequencing (scRNA-seq) data. The results show that classification in low-dimensional product space forms for scRNA-seq data offers, on average, a performance improvement of $\sim15\%$ when compared to that in Euclidean spaces of the same dimension.
A Game-Theoretic Approach for Hierarchical Epidemic Control
Venue: arXiv cs.GT 2022
Year: 2022

We design and analyze a multi-level game-theoretic model of hierarchical policy interventions for epidemic control, such as those in response to the COVID-19 pandemic. Our model captures the potentially mismatched priorities among a hierarchy of policy-makers (e.g., federal, state, and local governments) with respect to two cost components that have opposite dependence on the policy strength -- post-intervention infection rates and the socio-economic cost of policy implementation. Additionally, our model includes a crucial third factor in decisions: a cost of non-compliance with the policy-maker immediately above in the hierarchy, such as non-compliance of counties with state-level policies. We propose two novel algorithms for approximating solutions to such games. The first is based on best response dynamics (BRD), and exploits the tree structure of the game. The second combines quadratic integer programming (QIP), which enables us to collapse the two lowest levels of the game, with best response dynamics. Through extensive experiments, we show that our QIP-based approach significantly outperforms the BRD algorithm both in running time and the quality of equilibrium solutions. Finally, we apply the QIP-based algorithm to experiments based on both synthetic and real-world data under various parameter configurations and analyze the resulting (approximate) equilibria to gain insight into the impact of decentralization on overall welfare (measured as the negative sum of costs) as well as emergent properties like free-riding and fairness in cost distribution among policy-makers.
Residual-Aided End-to-End Learning of Communication System without Known Channel
Venue: arXiv cs.IT 2022
Year: 2022

Leveraging powerful deep learning techniques, the end-to-end (E2E) learning of communication system is able to outperform the classical communication system. Unfortunately, this communication system cannot be trained by deep learning without known channel. To deal with this problem, a generative adversarial network (GAN) based training scheme has been recently proposed to imitate the real channel. However, the gradient vanishing and overfitting problems of GAN will result in the serious performance degradation of E2E learning of communication system. To mitigate these two problems, we propose a residual aided GAN (RA-GAN) based training scheme in this paper. Particularly, inspired by the idea of residual learning, we propose a residual generator to mitigate the gradient vanishing problem by realizing a more robust gradient backpropagation. Moreover, to cope with the overfitting problem, we reconstruct the loss function for training by adding a regularizer, which limits the representation ability of RA-GAN. Simulation results show that the trained residual generator has better generation performance than the conventional generator, and the proposed RA-GAN based training scheme can achieve the near-optimal block error rate (BLER) performance with a negligible computational complexity increase in both the theoretical channel model and the ray-tracing based channel dataset.
Learning Purified Feature Representations from Task-irrelevant Labels
Venue: arXiv cs.LG 2022
Year: 2022

Learning an empirically effective model with generalization using limited data is a challenging task for deep neural networks. In this paper, we propose a novel learning framework called PurifiedLearning to exploit task-irrelevant features extracted from task-irrelevant labels when training models on small-scale datasets. Particularly, we purify feature representations by using the expression of task-irrelevant information, thus facilitating the learning process of classification. Our work is built on solid theoretical analysis and extensive experiments, which demonstrate the effectiveness of PurifiedLearning. According to the theory we proved, PurifiedLearning is model-agnostic and doesn't have any restrictions on the model needed, so it can be combined with any existing deep neural networks with ease to achieve better performance. The source code of this paper will be available in the future for reproducibility.
Learning Contact Dynamics using Physically Structured Neural Networks
Venue: arXiv cs.LG 2022
Year: 2022

Learning physically structured representations of dynamical systems that include contact between different objects is an important problem for learning-based approaches in robotics. Black-box neural networks can learn to approximately represent discontinuous dynamics, but they typically require large quantities of data and often suffer from pathological behaviour when forecasting for longer time horizons. In this work, we use connections between deep neural networks and differential equations to design a family of deep network architectures for representing contact dynamics between objects. We show that these networks can learn discontinuous contact events in a data-efficient manner from noisy observations in settings that are traditionally difficult for black-box approaches and recent physics inspired neural networks. Our results indicate that an idealised form of touch feedback -- which is heavily relied upon by biological systems -- is a key component of making this learning problem tractable. Together with the inductive biases introduced through the network architectures, our techniques enable accurate learning of contact dynamics from observations.
When is Early Classification of Time Series Meaningful?
Venue: arXiv cs.LG 2022
Year: 2022

Since its introduction two decades ago, there has been increasing interest in the problem of early classification of time series. This problem generalizes classic time series classification to ask if we can classify a time series subsequence with sufficient accuracy and confidence after seeing only some prefix of a target pattern. The idea is that the earlier classification would allow us to take immediate action, in a domain in which some practical interventions are possible. For example, that intervention might be sounding an alarm or applying the brakes in an automobile. In this work, we make a surprising claim. In spite of the fact that there are dozens of papers on early classification of time series, it is not clear that any of them could ever work in a real-world setting. The problem is not with the algorithms per se but with the vague and underspecified problem description. Essentially all algorithms make implicit and unwarranted assumptions about the problem that will ensure that they will be plagued by false positives and false negatives even if their results suggested that they could obtain near-perfect results. We will explain our findings with novel insights and experiments and offer recommendations to the community.
ROAD: The ROad event Awareness Dataset for Autonomous Driving
Venue: arXiv cs.CV 2022
Year: 2022

Humans drive in a holistic fashion which entails, in particular, understanding dynamic road events and their evolution. Injecting these capabilities in autonomous vehicles can thus take situational awareness and decision making closer to human-level performance. To this purpose, we introduce the ROad event Awareness Dataset (ROAD) for Autonomous Driving, to our knowledge the first of its kind. ROAD is designed to test an autonomous vehicle's ability to detect road events, defined as triplets composed by an active agent, the action(s) it performs and the corresponding scene locations. ROAD comprises videos originally from the Oxford RobotCar Dataset annotated with bounding boxes showing the location in the image plane of each road event. We benchmark various detection tasks, proposing as a baseline a new incremental algorithm for online road event awareness termed 3D-RetinaNet. We also report the performance on the ROAD tasks of Slowfast and YOLOv5 detectors, as well as that of the winners of the ICCV2021 ROAD challenge, which highlight the challenges faced by situation awareness in autonomous driving. ROAD is designed to allow scholars to investigate exciting tasks such as complex (road) activity detection, future event anticipation and continual learning. The dataset is available at https://github.com/gurkirt/road-dataset; the baseline can be found at https://github.com/gurkirt/3D-RetinaNet.
New Characterizations of Strategy-Proofness under Single-Peakedness
Venue: arXiv cs.GT 2022
Year: 2022

We provide novel simple representations of strategy-proof voting rules when voters have uni-dimensional single-peaked preferences (as well as multi-dimensional separable preferences). The analysis recovers, links and unifies existing results in the literature such as Moulin's classic characterization in terms of phantom voters and Barberà, Gul and Stacchetti's in terms of winning coalitions ("generalized median voter schemes"). First, we compare the computational properties of the various representations and show that the grading curve representation is superior in terms of computational complexity. Moreover, the new approach allows us to obtain new characterizations when strategy-proofness is combined with other desirable properties such as anonymity, responsiveness, ordinality, participation, consistency, or proportionality. In the anonymous case, two methods are single out: the -- well know -- ordinal median and the -- most recent -- linear median.
Nonlinear Invariant Risk Minimization: A Causal Approach
Venue: arXiv cs.LG 2022
Year: 2022

Due to spurious correlations, machine learning systems often fail to generalize to environments whose distributions differ from the ones used at training time. Prior work addressing this, either explicitly or implicitly, attempted to find a data representation that has an invariant relationship with the target. This is done by leveraging a diverse set of training environments to reduce the effect of spurious features and build an invariant predictor. However, these methods have generalization guarantees only when both data representation and classifiers come from a linear model class. We propose invariant Causal Representation Learning (iCaRL), an approach that enables out-of-distribution (OOD) generalization in the nonlinear setting (i.e., nonlinear representations and nonlinear classifiers). It builds upon a practical and general assumption: the prior over the data representation (i.e., a set of latent variables encoding the data) given the target and the environment belongs to general exponential family distributions. Based on this, we show that it is possible to identify the data representation up to simple transformations. We also prove that all direct causes of the target can be fully discovered, which further enables us to obtain generalization guarantees in the nonlinear setting. Extensive experiments on both synthetic and real-world datasets show that our approach outperforms a variety of baseline methods. Finally, in the discussion, we further explore the aforementioned assumption and propose a more general hypothesis, called the Agnostic Hypothesis: there exist a set of hidden causal factors affecting both inputs and outcomes. The Agnostic Hypothesis can provide a unifying view of machine learning. More importantly, it can inspire a new direction to explore a general theory for identifying hidden causal factors, which is key to enabling the OOD generalization guarantees.
Coalgebra Encoding for Efficient Minimization
Venue: arXiv cs.DS 2022
Year: 2022

Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.
PredDiff: Explanations and Interactions from Conditional Expectations
Venue: arXiv cs.LG 2022
Year: 2022

PredDiff is a model-agnostic, local attribution method that is firmly rooted in probability theory. Its simple intuition is to measure prediction changes while marginalizing features. In this work, we clarify properties of PredDiff and its close connection to Shapley values. We stress important differences between classification and regression, which require a specific treatment within both formalisms. We extend PredDiff by introducing a new, well-founded measure for interaction effects between arbitrary feature subsets. The study of interaction effects represents an inevitable step towards a comprehensive understanding of black-box models and is particularly important for science applications. Equipped with our novel interaction measure, PredDiff is a promising model-agnostic approach for obtaining reliable, numerically inexpensive and theoretically sound attributions.