Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems

I. Samuel Akinwande; Mykel J. Kochenderfer; Clark Barrett

cs.AISep 14, 2026

Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems

Authors: I. Samuel Akinwande, Mykel J. Kochenderfer, Clark Barrett

Organizations: Department of Aeronautics and Astronautics, Stanford University Stanford, CA, 94305, USA · Department of Computer Science, Stanford University Stanford, CA, 94305, USA

Abstract

Despite recent advances in the verification of nonlinear neural feedback systems, scalability remains the central obstacle, as state-of-the-art solvers do not yet handle the network sizes and nonlinear dynamics of autonomy applications. Combinatorial solvers do not scale to large networks, whereas propagative solvers excessively sacrifice precision. This work seeks to improve the scalability of combinatorial solvers by formulating verification as branch-and-bound on an abstraction of the closed-loop system. We introduce \rail, an interface that exposes polyhedral enclosures of the dynamics to LiRPA-style bound propagation, and \clipper, a branch-and-bound algorithm that jointly refines enclosures and splits controller activations. This framework enables joint reasoning on the computational graph of the closed-loop system, preserving symbolic correlations across time steps. We present our construction and show that it yields significant improvements over the state of the art.

Figures & tables

Panel of Figure 1 — Figure 1: Anatomy of one time step in the neural feedback graph $\mathcal{G}^{\mathcal{D}}_{T}$ . The state $\mathbf{x}_{t}$ feeds the controller $\pi_{(t)}$ (top) and dynamics $F^{(t)}$ (bottom), which are composed with an affine combiner with disturbance $\mathbf{\epsilon}_{t}$ to produce $\mathbf{x}_{t+1}$ . Each nonlinear node admits a sound linear relaxation (LiRPA at activations, bart at rail enclosure nodes) and a corresponding split or refinement action (neuron splits at activations, rer refinement at rail nodes). Callouts illustrate the relaxations (left column) and the actions (right column).

Benchmark	$n$	$T$	clipper ( $\bigstar$ )	OvertPoly	OVERTVerify	immrax	CROWN-Reach	CORA
\csvreader [late after line=
\csvcolix

Table 1: Verification results on ARCH-COMP 2025 AINNCS benchmarks supported by clipper . Instances are defined in Appendix C.1 .

n

is the state dimension,

T

the horizon. Cells report wall-clock seconds to certify,

\times

denotes an inconclusive result (error or too imprecise), U an unsupported instance, and an (F) prefix a specification that does not hold, whose row instead reports set-computation time. Per instance the fastest tool is bold and the tightest (smallest terminal volume) underlined .

\bigstar

marks our method.

Panel of Figure 2 — Figure 2: Cactus plots over the 12 AINNCS instances. An instance is solved when a tool produces its reachable-set result (a certification, or a set computation on falsifiable instances), and each tool’s solved instances are sorted by the plotted quantity. A point $(x,y)$ means $x$ instances were solved within $y$ , so lower and farther right is better. Left: per-instance time. Right: terminal reachable-set volume (tightness).

	bart ( $\bigstar$ )	bart $+$ OVERT	bart $+$ CROWN
\csvreader [late after line=
\csvcoliv

Table 2: Relaxation ablation on Unicycle at

t^{\ast}=15

. Volume is the reachable-set volume at

t^{\ast}

; Time is the wall-clock time to compute and optimize the relaxation.

	Enclosure refinement ( $\bigstar$ )		Input splitting
Benchmark	Time	Volume	Time	Volume
\csvreader [late after line=
\csvcolv

Table 3: Branching ablation on a benchmark subset. Time is wall-clock seconds and Volume the terminal reachable-set volume.

\bigstar

marks our method.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Cells in the state space	$10{,}000$
Unsafe by simulation	$3463$
Proven safe, $1$ -step	$0$
Proven safe, $2$ -step	$384$
Proven safe, $3$ -step	$2669$
Inconclusive after $3$ -step	$3868$
Settled by the kinematic lemma	1105

Appendix

Table 4: The

20

Hz convolutional configuration of Cai, Fan, and Bak (2025) and the part of its inconclusive band clipper resolves. Counts are cells of their

100\times 100

grid, and their reported cost for this configuration is

374

GPU-hours normalized to a single machine. The three routes overlap, so the rows attributing cells to them need not sum to the total resolved.

Neural Network Verification

Neural network verification develops methods to prove whether networks satisfy properties such as robustness, safety, and bounded output behavior.

See all 122 papers

The FABRIC Strategy for Verifying Neural Feedback Systems
Mar 9, 2026Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer +1Reachability Analysis Neural Network Verification
Department of Aeronautics and Astronautics, Stanford University, Stanford, USA · Department of Computer Science, Stanford University, Stanford, USA
Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial
May 26, 2026Haoyu Li, Xiangru Zhong, Hao Cheng +2Neural Network Verification
Department of Computer Science · Department of Electrical and Computer Engineering, University of Illinois Urbana-Champaign, Urbana, IL 61801, USA
Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
May 8, 2026Jun Zhang, Haibo Zhang, Chun Liu +2Neural Network Verification Control Barrier Functions
School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China · Beijing Institute of Control Engineering, Beijing, China · School of Mechatronic Engineering and Automation, Shanghai2026 University, Shanghai, China +1

Mar 9, 2026J/K move · Enter open · S save

The FABRIC Strategy for Verifying Neural Feedback Systems

Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer, Clark Barrett

Department of Aeronautics and Astronautics, Stanford University, Stanford, USA · Department of Computer Science, Stanford University, Stanford, USA

Reachability Analysis Neural Network Verification Feedback Control

Open paper AskPDF arXiv

Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been proposed and studied. In contrast, far less attention has been given to backward reachability analysis for these systems, in part because of the limited scalability of known techniques. In this work, we begin to address this gap by introducing new algorithms for computing both over- and underapproximations of backward reachable sets for nonlinear neural feedback systems. We also describe and implement an integration of these backward reachability techniques with existing ones for forward analysis. We call the resulting algorithm Forward and Backward Reachability Integration for Certification (FaBRIC). We evaluate our algorithms on a representative set of benchmarks and show that they significantly outperform the prior state of the art.

Abstract

Neural Network Verification

Explore similar work

The FABRIC Strategy for Verifying Neural Feedback Systems

Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations