Bayesian neural networks (BNNs), a family of neural networks with a probability distribution placed on their weights, have the advantage of being able to reason about uncertainty in their predictions as well as data. Their deployment in safety-critical applications demands rigorous robustness guarantees. This paper summarises recent progress in developing algorithmic methods to ensure certifiable safety and robustness guarantees for BNNs, with the view to support design automation for systems incorporating BNN components.

Real-world adoption of deep neural networks (DNNs) in critical applications requires ensuring strong generalization beyond testing datasets. Unfortunately, the standard practice of measuring DNN performance on a finite set of test inputs cannot ensure DNN safety on inputs in the wild. In this talk, I will focus on how certified AI can be leveraged as a service to bridge this gap by building DNNs with strong generalization on an infinite set of unseen inputs. In the process, I will discuss some of our recent work for building trust and safety in diverse domains such as vision, systems, finance, and more. I will also describe a path toward making certified AI more scalable, easy to develop, and accessible to DNN developers lacking formal backgrounds.

In this talk, we study safety properties of a dynamical system in feedback with a neural network controller from a reachability perspective. We first embed the closed-loop dynamics into a larger system using the theory of mixed monotone dynamical systems with favorable control theoretic properties. In particular, we show that hyper-rectangular over-approximations of the reachable sets are efficiently computed using a single trajectory of the embedding system. Numerically computing this trajectory requires bounds on the input-output behavior of the neural network controller, which we obtain via carefully selected and infrequent queries to an oracle. We assume the oracle provides these input-output bounds as intervals or as affine bounding functions, which is common for many state-of-the-art methods. Moreover, we show that, if this embedding system is constructed in a certain way, the contraction rate of the embedding system is the same as the original closed-loop system. Thus, this embedding provides a scalable approach for reachability analysis of the neural network control loop while preserving the nonlinear structure of the system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters.

Numerous methods have emerged to verify the robustness of deep neural networks (DNNs). While effective in providing theoretical guarantees, the proofs generated using these techniques often lack human interpretability. Our paper bridges this gap by introducing new concepts, algorithms, and representations that generate human-understandable interpretations of the proofs. Using our approach, we discover that standard DNN proofs rely more on irrelevant input features compared to provably robust DNNs. Provably robust DNNs filter out spurious input features, but sometimes it comes at the cost of semantically meaningful ones. DNNs combining adversarial and provably robust training strike a balance between the two. Overall, our work enhances human comprehension of proofs and sheds light on their reliance on different types of input features.

Physics-informed neural networks (PINN) have been proven efficient at solving partial differential equations (PDE). However, previous works have failed to provide guarantees on the worstcase residual error of a PINN across the spatiotemporal domain – a measure akin to the tolerance of numerical solvers – focusing instead on pointwise comparisons between their solution and the ones obtained by a solver at a set of inputs. In real-world applications, one cannot consider tests on a finite set of points to be sufficient grounds for deployment. To alleviate this issue, we establish tolerance-based correctness conditions for PINNs over the entire input domain. To verify the extent to which they hold, we introduce ∂-CROWN: a general and efficient post-training framework to bound PINN errors. We demonstrate its effectiveness in obtaining tight certificates by applying it to two classical PINNs – Burgers’ and Schrodinger’s equations –, and two more challenging ones – the Allan-Cahn and Diffusion-Sorption equations.

"Stability Guarantees for Feature Attributions with Multiplicative Smoothing" Anton Xue (University of Pennsylvania)*; Rajeev Alur (University of Pennsylvania ); Eric Wong (University of Pennsylvania)

"DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation" Haitham Khedr (University of California, Irvine)*; Yasser Shoukry (University of California, Irvine)

"Probabilistic Global Robustness Verification of Arbitrary Supervised Machine Learning Models" Max-Lion Schumacher (Fraunhofer IPA)*; Marco Huber (University of Stuttgart)

"Formal Verification for Counting Unsafe Inputs in Deep Neural Networks" Luca Marzari (University of Verona)*; Davide Corsi (University of Verona); Ferdinando Cicalese (University of Verona); Alessandro Farinelli (University of Verona, Italy)

