The FABRIC Strategy for Verifying Neural Feedback Systems

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

cs.AIMar 9, 2026

The FABRIC Strategy for Verifying Neural Feedback Systems

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

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

Abstract

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.

Figures & tables

	HyBReach-MILP		DRiPy (★)		DRiPy (★ $\ddagger$ )		Improvement
	Time (s)	Vol.	Time (s)	Vol.	Time (s)	Vol.	Time ( $\downarrow$ )	Vol. ( $\downarrow$ )
Tora (sma.)	$\mathbf{1.14}$	$1.44\textsc{E-01}$	$1.63$	$1.67\textsc{E-01}$	$5.17$	$\mathbf{4.16\textsc{E-02}}$	$-1.43$	$-1.16$
Tora (med.)	$\mathbf{1.14}$	$1.39\textsc{E-01}$	$2.63$	$1.57\textsc{E-01}$	$5.20$	$\mathbf{4.11\textsc{E-02}}$	$-2.22$	$-1.13$
Tora (larg.)	$\mathbf{1.40}$	$1.44\textsc{E-01}$	$2.53$	$1.66\textsc{E-01}$	$6.68$	$\mathbf{4.16\textsc{E-02}}$	$-1.81$	$-1.15$
Unicycle (sma.)	$5501.0$	$1.84\textsc{E+03}$	$\mathbf{60.59}$	$1.51\textsc{E+02}$	$1897.94$	$\mathbf{4.00}\textsc{E+01}$	$90.79$	$12.23$
Unicycle (med.)	$4980.90$	$1.70\textsc{E+03}$	$\mathbf{55.04}$	$1.51\textsc{E+02}$	$124.913$	$\mathbf{4.20}\textsc{E+01}$	$90.50$	$11.30$

Table 1: Benchmark computation time (s) and set volumes. ★ denotes our polyhedral-enclosure based algorithm to solve Eq. 8 , and

\ddagger

denotes our algorithm combined with the modified refinement scheme. Improvement is calculated as the time and volume fraction between HyBReach-MILP and a configuration of DRiPy without domain refinement.

	BURNS		SHARP (★)		CRISP (★)		CLEAN (★)
	Time (s)	Vol.	Time (s)	Vol.	Time (s)	Vol.	Time (s)	Vol.
Tora (sma.)	$32.59$	$\mathbf{6.35\textsc{E-04}}$	$\mathbf{6.62}$	$1.85$ E-05	$8.52$	$3.82\textsc{E-04}$	$6.82$	$2.41\textsc{E-06}$
Tora (med.)	$32.59$	$\mathbf{6.35}\textsc{E-04}$	$\mathbf{6.72}$	$1.85$ E-05	$8.83$	$3.82\textsc{E-04}$	$6.79$	$2.40\textsc{E-06}$
Tora (lar.)	$65.92$	$\mathbf{4.70}\textsc{E-04}$	$10.83$	$7.66$ E-05	$14.15$	$3.84\textsc{E-04}$	$\mathbf{10.32}$	$2.35\textsc{E-06}$
Unicycle (sma.)	$606.11$	$-$	$157.92$	$5.88$ E-03	$136.52$	$\mathbf{1.94}\textsc{E-02}$	$\mathbf{50.18}$	$1.67\textsc{E-02}$
Unicycle (med.)	$1524.04$	$-$	$126.33$	$5.89\textsc{E-03}$	$116.70$	$\mathbf{3.43}\textsc{E-02}$	$\mathbf{36.41}$	$1.47\textsc{E-02}$

Table 2: Benchmark computation time (s) and set volumes. ★ denotes our polyhedral-enclosure based FITS algorithm to solve Eq. 9 ,

-

denotes instances where the procedure runs but fails to return a set with nonzero volume, and

\times

denotes a failure for any other reason

	Forward analysis	FaBRIC (★)		Improvement
		Reach	Avoid	Reach ( $\downarrow$ )	Avoid ( $\downarrow$ )
Tora (Small)	$1.99$	$10.87$	$6.41$	$-5.46$	$-3.22$
Tora (Med)	$2.21$	$10.09$	$6.61$	$-4.57$	$-2.99$
Tora (Large)	$3.29$	$16.70$	$8.92$	$-5.08$	$-2.71$
Unicycle (Small)	$1302.98$	$280.51$	$292.02$	$4.65$	$4.46$
Unicycle (Medium)	$1157.98$	$261.27$	$260.15$	$4.43$	$4.45$

Table 3: Comparison of FaBRIC and Forward-only analysis with measured improvements

Reachability Analysis

Reachability analysis determines which states a system can enter from given initial conditions, actions, and disturbances.

See all 76 papers

Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems
Sep 14, 2026I. Samuel Akinwande, Mykel J. Kochenderfer, Clark BarrettNeural Network Verification Branch and Bound
Department of Aeronautics and Astronautics, Stanford University Stanford, CA, 94305, USA · Department of Computer Science, Stanford University Stanford, CA, 94305, USA
Quadratic Characterizations for Reachability Analysis of Neural Networks
May 19, 2026Elias Khalife, Mazen Farhood, Pierre-Loic GarocheNeural Network Verification Reachability Analysis
Kevin T. Crofton Department of Aerospace and Ocean Engineering, Virginia Tech, Blacksburg, VA 24061, USA · Federation ENAC ISAE-SUPAERO ONERA, Universite de Toulouse, Toulouse, France
Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification
May 11, 2026Taha Entesari, Mahyar FazlyabNeural Network Verification Neural Network Robustness
Johns Hopkins University

Sep 14, 2026J/K move · Enter open · S save

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

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

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

Neural Network Verification Branch and Bound Feedback Control

Open paper AskPDF arXiv

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.

Abstract

Reachability Analysis

Explore similar work

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

Quadratic Characterizations for Reachability Analysis of Neural Networks

Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification