ABSTRACT. Modern neural networks are powerful but opaque: they encode meaning in high-dimensional latent spaces that are hard to inspect. Interpretability research asks what these internal representations contain, and whether we can read, probe, and even steer them. In this talk, I'll give an accessible introduction to latent-space interpretability for a broad audience and connect it to my own work on the structure of learned representations. I'll show how human-meaningful concepts emerge across the layers of a network, and how concept regions tend to be approximately convex - structural regularities that offer a window into what these models have actually learned.

ABSTRACT. Accelerated by rapid advances in machine learning and AI, there has been tremendous success in the design of learning-enabled autonomous systems in areas such as autonomous driving and robotics. These exciting developments are accompanied by new fundamental challenges that arise regarding the safety and reliability of these increasingly complex systems due to imperfect learning, system unknowns, and uncertain environments. Statistical tools for uncertainty quantification have gained popularity due to their ability to deal with these challenges. However, their guarantees rely on i.i.d. data, an assumption that is violated when control actions change the underlying data distribution. In this talk, I will provide new insight to design safe controllers under distribution shifts using robust conformal prediction (CP). I will begin by advocating for the use of CP due to its simplicity, generality, and efficiency as opposed to existing optimization-based verification techniques. I will then provide an introduction to CP and summarize existing work that uses CP to design probabilistically safe controllers in dynamic environments. Subsequently, we will look into interactive settings where the system’s behavior may change the environment's behavior, and vice versa. This circular dependency creates an interaction-driven distribution shift that invalidates existing CP guarantees. To deal with this problem, we propose an iterative framework that episodically updates the controller while robustly maintaining safety guarantees by quantifying the potential impact of a controller update on the environment's behavior. We realize this via adversarially robust CP where we perform a regular CP step in each episode using observed data under the current controller, but then transfer safety guarantees across controller updates by analytically adjusting the CP result to account for distribution shifts. Lastly, I will show how these ideas extend to handling policy-induced distribution shifts that arise when using barrier/Lyapunov functions to control uncertain systems. Bio: Lars Lindemann is currently an Assistant Professor for Algorithmic Systems Theory in the Automatic Control Laboratory at ETH Zürich. From 2023 to 2025 he was an Assistant Professor in the Thomas Lord Department of Computer Science at the University of Southern California. From 2020 to 2022 he was a Postdoctoral Fellow in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. degree in Electrical Engineering from KTH Royal Institute of Technology in 2020. His research interests include systems and control theory, formal methods, machine learning, and autonomous systems. Professor Lindemann received the Outstanding Student Paper Award at the 58th IEEE Conference on Decision and Control and the Student Best Paper Award (as an advisor) at the 60th IEEE Conference on Decision and Control. He was finalist for the Best Paper Award (as an advisor) at the 2024 International Conference on Cyber-Physical Systems, the Best Paper Award at the 2022 Conference on Hybrid Systems: Computation and Control, and the Best Student Paper Award at the 2018 American Control Conference.

ABSTRACT. Neural networks hold great potential to act as approximate models of nonlinear dynamical systems, with the resulting neural approximations enabling verification and control of such systems. However, in safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system. To address this fundamental challenge, we propose a novel, adaptive, and parallelizable verification method based on certified first-order models. Our approach provides formal error bounds on the neural approximations of dynamical systems, allowing them to be safely employed as surrogates by interpreting the error bound as bounded disturbances acting on the approximated dynamics. We demonstrate the effectiveness and scalability of our method on a range of established benchmarks from the literature, showing that it significantly outperforms the state-of-the-art. Furthermore, we show that our framework can successfully address additional scenarios previously intractable for existing methods -- neural network compression and an autoencoder-based deep learning architecture for learning Koopman operators for the purpose of trajectory prediction.

ABSTRACT. The specification and verification of temporal properties is crucial to assess the safety of monitoring systems. Said systems need to ensure that certain properties are validated during its full operation time. The rich pattern-finding capabilities of deep learning are a strong incitation to implement such monitors as neural networks. However, neural networks verification historically focused on properties related to a single point in time. In this paper, we present a way to encode Linear Temporal Logic (LTL) properties in a neural network specification language. We derive from this encoding an automated translation to existing off-the-shelf provers. We apply our system to the verification of an industrial use case: a monitoring system for batch distillation. We were able to successfully specify and verify most of the properties in a small runtime.