"Toward Continuous Verification of DNNs" Shubham Ugare (UIUC)*; Debangshu Banerjee (University of Illinois Urbana-Champaign); Tarun Suresh (University of Illinois Urbana-Champaign); Sasa Misailovic (UIUC); Gagandeep Singh (VMware Research and UIUC)

"Formal Verification for Neural Networks with General Nonlinearities via Branch-and-Bound" Zhouxing Shi (UCLA)*; Qirui Jin (University of Michigan); Huan Zhang (CMU); Zico Kolter (Carnegie Mellon University); Suman Jana (Columbia University); Cho-Jui Hsieh (UCLA)

"Towards Verifying Monotonicity and Robustness Properties for Domain-Specific DRL Algorithms" Mohammad Zangooei (University of Waterloo)*; Mina Tahmasbi Arashloo (University of Waterloo); Raouf Boutaba (University of Waterloo)

"Benchmarking Formal Verification for Autonomous Driving in the Wild" Yonggang Luo (Chongqing Changan Automobile)*; Jinyan Ma (Chongqing Changan Automobile); Sanchu Han (Chongqing Changan Automobile); Lecheng Xie (Chongqing Changan Automobile)

"Formal Control Synthesis for Stochastic Neural Network Dynamic Models" Steven J.L. Adams (TU Delft)*; Morteza Lahijanian (University of Colorado Boulder); Luca Laurenti (TU Delft)

"A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems" Akash Harapanahalli (Georgia Institute of Technology)*; Saber Jafarpour (Georgia Institute of Technology); Sam Coogan (Georgia Tech)

"Fast Feature Selection with Fairness Constraints" Francesco Quinzan (Hasso Plattner Institute)*; Rajiv Khanna (Purdue University); Moshik Hershcovitch (IBM Research); Sarel Cohen (Hasso Plattner Institute); Daniel G Waddington (IBM Research); Tobias Friedrich (Hasso Plattner Institute); Michael Mahoney (University of California, Berkeley)

"Understanding Certified Training with Interval Bound Propagation" Yuhao Mao (ETH Zurich); Mark Niklas Müller (ETH Zurich)*; Marc Fischer (ETH Zurich); Martin Vechev (ETH Zurich)

Traditionally, Formal Verification (FV) of Deep Neural Networks (DNN) can be employed to check whether a DNN is unsafe w.r.t. some given property (i.e., whether there is at least one unsafe input configuration). However, the binary answer typically returned could be not informative enough for other purposes, such as shielding, model selection, or training improvements. In this paper, we introduce the #DNN-Verification problem, which involves counting the number of input configurations of a DNN that result in a violation of a particular safety property. We analyze the complexity of this problem and propose a novel approach that returns the exact count of violations. Due to the #P-completeness of the problem, we also propose a randomized, approximate method that provides a provable probabilistic bound of the correct count while significantly reducing computational requirements tested on a set of safety-critical benchmarks.

Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus is on specifications expressed in linear temporal logic interpreted over finite traces (LTLf), and the approach is based on finite abstraction. Specifically, we leverage recent techniques for convex relaxation of NNs to formally abstract a NNDM into an interval Markov decision process (IMDP). Then, a strategy that maximizes the probability of satisfying a given specification is synthesized over the IMDP and mapped back to the underlying NNDM. We show that the process of abstracting NNDMs to IMDPs reduces to a set of convex optimization problems, hence guaranteeing efficiency. We also present an adaptive refinement procedure that makes the framework scalable. On several case studies, we illustrate the our framework is able to provide non-trivial guarantees of correctness for NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer.

Many works have been devoted to evaluating the robustness of a classifier in the neighborhood of single points of input data. Recently, in particular, probabilistic settings have been considered, where robustness is defined in terms of random perturbations of input data. In this paper, we consider robustness on the entire input domain as opposed to single points of input. For the first time, we provide formal guarantees on the probability of robustness, given a random input and a random perturbation, based only on sampling or in combination with existing pointwise methods. This is applicable to any classification or regression model and any random input perturbation. We then illustrate the resulting bounds on classifiers for the MNIST and CIFAR-10 datasets.

