Talks

Provable Repair of Deep Neural Network Defects by Preimage Synthesis and Property Refinement

Deep neural networks may exhibit dangerous behaviors under various security threats and there exists an ongoing arms race between attackers and defenders. In this work, we propose to utilize recent progress on neural network repair to mitigate these threats and repair various kinds of neural network defects within a unified framework. To push the boundary of existing repairs (suffering from limitations such as lack of guarantees, limited scalability, etc) in addressing more practical contexts, we propose ProRepair, a novel provable repair framework driven by formal preimage synthesis and property refinement. The key ideas are: (i) synthesizing a proxy box to characterize the feature-space preimage, which can guide the subsequent repair step towards the correct outputs, and (ii) performing property refinement to enable surgical corrections and scale to more complex tasks. We evaluate ProRepair across various repair tasks and the results demonstrate it outperforms existing methods.

The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification

While existing formal verification tools are increasingly effective at verifying local robustness properties, more complex ones, such as those involving multiple neural networks, remain beyond their capabilities: these properties cannot currently be expressed in their specification languages, nor can they be directly verified. We present CAISAR, an open-source platform for specifying and verifying properties of machine learning models, with particular focus on neural networks and support vector machines. CAISAR provides a high-level language for specifying complex properties and integrates several state-of-the-art verifiers for their automatic verification. Through concrete use cases, we show how CAISAR leverages automated graph-editing techniques to translates high-level specifications into queries for the supported verifiers, bridging the embedding gap between user specifications and the corresponding ones that are actually verified.

From Decision Trees to Boolean Logic: A Fast and Unified SHAP Algorithm

SHapley Additive exPlanations (SHAP) is a key tool for interpreting decision tree ensembles by assigning contribution values to features. The most accurate variant, Background SHAP, uses a background dataset to estimate feature distributions. We introduce WOODELF, a SHAP algorithm that unifies decision trees, game theory, and Boolean logic within a single framework. For each instance, WOODELF constructs a pseudo-Boolean formula that captures their feature values, the structure of the decision tree ensemble, and the entire background dataset. It then leverages this representation to compute Background SHAP in linear time. WOODELF can also compute Shapley interaction values, Banzhaf values, and Banzhaf interaction values. WOODELF runs efficiently on both CPU and GPU. We demonstrate these advantages empirically on two large, commonly used datasets, where WOODELF achieves at least an order-of-magnitude speedup over state-of-the-art methods.

AAAI Main Conference Oral Presentation: Thu 22/01, 9:30-10:30 - ML1 (Garnet 218) & Poster: 22/01

Formal Abductive Latent Explanations for Prototype-Based Networks

Case-based reasoning networks are models that make predictions based on similarity between the input and prototypical parts of training samples. Such models explain each decision by pointing to the prototypes that contributed the most to the final outcome. While promising, such explanations are sometimes misleading, which hampers their usefulness in safety-critical contexts. Several instances may lead to different predictions and yet have the same explanation. Drawing inspiration from formal eXplainable AI, we propose Abductive Latent Explanations (ALEs), a formalism to express sufficient conditions on the latent representation of the instance that imply the prediction. Our approach combines the inherent interpretability of case-based reasoning models and the guarantees provided by formal XAI. We propose a solver-free algorithm for generating ALEs based on three distinct paradigms, compare them, and present the feasibility of our approach on diverse datasets for image classification.



AAAI Main Conference Poster Presentation: Thu 22/01

Improving Stochastic Action-Constrained Reinforcement Learning via Truncated Distributions

In reinforcement learning (RL), it is advantageous to consider additional constraints on the action space to ensure safety. Existing work on such action-constrained RL often lacks expressive policy updates, computational efficiency, and predictable runtime. Recent work proposes to use truncated normal distributions for stochastic policy gradient methods. However, the computation of key characteristics, such as the entropy, log-probability, and their gradients, becomes intractable. Hence, prior work approximates these using the non-truncated distributions, which severely degrades performance. We argue that accurate estimation of these characteristics is crucial in the action-constrained RL setting, and propose efficient numerical approximations for them. We also provide an efficient sampling strategy for truncated policy distributions and validate our approach on three benchmark environments, which demonstrate significant performance improvements when using accurate estimations.

Space Explanations of Neural Network Classification

We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by state-of-the-art.

Qualitative Analysis of $\omega$-Regular Objectives on Robust MDPs

Robust Markov Decision Processes generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for $\omega$-regular objectives. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. We present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives, together with experimental results.

PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C

Python has become the dominant language for general-purpose programming, yet it lacks robust tools for formal verification. In contrast, programmers working in languages such as C benefit from mature model checkers, for example CBMC, which enable exhaustive symbolic reasoning and fault localisation. In this paper, we propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model checking and MaxSAT-based fault localisation in the generated C code. PyVeritas enables verification and bug localisation for Python code using existing model checking tools for C. Our empirical evaluation demonstrates that LLM-based transpilation can achieve a high degree of accuracy, up to 90% for some LLMs, enabling effective development environment that supports assertion-based verification and interpretable fault diagnosis for small yet non-trivial Python programs.