ABSTRACT. Neural network controllers for autonomous decision-making are well-established in cyber-physical systems, yet their deployment in safety-critical healthcare settings remains largely unverified. This paper presents a methodology and case study for the formal verification of a neural network controller for antibiotic dosing, motivated by the challenge of systems that must be simultaneously adaptive and provably safe across unbounded time horizons. We construct a simplified yet clinically-interpretable model that tracks drug concentration, body temperature, and white blood cell count. Vancomycin is selected as a representative antibiotic, widely prescribed for severe infections yet carrying a narrow therapeutic window, where supratherapeutic concentrations risk nephrotoxicity and subtherapeutic dosing risks treatment failure. A supervised neural network controller is trained on synthetic clinician-style dosing data. We establish formal verification of input-output safety properties, specifically verifying a property of a neural network that implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary. This system property is proven in Rocq using the Vehicle interactive theorem prover backend to integrate the different proof systems. The end result is a verification pipeline that allows for a wide variety of treatment approaches whilst maintaining safety for each specific patient.

ABSTRACT. We present our ongoing work on the veriFIRE project: a collaboration between industry and academia, aimed at applying verification to increase the reliability of a real-world, safety-critical system. The system we target is an airborne platform for wildfire detection, which incorporates two deep neural networks. We present an end-to-end methodology for verifying consistency properties of this system. Our approach encodes application-grounded requirements into solver-compatible queries for existing neural network verifiers. We study properties of interest over critical operational scenarios: (i) monotonicity of detector confidence as target intensity increases; and (ii) bounded detector response under physically plausible blur over the sensor. We instantiate these encodings using state-of-the-art neural network verification backends and evaluate them at scale on real background samples. For the first property, all verification queries are solved in under five minutes. For the second property, verification is substantially harder, highlighting key scalability challenges for richer, higher-dimensional specifications. Overall, the results demonstrate that meaningful, domain-specific guarantees can be obtained for industrial systems.

ABSTRACT. Translating human-written mathematical theorems and proofs from natural language (NL) into formal languages (FLs) like Lean 4 has long been a significant challenge for AI. Most state-of-the-art methods either focus on theorem-only NL-to-FL auto-formalization or on FL proof synthesis from FL theorems. In practice, auto-formalization of both theorem and proof still requires human intervention, as seen in AlphaProof’s silver-medal performance at the 2024 IMO, where problem statements were manually translated before automated proof synthesis. We present ProofBridge, a unified framework for automatically translating entire NL theorems and proofs into Lean 4. At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem+proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant FL examples to guide translation. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean’s type checker and semantic equivalence feedback to ensure both syntactic correctness and semantic fidelity. Experiments show substantial improvements in proof auto-formalization over strong baselines (including GPT-5, Gemini-2.5, Kimina-Prover, DeepSeek-Prover), with our retrieval-augmented approach yielding significant gains in semantic correctness (SC, via proving bi-directional equivalence) and type correctness (TC, via type-checking theorem+proof) across pass@k metrics on miniF2F-Test-PF, a dataset we curated. In particular, ProofBridge improves cross-modal retrieval quality by up to 3.28x Recall@1 over all-MiniLM-L6-v2, and achieves +31.14% SC and +1.64% TC (pass@32) compared to the baseline Kimina-Prover-RL-1.7B.

ABSTRACT. As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be ensured throughout their entire operation, necessitating infinite-time horizon verification. To verify the infinite-time horizon safety of NNCSs, recent approaches leverage Differential Dynamic Logic (dL). However, these dL-based guarantees rely on idealized, real-valued NN semantics and fail to account for roundoff errors introduced by finite-precision implementations. This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations --- in sensing, actuation, and computation --- into the safety verification. We model the problem as a hybrid game between a good Demon, responsible for control actions, and a bad Angel, introducing perturbations. This formulation enables formal proofs of robustness w.r.t. a given (bounded) perturbation. Leveraging this bound, we employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution. We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.

ABSTRACT. The rise in popularity and deployment of deep neural networks has resulted in an increased demand for trustworthy models, particularly in safety-critical applications. As a result, several solvers that formally verify properties of neural networks have been developed. However, state of the art solvers have combinatorially large configuration spaces. The task of selecting the best configuration for an instance or benchmark is non-trivial. Furthermore, current methods for algorithm selection and algorithm configuration are insufficient for large configuration spaces. We present REGENT, an automated selection tool for verification of neural network (VNN) solver configurations via Large Language Model (LLM) prompting. Our zero-shot selection method is a three stage LLM inference tool that takes as input a feature description of a VNN instance and outputs a solver configuration. In case of failure, feedback from the solver is passed back to the LLM, after which a new configuration is queried. Our reinforcement learning with optimization feedback (RLOF) method fine-tunes LLMs to output configurations that cause VNN solvers to improve on an optimization objective. We perform extensive empirical evaluations that show that the configurations selected by REGENT achieve comparable performance to hand-tuned configurations on a large set of competition grade test instances. When applying our fine-tuning approach, we show that LLMs can configure solvers to prove tighter bounds than those proven using hand-tuned configurations on up to 58% of the most challenging test instances. REGENT allows non-expert users of VNN solvers to automatically generate significantly better configurations, and therefore can save several human hours involved in hyperparameter-tuning.