Formal certification of Neural Networks (NNs) is crucial for ensuring their safety, fairness, and robustness. Unfortunately, on the one hand, sound and complete certification algorithms of ReLU-based NNs do not scale to large-scale NNs. On the other hand, incomplete certification algorithms are easier to compute, but they result in loose bounds that deteriorate with the depth of NN, which diminishes their effectiveness. In this paper, we ask the following question; can we replace the ReLU activation function with one that opens the door to incomplete certification algorithms that are easy to compute but can produce tight bounds on the NN's outputs? We introduce DeepBern-Nets, a class of NNs with activation functions based on Bernstein polynomials instead of the commonly used ReLU activation. Bernstein polynomials are smooth and differentiable functions with desirable properties such as the so-called range enclosure and subdivision properties. We design a novel Interval Bound Propagation (IBP) algorithm, called Bern-IBP, to efficiently compute tight bounds on DeepBern-Nets outputs. Our approach leverages the properties of Bernstein polynomials to improve the tractability of neural network certification tasks while maintaining the accuracy of the trained networks. We conduct comprehensive experiments in adversarial robustness and reachability analysis settings to assess the effectiveness of the proposed Bernstein polynomial activation in enhancing the certification process. Our proposed framework achieves high certified accuracy for adversarially-trained NNs, which is often a challenging task for certifiers of ReLU-based NNs. Moreover, using Bern-IBP bounds for certified training results in NNs with state-of-the-art certified accuracy compared to ReLU networks. This work establishes Bernstein polynomial activation as a promising alternative for improving neural network certification tasks across various NNs applications.

Explanation methods for machine learning models tend to not provide any formal guarantees and may not reflect the underlying decision-making process. In this work, we analyze stability as a property for reliable feature attribution methods. We prove that a relaxed variant of stability is guaranteed if the model is sufficiently Lipschitz with respect to the masking of features. To achieve such a model, we develop a smoothing method called Multiplicative Smoothing (MuS). We show that MuS overcomes theoretical limitations of standard smoothing techniques and can be integrated with any classifier and feature attribution method. We evaluate MuS on vision and language models with a variety of feature attribution methods, such as LIME and SHAP, and demonstrate that MuS endows feature attributions with non-trivial stability guarantees.

Deep Reinforcement Learning (DRL) algorithms have demonstrated significant performance benefits compared to traditional heuristics in various systems and networking applications. However, concerns surrounding their explainability, generalizability, and robustness pose obstacles to their widespread deployment. In response, the research community has explored the application of formal verification techniques to ensure the safe deployment of DRL algorithms. This study focuses on DRL algorithms with discrete numerical action spaces, which are commonly utilized in systems and networking domains but have been under-explored when it comes to formal analysis. We investigate two fundamental properties: monotonicity and robustness. We employ formal methods to verify these properties beyond the confines of the training set, thereby enhancing generalization and validating robustness. To illustrate the effectiveness and tractability of the proposed verification approach, we implement a proof of concept using Gurobi and present a case study involving two systems and networking DRL algorithms.

Deep neural network (DNN) verification is used to assess whether a DNN meets a desired trustworthy property (e.g., robustness, fairness) on an infinite input set. While there have been significant advancements in scalable verifiers for individual DNNs, they suffer from inefficiency when developers update a deployed DNN (e.g. through quantization, pruning, or fine-tuning) to enhance its inference speed or accuracy. The verification is inefficient because the developers need to rerun the computationally expensive verifier from scratch on the updated DNN. To address this issue, we propose an incremental DNN verification framework, leveraging novel theory, data structures, and algorithms. Our previous works anonymous (2023) and anonymous (2022) focused on incremental verification, and in this paper, we provide a summary of these advancements and explore the potential of incremental verification in enabling real-world DNN verification systems.

In this paper, we present a toolbox for interval analysis in \texttt{numpy}, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of mappings. The toolbox offers efficient computation of natural inclusion functions using compiled C code, as well as a familiar interface in \texttt{numpy} with its canonical features, such as $n$-dimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in formal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.

