# Provably-Safe Neural Network Training Using Hybrid Zonotope Reachability Analysis

arXiv: https://arxiv.org/abs/2501.13023 · HTML: https://mlsanity.com/paper/2501.13023/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 61 references that are in the map.
- First posted on arXiv 22 Jan 2025.

## Builds on (most cited first, 30 of 35)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learning](https://mlsanity.com/paper/2108.06266/) (2021)
- [A Review of Safe Reinforcement Learning: Methods, Theory and Applications](https://mlsanity.com/paper/2205.10330/) (2022)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Interior Point Solving for LP-based prediction+optimisation](https://mlsanity.com/paper/2010.13943/) (2020)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Constrained Decision Transformer for Offline Safe Reinforcement Learning](https://mlsanity.com/paper/2302.07351/) (2023)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [ISAACS: Iterative Soft Adversarial Actor-Critic for Safety](https://mlsanity.com/paper/2212.03228/) (2022)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [POLICE: Provably Optimal Linear Constraint Enforcement for Deep Neural Networks](https://mlsanity.com/paper/2211.01340/) (2022)
- [ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks](https://mlsanity.com/paper/1907.10662/) (2019)
- [Hybrid zonotopes: a new set representation for reachability analysis of mixed logical dynamical systems](https://mlsanity.com/paper/2106.14831/) (2021)
- [Safety Verification of Neural Feedback Systems Based on Constrained Zonotopes](https://mlsanity.com/paper/2204.00903/) (2022)
- [Constrained Feedforward Neural Network Training via Reachability Analysis](https://mlsanity.com/paper/2107.07696/) (2021)
- [Reachability Analysis and Safety Verification of Neural Feedback Systems via Hybrid Zonotopes](https://mlsanity.com/paper/2210.03244/) (2022)
- [POLICEd RL: Learning Closed-Loop Robot Control Policies with Provable Satisfaction of Hard Constraints](https://mlsanity.com/paper/2403.13297/) (2024)
- [Backward Reachability Analysis of Neural Feedback Systems Using Hybrid Zonotopes](https://mlsanity.com/paper/2303.10513/) (2023)
- [Hybrid Zonotopes Exactly Represent ReLU Neural Networks](https://mlsanity.com/paper/2304.02755/) (2023)
- [Goal-Reaching Trajectory Design Near Danger with Piecewise Affine Reach-avoid Computation](https://mlsanity.com/paper/2402.15604/) (2024)
- [Guaranteed Reach-Avoid for Black-Box Systems through Narrow Gaps via Neural Network Reachability](https://mlsanity.com/paper/2409.13195/) (2024)
- [Enhancing Safety and Robustness of Vision-Based Controllers via Reachability Analysis](https://mlsanity.com/paper/2410.21736/) (2024)
- [Scalable Zonotopic Under-approximation of Backward Reachable Sets for Uncertain Linear Systems](https://mlsanity.com/paper/2107.01724/) (2021)
- [Hybrid Zonotope-Based Backward Reachability Analysis for Neural Feedback Systems With Nonlinear Plant Models](https://mlsanity.com/paper/2310.06921/) (2023)

## Built on by (most cited first, 3 of 3)

- [DisjunctiveNet: Neural Symbolic Learning via Differentiable Convexified Optimization Layers](https://mlsanity.com/paper/2605.30456/) (2026)
- [ShardNet: Training Neural Controllers with Hard, Non-Convex Constraints](https://mlsanity.com/paper/2606.30935/) (2026)
- [Matrix Zonotopic Attention: A Context-Adaptive Value Projection for Set Transformers](https://mlsanity.com/paper/2608.05472/) (2026)

## Abstract (arXiv)

Even though neural networks are being increasingly deployed in safety-critical control applications, it remains difficult to enforce constraints on their output, meaning that it is hard to guarantee safety in such settings. While many existing methods seek to verify a neural network's satisfaction of safety constraints, few address how to correct an unsafe network. The handful of works that extract a training signal from verification cannot handle non-convex sets, and are either conservative or slow. To begin addressing these challenges, this work proposes a neural network training method that can encourage the exact image of a non-convex input set for a neural network with rectified linear unit (ReLU) nonlinearities to avoid a non-convex unsafe region. This is accomplished by reachability analysis with scaled hybrid zonotopes, a modification of the existing hybrid zonotope set representation that enables parameterized scaling of non-convex polytopic sets with a differentiable collision check via mixed-integer linear programs (MILPs). The proposed method was shown to be effective and fast for networks with up to 240 neurons, with the computational complexity dominated by inverse operations on matrices that scale linearly in size with the number of neurons and complexity of input and unsafe sets. We demonstrate the practicality of our method by training a forward-invariant neural network controller for an affine dynamical system with a non-convex input set, as well as generating safe reach-avoid plans for a black-box dynamical system.