ABSTRACT. Sound program analysis promises to catch every instance of particular kinds of bugs in a program. In practice, though, it has never been able to fulfill that promise in a practical way, and despite some limited success in the form of bug finding tools used at large companies, it has never become part of the standard toolkit used by programmers. In this talk, I will argue that AI is about to change that. On the one hand, Language Models enable new forms of sound program analysis that get around many of the limitations of traditional program analysis tools. On the other hand, they also make the use of program analysis essential as coding tools enable attackers to turn a vulnerability into an exploit with the push of a button. The contents of this talk will be based on the work in collaboration with my student Michael Wang.

ABSTRACT. Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of $\omega$-regular properties (and therefore linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for $\omega$-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an $\omega$-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.

ABSTRACT. Neural networks (NN) are often represented using the Open Neural Network Exchange (ONNX) format that provides a rich set of operators. This richness implies that many tools support only a subset of ONNX operators and, consequently, a subset of NNs. However, some of these operators can be expressed equivalently as combinations of simpler, already supported, operators. In this work, we present an extension of CAISAR---a platform for verification of NN that uses external solvers---that automatically transforms these redundant operators into simpler ones before calling existing solvers, thus extending the range of these solvers. This work focuses on the argmax operator, proposing a transformation, proving its correctness, and presenting experimental results.

ABSTRACT. Safety analysis of neural-network controllers for cyber-physical systems requires combining closed-loop dynamical reasoning with formal neural-network verification. Standard invariant-based workflows typically compute the maximal controlled-invariant set before controller checking, although a violating execution may be detectable for an invariant inner-approximation. This paper proposes an incremental workflow for checking controller safe-set preservation. Starting from an initial inner-approximation, the method interleaves invariant refinement with verification, reuses proof results, checks only the newly added region between successive iterates, and supports early termination with a counterexample. If no violation is found, the verified domain grows progressively with each refinement step. Case studies on adaptive-cruise and lane-keeping neural controllers show that interleaving reduces time to counterexample in unsafe cases, lowers runtime in safe cases, and proof reuse becomes more beneficial as verification cost increases.

ABSTRACT. Markov Decision Processes (MDPs) are a powerful modeling paradigm for sequential decision-making problems, e.g., robot navigation and game playing. Decades of research have produced highly efficient algorithms for solving MDPs. A common limitation, however, is that the solutions (policies) are typically represented as large lookup tables that map agents' actions to thousands or even millions of states. In this work, we present a fast approach to optimizing (fixed-size) decision tree policies for MDPs, which are easier for human experts to analyze and for specialized tools to verify. Previous work tackled this problem using computationally intensive techniques, such as integer programming or abstraction refinement. While our method, Lipa, which combines branch-and-bound with smart heuristics, can often find high-quality policies orders of magnitude faster and prove optimality where previous methods fail. We evaluate Lipa on 21 discounted-return and model-checking benchmark MDPs of varying sizes and demonstrate consistent, significant improvement over the state of the art.

ABSTRACT. Counterfactual explanations (CEs) provide a simple, yet powerful interpretive approach to understanding neural network behavior, envisioning hypothetical scenarios by systematically altering input features and analyzing the resulting changes in model predictions. However, CEs are useful only if they are robust, i.e., they remain consistent and meaningful even when adversarially perturbed. While prior work has explored the development of generators for robust CEs, checking the robustness of CEs produced for DNNs has not been explored within the verification context, nor has it been studied under adversarial training. We present a systematic study utilizing adversarial training to fortify the underlying neural network, observing its effect on the formal robustness of DNNs with respect to CEs using α, β-CROWN, a state-of-the-art NNV. Our experiments across multiple datasets, network architectures, and CE generators indicate that adversarial training has a positive impact on the number of formally verified robust CEs. We also measure the impact of adversarial training on other desirable properties of CEs, such as plausibility and proximity. While plausibility does not change, there is a trade-off with proximity when using a gradient-based CE generator.