We study the fundamental problem of selecting optimal features for model construction. This problem is computationally challenging on large datasets, even with the use of greedy algorithm variants. To address this challenge, we extend the adaptive query model, recently proposed for the greedy forward selection for submodular functions, to the faster paradigm of Orthogonal Matching Pursuit for non-submodular functions. The proposed algorithm achieves exponentially fast parallel run time in the adaptive query model, scaling much better than prior work. Furthermore, our extension allows the use of downward-closed constraints, which can be used to encode certain fairness criteria into the feature selection process. We prove strong approximation guarantees for the algorithm based on standard assumptions. These guarantees are applicable to many parametric models, including Generalized Linear Models. Finally, we demonstrate empirically that the proposed algorithm competes favorably with state-of-the-art techniques for feature selection, on real-world and synthetic datasets.

Bound propagation with branch-and-bound (BaB) is so far among the most effective methods for neural network (NN) verification. However, existing works with BaB have mostly focused on NNs with piecewise linear activations only, especially ReLU neurons. In this paper, we develop a framework for conducting BaB based on bound propagation with general branching points and an arbitrary number of branches, as an important move for extending verification to models with various nonlinearities beyond ReLU. Our framework strengthens verification for common \emph{element-wise} activation functions, as well as other \emph{multi-dimensional} nonlinear operations that arise naturally in computation graphs, such as multiplication and division. In addition, we find that existing branching heuristics for choosing neurons to branch for ReLU networks are insufficient for general nonlinearities, and we design a new heuristic named BBPS, which outperforms the heuristic obtained by directly extending the existing ones originally developed for ReLU networks. We empirically demonstrate the effectiveness of our BaB framework on verifying a wide range of NNs, including networks with Sigmoid, Tanh, or Sin activations, LSTMs, and ViTs, which have various nonlinearities.

The verification of the security of neural networks is cruicial, especially for the field of autonomous driving. Although there are currently benchmarks for the verification of the robustness of neural networks, there are hardly any benchmarks related to the field of autonomous driving, especially those related to object detection and semantic segmentation. Thus, a notable gap exists in formally verifying the robustness of semantic semantic segmentation and object detection tasks under complex, real-world conditions. To address this, we present an innovative approach to benchamark formal verification for autonomous driving perception tasks. Firstly, we propose robust verification benchmarks for semantic segmentation and object detection, supplementing existing methods. Secondly, and more significantly, we introduce a novel patch-level disturbance approach for object detection, providing a more realistic representation of real-world scenarios. By augmenting the current verification benchmarks with our novel proposals, our work contributes towards developing a more comprehensive, practical, and realistic benchmarking methodology for perception tasks in autonomous driving, thereby propelling the field towards improved safety and reliability.

As robustness verification methods are becoming more precise, training certifiably robust neural networks is becoming ever more relevant. To this end, certified training methods compute and then optimize an upper bound on the worst-case loss over a robustness specification. Curiously, training methods based on the imprecise interval bound propagation (IBP) consistently outperform those leveraging more precise bounding methods. Still, we lack an understanding of the mechanisms making IBP so successful.In this work, we thoroughly investigate these mechanisms theoretically and empirically by leveraging a novel metric measuring the tightness of IBP bounds.

State density distribution, in contrast to worst-case reachability, can be leveraged for safety-related problems to better quantify the likelihood of the risk for potentially hazardous situations. We developed a data-driven method to compute the density distribution of reachable states for nonlinear and even black-box systems. Our approach can estimate the set of all possible future states as well as their density. Moreover, we could perform online safety verification with probability ranges for unsafe behaviors to occur. We show that our approach can learn the density distribution of the reachable set more accurately with less data and quantify risks less conservatively and flexibly compared with worst-case analysis. We also study the use of such an approach in combination with model predictive control for verifiable safe path planning under uncertainties.

Researchers have demonstrated that the machine-learning pipeline is susceptible to attacks both at training and inference time -- poisoning, backdoor, and evasion attacks. In this talk, we will describe new results on holistic approaches for certifying robustness. Our techniques draw upon ideas from test-time certification and ensembling to simultaneously establish formal robustness guarantees for both training and inference.

Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus is on specifications expressed in linear temporal logic interpreted over finite traces (LTLf), and the approach is based on finite abstraction. Specifically, we leverage recent techniques for convex relaxation of NNs to formally abstract a NNDM into an interval Markov decision process (IMDP). Then, a strategy that maximizes the probability of satisfying a given specification is synthesized over the IMDP and mapped back to the underlying NNDM. We show that the process of abstracting NNDMs to IMDPs reduces to a set of convex optimization problems, hence guaranteeing efficiency. We also present an adaptive refinement procedure that makes the framework scalable. On several case studies, we illustrate that our framework is able to provide non-trivial guarantees of correctness for NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer.

Guaranteeing safe behaviour of reinforcement learning (RL) policies poses significant challenges for safety-critical applications, despite RL’s generality and scalability. To address this, we propose a new approach to apply verification methods from control theory to learned value functions. By analyzing task structures for safety preservation, we formalize original theorems that establish links between value functions and control barrier functions. Further, we propose novel metrics for verifying value functions in safe control tasks and practical implementation details to improve learning. Our work presents a novel method for certificate learning, which unlocks a diversity of verification techniques from control theory for RL policies, and marks a significant step towards a formal framework for the general, scalable, and verifiable design of RL-based control systems.

"Meaning in Language Models: A Formal Semantics Approach" Charles Jin (MIT)*; Martin Rinard (MIT)

"Provably Correct Physics-Informed Neural Networks" Francisco Girbal Eiras (University of Oxford)*; Adel Bibi (University of Oxford); Rudy Bunel (Deepmind); Krishnamurthy Dvijotham (Google Research); Philip Torr (University of Oxford); M. Pawan Kumar (Google DeepMind)

"Your Value Function is a Control Barrier Function" Daniel CH Tan (University College London)*; Fernando Acero (University College London); Robert McCarthy (University College London); Dimitrios Kanoulas (University College London); Zhibin (Alex) Li (University College London)

"Constraint Satisfied Sampling for Formal Verification in Geometric Deep Learning and Molecular Modelling" Justin S Diamond (University of Basel)*; Markus Lill (University of Basel)

"One Pixel Adversarial Attacks via Sketched Programs" Tom Yuviler (Technion)*; Dana Drachsler-Cohen (Technion)

"Robustness Verification for Perception Models against Camera Motion Perturbations" Hanjiang Hu (Carnegie Mellon University)*; Changliu Liu (Carnegie Mellon University); DING ZHAO (Carnegie Mellon University)

"Efficient Estimation of Local Robustness of Machine Learning Models" Tessa Han (Harvard University)*; Suraj Srinivas (Harvard University); Himabindu Lakkaraju (Harvard)

"(Almost) Provable Error Bounds Under Distribution Shift via Disagreement Discrepancy" Elan Rosenfeld (Carnegie Mellon University)*; Saurabh Garg (CMU)

"Learning Counterfactually Invariant Predictors" Francesco Quinzan (Hasso Plattner Institute)*; Cecilia Casolo (Helmholtz München); John Doe (Dark Matter); Yucen Luo (Max Planck Institute for Intelligent Systems); Niki Kilbertus (Helmholtz AI)

"Interpreting Robustness Proofs of Deep Neural Networks" Debangshu Banerjee (University of Illinois Urbana-Champaign)*; Avaljot Singh (UIUC); Gagandeep Singh (VMware Research and UIUC)

"Connecting Certified and Adversarial Training" Yuhao Mao (ETH Zurich); Mark Niklas Müller (ETH Zurich)*; Marc Fischer (ETH Zurich); Martin Vechev (ETH Zurich)

Physics-informed neural networks (PINN) have been proven efficient at solving partial differential equations (PDE). However, previous works have failed to provide guarantees on the worst-case residual error of a PINN across the spatio-temporal domain – a measure akin to the tolerance of numerical solvers – focusing instead on point-wise comparisons between their solution and the ones obtained by a solver at a set of inputs. In real-world applications, one cannot consider tests on a finite set of points to be sufficient grounds for deployment. To alleviate this issue, we establish tolerance-based correctness conditions for PINNs over the entire input domain. To verify the extent to which they hold, we introduce ∂-CROWN: a general and efficient post-training framework to bound PINN errors. We demonstrate its effectiveness in obtaining tight certificates by applying it to two classical PINNs – Burgers’ and Schrödinger's equations –, and two more challenging ones – the Allan-Cahn and Diffusion-Sorption equations.

We derive an (almost) guaranteed upper bound on the error of deep neural networks under distribution shift using unlabeled test data. Prior methods either give bounds that are vacuous in practice or give \emph{estimates} that are accurate on average but heavily underestimate error for a sizeable fraction of shifts. Our bound requires a simple, intuitive condition which is well justified by prior empirical works and holds in practice effectively 100\% of the time. The bound is inspired by HΔH-divergence but is easier to evaluate and substantially tighter, consistently providing non-vacuous guarantees. Estimating the bound requires optimizing one multiclass classifier to disagree with another, for which some prior works have used sub-optimal proxy losses; we devise a ``disagreement loss'' which is theoretically justified and performs better in practice. Across a wide range of benchmarks, our method gives valid error bounds while achieving average accuracy comparable to competitive estimation baselines.

Neural networks are susceptible to adversarial examples, including one pixel attacks. Existing one pixel attacks iteratively generate candidate adversarial examples and submit them to the network until finding a successful candidate. However, current attacks require a very large number of queries, which is infeasible in many practical settings. In this work, we leverage program synthesis and identify an expressive program sketch that enables the computation of adversarial examples using significantly fewer queries. We introduce OPPSLA, a synthesizer that instantiates the sketch with customized conditions. Experimental results show that OPPSLA achieves a state-of-the-art success rate while requiring an order of magnitude fewer queries than existing attacks.

Although RL is highly general and scalable, the difficulty of verifying out-of-distribution behaviour poses challenges for safety-critical applications. To remedy this, we propose to apply verification methods used in control theory to learned value functions. By analyzing a simple task structure for safety preservation, we derive original theorems linking value functions to control barrier functions. Inspired by this analogy, we propose novel metrics for value functions in safe control tasks and propose practical implementation details that improve learning. Besides proposing a novel method for certificate learning, our work unlocks a wealth of verification methods in control theory for RL policies, and represents a first step towards a framework for general, scalable, and verifiable design of control systems.

Analyzing the macroscopic traits of biologicalmolecules and protein complexes requires accu-rate and specific descriptions of statistical en-sembles. A notable challenge is the samplingfrom subspaces of a state-space, either becausewe have prior structural knowledge or only cer-tain subsets of the state-space are of interest. Weintroduce a method to samples from distributionsthat formally satisfy sets of geometric constraintsin Euclidean spaces. This is accomplished by in-corporating a constraint projection operator intothe well-established structure of Denoising Dif-fusion Probabilistic Models. In deep learning-based drug design, maintaining specific molecu-lar interactions is essential for achieving desiredtherapeutic effects and ensuring safety. Thisstarts a meaningful intersection between formalverification principles and machine learning inthe realm of biochemical studies of compoundsand generative modeling. It offers a way to for-mally verify the distributions from which sam-ples are drawn.

Notions of counterfactual invariance have proven essential for predictors that are fair, robust, and generalizable in the real world. We propose simple graphical criteria that yield a sufficient condition for a predictor to be counterfactually invariant in terms of (conditional independence in) the observational distribution. Any predictor that satisfies our criterion is provably counterfactually invariant. In order to learn such predictors, we propose a model-agnostic framework, called Counterfactual Invariance Prediction (CIP), building on a kernel-based conditional dependence measure called Hilbert-Schmidt Conditional Independence Criterion (HSCIC). Our experimental results demonstrate the effectiveness of CIP in enforcing counterfactual invariance across various simulated and real-world datasets including scalar and multi-variate settings.

Machine learning models often need to be robust to noisy input data. The effect of real-world noise (which is often random) on model predictions is captured by a model’s local robustness, i.e., the consistency of model predictions in a local region around an input. However, the naïve approach to computing local robustness based on Monte-Carlo sampling is statistically inefficient, leading to prohibitive computational costs for large-scale applications. In this work, we develop the first analytical estimators to efficiently compute local robustness of multi-class discriminative models using local linear function approximation and the multivariate Normal CDF. Through the derivation of these estimators, we show how local robustness is connected to concepts such as randomized smoothing and softmax probability. We also confirm empirically that these estimators accurately and efficiently compute the local robustness of standard deep learning models. In addition, we demonstrate these estimators’ usefulness for various tasks involving local robustness, such as measuring robustness bias and identifying examples that are vulnerable to noise perturbation in a dataset. By developing these analytical estimators, this work not only advances conceptual understanding of local robustness, but also makes its computation practical, enabling the use of local robustness in critical downstream applications.

Robust perception is still challenging due to the internal vulnerability of DNNs to adversarial examples as well as the external uncertainty of sensing data, e.g. sensor placement and motion perturbation. Recent work can only give provable robustness guarantees in a probabilistic way which is not enough for safety-critical scenarios due to false positive certificates. To this end, we propose the first deterministic provable defense framework against camera motion by extending the verification of neural networks (VNN) method from lp bounded perturbation to parameterized camera motion space for robotics applications. Through the dense partitions of image projection from 3D dense point cloud to fully cover all the pixels, all the pixel values can be bounded by linear relaxations using linear programming, which makes the camera motion perturbation verifiable and compatible with current incomplete and complete formal VNN methods given DNN models. Extensive experiments are conducted on the Metaroom dataset for the dense image projection and our sound and complete method is more computationally efficient than the randomized smoothing based method at small perturbation radii.

Numerous methods have emerged to verify the robustness of deep neural networks (DNNs). While effective in providing theoretical guarantees, the proofs generated using these techniques often lack human interpretability. Our paper bridges this gap by introducing new concepts, algorithms, and representations that generate human-understandable interpretations of the proofs. Using our approach, we discover that standard DNN proofs rely more on irrelevant input features compared to provably robust DNNs. Provably robust DNNs filter out spurious input features, but sometimes it comes at the cost of semantically meaningful ones. DNNs combining adversarial and provably robust training strike a balance between the two. Overall, our work enhances human comprehension of proofs and sheds light on their reliance on different types of input features.

We present a framework for studying the emergence of meaning in language models based on the formal semantics of programs. Working with programs enables us to precisely define concepts relevant to meaning in language (e.g., correctness and semantics), making this domain well-suited as an intermediate testbed for characterizing the presence (or absence) of meaning in language models. Specifically, we first train a Transformer model on the corpus of programs, then probe the trained model's hidden states as it completes a program given a specification. Our findings include evidence that (1) the model states linear encode an abstraction of the program semantics, (2) such encodings emerge nearly in lockstep with the ability of the model to generate correct code during training, and (3) the model learns to generate correct programs that are, on average, shorter than those in the training set. In summary, this paper does not propose any new techniques for improving language models, but develops an experimental framework for and provides insights into the acquisition and representation of (formal) meaning in language models.

Training certifiably robust neural networks remains a notoriously hard problem. While adversarial training optimizes under-approximations of the worst-case loss, which leads to insufficient regularization for certification, certified training methods, optimize loose over-approximations, leading to over-regularization and poor accuracy. In this work, we propose TAPS, a novel certified training method combining IBP and PGD training to optimize more precise, although not necessarily sound, worst-case loss approximations, reducing over-regularization and increasing certified accuracy. Empirically, TAPS achieves a new state-of-the-art in many settings, e.g., reaching a certified accuracy of 22\% on TinyImageNet for $\ell_\infty$-perturbations with radius $\epsilon=1/255$.

Learning representations that combine program structure with neural components can help provide a path to learned systems with stronger safety guarantees. In this talk, I will describe some of our recent work on learning with program representations and its connection to safety and verification.