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

# Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems
Source: [https://arxiv.org/html/2609.16298](https://arxiv.org/html/2609.16298)
###### 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 introducerail, an interface that exposes polyhedral enclosures of the dynamics to LiRPA\-style bound propagation, andclipper, 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\.

1Department of Aeronautics and Astronautics, Stanford University

2Department of Computer Science, Stanford University

Stanford, CA, 94305, USA

samakin@stanford\.edu, mykel@stanford\.edu, barrett@cs\.stanford\.edu

## Introduction

Autonomy is increasingly integral to modern engineered systems, many of which are dynamical systems operating in a closed loop with neural network controllers\. Such*neural feedback systems*\(NFS\) are prevalent in safety\-critical domains including aerial navigation\([Kaufmann et al\. 2023](https://arxiv.org/html/2609.16298#bib.bib11)\), autonomous vehicles\([Ettinger et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib7)\), and legged robotics\([Rodriguez et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib15)\), motivating principled approaches to safety verification\. The complex interactions between the system dynamics and the neural controller make safety verification challenging, and this challenge is heightened when the dynamics are nonlinear\. In this work, we develop techniques that apply to both linear and nonlinear dynamics, but our exposition focuses on nonlinear dynamics as the harder and more relevant setting\.

Current approaches to NFS verification fall broadly into*propagative*and*combinatorial*families\([Akinwande et al\. 2026a](https://arxiv.org/html/2609.16298#bib.bib1)\)\. Propagative solvers represent nonlinear dynamics using control\-native abstractions such as Taylor models\([Dutta, Chen, and Sankaranarayanan 2019](https://arxiv.org/html/2609.16298#bib.bib6);[Huang et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib10)\), Bernstein polynomials\([Fan et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib8)\), polynomial zonotopes\([Kochdumper et al\. 2023](https://arxiv.org/html/2609.16298#bib.bib12)\), and inclusion functions\([Harapanahalli, Jafarpour, and Coogan 2024](https://arxiv.org/html/2609.16298#bib.bib9)\)\. Monolithic variants such as CORA\([Kochdumper et al\. 2023](https://arxiv.org/html/2609.16298#bib.bib12)\), ReachNN\([Fan et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib8)\), and POLAR\([Huang et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib10)\)encode the neural network directly in these abstractions, enabling joint reasoning but limiting neural\-network analysis to control\-native machinery\. Compositional variants such as immrax\([Harapanahalli, Jafarpour, and Coogan 2024](https://arxiv.org/html/2609.16298#bib.bib9)\)and CROWN\-Reach\([Manzanas Lopez et al\. 2024](https://arxiv.org/html/2609.16298#bib.bib13);[Verified\-Intelligence 2024](https://arxiv.org/html/2609.16298#bib.bib18)\)analyze the network and the dynamics separately, gaining scalability on the network but requiring reasoning across distinct abstractions\. Combinatorial solvers \(OVERTVerify\([Sidrane et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib17)\), OvertPoly\([Akinwande et al\. 2026a](https://arxiv.org/html/2609.16298#bib.bib1)\)\) encode both the dynamics and the network as mixed\-integer linear programs \(MILPs\), enabling joint reasoning over a shared abstraction\. Like the monolithic propagative tools, they trade scalability for structural uniformity, though here the shared abstraction is network\-native rather than control\-native\. MILP encodings do not scale to large networks, and requiring exact MILP\-encodable activations restricts the class of admissible controllers\.

Open\-loop neural\-network verification \(certifying the network in isolation rather than in closed loop with the system dynamics\) faces neither barrier, as state\-of\-the\-art verifiers combine linear bound propagation \(LiRPA\)\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\), often derived from dual LP formulations\([De Palma et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib5)\), with branch\-and\-bound \(BaB\) over activation\-pattern prefixes\([Bunel et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib3);[Xu et al\. 2020b](https://arxiv.org/html/2609.16298#bib.bib21)\)\. Bounds are computed in parallel on GPUs, scaling to large networks\. This combination closely mirrors MILP solver strategies and suggests compatibility with the abstractions used by combinatorial NFS solvers\.

The key research question in this work is whether open\- and closed\-loop verification can be unified in a single, scalable framework\. We answer affirmatively, with three contributions:\(i\)\(i\)rail, aunified graph interface, exposes polyhedral enclosures of the dynamics to LiRPA, enabling joint reasoning over system dynamics and network activations;\(i​i\)\(ii\)clipper, astructure\-aware branch\-and\-boundalgorithm, jointly refines these enclosures and splits controller activations, with branching heuristics that exploit the structure of both the dynamics and the network while leveraging GPU parallelism; and\(i​i​i\)\(iii\)an implementation for verifying reach\-avoid specifications for nonlinear NFS atcompetitive precision using GPU\-accelerated BaByields significant improvements over the state of the art\.

## Background

#### Notation and Definitions

For a set𝐗\\mathbf\{X\},2𝐗2^\{\\mathbf\{X\}\}denotes its power set\. For integersi≤ji\\leq j,\[i\.\.j\]≔\{z∣i≤z≤j\}\[i\.\.j\]\\coloneqq\\\{z\\mid i\\leq z\\leq j\\\}, and\[n\]≔\[1\.\.n\]\[n\]\\coloneqq\[1\.\.n\]\. IfS=\(s1,…,sn\)S=\(s\_\{1\},\\ldots,s\_\{n\}\)is a finite sequence, thenSiS\_\{i\}denotes itsii\-th element\. We useconvto denote the convex hull operator,ℕ\\mathbb\{N\}the nonnegative integers, andℝ\\mathbb\{R\}the real numbers\. For𝐯,𝐰∈ℝn\\mathbf\{v\},\\mathbf\{w\}\\in\\mathbb\{R\}^\{n\}, we write𝐯⪯𝐰\\mathbf\{v\}\\preceq\\mathbf\{w\}to denote𝐯i≤𝐰i\\mathbf\{v\}\_\{i\}\\leq\\mathbf\{w\}\_\{i\}for everyi∈\[n\]i\\in\[n\]\. For a functionf:X→Yf:X\\to Yand a subsetS⊆XS\\subseteq X, we writef\|Sf\|\_\{S\}for the restriction offftoSS\. If a set is used where a point is expected, the function is applied to each element and the resulting sets are unioned\. We use several geometric terms informally and provide formal definitions in Appendix[A\.1](https://arxiv.org/html/2609.16298#A1.SS1)\.

### Neural Feedback Systems

A neural feedback system is a discrete\-time dynamical system governed by a neural network controller\. Its trajectories are assessed against a goal set𝐆\\mathbf\{G\}and unsafe states𝐀\\mathbf\{A\}\. Formally, the tuple⟨m,n,𝐈,𝐅,𝐄,𝐮,B,δ,T,𝐆,𝐀⟩\\langle m,n,\\mathbf\{I\},\\mathbf\{F\},\\mathbf\{E\},\\mathbf\{u\},B,\\delta,T,\\mathbf\{G\},\\mathbf\{A\}\\rangledefines a neural feedback system𝒟\\mathcal\{D\}, wherem,n∈ℕm,n\\in\\mathbb\{N\}are the controller\-output \(𝐮⁡\(𝐱\)∈ℝm\\mathbf\{u\}\(\\mathbf\{x\}\)\\in\\mathbb\{R\}^\{m\}\) and state dimensions \(𝐱∈ℝn\\mathbf\{x\}\\in\\mathbb\{R\}^\{n\}\),𝐈⊆ℝn\\mathbf\{I\}\\subseteq\\mathbb\{R\}^\{n\}the initial states,𝐅=\(f1,…,fn\)\\mathbf\{F\}=\(f\_\{1\},\\ldots,f\_\{n\}\)a vector field withfi:ℝn→ℝf\_\{i\}:\\mathbb\{R\}^\{n\}\\to\\mathbb\{R\},𝐄⊆ℝn\\mathbf\{E\}\\subseteq\\mathbb\{R\}^\{n\}admissible perturbations,𝐮:ℝn→ℝm\\mathbf\{u\}:\\mathbb\{R\}^\{n\}\\to\\mathbb\{R\}^\{m\}a neural network controller,B∈ℝn×mB\\in\\mathbb\{R\}^\{n\\times m\}a controller\-input matrix,δ∈ℝ\\delta\\in\\mathbb\{R\}the time step,T∈ℕT\\in\\mathbb\{N\}the time horizon,𝐆⊆ℝn\\mathbf\{G\}\\subseteq\\mathbb\{R\}^\{n\}the goal set, and𝐀:\[0\.\.T\]→2ℝn\\mathbf\{A\}:\[0\.\.T\]\\to 2^\{\\mathbb\{R\}^\{n\}\}unsafe states at each step\.

The system evolves overTTdiscrete time steps, with total time horizonT⋅δT\\cdot\\delta\. The next\-state function𝑛𝑒𝑥𝑡𝒟:ℝn→2ℝn\\mathit\{next\}^\{\\mathcal\{D\}\}:\\mathbb\{R\}^\{n\}\\to 2^\{\\mathbb\{R\}^\{n\}\}is defined by

𝑛𝑒𝑥𝑡𝒟​\(𝐱\)\\displaystyle\\mathit\{next\}^\{\\mathcal\{D\}\}\(\\mathbf\{x\}\)≔\{𝐱\+\(𝐅⁡\(𝐱\)\+B​𝐮​\(𝐱\)\+ϵ\)​δ∣ϵ∈𝐄\}\.\\displaystyle\\coloneqq\\\{\\mathbf\{x\}\+\(\\mathbf\{F\}\(\\mathbf\{x\}\)\+B\\mathbf\{u\}\(\\mathbf\{x\}\)\+\\mathbf\{\\epsilon\}\)\\,\\delta\\mid\\mathbf\{\\epsilon\}\\in\\mathbf\{E\}\\\}\.\(1\)
For𝐗0⊆𝐈\\mathbf\{X\}\_\{0\}\\subseteq\\mathbf\{I\}, the trajectoryτ𝒟​\(𝐗0\)≔\(𝐗0,…,𝐗T\)\\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\mathbf\{X\}\_\{0\}\)\\coloneqq\(\\mathbf\{X\}\_\{0\},\\ldots,\\mathbf\{X\}\_\{T\}\)is a sequence of state sets, where𝐗t≔𝑛𝑒𝑥𝑡𝒟​\(𝐗t−1\)\\mathbf\{X\}\_\{t\}\\coloneqq\\mathit\{next\}^\{\\mathcal\{D\}\}\(\\mathbf\{X\}\_\{t\-1\}\)fort∈\[T\]t\\in\[T\]\. The system𝒟\\mathcal\{D\}is*safe*if

∀𝐱∈𝐈\.∃t∈\[0\.\.T\]\.τ𝒟\(\{𝐱\}\)t⊆𝐆\\displaystyle\\forall\\mathbf\{x\}\\in\\mathbf\{I\}\.\\ \\exists t\\in\[0\.\.T\]\.\\ \\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\\{\\mathbf\{x\}\\\}\)\_\{t\}\\subseteq\\mathbf\{G\}\(2\)∀t∈\[0\.\.T\]\.τ𝒟\(𝐈\)t∩𝐀\(t\)=∅\\displaystyle\\forall t\\in\[0\.\.T\]\.\\ \\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\mathbf\{I\}\)\_\{t\}\\cap\\mathbf\{A\}\(t\)=\\emptyset\(3\)Equation \([2](https://arxiv.org/html/2609.16298#Sx2.E2)\) is the reach property, requiring all trajectories to reach𝐆\\mathbf\{G\}, while \([3](https://arxiv.org/html/2609.16298#Sx2.E3)\) is the avoid property, requiring all trajectories to avoid unsafe states at eachtt\.

### Polyhedral Enclosures

Polyhedral enclosures are a combinatorial abstraction for nonlinear NFS verification\([Akinwande et al\. 2026a](https://arxiv.org/html/2609.16298#bib.bib1);[Akinwande et al\. 2026b](https://arxiv.org/html/2609.16298#bib.bib2)\), underpinning state\-of\-the\-art combinatorial solvers\. A bounding set is a tupleB=⟨n,P,L,U⟩B=\\langle n,P,L,U\\rangle, whereP⊆ℝnP\\subseteq\\mathbb\{R\}^\{n\}is a grid andL,U:P→ℝL,U:P\\to\\mathbb\{R\}are lower and upper bounding functions\. Component names follow the bounding set’s decoration, so the grid ofBjB^\{j\}isPjP\_\{j\}\. Given a Delaunay triangulationΔ\\DeltaofPP\(see Appendix[B\.1](https://arxiv.org/html/2609.16298#A2.SS1)\), we obtain a collection of\(n\+1\)\(n\+1\)\-dimensional polytopes by lifting eachnn\-simplex’sn\+1n\+1verticesp→\\vec\{p\}to the pairs\(p→,L⁡\(p→\)\)\(\\vec\{p\},L\(\\vec\{p\}\)\)and\(p→,U⁡\(p→\)\)\(\\vec\{p\},U\(\\vec\{p\}\)\)and taking their convex hull\. The*polyhedral enclosure*ℰ⁡\(B,Δ\)⊆ℝn×ℝ\\mathcal\{E\}\(B,\\Delta\)\\subseteq\\mathbb\{R\}^\{n\}\\times\\mathbb\{R\}is the union of these per\-simplex polytopes\.

LetD≔conv​\(P\)D\\coloneqq\\textbf\{conv\}\(P\)\. The lower and upper surfaces ofℰ⁡\(B,Δ\)\\mathcal\{E\}\(B,\\Delta\)define functionsLΔ,UΔ:D→ℝL\_\{\\Delta\},U\_\{\\Delta\}:D\\to\\mathbb\{R\}, affine on each simplex ofΔ\\Delta\. We sayBB*encloses*f:D→ℝf:D\\to\\mathbb\{R\}ifLΔ​\(𝐱\)≤f⁡\(𝐱\)≤UΔ​\(𝐱\)L\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq f\(\\mathbf\{x\}\)\\leq U\_\{\\Delta\}\(\\mathbf\{x\}\)for all𝐱∈D\\mathbf\{x\}\\in Dand every Delaunay triangulationΔ\\DeltaofPP\. Formal definitions appear in Appendix[A\.2](https://arxiv.org/html/2609.16298#A1.SS2)\.

### Linear Relaxation\-Based Perturbation Analysis

Linear relaxation\-based perturbation analysis \(LiRPA\)\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\), the basis of state\-of\-the\-art neural network verification, computes linear bounds on network outputs\. Given a neural networkπ:𝒳→ℝo\\pi:\\mathcal\{X\}\\to\\mathbb\{R\}^\{o\}and𝐗⊆𝒳\\mathbf\{X\}\\subseteq\\mathcal\{X\}, LiRPA produces𝐖¯o,𝐖¯o\\underline\{\\mathbf\{W\}\}\_\{o\},\\overline\{\\mathbf\{W\}\}\_\{o\}and𝐛¯o,𝐛¯o\\underline\{\\mathbf\{b\}\}\_\{o\},\\overline\{\\mathbf\{b\}\}\_\{o\}such that

∀𝐱∈𝐗\.𝐖¯o​𝐱\+𝐛¯o⪯π⁡\(𝐱\)⪯𝐖¯o​𝐱\+𝐛¯o\.\\displaystyle\\forall\\mathbf\{x\}\\in\\mathbf\{X\}\.\\quad\\underline\{\\mathbf\{W\}\}\_\{o\}\\mathbf\{x\}\+\\underline\{\\mathbf\{b\}\}\_\{o\}\\;\\preceq\\;\\pi\(\\mathbf\{x\}\)\\;\\preceq\\;\\overline\{\\mathbf\{W\}\}\_\{o\}\\mathbf\{x\}\+\\overline\{\\mathbf\{b\}\}\_\{o\}\.\(4\)Bounds are computed by composing per\-node linear relaxations, which are exact at affine layers and sound but inexact at nonlinearities \(see[Proposition3](https://arxiv.org/html/2609.16298#Thmproposition3)\)\. Slope parametersα\\alphaat piecewise\-linear activations can be optimized via gradient methods, yielding bounds competitive with LP relaxations \(α\\alpha\-CROWN\) while retaining efficient GPU implementation\. When𝐗\\mathbf\{X\}is anℓp\\ell\_\{p\}\-norm ball, the linear bounds concretize to scalar bounds via Hölder’s inequality without explicit optimization over𝐗\\mathbf\{X\}\. Formal definitions appear in Appendix[A\.3](https://arxiv.org/html/2609.16298#A1.SS3)\.

### Branch and Bound for Neural Network Verification

LiRPA bounds are sound but may be too loose to certify a property on their own, leaving verification incomplete\. State\-of\-the\-art verifiers recover completeness by combining LiRPA with branch\-and\-bound \(BaB\)\([Xu et al\. 2020b](https://arxiv.org/html/2609.16298#bib.bib21)\)\. BaB first partitions the verification problem into subproblems by splitting the input set𝐗\\mathbf\{X\}or fixing the activation pattern of an unstable neuron \(one whose pre\-activation can be positive or negative over𝐗\\mathbf\{X\}\), then computes LiRPA bounds on each, and finally, either certifies the property once every subproblem is verified, or refutes it once a subproblem yields a counterexample\. Bound propagation parallelizes across subproblems, enabling efficient GPU\-based implementations\. Naïve neuron splits may not tighten LiRPA bounds directly, since LiRPA bounds each neuron independently and cannot propagate split constraints\.β\\beta\-CROWN\([Wang et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib19)\)addresses this by incorporating split constraints into bound propagation via Lagrangian relaxation, with multipliersβ≥0\\beta\\geq 0jointly optimized alongsideα\\alpha\. The split dimension or neuron is selected by a*branching heuristic*\. A detailed treatment appears in Appendix[A\.4](https://arxiv.org/html/2609.16298#A1.SS4)\.

## The CLIPPER Algorithm

This section developsclipperin four stages\. We first introduce an algorithm calledbartfor constructing*relaxed bounding sets*, affine enclosures that bound a polyhedral enclosure over its hyperrectangular domain while leaving slope parameters free\. We then define*recursive enclosure refinement*\(rer\), which tightens these bounds by subdividing cells\.clipperis then a branch\-and\-bound procedure over graphs, whose nodes are either neurons in a neural network or polyhedral enclosures constructed using thererandbartalgorithms\. We call the nodes in this graphrailnodes\.[Figure1](https://arxiv.org/html/2609.16298#Sx3.F1)shows one time step of such a graph\. In what follows, proofs are omitted due to space constraints \(they can be found in Appendix[B\.2](https://arxiv.org/html/2609.16298#A2.SS2)\)\.

𝐱t\\mathbf\{x\}\_\{t\}f^1\\hat\{f\}\_\{1\}f^2\\hat\{f\}\_\{2\}f^3\\hat\{f\}\_\{3\}⊕\\oplusϵt\\epsilon\_\{t\}𝐱t\+1\\mathbf\{x\}\_\{t\+1\}BARTRERLiRPANeuron SplitrefinementsplitFigure 1:Anatomy of one time step in the neural feedback graph𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}\. The state𝐱t\\mathbf\{x\}\_\{t\}feeds the controllerπ\(t\)\\pi\_\{\(t\)\}\(top\) and dynamicsF\(t\)F^\{\(t\)\}\(bottom\), which are composed with an affine combiner with disturbanceϵt\\mathbf\{\\epsilon\}\_\{t\}to produce𝐱t\+1\\mathbf\{x\}\_\{t\+1\}\. Each nonlinear node admits a sound linear relaxation \(LiRPA at activations,bartatrailenclosure nodes\) and a corresponding split or refinement action \(neuron splits at activations,rerrefinement atrailnodes\)\. Callouts illustrate the relaxations \(left column\) and the actions \(right column\)\.### Polyhedral Enclosure Relaxations

Polyhedral enclosures and LiRPA share linear structure but operate over different domains\. Polyhedral enclosures provide piecewise\-affine bounds over simplices, while LiRPA takes linear bounds overℓp\\ell\_\{p\}\-norm balls \(most commonlyℓ∞\\ell\_\{\\infty\}\) and propagates them through neural graphs\. Since hyperrectangles generalizeℓ∞\\ell\_\{\\infty\}balls, unifying the two requires extending polyhedral enclosures from simplices to hyperrectangular domains\.

#### Relaxing Enclosures

We extend polyhedral enclosures to hyperrectangular domains by introducing sound*relaxations*\. We call these relaxationsbart\(Bounding\-setAffineRelaxationTechnique\)\. Consider a bounding setBB\. Recall that any Delaunay triangulationΔ\\DeltaofPPyields an enclosureℰ⁡\(B,Δ\)\\mathcal\{E\}\(B,\\Delta\)whose lower and upper surfaces are piecewise\-affine functions\. Letf:ℝn→ℝf:\\mathbb\{R\}^\{n\}\\to\\mathbb\{R\}be a nonlinear function enclosed byBBso thatLΔ​\(𝐱\)≤f⁡\(𝐱\)≤UΔ​\(𝐱\)L\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq f\(\\mathbf\{x\}\)\\leq U\_\{\\Delta\}\(\\mathbf\{x\}\)\.

###### Definition 1\(Relaxed Bounding Set\)\.

LetBBbe a bounding set, and let𝐚L,𝐚U∈ℝn\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\\in\\mathbb\{R\}^\{n\}\. The*relaxation*ofBBwith parameters\(𝐚L,𝐚U\)\(\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\)is the bounding setB□=⟨n,P□,L□,U□⟩B\_\{\\square\}=\\langle n,P\_\{\\square\},L\_\{\\square\},U\_\{\\square\}\\rangle, whereP□P\_\{\\square\}is the set of2n2^\{n\}corners ofconv​\(P\)\\textbf\{conv\}\(P\),L□​\(𝐩\)=𝐚L⋅𝐩\+bLL\_\{\\square\}\(\\mathbf\{p\}\)=\\mathbf\{a\}\_\{L\}\\cdot\\mathbf\{p\}\+b\_\{L\}andU□​\(𝐩\)=𝐚U⋅𝐩\+bUU\_\{\\square\}\(\\mathbf\{p\}\)=\\mathbf\{a\}\_\{U\}\\cdot\\mathbf\{p\}\+b\_\{U\}withbL=min𝐩∈P⁡\(L⁡\(𝐩\)−𝐚L⋅𝐩\)b\_\{L\}=\\min\_\{\\mathbf\{p\}\\in P\}\(L\(\\mathbf\{p\}\)\-\\mathbf\{a\}\_\{L\}\\cdot\\mathbf\{p\}\), andbU=max𝐩∈P⁡\(U⁡\(𝐩\)−𝐚U⋅𝐩\)b\_\{U\}=\\max\_\{\\mathbf\{p\}\\in P\}\(U\(\\mathbf\{p\}\)\-\\mathbf\{a\}\_\{U\}\\cdot\\mathbf\{p\}\)\. We say a bounding set is*relaxed*if it is the relaxation of some bounding set, and*unrelaxed*otherwise\.

The box labeledbartin Figure 1 shows an example withn=2n=2: the black curve representsff; the purple segments representBB; and the orange lines areL□L\_\{\\square\}andU□U\_\{\\square\}\. We writeL□,U□L\_\{\\square\},U\_\{\\square\}also for the lower and upper surfaces of any enclosure based onB□B\_\{\\square\}: sinceL□L\_\{\\square\}andU□U\_\{\\square\}are affine,L□​\(𝐱\)=𝐚L⋅𝐱\+bLL\_\{\\square\}\(\\mathbf\{x\}\)=\\mathbf\{a\}\_\{L\}\\cdot\\mathbf\{x\}\+b\_\{L\}andU□​\(𝐱\)=𝐚U⋅𝐱\+bUU\_\{\\square\}\(\\mathbf\{x\}\)=\\mathbf\{a\}\_\{U\}\\cdot\\mathbf\{x\}\+b\_\{U\}onconv​\(P□\)=conv​\(P\)\\textbf\{conv\}\(P\_\{\\square\}\)=\\textbf\{conv\}\(P\), they are the same for every enclosureℰ⁡\(B□,Δ\)\\mathcal\{E\}\(B\_\{\\square\},\\Delta\), regardless ofΔ\\Delta\. The following theorem establishes thatB□B\_\{\\square\}enclosesffoverconv​\(P\)\\textbf\{conv\}\(P\)\.

###### Theorem 1\(Soundness of Relaxation\)\.

Ifffis enclosed byBB, then for any𝐚L,𝐚U∈ℝn\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\\in\\mathbb\{R\}^\{n\}, any𝐱∈conv​\(P\)\\mathbf\{x\}\\in\\textbf\{conv\}\(P\), and any Delaunay triangulationΔ\\DeltaofPP,L□​\(𝐱\)≤LΔ​\(𝐱\)≤f⁡\(𝐱\)≤UΔ​\(𝐱\)≤U□​\(𝐱\)L\_\{\\square\}\(\\mathbf\{x\}\)\\leq L\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq f\(\\mathbf\{x\}\)\\leq U\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq U\_\{\\square\}\(\\mathbf\{x\}\)\.

This construction leaves𝐚L\\mathbf\{a\}\_\{L\}and𝐚U\\mathbf\{a\}\_\{U\}as free parameters that can be optimized with respect to an arbitrary objective \(e\.g\., tightness\)\. The optimization is amenable to first\-order methods, analogous toα\\alphaoptimization inα\\alpha\-CROWN\. The relaxation is sound for any𝐚L,𝐚U∈ℝn\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\\in\\mathbb\{R\}^\{n\}, with the tightness objective implicitly bounding the optimal parameters\. As𝐚L\\mathbf\{a\}\_\{L\}varies, the affine boundL□L\_\{\\square\}sweeps the supporting hyperplanes of the convex envelope ofLΔL\_\{\\Delta\}overconv​\(P\)\\textbf\{conv\}\(P\)\. A single relaxation is thus exact only whenLΔL\_\{\\Delta\}is affine and loose otherwise\. Refinement \(next section\) restores tightness by relaxing subregions independently, and is exact on any subregion whereLΔL\_\{\\Delta\}is affine\.

Since relaxed bounding sets are sound \([Theorem1](https://arxiv.org/html/2609.16298#Thmtheorem1)\), they compose under the same rules as unrelaxed enclosures, at substantially reduced encoding cost\.

### Refining Enclosure Relaxations

Thebartrelaxation loosens the tight bounds generated by polyhedral enclosures\. When necessary, a degree of tightness can be recovered by partitioning the domain into subregions on which the relaxation is applied independently\. This forms the foundation for the branch\-and\-bound algorithm we develop later\.

#### Refining Relaxations

Relaxation produces a bounding setB□B\_\{\\square\}whose enclosure is sound but may be excessively loose, particularly when the curvature of the enclosed function changes over the domain, or when the domain is large\. We tighten such enclosures via the*refinement*operation, which subdivides a bounding set into pieces over sub\-hyperrectangles of the domain\. We call this refinement operationrer\(RecursiveEnclosureRefinement\)\. Each piece can be relaxed independently, yielding a piecewise\-affine bound that is no looser than the single relaxation and strictly tighter whenever either piece attains a tighter offset \([Theorem2](https://arxiv.org/html/2609.16298#Thmtheorem2)\)\.

###### Definition 2\(Enclosure Refinement\)\.

LetBBbe a bounding set, and letHHbe a*grid hyperplane*ofPP\(an axis\-aligned hyperplane that splitsPPat an interior grid coordinate, formalized in Appendix[A\.1\.5](https://arxiv.org/html/2609.16298#A1.SS1.SSS5)\)\. LetP1,P2P\_\{1\},P\_\{2\}be the sub\-grids ofPPon the two closed sides ofHH, so thatP1∪P2=PP\_\{1\}\\cup P\_\{2\}=PandP1∩P2=P∩HP\_\{1\}\\cap P\_\{2\}=P\\cap H\. ThenB1:=⟨n,P1,L\|P1,U\|P1⟩B^\{1\}:=\\langle n,P\_\{1\},L\|\_\{P\_\{1\}\},U\|\_\{P\_\{1\}\}\\rangleandB2:=⟨n,P2,L\|P2,U\|P2⟩B^\{2\}:=\\langle n,P\_\{2\},L\|\_\{P\_\{2\}\},U\|\_\{P\_\{2\}\}\\rangleare*refinements*ofBBalongHH\.

Refinement tightens enclosures only when combined with relaxation\. Refining an unrelaxed bounding set preserves the original enclosure exactly, whereas relaxing the refined pieces can produce a tighter enclosure than the single relaxation on regions where it is not exact\.

###### Theorem 2\(Soundness of Refinement\)\.

LetBBbe a bounding set, letHHbe a grid hyperplane ofPP, and letB1,B2B^\{1\},B^\{2\}be the refinements ofBBalongHH\. LetΔ\\Deltabe a Delaunay triangulation ofPP, and let

Δj≔\{𝒮∈Δ∣𝒮⊆conv​\(Pj\)\}for​j∈\{1,2\}\.\\Delta\_\{j\}\\coloneqq\\\{\\mathcal\{S\}\\in\\Delta\\mid\\mathcal\{S\}\\subseteq\\textbf\{conv\}\(P\_\{j\}\)\\\}\\quad\\text\{for \}j\\in\\\{1,2\\\}\.EachΔj\\Delta\_\{j\}is a Delaunay triangulation ofPjP\_\{j\}by the Delaunay splitting lemma \(see Appendix[B\.1\.3](https://arxiv.org/html/2609.16298#A2.SS1.SSS3)\)\. Then:

1. 1\.\(Unrelaxed\.\)ℰ⁡\(B1,Δ1\)∪ℰ⁡\(B2,Δ2\)=ℰ⁡\(B,Δ\)\\mathcal\{E\}\(B^\{1\},\\Delta\_\{1\}\)\\cup\\mathcal\{E\}\(B^\{2\},\\Delta\_\{2\}\)=\\mathcal\{E\}\(B,\\Delta\)\.
2. 2\.\(Relaxed\.\)Let𝐚L,𝐚U∈ℝn\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\\in\\mathbb\{R\}^\{n\}, letB□B\_\{\\square\}andB□jB\_\{\\square\}^\{j\}be the relaxations ofBBandBjB^\{j\}with the same parameters\(𝐚L,𝐚U\)\(\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\), and letbLj,bUjb\_\{L\}^\{j\},b\_\{U\}^\{j\}denote the offsets ofB□jB\_\{\\square\}^\{j\}\. For any Delaunay triangulationsΔ□\\Delta\_\{\\square\}ofP□P\_\{\\square\}andΔ□j\\Delta\_\{\\square\}^\{j\}ofP□jP\_\{\\square\}^\{j\}, ℰ⁡\(B□1,Δ□1\)∪ℰ⁡\(B□2,Δ□2\)⊆ℰ⁡\(B□,Δ□\),\\mathcal\{E\}\(B\_\{\\square\}^\{1\},\\Delta\_\{\\square\}^\{1\}\)\\cup\\mathcal\{E\}\(B\_\{\\square\}^\{2\},\\Delta\_\{\\square\}^\{2\}\)\\subseteq\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\),with strict containment whenever\(bLj,bUj\)≠\(bL,bU\)\(b\_\{L\}^\{j\},b\_\{U\}^\{j\}\)\\neq\(b\_\{L\},b\_\{U\}\)for somej∈\{1,2\}j\\in\\\{1,2\\\}\.

### rail: Composing Enclosures with LiRPA

The bounds \(L□L\_\{\\square\}andU□U\_\{\\square\}\) of a relaxed bounding set are affine, matching LiRPA’s native representation\. A relaxed bounding setB□B\_\{\\square\}can be embedded in a LiRPA computational graph as a node with known linear bounds, and LiRPA’s propagation rules can be used to propagate these bounds through the network\. We call the resulting approachrail\(RelaxedAffineInterface forLiRPA\)\.bartandrerbound the nonlinear dynamics, and LiRPA propagates the bounds\.

### Neural Feedback Graphs

A neural feedback system unrolls over its horizon into a computational graph\. This view is implicit in the dependency\-graph formalism of OvertPoly\([Akinwande et al\. 2026a](https://arxiv.org/html/2609.16298#bib.bib1)\), which encodes each node as MILP constraints\. The contribution here is to realize the dynamics asrailnodes, exposing the graph to bound propagation and joint branch\-and\-bound over enclosure refinements and neuron splits\.

###### Definition 3\(Neural Feedback Graph\)\.

Let𝒟\\mathcal\{D\}be a neural feedback system\. Its*neural feedback graph*𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}is a directed acyclic graph with input nodes𝐱0∈𝐈\\mathbf\{x\}\_\{0\}\\in\\mathbf\{I\}andϵ0,…,ϵT−1∈𝐄\\mathbf\{\\epsilon\}\_\{0\},\\ldots,\\mathbf\{\\epsilon\}\_\{T\-1\}\\in\\mathbf\{E\}, andTTper\-step subgraphs chained through state nodes𝐱1,…,𝐱T\\mathbf\{x\}\_\{1\},\\ldots,\\mathbf\{x\}\_\{T\}\. The subgraph at timetttakes𝐱t\\mathbf\{x\}\_\{t\}andϵt\\mathbf\{\\epsilon\}\_\{t\}as inputs and realizes𝑛𝑒𝑥𝑡𝒟\\mathit\{next\}^\{\\mathcal\{D\}\}via a controllerπt\\pi\_\{t\}computing𝐮⁡\(𝐱t\)\\mathbf\{u\}\(\\mathbf\{x\}\_\{t\}\), scalarrailenclosure nodes realizingF⁡\(𝐱t\)F\(\\mathbf\{x\}\_\{t\}\), and an affine layer computing𝐱t\+1=𝐱t\+\(F⁡\(𝐱t\)\+B​πt​\(𝐱t\)\+ϵt\)​δ\\mathbf\{x\}\_\{t\+1\}=\\mathbf\{x\}\_\{t\}\+\\bigl\(F\(\\mathbf\{x\}\_\{t\}\)\+B\\,\\pi\_\{t\}\(\\mathbf\{x\}\_\{t\}\)\+\\mathbf\{\\epsilon\}\_\{t\}\\bigr\)\\,\\delta\.

###### Proposition 1\(Soundness of Bound Propagation on𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}\)\.

Let𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}have abartrelaxation at eachrailnode and a LiRPA bound at each nonlinear node in everyπ\(t\)\\pi\_\{\(t\)\}\. Then any application ofrailto𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}over𝐈×𝐄T\\mathbf\{I\}\\times\\mathbf\{E\}^\{T\}produces linear bounds on𝐱t\\mathbf\{x\}\_\{t\}that overapproximateτ𝒟​\(𝐈\)t\\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\mathbf\{I\}\)\_\{t\}for everyt∈\[0\.\.T\]t\\in\[0\.\.T\]\.

### Branch and Bound viarail

We extend BaB to𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}with*enclosure refinement*: splitting a state node𝐱t\\mathbf\{x\}\_\{t\}along a coordinate hyperplane, thereby refining every enclosure that reads the split coordinate\.

###### Definition 4\(railSubproblem\)\.

Arailsubproblem for𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}is a tupleR=⟨C,ℋ,ℬ,𝒩⟩R=\\langle C,\\mathcal\{H\},\\mathcal\{B\},\\mathcal\{N\}\\rangleconsisting of an*input cell*CCwhich is a hyperrectangle over the inputs\(𝐱0,ϵ0,…,ϵT−1\)\(\\mathbf\{x\}\_\{0\},\\mathbf\{\\epsilon\}\_\{0\},\\ldots,\\mathbf\{\\epsilon\}\_\{T\-1\}\)of𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}; a setℋ\\mathcal\{H\}of*state constraints*which are axis\-aligned half\-spaces of the form\{𝐱tk≤γ\}\\\{\\mathbf\{x\}\_\{t\}^\{k\}\\leq\\gamma\\\}or\{𝐱tk≥γ\}\\\{\\mathbf\{x\}\_\{t\}^\{k\}\\geq\\gamma\\\}, where𝐱tk\\mathbf\{x\}\_\{t\}^\{k\}indicates thekkth element of the state vector𝐱t\\mathbf\{x\}\_\{t\}; a familyℬ=\{B□\(i,t\)\}\\mathcal\{B\}=\\\{B^\{\(i,t\)\}\_\{\\square\}\\\}of relaxed bounding sets, one for eachrailenclosure nodeftif^\{i\}\_\{t\}inF⁡\(𝐱t\)F\(\\mathbf\{x\}\_\{t\}\), each with domain induced byCCandℋ\\mathcal\{H\}; and a set𝒩\\mathcal\{N\}of*pre\-activation constraints*, one interval per split neuron across the controllersπ0,…,π\(T−1\)\\pi\_\{0\},\\ldots,\\pi\_\{\(T\-1\)\}\.

The subproblemRRcovers the trajectories that satisfy its constraints: inputs inCC, states in every half\-space ofℋ\\mathcal\{H\}, and controller pre\-activations in every interval of𝒩\\mathcal\{N\}\. Constraints inℋ\\mathcal\{H\}on input nodes can be absorbed intoCC, since intersecting a hyperrectangle with an axis\-aligned half\-space yields a hyperrectangle,ℋ\\mathcal\{H\}thus retains only constraints on interior nodes\. A subproblem admits two split actions, each yeilding two*child*subproblems:

- •*enclosure refinement*: split a state node𝐱t\\mathbf\{x\}\_\{t\}, input or interior, along a coordinate hyperplane\{𝐱tk=γ\}\\\{\\mathbf\{x\}^\{k\}\_\{t\}=\\gamma\\\}\. One child receives the constraint\{𝐱tk≤γ\}\\\{\\mathbf\{x\}^\{k\}\_\{t\}\\leq\\gamma\\\}and the other\{𝐱kt≥γ\}\\\{\\mathbf\{x\}\_\{k\}^\{t\}\\geq\\gamma\\\}\. Att=0t=0, this is equivalent to partitioningCCalong the hyperplane\. Every enclosure that depends on𝐱tk\\mathbf\{x\}^\{k\}\_\{t\}is refined along the grid hyperplane atγ\\gammawhenγ\\gammais one of its grid coordinates \([Theorem2](https://arxiv.org/html/2609.16298#Thmtheorem2)\), and otherwise*snapped*outwards \(yielding an overapproximation\) to be refined along the nearest grid hyperplane bounding the child’s constrained region\. The controllerπt\\pi\_\{t\}also has its input domain tightened\.
- •*neuron split*: partition the pre\-activation interval of a neuron in someπt\\pi\_\{t\}\. Each child receives the corresponding subinterval in𝒩\\mathcal\{N\}\. For piecewise\-linear activations, splitting an unstable neuron at zero fixes its phase\.

Enclosure refinement generalizes input splitting from open\-loop neural network verification\. An open\-loop input split bisects the input region along a chosen dimension \(thet=0t=0case of enclosure refinement\)\. An interior split has no open\-loop counterpart\. It constrains an interior state node, propagating the constraint to every enclosure that depends on the split coordinate without further branching\. Enclosure refinement integrates elements of input splitting and neuron splitting\. The operation is further complicated by grid alignment: refinement yields non\-overlapping child domains only when the split hyperplane is a grid hyperplane, and the snapped domains overlap otherwise\. Overlapping children have no analog in LiRPA\-based BaB, where input split actions partition their domain\.

##### Branching Heuristic

Integrating enclosure refinements and neuron splits requires a branching heuristic that scores both action types on a common scale\. Our heuristic,muni\(Multi\-actionUnifiedNodeImprovement\), uses backward bound propagation to compute the gradient of the objective’s bound with respect to each node, and takes the gradient magnitude as the estimated bound improvement of the split action the node admits \(enclosure refinement at state andrailnodes, neuron splits at pre\-activation nodes\)\. The split point is the midpoint of the relevant interval, snapped to the nearest grid hyperplane forrailnodes\.munigeneralizes BaBSR\([Bunel et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib3)\), which scores neuron splits by cheap estimates of bound improvement and is detailed alongside other branching heuristics in Appendix[A\.4](https://arxiv.org/html/2609.16298#A1.SS4)\. We leave more sophisticated heuristics to future work\.

We call the resulting algorithmclipper\(Closed\-LoopIterativePropagation withPolyhedralEnclosureRefinement\), and we show it in[Algorithm1](https://arxiv.org/html/2609.16298#alg1)\. Its soundness follows by induction on the subproblem tree\. Refinements preserve the parent enclosure \([Theorem2](https://arxiv.org/html/2609.16298#Thmtheorem2)\), relaxations are sound for any slope \([Theorem1](https://arxiv.org/html/2609.16298#Thmtheorem1)\), and neuron splits were previously shown to be sound\([Shi et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib16)\)\. A parent is sound if all of its children are, since every parent trajectory lies in some child\. The root covers every trajectory over the input cell, so returningVerifiedcertifies the given specification\.

Algorithm 1clipper: BaB onrail0:Neural feedback graph

𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}, input cell

C0C\_\{0\}, property

φ\\varphi, branching heuristicmuni

0:Verifiedor counterexample

𝐱∗\\mathbf\{x\}^\{\*\}
1:

ℬ0←\\mathcal\{B\}\_\{0\}\\leftarrowbartrelaxations of therailnodes of

𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}
2:

ℛ←\{⟨C0,∅,ℬ0,∅⟩\}\\mathcal\{R\}\\leftarrow\\\{\\langle C\_\{0\},\\emptyset,\\mathcal\{B\}\_\{0\},\\emptyset\\rangle\\\}
3:while

ℛ≠∅\\mathcal\{R\}\\neq\\emptysetdo

4:Select

R=⟨C,ℋ,ℬ,𝒩⟩∈ℛR=\\langle C,\\mathcal\{H\},\\mathcal\{B\},\\mathcal\{N\}\\rangle\\in\\mathcal\{R\}and remove it from

ℛ\\mathcal\{R\}
5:

\(y¯,y¯\)←railBound​\(𝒢T𝒟,R\)\(\\underline\{y\},\\overline\{y\}\)\\leftarrow\\textsc\{railBound\}\(\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\},R\)
6:if

\[y¯,y¯\]\[\\underline\{y\},\\overline\{y\}\]verifies

φ\\varphithen

7:continue\{

RRis verified\}

8:elseifa counterexample

𝐱∗∈C\\mathbf\{x\}^\{\*\}\\in Cis foundthen

9:return

𝐱∗\\mathbf\{x\}^\{\*\}
10:else

11:

a∗←arg⁡maxa∈Actions​\(R\)​muni​\(a,R\)a^\{\*\}\\leftarrow\\arg\\max\_\{a\\in\\textsc\{Actions\}\(R\)\}\\textsc\{muni\}\(a,R\)
12:

ℛ←ℛ∪Split​\(R,a∗\)\\mathcal\{R\}\\leftarrow\\mathcal\{R\}\\cup\\textsc\{Split\}\(R,a^\{\*\}\)
13:endif

14:endwhile

15:returnVerified

## Forward Reachability Analysis

Forward reachability analysis verifies a system𝒟\\mathcal\{D\}by constructing a sequence of over\-approximations𝐗^0,…,𝐗^T\\hat\{\\mathbf\{X\}\}\_\{0\},\\ldots,\\hat\{\\mathbf\{X\}\}\_\{T\}with𝐗^t⊇𝐗t\\hat\{\\mathbf\{X\}\}\_\{t\}\\supseteq\\mathbf\{X\}\_\{t\}for eacht∈\[0\.\.T\]t\\in\[0\.\.T\], where𝐗t=τ𝒟​\(𝐈\)t\\mathbf\{X\}\_\{t\}=\\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\mathbf\{I\}\)\_\{t\}\. Safety is then checked against this sequence\.

###### Proposition 2\(Sufficient Condition for Safety\)\.

Let𝐗^0,…,𝐗^T\\hat\{\\mathbf\{X\}\}\_\{0\},\\ldots,\\hat\{\\mathbf\{X\}\}\_\{T\}satisfy𝐗^t⊇𝐗t\\hat\{\\mathbf\{X\}\}\_\{t\}\\supseteq\\mathbf\{X\}\_\{t\}for allt∈\[0\.\.T\]t\\in\[0\.\.T\]\. If𝐗^t∩𝐀⁡\(t\)=∅\\hat\{\\mathbf\{X\}\}\_\{t\}\\cap\\mathbf\{A\}\(t\)=\\emptysetfor allttand𝐗^t∗⊆𝐆\\hat\{\\mathbf\{X\}\}\_\{t^\{\*\}\}\\subseteq\\mathbf\{G\}for somet∗∈\[0\.\.T\]t^\{\*\}\\in\[0\.\.T\], then𝒟\\mathcal\{D\}is safe\.

A reachability procedure returns*verified*when it produces a sequence satisfying the conditions of[Proposition2](https://arxiv.org/html/2609.16298#Thmproposition2), and*inconclusive*otherwise; because the check is against over\-approximations, an inconclusive result does not imply that𝒟\\mathcal\{D\}is unsafe\. We define two procedures:*concrete*reachability, the loose default, and*symbolic*reachability, a tighter refinement\. Both are evaluation strategies on𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}, invokingclipperas their bounding oracle\.

Table 1:Verification results on ARCH\-COMP 2025 AINNCS benchmarks supported byclipper\. Instances are defined in Appendix[C\.1](https://arxiv.org/html/2609.16298#A3.SS1)\.nnis the state dimension,TTthe horizon\. Cells report wall\-clock seconds to certify,×\\timesdenotes an inconclusive result \(error or too imprecise\),Uan unsupported instance, and an\(F\)prefix a specification that does not hold, whose row instead reports set\-computation time\. Per instance the fastest tool isboldand the tightest \(smallest terminal volume\)underlined\.★\\bigstarmarks our method\.#### Concrete Reachability

Concrete reachability evaluates𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}in the manner of interval bound propagation \(IBP\) on the time axis\. Each𝐗^t\\hat\{\\mathbf\{X\}\}\_\{t\}is a hyperrectangle, with𝐗^0\\hat\{\\mathbf\{X\}\}\_\{0\}the bounding box of𝐈\\mathbf\{I\}\. Given𝐗^t\\hat\{\\mathbf\{X\}\}\_\{t\}, each component𝐗^t\+1i,i∈\[n\]\\hat\{\\mathbf\{X\}\}^\{i\}\_\{t\+1\},i\\in\[n\]of the next state set is bounded by invokingclippertwice \(once per bound direction\) on theii\-th component of𝑛𝑒𝑥𝑡𝒟\\mathit\{next\}^\{\\mathcal\{D\}\}over𝐱∈𝐗^t\\mathbf\{x\}\\in\\hat\{\\mathbf\{X\}\}\_\{t\}andϵ∈𝐄\\mathbf\{\\epsilon\}\\in\\mathbf\{E\}, returning an interval\[g¯i,g¯i\]\[\\underline\{g\}\_\{i\},\\overline\{g\}\_\{i\}\]\. The product𝐗^t\+1=∏i=1n\[g¯i,g¯i\]\\hat\{\\mathbf\{X\}\}\_\{t\+1\}=\\prod\_\{i=1\}^\{n\}\[\\underline\{g\}\_\{i\},\\overline\{g\}\_\{i\}\]is a hyperrectangle and feeds the next step\. Cross\-coordinate and cross\-time correlations are discarded at each step\.

#### Symbolic Reachability

Symbolic reachability evaluates𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}by propagating linear bounds in\(𝐱0,ϵ0,…,ϵT−1\)\(\\mathbf\{x\}\_\{0\},\\mathbf\{\\epsilon\}\_\{0\},\\ldots,\\mathbf\{\\epsilon\}\_\{T\-1\}\)across each time step, preserving the cross\-time and cross\-coordinate correlations that concrete reachability discards\. Each per\-step subgraph contributesbartrelaxations at therailnodes representingFF, sized from the concrete over\-approximations𝐗^t\\hat\{\\mathbf\{X\}\}\_\{t\}, and LiRPA relaxations at the nonlinear nodes inπt\\pi\_\{t\}, sized from IBP bounds within the controller\.

This scaffolding is common to both traditionsclipperunifies\. Within a feedforward network, IBP bounds provide the domains over which LiRPA bounds are defined\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\), whereas in combinatorial NFS solvers, per\-step concrete reachable sets are the abstractions over which the symbolic problem is defined\([Sidrane et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib17);[Akinwande et al\. 2026a](https://arxiv.org/html/2609.16298#bib.bib1)\)\. Symbolic reachability viaclipperinherits both: a single concrete pre\-pass sizes thebartrelaxations of the dynamics and the LiRPA relaxations of the controller across the horizon of𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}\.

Whenclipperrefines a step, the scaffolding must be refined as well\. Splitting the state node at stept∗t^\{\*\}partitions𝐗^t∗\\hat\{\\mathbf\{X\}\}\_\{t^\{\*\}\}into cells\. Thebartrelaxation on a cellSSover\-approximatesFFonly overSS, so the bound it induces at a later step is sound only for trajectories whose state att∗t^\{\*\}lies inSS\. Each cell therefore receives its own scaffolding, sized by concrete reachability restarted fromSSrather than by the parent sets𝐗^t\\hat\{\\mathbf\{X\}\}\_\{t\}, and a backward pass over the remaining horizon yields its bounds\. Each cell is checked against the specification independently, and the check succeeds when every cell passes\. This isclipper’s branch\-and\-bound applied to reachability analysis, and the cells are the children of an enclosure refinement att∗t^\{\*\}\.

Concrete reachability is the default\. However, because it discards cross\-time correlations, it may fail to certify challenging reach\-avoid specifications\. Symbolic reachability then tightens the specific𝐗^t\\hat\{\\mathbf\{X\}\}\_\{t\}at which the check fails\.

## Evaluation

We evaluateclipperon the ARCH\-COMP 2025 AINNCS suite\([Manzanas Lopez et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib14)\), which comprises 12 reach\-avoid instances across nine neural feedback systems \(two systems contribute multiple instances\)\. Following the guidelines of the organizers, we discretize the continuous\-time plants using forward Euler integration\. On AINNCS we compare against the 2025 participants that permit discrete\-time analysis, either natively \(CORA\) or via a fair modification \(CROWN\-Reach, immrax;[SectionC\.2](https://arxiv.org/html/2609.16298#A3.SS2)\), together with the combinatorial solvers OvertPoly and OVERTVerify\. Continuous\-time performance does not automatically transfer to the discrete\-time setting, as the resulting closed\-loop behavior differs\. Details about the AINNCS benchmarks are provided in Appendix[C](https://arxiv.org/html/2609.16298#A3)\.

1133557799111110−110^\{\-1\}10210^\{2\}10510^\{5\}Instances solvedTime \(s\)

1133557799111110−1310^\{\-13\}10−610^\{\-6\}10110^\{1\}Instances solvedTerminal volume

clipperOvertPolyOVERTVerifyimmraxCROWN\-ReachCORA

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\)\(x,y\)meansxxinstances were solved withinyy, so lower and farther right is better\.Left:per\-instance time\.Right:terminal reachable\-set volume \(tightness\)\.##### Falsifiable AINNCS specifications\.

A few AINNCS specifications do not hold\. We cross\-check this with one sampler over𝐈\\mathbf\{I\}\(fixed seed and budget\) applied identically across tools: a sampled trajectory that intersects𝐀⁡\(t\)\\mathbf\{A\}\(t\)at somettwitnesses \([3](https://arxiv.org/html/2609.16298#Sx2.E3)\) failing, and one that lies outside𝐆\\mathbf\{G\}at everyttsuggests \([2](https://arxiv.org/html/2609.16298#Sx2.E2)\) failing\. We report set\-computation time on these instances as for the others to measure scalability and tightness on identical dynamics\. Such rows are marked\(F\)\.

##### Coverage\.

clippersolves 10 of the 12 instances \([Table1](https://arxiv.org/html/2609.16298#Sx4.T1)\), certifying six of the eight instances whose specifications hold, and computing reachable sets on all four that do not\. No baseline solves an instance thatclipperdoes not\. CORA is the closest, solving eight\. Its strength in the continuous\-time setting carries over here, which makes it the state\-of\-the\-art baseline for discrete\-time reachability\. The next best is immrax with seven instances, and OvertPoly, OVERTVerify, and CROWN\-Reach solve four each\. The combinatorial solvers account for most of the coverage gap, as OvertPoly and OVERTVerify support only 4 of the 12 instances\. Their MILP encodings require𝖱𝖾𝖫𝖴\\mathsf\{ReLU\}controllers, which rules out seven of the eight instances they leave unsupported \([SectionC\.1](https://arxiv.org/html/2609.16298#A3.SS1)\)\.clipperinherits their grid\-based enclosure of the dynamics but places no restriction on the controller’s activations, and therefore supports all 12 instances\. These tools are the closest antecedents toclipper, and the coverage gain over them is substantial\.

##### Tightness\.

Tools that unify dynamics and controller abstractions \(CORA andclipper\) lead on both tightness and coverage\. CORA attains the smallest terminal volume on six instances andclipperon two, leaving one each to immrax and CROWN\-Reach\. The volume cactus plot \([Figure2](https://arxiv.org/html/2609.16298#Sx5.F2), right\) sharpens the split: CORA’s points lie belowclipper’s on most instances, whileclipper’s extends two instances further\. immrax solves Airplane and Attitude Control, which CORA leaves inconclusive, but takes four to six times longer on them thanclipper\. CORA’s unified abstraction does not scale with dimension\. The two instancesclippersolves and CORA does not, Airplane \(n=12n=12\) and Attitude Control \(n=6n=6\), are among the largest in the suite, and we attribute this to a control\-native abstraction whose cost grows with the state dimension and the network size\. Conversely,clipperreports each𝐗^t\\hat\{\\mathbf\{X\}\}\_\{t\}as an axis\-aligned hyperrectangle, which is less expressive than CORA’s zonotopes and accumulates wrapping error when the reachable set rotates\. This is the likely reason CORA outperformsclipperon Unicycle and the Navigation instances, whose vector fields rotate the set as the heading turns\.clippercompensates by refining more, which costs time\. We leave the exploration of more expressive abstractions to future work\.

##### Time\.

clipperis fastest on most of the instances it solves, and its time cactus plot reflects this \([Figure2](https://arxiv.org/html/2609.16298#Sx5.F2), left\)\. Against the combinatorial solvers,clipperis faster on every instance they support, by factors between3\.53\.5and10001000\. Against the other participants, the margin is smaller and not uniform\. CORA is faster on the Unicycle and the Navigation instances, and CROWN\-Reach edgesclipperout on Attitude Control\.

Table 2:Relaxation ablation onUnicycleatt∗=15t^\{\\ast\}=15\.*Volume*is the reachable\-set volume att∗t^\{\\ast\};*Time*is the wall\-clock time to compute and optimize the relaxation\.
### Ablations

On theUnicyclebenchmark, whose vector field couples speed and heading throughx4cosx3x\_\{4\}\\cos x\_\{3\}andx4sinx3x\_\{4\}\\sin x\_\{3\}\(Appendix[C\.1](https://arxiv.org/html/2609.16298#A3.SS1)\), we compare ourbartapproach against two alternatives that decompose each coupled term into primitives, relax each independently, and compose by backward substitution, as𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}would if the dynamics used LiRPA’s native operators\.bart\+\+*OVERT*\([Sidrane et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib17)\)bounds each primitive with the enclosure’s grid\-derived bound, whilebart\+\+CROWN uses LiRPA native relaxations\([Shi et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib16)\)\. All three optimize their slopes for the same 50 gradient steps and none refines or splits, so the comparison isolates relaxation quality \([Table2](https://arxiv.org/html/2609.16298#Sx5.T2)\)\. At that fixed budget, the alternative approaches are3\.3×3\.3\\timestighter att∗t^\{\\ast\}but7×7\\timesslower; thebartbaseline stays within the same order of magnitude at a fraction of the cost\. This is consistent with the pattern of enclosure composition being computationally efficient at the cost of precision\.

We then ablateclipper’s branching actions \([Table3](https://arxiv.org/html/2609.16298#Sx5.T3)\)\.*Input splitting*restricts refinement tot=0t=0, the open\-loop default, while*enclosure refinement*also splits interior state nodes, refining every enclosure that reads them\. Both branch until 96 children, isolating where the splits fall\. At that fixed budget, enclosure refinement returns a1\.4×1\.4\\timesto1\.7×1\.7\\timestighter terminal set on both benchmarks\.

Table 3:Branching ablation on a benchmark subset\.*Time*is wall\-clock seconds and*Volume*the terminal reachable\-set volume\.★\\bigstarmarks our method\.

## Conclusions and Future Work

railexposes polyhedral enclosures of nonlinear dynamics to LiRPA, andclipperbranches over enclosure refinements and neuron splits on the resulting graph, bringing parallelizable bound propagation to neural feedback systems\. On ARCH\-COMP 2025 AINNCS,clippersolves more instances than the discrete\-time state of the art\.clipper’s main limitation is that it reports each reachable set as axis\-aligned hyperrectangles, losing tightness to more expressive representations\. Richer representations and stronger branching heuristics are the natural next steps\.

## References

- Akinwande et al\. \(2026a\)Akinwande, I\. S\.; Sidrane, C\.; Kochenderfer, M\. J\.; and Barrett, C\. 2026a\.Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems\.arXiv:2503\.22660\.
- Akinwande et al\. \(2026b\)Akinwande, S\. I\.; Katz, S\. M\.; Kochenderfer, M\. J\.; and Barrett, C\. 2026b\.The FABRIC Strategy for Verifying Neural Feedback Systems\.arXiv:2603\.08964\.
- Bunel et al\. \(2020\)Bunel, R\.; Lu, J\.; Turkaslan, I\.; Torr, P\. H\.; Kohli, P\.; and Kumar, M\. P\. 2020\.Branch and bound for piecewise linear neural network verification\.*Journal of Machine Learning Research*, 21\(42\): 1–39\.
- Cai, Fan, and Bak \(2025\)Cai, F\.; Fan, C\.; and Bak, S\. 2025\.Scalable Surrogate Verification of Image\-based Neural Network Control Systems Using Composition and Unrolling\.In*Proceedings of the AAAI Conference on Artificial Intelligence*\.
- De Palma et al\. \(2021\)De Palma, A\.; Bunel, R\.; Desmaison, A\.; Dvijotham, K\.; Kohli, P\.; Torr, P\. H\.; and Kumar, M\. P\. 2021\.Improved branch and bound for neural network verification via lagrangian decomposition\.*arXiv preprint arXiv:2104\.06718*\.
- Dutta, Chen, and Sankaranarayanan \(2019\)Dutta, S\.; Chen, X\.; and Sankaranarayanan, S\. 2019\.Reachability analysis for neural feedback systems using regressive polynomial rule inference\.In*Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control*, 157–168\.
- Ettinger et al\. \(2021\)Ettinger, S\.; Cheng, S\.; Caine, B\.; Liu, C\.; Zhao, H\.; Pradhan, S\.; Chai, Y\.; Sapp, B\.; Qi, C\. R\.; Zhou, Y\.; et al\. 2021\.Large scale interactive motion forecasting for autonomous driving: The waymo open motion dataset\.In*Proceedings of the IEEE/CVF International Conference on Computer Vision*, 9710–9719\.
- Fan et al\. \(2020\)Fan, J\.; Huang, C\.; Chen, X\.; Li, W\.; and Zhu, Q\. 2020\.Reachnn\*: A tool for reachability analysis of neural\-network controlled systems\.In*International Symposium on Automated Technology for Verification and Analysis*, 537–542\. Springer\.
- Harapanahalli, Jafarpour, and Coogan \(2024\)Harapanahalli, A\.; Jafarpour, S\.; and Coogan, S\. 2024\.immrax: A parallelizable and differentiable toolbox for interval analysis and mixed monotone reachability in jax\.*IFAC\-PapersOnLine*, 58\(11\): 75–80\.
- Huang et al\. \(2022\)Huang, C\.; Fan, J\.; Chen, X\.; Li, W\.; and Zhu, Q\. 2022\.Polar: A polynomial arithmetic framework for verifying neural\-network controlled systems\.In*International Symposium on Automated Technology for Verification and Analysis*, 414–430\. Springer\.
- Kaufmann et al\. \(2023\)Kaufmann, E\.; Bauersfeld, L\.; Loquercio, A\.; Müller, M\.; Koltun, V\.; and Scaramuzza, D\. 2023\.Champion\-level drone racing using deep reinforcement learning\.*Nature*, 620\(7976\): 982–987\.
- Kochdumper et al\. \(2023\)Kochdumper, N\.; Schilling, C\.; Althoff, M\.; and Bak, S\. 2023\.Open\-and closed\-loop neural network verification using polynomial zonotopes\.In*NASA Formal Methods Symposium*, 16–36\. Springer\.
- Manzanas Lopez et al\. \(2024\)Manzanas Lopez, D\.; Althoff, M\.; Benet, L\.; Blab, C\.; Forets, M\.; Jia, Y\.; Johnson, T\. T\.; Kranzl, M\.; Ladner, T\.; Linauer, L\.; et al\. 2024\.Arch\-comp24 category report: Artificial intelligence and neural network control systems \(ainncs\) for continuous and hybrid systems plants\.
- Manzanas Lopez et al\. \(2025\)Manzanas Lopez, D\.; Althoff, M\.; Benet, L\.; Coogan, S\.; Forets, M\.; Harapanahalli, A\.; Johnson, T\. T\.; Ladner, T\.; Schilling, C\.; Zhang, H\.; and Zhong, X\. 2025\.Arch\-comp25 category report: Artificial intelligence and neural network control systems \(ainncs\) for continuous and hybrid systems plants\.*EPiC Series in Computing*, 108: 71–121\.
- Rodriguez et al\. \(2022\)Rodriguez, I\. D\. J\.; Csomay\-Shanklin, N\.; Yue, Y\.; and Ames, A\. D\. 2022\.Neural gaits: Learning bipedal locomotion via control barrier functions and zero dynamics policies\.In*Proceedings of the 4th Annual Learning for Dynamics and Control Conference*, volume 168 of*Proceedings of Machine Learning Research*, 1060–1072\. PMLR\.
- Shi et al\. \(2025\)Shi, Z\.; Jin, Q\.; Kolter, Z\.; Jana, S\.; Hsieh, C\.\-J\.; and Zhang, H\. 2025\.Neural network verification with branch\-and\-bound for general nonlinearities\.In*International Conference on Tools and Algorithms for the Construction and Analysis of Systems*, 315–335\. Springer\.
- Sidrane et al\. \(2022\)Sidrane, C\.; Maleki, A\.; Irfan, A\.; and Kochenderfer, M\. J\. 2022\.Overt: An algorithm for safety verification of neural network control policies for nonlinear systems\.*Journal of Machine Learning Research*, 23\(117\): 1–45\.
- Verified\-Intelligence \(2024\)Verified\-Intelligence\. 2024\.CROWN\-Reach: A Reachability Analysis Tool for Neural Network Controlled Systems, Based on the alpha\-beta\-CROWN Framework\.https://github\.com/Verified\-Intelligence/CROWN\-Reach\.Accessed: 2026\-04\-17\.
- Wang et al\. \(2021\)Wang, S\.; Zhang, H\.; Xu, K\.; Lin, X\.; Jana, S\.; Hsieh, C\.\-J\.; and Kolter, J\. Z\. 2021\.Beta\-crown: Efficient bound propagation with per\-neuron split constraints for neural network robustness verification\.*Advances in neural information processing systems*, 34: 29909–29921\.
- Xu et al\. \(2020a\)Xu, K\.; Shi, Z\.; Zhang, H\.; Wang, Y\.; Chang, K\.\-W\.; Huang, M\.; Kailkhura, B\.; Lin, X\.; and Hsieh, C\.\-J\. 2020a\.Automatic perturbation analysis for scalable certified robustness and beyond\.*Advances in Neural Information Processing Systems*, 33: 1129–1141\.
- Xu et al\. \(2020b\)Xu, K\.; Zhang, H\.; Wang, S\.; Wang, Y\.; Jana, S\.; Lin, X\.; and Hsieh, C\.\-J\. 2020b\.Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers\.*arXiv preprint arXiv:2011\.13824*\.

## Appendix Contents

## Appendix AFormal Definitions

### A\.1Polyhedra

LetP=\{p→0,…,p→k\}⊂ℝnP=\\\{\\vec\{p\}\_\{0\},\\dots,\\vec\{p\}\_\{k\}\\\}\\subset\\mathbb\{R\}^\{n\}\. The*convex hull*ofPPis

conv\(P\)=\{θ0p→0\+…\+θkp→k∣θ→⋅1→=1,θ→⪰0→\},\\textbf\{conv\}\(P\)=\\\{\\theta\_\{0\}\\vec\{p\}\_\{0\}\+\\ldots\+\\theta\_\{k\}\\vec\{p\}\_\{k\}\\mid\\vec\{\\theta\}\\cdot\\vec\{1\}=1,\\ \\vec\{\\theta\}\\succeq\\vec\{0\}\\\},\(5\)and the*affine hull*aff​\(P\)\\textbf\{aff\}\(P\)is defined identically but without the constraintθ→⪰0→\\vec\{\\theta\}\\succeq\\vec\{0\}\.PPis*affinely independent*iff\{p→1−p→0,…,p→k−p→0\}\\\{\\vec\{p\}\_\{1\}\-\\vec\{p\}\_\{0\},\\dots,\\vec\{p\}\_\{k\}\-\\vec\{p\}\_\{0\}\\\}is linearly independent, equivalently iffdimaff​\(P\)=k\\dim\\textbf\{aff\}\(P\)=k\. In generaldimaff​\(P\)≤k\\dim\\textbf\{aff\}\(P\)\\leq k\. The*polyhedron formed by*PPisconv​\(P\)\\textbf\{conv\}\(P\)\. A subset ofℝn\\mathbb\{R\}^\{n\}is a*polyhedron*if it is the convex hull of a finite set of points inℝn\\mathbb\{R\}^\{n\}\.

#### A\.1\.1kk\-Simplex

###### Definition 5\.

A polyhedron𝒮\\mathcal\{S\}is a*kk\-simplex*if it is the convex hull ofk\+1k\+1affinely independent points\. A polyhedron is a*simplex*if it is akk\-simplex for somekk, andkkis called its*dimension*\.

If𝒮\\mathcal\{S\}is akk\-simplex, its*vertices*, denotedvert​\(𝒮\)\\textbf\{vert\}\(\\mathcal\{S\}\), are the unique setPPofk\+1k\+1points with𝒮=conv​\(P\)\\mathcal\{S\}=\\textbf\{conv\}\(P\)\. A*face*of𝒮\\mathcal\{S\}is the convex hull of any non\-empty subset ofvert​\(𝒮\)\\textbf\{vert\}\(\\mathcal\{S\}\)\.

#### A\.1\.2Simplicial Complex

###### Definition 6\.

A*simplicial complex*Δ\\Deltais a finite set of simplices such that:

- •every face of a simplex inΔ\\Deltais also inΔ\\Delta;
- •every non\-empty intersection of two simplices𝒮1,𝒮2∈Δ\\mathcal\{S\}\_\{1\},\\mathcal\{S\}\_\{2\}\\in\\Deltais a face of both𝒮1\\mathcal\{S\}\_\{1\}and𝒮2\\mathcal\{S\}\_\{2\}\.

The*dimension*ofΔ\\Deltais the largest dimension of any simplex it contains\. A simplicial complex of dimensionkkis a*pure simplicialkk\-complex*if every simplex inΔ\\Deltais a face of somekk\-dimensional simplex inΔ\\Delta\.

#### A\.1\.3Point Set Triangulation

LetPPbe a finite set of points inℝn\\mathbb\{R\}^\{n\}\. We sayPPis*full\-dimensional*if it containsn\+1n\+1affinely independent points\.

###### Definition 7\.

IfPPis a finite, full\-dimensional set of points inℝn\\mathbb\{R\}^\{n\}, then a pure simplicialnn\-complexΔ\\Deltais a*triangulation ofPP*ifP=⋃𝒮∈Δvert​\(𝒮\)P=\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\}\\textbf\{vert\}\(\\mathcal\{S\}\)andconv​\(P\)=⋃𝒮∈Δ𝒮\\textbf\{conv\}\(P\)=\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\}\\mathcal\{S\}\.

LetCCbe a closednn\-ball, we writeCOC^\{O\}for the corresponding opennn\-ball andCSC^\{S\}for the hypersphere forming its surface\. For a set of pointsPP, letVP​\(C\)=C∩PV\_\{P\}\(C\)=C\\cap P\. For a polyhedron𝒫\\mathcal\{P\}, the*circumsphere*of𝒫\\mathcal\{P\}\(when it exists\) is the hypersphere passing through every vertex of𝒫\\mathcal\{P\}\. Circumspheres always exist for simplices and for hyperrectangles\.

LetPPbe a finite, full\-dimensional set of points inℝn\\mathbb\{R\}^\{n\}and letΔ\\Deltabe a triangulation ofPP\. For eachnn\-simplex𝒮∈Δ\\mathcal\{S\}\\in\\Delta, letC⁡\(𝒮\)C\(\\mathcal\{S\}\)denote thenn\-ball whose boundary is the circumsphere of𝒮\\mathcal\{S\}\. We say𝒮\\mathcal\{S\}satisfies the*Delaunay condition*, and call it a*Delaunay simplex ofPP*, ifVP​\(C​\(𝒮\)O\)=∅V\_\{P\}\(C\(\\mathcal\{S\}\)^\{O\}\)=\\emptyset\(equivalently, the only points ofPPinC⁡\(𝒮\)C\(\\mathcal\{S\}\)lie on its surface\)\.Δ\\Deltais a*Delaunay triangulation*if everynn\-simplex inΔ\\Deltasatisfies the Delaunay condition\.

Forx→∈conv​\(P\)\\vec\{x\}\\in\\textbf\{conv\}\(P\), let𝒮Δ​\(x→\)\\mathcal\{S\}\_\{\\Delta\}\(\\vec\{x\}\)denote thenn\-simplex ofΔ\\Deltacontainingx→\\vec\{x\}\. Ifx→\\vec\{x\}lies on a face of dimension less thannnand is therefore contained in multiplenn\-simplices,𝒮Δ​\(x→\)\\mathcal\{S\}\_\{\\Delta\}\(\\vec\{x\}\)chooses one in a deterministic way\. Writingvert​\(𝒮Δ​\(x→\)\)=𝐩\\textbf\{vert\}\(\\mathcal\{S\}\_\{\\Delta\}\(\\vec\{x\}\)\)=\\mathbf\{p\}in some fixed order,θ=θΔ​\(x→\)∈ℝn\+1\\theta=\\theta\_\{\\Delta\}\(\\vec\{x\}\)\\in\\mathbb\{R\}^\{n\+1\}is the unique convex combination vector withx→=θ⋅𝐩\\vec\{x\}=\\theta\\cdot\\mathbf\{p\}\.

#### A\.1\.4Grids

###### Definition 8\.

A*grid of dimensionnn*is the Cartesian productG=G1×⋯×GnG=G\_\{1\}\\times\\dots\\times G\_\{n\}, where eachGi⊂ℝG\_\{i\}\\subset\\mathbb\{R\}is a finite set with at least two elements\. The*domain*ofGGis𝑑𝑜𝑚​\(G\)=conv​\(G\)\\mathit\{dom\}\(G\)=\\textbf\{conv\}\(G\)\.

A*grid cell*ofGGis the vertex set𝐗\\mathbf\{X\}of annn\-dimensional hyperrectangleR⊆𝑑𝑜𝑚⁡\(G\)R\\subseteq\\mathit\{dom\}\(G\)satisfyingG∩R=𝐗G\\cap R=\\mathbf\{X\}; equivalently, the2n2^\{n\}vertices ofRRall lie inGG, and no other point ofGGlies inRR\. For𝐱∈G\\mathbf\{x\}\\in G, we write𝐶𝑒𝑙𝑙𝑠\(G,𝐱\)=\{𝐗∣𝐗is a grid cell ofG,𝐱∈𝐗\}\.\\mathit\{Cells\}\(G,\\mathbf\{x\}\)=\\\{\\mathbf\{X\}\\mid\\mathbf\{X\}\\text\{ is a grid cell of \}G,\\ \\mathbf\{x\}\\in\\mathbf\{X\}\\\}\.

#### A\.1\.5Grid Hyperplane

###### Definition 9\.

LetP=G1×⋯×GnP=G\_\{1\}\\times\\cdots\\times G\_\{n\}be a grid inℝn\\mathbb\{R\}^\{n\}\. A*grid hyperplane*ofPPis a hyperplane of the form

H:=\{𝐱∈ℝn:xi=c\},H:=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{n\}:x\_\{i\}=c\\\},for some axis indexi∈\{1,…,n\}i\\in\\\{1,\\ldots,n\\\}andc∈Gic\\in G\_\{i\}withmin⁡Gi<c<max⁡Gi\\min G\_\{i\}<c<\\max G\_\{i\}\.

### A\.2Polyhedral Enclosures

This section reproduces the formal machinery for polyhedral enclosures from the OvertPoly formulation cited in the main paper, we refer the reader there for full definitions and proofs\.

#### A\.2\.1Bounding Sets

###### Definition 10\.

A*bounding set*is a tupleB=⟨n,P,L,U⟩B=\\langle n,P,L,U\\ranglewheren∈ℕn\\in\\mathbb\{N\},PPis a grid of dimensionnn, andL,U:P→ℝL,U:P\\to\\mathbb\{R\}satisfyL⁡\(p→\)≤U⁡\(p→\)L\(\\vec\{p\}\)\\leq U\(\\vec\{p\}\)for everyp→∈P\\vec\{p\}\\in P\. The*domain*ofBBis𝑑𝑜𝑚​\(B\)=conv​\(P\)\\mathit\{dom\}\(B\)=\\textbf\{conv\}\(P\)\.

#### A\.2\.2Polyhedra formed by Bounding Sets

###### Definition 11\.

LetB=⟨n,P,L,U⟩B=\\langle n,P,L,U\\ranglebe a bounding set\. The*lifted vertex set*ofBBis

V⁡\(B\):=\{\(p→,L⁡\(p→\)\)∣p→∈P\}∪\{\(p→,U⁡\(p→\)\)∣p→∈P\}V\(B\):=\\\{\(\\vec\{p\},L\(\\vec\{p\}\)\)\\mid\\vec\{p\}\\in P\\\}\\cup\\\{\(\\vec\{p\},U\(\\vec\{p\}\)\)\\mid\\vec\{p\}\\in P\\\}whereV⁡\(B\)⊂ℝn\+1V\(B\)\\subset\\mathbb\{R\}^\{n\+1\}\. The*polyhedron formed byBB*is

𝒫​\(B\):=conv​\(V​\(B\)\)\.\\mathcal\{P\}\(B\):=\\textbf\{conv\}\(V\(B\)\)\.

#### A\.2\.3Polyhedral Enclosures

###### Definition 12\.

LetB=⟨n,P,L,U⟩B=\\langle n,P,L,U\\ranglebe a bounding set, letΔ\\Deltabe a Delaunay triangulation ofPP, and letΔn\\Delta\_\{n\}denote the set ofnn\-simplices inΔ\\Delta\. For each𝒮∈Δn\\mathcal\{S\}\\in\\Delta\_\{n\}, the*restriction ofBBto𝒮\\mathcal\{S\}*is the bounding set

B\|𝒮:=⟨n,vert​\(𝒮\),L\|vert​\(𝒮\),U\|vert​\(𝒮\)⟩\.B\|\_\{\\mathcal\{S\}\}:=\\langle n,\\textbf\{vert\}\(\\mathcal\{S\}\),L\|\_\{\\textbf\{vert\}\(\\mathcal\{S\}\)\},U\|\_\{\\textbf\{vert\}\(\\mathcal\{S\}\)\}\\rangle\.The*polyhedral enclosure formed byBBandΔ\\Delta*is

ℰ⁡\(B,Δ\):=⋃𝒮∈Δn𝒫⁡\(B\|𝒮\)\.\\mathcal\{E\}\(B,\\Delta\):=\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\_\{n\}\}\\mathcal\{P\}\(B\|\_\{\\mathcal\{S\}\}\)\.

The*lower*and*upper surfaces*ofℰ⁡\(B,Δ\)\\mathcal\{E\}\(B,\\Delta\)are the functionsLΔ,UΔ:𝑑𝑜𝑚⁡\(B\)→ℝL\_\{\\Delta\},U\_\{\\Delta\}:\\mathit\{dom\}\(B\)\\to\\mathbb\{R\}given by

LΔ​\(𝐱\)\\displaystyle L\_\{\\Delta\}\(\\mathbf\{x\}\):=min⁡\{y∈ℝ∣\(𝐱,y\)∈ℰ⁡\(B,Δ\)\},\\displaystyle:=\\min\\\{y\\in\\mathbb\{R\}\\mid\(\\mathbf\{x\},y\)\\in\\mathcal\{E\}\(B,\\Delta\)\\\},\(6a\)UΔ​\(𝐱\)\\displaystyle U\_\{\\Delta\}\(\\mathbf\{x\}\):=max⁡\{y∈ℝ∣\(𝐱,y\)∈ℰ⁡\(B,Δ\)\}\.\\displaystyle:=\\max\\\{y\\in\\mathbb\{R\}\\mid\(\\mathbf\{x\},y\)\\in\\mathcal\{E\}\(B,\\Delta\)\\\}\.\(6b\)

#### A\.2\.4Function Enclosures

###### Definition 13\.

LetB=⟨n,P,L,U⟩B=\\langle n,P,L,U\\ranglebe a bounding set\. A functionf:D→ℝf:D\\to\\mathbb\{R\}with𝑑𝑜𝑚⁡\(B\)⊆D⊆ℝn\\mathit\{dom\}\(B\)\\subseteq D\\subseteq\\mathbb\{R\}^\{n\}is*enclosed*byBBif\(𝐱,f⁡\(𝐱\)\)∈ℰ⁡\(B,Δ\)\(\\mathbf\{x\},f\(\\mathbf\{x\}\)\)\\in\\mathcal\{E\}\(B,\\Delta\)for every𝐱∈𝑑𝑜𝑚⁡\(B\)\\mathbf\{x\}\\in\\mathit\{dom\}\(B\)and every Delaunay triangulationΔ\\DeltaofPP\.

Equivalently,ffis enclosed byBBif and only ifLΔ​\(𝐱\)≤f⁡\(𝐱\)≤UΔ​\(𝐱\)L\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq f\(\\mathbf\{x\}\)\\leq U\_\{\\Delta\}\(\\mathbf\{x\}\)for every𝐱∈𝑑𝑜𝑚⁡\(B\)\\mathbf\{x\}\\in\\mathit\{dom\}\(B\)and every Delaunay triangulationΔ\\DeltaofPP\.

### A\.3LiRPA Algorithms

This section reproduces the formal machinery for linear relaxation based perturbation analysis \(LiRPA\) from\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\), we refer the reader there for full definitions and proofs\.

#### A\.3\.1Neural Network Graphs

###### Definition 14\.

A*neural network graph*is a tupleG=\(V,E,\{hi\}i∈V\)G=\(V,E,\\\{h\_\{i\}\\\}\_\{i\\in V\}\)where\(V,E\)\(V,E\)is a directed acyclic graph with topologically ordered node setV=\{1,…,n\}V=\\\{1,\\ldots,n\\\}and edge setE⊆V×VE\\subseteq V\\times V, where\(i,j\)∈E\(i,j\)\\in Edenotes that the value atiiis an input tojj\. For eachi∈Vi\\in V, writeu⁡\(i\)=\{j:\(j,i\)∈E\}u\(i\)=\\\{j:\(j,i\)\\in E\\\}for the predecessors ofiianddi∈ℕd\_\{i\}\\in\\mathbb\{N\}for the output dimension ofii\. Each node carries a \(possibly nonlinear\) functionhih\_\{i\}taking the concatenated predecessor values as input and producing an output inℝdi\\mathbb\{R\}^\{d\_\{i\}\}\. We single out node11as the input node, withu⁡\(1\)=∅u\(1\)=\\emptysetandh1​\(𝐱\)=𝐱h\_\{1\}\(\\mathbf\{x\}\)=\\mathbf\{x\}, and nodennas the output node, so that evaluating the graph in topological order on input𝐱∈𝒳\\mathbf\{x\}\\in\\mathcal\{X\}yieldsπ⁡\(𝐱\)=hn\\pi\(\\mathbf\{x\}\)=h\_\{n\}\.

#### A\.3\.2Linear Relaxations of Nodes

LiRPA decomposes the global bounding problem into per\-node*local*linear relaxations, which are then composed across the graph\.

###### Definition 15\(Local Linear Relaxation\)\.

Fix a nodei∈Vi\\in Vwith predecessor values constrained to a hyperrectangle𝐯∈\[𝐯¯u⁡\(i\),𝐯¯u⁡\(i\)\]\\mathbf\{v\}\\in\[\\underline\{\\mathbf\{v\}\}\_\{u\(i\)\},\\overline\{\\mathbf\{v\}\}\_\{u\(i\)\}\]\. A*linear relaxation*ofhih\_\{i\}on this domain is a tuple\(A¯i,c¯i,A¯i,c¯i\)\(\\underline\{A\}\_\{i\},\\underline\{c\}\_\{i\},\\overline\{A\}\_\{i\},\\overline\{c\}\_\{i\}\), with matricesA¯i,A¯i\\underline\{A\}\_\{i\},\\overline\{A\}\_\{i\}and vectorsc¯i,c¯i\\underline\{c\}\_\{i\},\\overline\{c\}\_\{i\}of dimensions matching the input and output ofhih\_\{i\}, satisfying, componentwise,

∀𝐯∈\[𝐯¯u⁡\(i\),𝐯¯u⁡\(i\)\]\.A¯i​𝐯\+c¯i≤hi​\(𝐯\)≤A¯i​𝐯\+c¯i\.\\forall\\mathbf\{v\}\\in\[\\underline\{\\mathbf\{v\}\}\_\{u\(i\)\},\\overline\{\\mathbf\{v\}\}\_\{u\(i\)\}\]\.\\quad\\underline\{A\}\_\{i\}\\mathbf\{v\}\+\\underline\{c\}\_\{i\}\\;\\leq\\;h\_\{i\}\(\\mathbf\{v\}\)\\;\\leq\\;\\overline\{A\}\_\{i\}\\mathbf\{v\}\+\\overline\{c\}\_\{i\}\.For affinehi​\(𝐯\)=W​𝐯\+bh\_\{i\}\(\\mathbf\{v\}\)=W\\mathbf\{v\}\+bthe relaxation is*exact*:A¯i=A¯i=W\\underline\{A\}\_\{i\}=\\overline\{A\}\_\{i\}=Wandc¯i=c¯i=b\\underline\{c\}\_\{i\}=\\overline\{c\}\_\{i\}=b\. For nonlinearhih\_\{i\}\(e\.g\.𝖱𝖾𝖫𝖴\\mathsf\{ReLU\}, sigmoid, tanh\) the relaxation is sound but inexact, and is typically chosen to minimize area between the bounding hyperplanes given the interval\[𝐯¯u⁡\(i\),𝐯¯u⁡\(i\)\]\[\\underline\{\\mathbf\{v\}\}\_\{u\(i\)\},\\overline\{\\mathbf\{v\}\}\_\{u\(i\)\}\]\.

###### Proposition 3\(Bound Propagation\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\)\)\.

Given a neural network graphπ\\pi, with neural graphGG, an input set𝐗⊆𝒳\\mathbf\{X\}\\subseteq\\mathcal\{X\}, and a local linear relaxation at each nonlinear node, LiRPA computes matrices𝐖¯o,𝐖¯o\\underline\{\\mathbf\{W\}\}\_\{o\},\\overline\{\\mathbf\{W\}\}\_\{o\}and vectors𝐛¯o,𝐛¯o\\underline\{\\mathbf\{b\}\}\_\{o\},\\overline\{\\mathbf\{b\}\}\_\{o\}such that

∀𝐱∈𝐗\.𝐖¯o​𝐱\+𝐛¯o≤π⁡\(𝐱\)≤𝐖¯o​𝐱\+𝐛¯o\.\\forall\\mathbf\{x\}\\in\\mathbf\{X\}\.\\quad\\underline\{\\mathbf\{W\}\}\_\{o\}\\mathbf\{x\}\+\\underline\{\\mathbf\{b\}\}\_\{o\}\\;\\leq\\;\\pi\(\\mathbf\{x\}\)\\;\\leq\\;\\overline\{\\mathbf\{W\}\}\_\{o\}\\mathbf\{x\}\+\\overline\{\\mathbf\{b\}\}\_\{o\}\.The bounds are computed by forward or backward propagation through the graph and admit efficient GPU implementation\.

We refer the reader to\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\)for details\.

#### A\.3\.3Concretization onℓp\\ell\_\{p\}Input Sets

When𝐗=\{𝐱:‖𝐱−𝐱0‖p≤ϵ\}\\mathbf\{X\}=\\\{\\mathbf\{x\}:\\\|\\mathbf\{x\}\-\\mathbf\{x\}\_\{0\}\\\|\_\{p\}\\leq\\epsilon\\\}is anℓp\\ell\_\{p\}\-ball, scalar \(componentwise\) bounds onπ⁡\(𝐱\)\\pi\(\\mathbf\{x\}\)follow from the linear bounds via Hölder’s inequality:

max𝐱∈𝐗⁡𝐖¯o​𝐱\+𝐛¯o=𝐖¯o​𝐱0\+ϵ​‖𝐖¯o‖q,row\+𝐛¯o,1p\+1q=1,\\max\_\{\\mathbf\{x\}\\in\\mathbf\{X\}\}\\overline\{\\mathbf\{W\}\}\_\{o\}\\mathbf\{x\}\+\\overline\{\\mathbf\{b\}\}\_\{o\}\\;=\\;\\overline\{\\mathbf\{W\}\}\_\{o\}\\mathbf\{x\}\_\{0\}\+\\epsilon\\,\\\|\\overline\{\\mathbf\{W\}\}\_\{o\}\\\|\_\{q,\\text\{row\}\}\+\\overline\{\\mathbf\{b\}\}\_\{o\},\\quad\\tfrac\{1\}\{p\}\+\\tfrac\{1\}\{q\}=1,where∥⋅∥q,row\\\|\\cdot\\\|\_\{q,\\text\{row\}\}denotes row\-wise dual norm\. This avoids any explicit optimization over𝐗\\mathbf\{X\}\.

#### A\.3\.4Optimizable Relaxations \(α\\alpha\-CROWN\)

For piecewise\-linear activations such as𝖱𝖾𝖫𝖴\\mathsf\{ReLU\}, the lower relaxation admits a free slope parameter per unstable neuron, which we collect into a vectorα∈\[0,1\]k\\alpha\\in\[0,1\]^\{k\}\. Each choice ofα\\alphayields a sound bound\. Tighter bounds are obtained by maximizing the lower bound \(resp\. minimizing the upper bound\) overα\\alphavia projected gradient ascent/descent\. The resulting tightened bounds are competitive with LP\-relaxation\-based verifiers while admitting efficient GPU implementation\. We refer to this scheme asα\\alpha\-CROWN\.

### A\.4Branching for Neural Network Verification

This section provides background on branch\-and\-bound \(BaB\) for neural network verification\. We refer the reader to\([Bunel et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib3);[De Palma et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib5);[Wang et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib19)\)for full treatments\.

The bounds produced by LiRPA \([Proposition3](https://arxiv.org/html/2609.16298#Thmproposition3)\) are sound but inexact, and may be too loose to certify a property of interest over𝐗\\mathbf\{X\}\. Branch\-and\-bound addresses this by partitioning𝐗\\mathbf\{X\}\(or the network’s internal activations\) into subdomains on which LiRPA produces tighter bounds, and recursing until each subdomain is either verified or a counterexample is found\.

###### Definition 16\(Branch\-and\-Bound for NN Verification\)\.

Given a networkπ\\pi, an input set𝐗\\mathbf\{X\}, and a propertyφ\\varphito verify, BaB maintains a set of subproblems𝒟=\{D1,D2,…\}\\mathcal\{D\}=\\\{D\_\{1\},D\_\{2\},\\ldots\\\}initialized with𝒟=\{⟨𝐗,∅⟩\}\\mathcal\{D\}=\\\{\\langle\\mathbf\{X\},\\emptyset\\rangle\\\}, where each subproblemD=⟨X,𝒩⟩D=\\langle X,\\mathcal\{N\}\\ranglepairs a subsetX⊆𝐗X\\subseteq\\mathbf\{X\}with a set𝒩\\mathcal\{N\}of fixed activation patterns\. At each iteration, BaB selects a subproblemD∈𝒟D\\in\\mathcal\{D\}, computes bounds onπ\\pioverDDusing a sound bounding procedure \(e\.g\. LiRPA\), and either \(i\) resolvesDDif the bounds verify or falsifyφ\\varphi, or \(ii\) splitsDDinto subdomains via a*branching heuristic*and adds them to𝒟\\mathcal\{D\}\. The procedure terminates when𝒟\\mathcal\{D\}is empty \(verified\) or a counterexample is found \(falsified\)\.

Splits fall into two families\.*Input splits*partition the input set𝐗\\mathbf\{X\}directly, typically by bisecting along a chosen input dimension\.*Neuron splits*fix the activation pattern of a chosen ReLU \(i\.e\., constrain its pre\-activation to be either nonnegative or nonpositive\), which tightens the network’s relaxation on that subdomain\. The choice of which dimension or neuron to split on is the branching heuristic\.

#### A\.4\.1Sound Neuron Splits \(β\\beta\-CROWN\)

A neuron split imposes a linear constraint on a pre\-activation, which a naive LiRPA pass cannot exploit since it bounds each neuron independently\.β\\beta\-CROWN\([Wang et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib19)\)extends LiRPA with per\-neuron split constraints using Lagrangians\. Each split constraint contributes a multiplierβ≥0\\beta\\geq 0that modifies the backward propagation rules at the constrained neuron\. For any choice ofβ≥0\\beta\\geq 0, the resulting bounds are sound, but tighter bounds can be obtained by jointly optimizingα\\alphaandβ\\betausing projected gradient methods in a manner analogous toα\\alpha\-CROWN\. The procedure can be run in parallel across subdomains in𝒟\\mathcal\{D\}, which makes GPU enabled BaB withβ\\beta\-CROWN as the bounding oracle the basis of state\-of\-the\-art complete verifiers\.

#### A\.4\.2Input Split Heuristics

##### BaBLL \(Longest Length,\([Bunel et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib3)\)\)\.

The simplest input splitting heuristic is to bisect along the input dimension with the largest current width,arg⁡maxj⁡\(x¯j−x¯j\)\\arg\\max\_\{j\}\(\\overline\{x\}\_\{j\}\-\\underline\{x\}\_\{j\}\), where\[x¯,x¯\]\[\\underline\{x\},\\overline\{x\}\]is the bounding box of the current subdomain\. This heuristic is cheap to compute and dimension\-agnostic, but ignores how the network depends on each input\.

##### BaBSB \(Smart Branching,\([Bunel et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib3)\)\)\.

This heuristic scores each input dimensionjjusing cheap estimates of expected bound improvement from splitting alongjj, and branches on the dimension with the highest score\. The estimate typically uses the bound coefficients already computed by LiRPA on the current subdomain, thereby weighting each dimension by its sensitivity in the current bound\.

#### A\.4\.3Neuron Split Heuristics

##### BaBSR \(Smart ReLU\([Bunel et al\. 2020](https://arxiv.org/html/2609.16298#bib.bib3)\)\)\.

Similar to BaBSB, this heuristic assigns each unstable ReLU a score based on a cheap estimate of the objective improvement after splitting it, and selects the neuron with the highest score\. BaBSR is cheap but its scores are coarse approximations of the true post\-split improvement\.

##### FSB \(Filtered Smart Branching\)\([De Palma et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib5)\)\.

This heuristic was designed to mimic strong branching on a filtered shortlist\. It uses BaBSR to propose a small set of promising candidates, and computes bounds \(using a LiRPA pass\) to select the candidate yielding the greatest bound improvement\. FSB produces higher\-quality splits than BaBSR at greater per\-step cost\.

##### k\-FSB\.

This heuristic parametrizes FSB using the shortlist sizekkAs implemented inα,β\\alpha,\\beta\-CROWN\([Wang et al\. 2021](https://arxiv.org/html/2609.16298#bib.bib19)\), BaBSR proposes the topkkcandidates and an FSB\-style heuristic selects among them\. Smaller values ofkkrecover behavior closer to BaBSR, while larger values ofkkapproach full FSB\. In practicekk\-FSB with smallkktrades a small amount of branching quality for substantially lower per\-step cost, and is the default branching heuristic inα,β\\alpha,\\beta\-CROWN\.

##### BBPS \(Propagation with Shortcuts\)\([Shi et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib16)\)\.

This heuristic generalizes FSB\-style scoring to non\-ReLU nonlinearities\. Rather than relying on ReLU\-specific bound estimates, it uses linear bounds propagated from the candidate split node directly to the input as a shortcut for estimating post\-split improvement, thereby making branching tractable for networks with general nonlinearities \(Sigmoid, Tanh, GeLU, etc\.\)\.

## Appendix BAuxiliary Results

### B\.1Triangulating Grids

#### B\.1\.1Delaunay Cell Containment

###### Lemma 1\.

LetPPbe a grid inℝn\\mathbb\{R\}^\{n\}and letΔ\\Deltabe a Delaunay triangulation ofPP\. Everynn\-simplex ofΔ\\Deltais contained in some grid cell ofPP\.

###### Proof\.

Let𝒮∈Δ\\mathcal\{S\}\\in\\Deltabe annn\-simplex with circumcenterc∈ℝnc\\in\\mathbb\{R\}^\{n\}and circumradiusrr\. Its vertices lie at distancerrfromcc, and by the Delaunay empty\-circumsphere property, no point ofPPlies at distance less thanrrfromcc\. Hence the vertices of𝒮\\mathcal\{S\}are contained inN:=arg⁡minp∈P​‖p−c‖N:=\\arg\\min\_\{p\\in P\}\\\|p\-c\\\|\.

SinceP=G1×⋯×GnP=G\_\{1\}\\times\\cdots\\times G\_\{n\}, the squared distance‖p−c‖2=∑i\(pi−ci\)2\\\|p\-c\\\|^\{2\}=\\sum\_\{i\}\(p\_\{i\}\-c\_\{i\}\)^\{2\}separates by coordinate, soN=N1×⋯×NnN=N\_\{1\}\\times\\cdots\\times N\_\{n\}whereNi:=arg⁡minq∈Gi⁡\(q−ci\)2N\_\{i\}:=\\arg\\min\_\{q\\in G\_\{i\}\}\(q\-c\_\{i\}\)^\{2\}\. EachNiN\_\{i\}has size11or22, with size22exactly whencic\_\{i\}is the midpoint of two adjacent elements ofGiG\_\{i\}\. Letkkbe the number of coordinatesiifor which\|Ni\|=2\|N\_\{i\}\|=2\. Then\|N\|=2k\|N\|=2^\{k\}anddimaff​\(N\)=k\\dim\\textbf\{aff\}\(N\)=k, withk≤nk\\leq nsince there are onlynncoordinates\.

Then\+1n\+1affinely independent vertices of𝒮\\mathcal\{S\}lie inNN, sodimaff​\(vert​\(𝒮\)\)=n≤dimaff​\(N\)=k\\dim\\textbf\{aff\}\(\\textbf\{vert\}\(\\mathcal\{S\}\)\)=n\\leq\\dim\\textbf\{aff\}\(N\)=k, hencen=kn=k\. Thusccis the midpoint of an adjacent pair in every coordinate\. That is,ccis the center of some grid cell𝒞\\mathcal\{C\}, andNNis exactly the2n2^\{n\}corners of𝒞\\mathcal\{C\}\. Therefore𝒮⊆𝒞\\mathcal\{S\}\\subseteq\\mathcal\{C\}\. ∎

#### B\.1\.2No Crossing Grid Hyperplanes

###### Corollary 1\.

LetPPbe a grid inℝn\\mathbb\{R\}^\{n\}, letHHbe a grid hyperplane ofPP, and letΔ\\Deltabe a Delaunay triangulation ofPP\. Eachnn\-simplex ofΔ\\Deltais contained in one of the closed half\-spaces bounded byHH\.

###### Proof\.

By Lemma[1](https://arxiv.org/html/2609.16298#Thmlemma1), everynn\-simplex ofΔ\\Deltais contained in a single grid cell\. Each grid cell lies in one of the two closed half\-spaces bounded byHH, so the simplex does too, and hence does not crossHH\. ∎

#### B\.1\.3Splitting Delaunay Triangulations

###### Lemma 2\.

LetPPbe a grid inℝn\\mathbb\{R\}^\{n\}, letHHbe a grid hyperplane ofPP, and letP1,P2P\_\{1\},P\_\{2\}be the sub\-grids ofPPon the two closed sides ofHH\. LetΔ\\Deltabe a Delaunay triangulation ofPP, and letΔj:=\{𝒮∈Δ∣𝒮⊆conv​\(Pj\)\}\\Delta\_\{j\}:=\\\{\\mathcal\{S\}\\in\\Delta\\mid\\mathcal\{S\}\\subseteq\\textbf\{conv\}\(P\_\{j\}\)\\\}forj∈\{1,2\}j\\in\\\{1,2\\\}\. ThenΔ1\\Delta\_\{1\}andΔ2\\Delta\_\{2\}are Delaunay triangulations ofP1P\_\{1\}andP2P\_\{2\}, respectively\.

###### Proof\.

By definition,Pj=P∩H¯jP\_\{j\}=P\\cap\\overline\{H\}\_\{j\}for the closed half\-spacesH¯1,H¯2\\overline\{H\}\_\{1\},\\overline\{H\}\_\{2\}bounded byHH\. Consequentlyconv​\(Pj\)\\textbf\{conv\}\(P\_\{j\}\)is the union of the grid cells ofPPcontained inH¯j\\overline\{H\}\_\{j\}\.

Fix a grid cell𝒞⊆H¯j\\mathcal\{C\}\\subseteq\\overline\{H\}\_\{j\}, and letΔ𝒞:=\{𝒮∈Δ:𝒮⊆𝒞\}\\Delta\_\{\\mathcal\{C\}\}:=\\\{\\mathcal\{S\}\\in\\Delta:\\mathcal\{S\}\\subseteq\\mathcal\{C\}\\\}\. SinceΔ\\Deltatriangulatesconv​\(P\)⊇𝒞\\textbf\{conv\}\(P\)\\supseteq\\mathcal\{C\}, the cell𝒞\\mathcal\{C\}is covered by simplices ofΔ\\Delta\. By Lemma[1](https://arxiv.org/html/2609.16298#Thmlemma1), each such simplex lies in a single grid cell, and since grid cells have pairwise\-disjoint interiors, any simplex with interior points in𝒞\\mathcal\{C\}must be contained in𝒞\\mathcal\{C\}\. Hence the simplices covering the interior of𝒞\\mathcal\{C\}all belong toΔ𝒞\\Delta\_\{\\mathcal\{C\}\}, and⋃𝒮∈Δ𝒞𝒮\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\_\{\\mathcal\{C\}\}\}\\mathcal\{S\}is a closed set containing the interior of𝒞\\mathcal\{C\}, hence containing𝒞\\mathcal\{C\}\. The corners of𝒞\\mathcal\{C\}lie inPjP\_\{j\}, soΔ𝒞⊆Δj\\Delta\_\{\\mathcal\{C\}\}\\subseteq\\Delta\_\{j\}, and𝒞⊆⋃𝒮∈Δj𝒮\\mathcal\{C\}\\subseteq\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\_\{j\}\}\\mathcal\{S\}\. Taking the union over cells,Δj\\Delta\_\{j\}is a triangulation ofPjP\_\{j\}\.

Each𝒮∈Δj⊆Δ\\mathcal\{S\}\\in\\Delta\_\{j\}\\subseteq\\Deltahas empty open circumball with respect toPP, hence with respect toPj⊆PP\_\{j\}\\subseteq P\. SoΔj\\Delta\_\{j\}is a Delaunay triangulation ofPjP\_\{j\}\. ∎

### B\.2Proofs of Technical Claims

#### B\.2\.1Theorem 1

##### Statement\.

Ifffis enclosed byBB, then for any𝐚L,𝐚U∈ℝn\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\\in\\mathbb\{R\}^\{n\}, any𝐱∈conv​\(P\)\\mathbf\{x\}\\in\\textbf\{conv\}\(P\), and any Delaunay triangulationΔ\\DeltaofPP,L□​\(𝐱\)≤LΔ​\(𝐱\)≤f⁡\(𝐱\)≤UΔ​\(𝐱\)≤U□​\(𝐱\)L\_\{\\square\}\(\\mathbf\{x\}\)\\leq L\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq f\(\\mathbf\{x\}\)\\leq U\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq U\_\{\\square\}\(\\mathbf\{x\}\)\.

###### Proof\.

Begin by considering the vertices𝐩∈P\\mathbf\{p\}\\in P\. For any𝐩∈P\\mathbf\{p\}\\in P,L□​\(𝐩\)=𝐚L⋅𝐩\+bLL\_\{\\square\}\(\\mathbf\{p\}\)=\\mathbf\{a\}\_\{L\}\\cdot\\mathbf\{p\}\+b\_\{L\}\. SincebLb\_\{L\}is defined as the minimum,L□​\(𝐩\)≤𝐚L⋅𝐩\+\(L⁡\(𝐩\)−𝐚L⋅𝐩\)L\_\{\\square\}\(\\mathbf\{p\}\)\\leq\\mathbf\{a\}\_\{L\}\\cdot\\mathbf\{p\}\+\(L\(\\mathbf\{p\}\)\-\\mathbf\{a\}\_\{L\}\\cdot\\mathbf\{p\}\)\. Simplifying yieldsL□​\(𝐩\)≤L⁡\(𝐩\)L\_\{\\square\}\(\\mathbf\{p\}\)\\leq L\(\\mathbf\{p\}\)\. Note that this holds for any𝐚L\\mathbf\{a\}\_\{L\}\.

Now consider𝐱∈conv​\(P\)\\mathbf\{x\}\\in\\textbf\{conv\}\(P\)\. Let𝒮=𝒮Δ​\(𝐱\)\\mathcal\{S\}=\\mathcal\{S\}\_\{\\Delta\}\(\\mathbf\{x\}\)be a simplex inΔ\\Deltacontaining𝐱\\mathbf\{x\}\. LetV=\(v0,v1,…,vn\)V=\(v\_\{0\},v\_\{1\},\\ldots,v\_\{n\}\)denote the vertices of𝒮\\mathcal\{S\}, andθ=θΔ​\(𝐱\)\\theta=\\theta\_\{\\Delta\}\(\\mathbf\{x\}\)denote barycentric coordinates such that𝐱=θ⋅V\\mathbf\{x\}=\\theta\\cdot V\. Then by definition,L𝒮​\(𝐱\)=θ⋅L⁡\(V\)L\_\{\\mathcal\{S\}\}\(\\mathbf\{x\}\)=\\theta\\cdot L\(V\), whereL𝒮L\_\{\\mathcal\{S\}\}is the restriction ofLΔL\_\{\\Delta\}to𝒮\\mathcal\{S\}\. SinceL□L\_\{\\square\}is affine,L□​\(𝐱\)=θ⋅L□​\(V\)L\_\{\\square\}\(\\mathbf\{x\}\)=\\theta\\cdot L\_\{\\square\}\(V\)\. But from the previous paragraph, we know thatL□​\(vi\)≤L⁡\(vi\)L\_\{\\square\}\(v\_\{i\}\)\\leq L\(v\_\{i\}\)for allvi∈Vv\_\{i\}\\in V\(since eachvi∈Pv\_\{i\}\\in P\)\. ThereforeL□​\(𝐱\)≤L𝒮​\(𝐱\)=LΔ​\(𝐱\)L\_\{\\square\}\(\\mathbf\{x\}\)\\leq L\_\{\\mathcal\{S\}\}\(\\mathbf\{x\}\)=L\_\{\\Delta\}\(\\mathbf\{x\}\)\. The soundness of the upper bound follows from symmetry, and the middle inequalitiesLΔ​\(𝐱\)≤f⁡\(𝐱\)≤UΔ​\(𝐱\)L\_\{\\Delta\}\(\\mathbf\{x\}\)\\leq f\(\\mathbf\{x\}\)\\leq U\_\{\\Delta\}\(\\mathbf\{x\}\)are precisely the hypothesis thatffis enclosed byBB\. ∎

#### B\.2\.2Theorem 2

##### Statement\.

LetBBbe a bounding set, letHHbe a grid hyperplane ofPP, and letB1,B2B^\{1\},B^\{2\}be the refinements ofBBalongHH\. LetΔ\\Deltabe a Delaunay triangulation ofPP, and let

Δj≔\{𝒮∈Δ∣𝒮⊆conv​\(Pj\)\}for​j∈\{1,2\}\.\\Delta\_\{j\}\\coloneqq\\\{\\mathcal\{S\}\\in\\Delta\\mid\\mathcal\{S\}\\subseteq\\textbf\{conv\}\(P\_\{j\}\)\\\}\\quad\\text\{for \}j\\in\\\{1,2\\\}\.EachΔj\\Delta\_\{j\}is a Delaunay triangulation ofPjP\_\{j\}by the Delaunay splitting lemma \(see Appendix[B\.1\.3](https://arxiv.org/html/2609.16298#A2.SS1.SSS3)\)\. Then:

1. 1\.\(Unrelaxed\.\)ℰ⁡\(B1,Δ1\)∪ℰ⁡\(B2,Δ2\)=ℰ⁡\(B,Δ\)\\mathcal\{E\}\(B^\{1\},\\Delta\_\{1\}\)\\cup\\mathcal\{E\}\(B^\{2\},\\Delta\_\{2\}\)=\\mathcal\{E\}\(B,\\Delta\)\.
2. 2\.\(Relaxed\.\)Let𝐚L,𝐚U∈ℝn\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\\in\\mathbb\{R\}^\{n\}, letB□B\_\{\\square\}andB□jB\_\{\\square\}^\{j\}be the relaxations ofBBandBjB^\{j\}with the same parameters\(𝐚L,𝐚U\)\(\\mathbf\{a\}\_\{L\},\\mathbf\{a\}\_\{U\}\), and letbLj,bUjb\_\{L\}^\{j\},b\_\{U\}^\{j\}denote the offsets ofB□jB\_\{\\square\}^\{j\}\. For any Delaunay triangulationsΔ□\\Delta\_\{\\square\}ofP□P\_\{\\square\}andΔ□j\\Delta\_\{\\square\}^\{j\}ofP□jP\_\{\\square\}^\{j\}, ℰ⁡\(B□1,Δ□1\)∪ℰ⁡\(B□2,Δ□2\)⊆ℰ⁡\(B□,Δ□\),\\mathcal\{E\}\(B\_\{\\square\}^\{1\},\\Delta\_\{\\square\}^\{1\}\)\\cup\\mathcal\{E\}\(B\_\{\\square\}^\{2\},\\Delta\_\{\\square\}^\{2\}\)\\subseteq\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\),with strict containment whenever\(bLj,bUj\)≠\(bL,bU\)\(b\_\{L\}^\{j\},b\_\{U\}^\{j\}\)\\neq\(b\_\{L\},b\_\{U\}\)for somej∈\{1,2\}j\\in\\\{1,2\\\}\.

###### Proof\.

LetΔn⊆Δ\\Delta\_\{n\}\\subseteq\\Deltadenote the set ofnn\-simplices ofΔ\\Delta\. By Delaunay Cell Containment \(Appendix[B\.1\.1](https://arxiv.org/html/2609.16298#A2.SS1.SSS1)\), everynn\-simplex ofΔ\\Deltais contained in a grid cell ofPP\. Each grid cell lies on one side of any grid hyperplane, hence in eitherconv​\(P1\)\\textbf\{conv\}\(P\_\{1\}\)orconv​\(P2\)\\textbf\{conv\}\(P\_\{2\}\), so everynn\-simplex ofΔ\\Deltadoes too\. Annn\-simplex contained in both halves would lie inconv​\(P1\)∩conv​\(P2\)⊆H\\textbf\{conv\}\(P\_\{1\}\)\\cap\\textbf\{conv\}\(P\_\{2\}\)\\subseteq H, contradicting its dimension\. ThereforeΔn=Δ1,n⊔Δ2,n\\Delta\_\{n\}=\\Delta\_\{1,n\}\\sqcup\\Delta\_\{2,n\}, whereΔj,n:=Δn∩Δj\\Delta\_\{j,n\}:=\\Delta\_\{n\}\\cap\\Delta\_\{j\}\.

\(Unrelaxed\.\)For𝒮∈Δn\\mathcal\{S\}\\in\\Delta\_\{n\}, letB\|𝒮B\|\_\{\\mathcal\{S\}\}denote the restriction ofBBtovert​\(𝒮\)\\textbf\{vert\}\(\\mathcal\{S\}\), and let𝒫⁡\(B\|𝒮\)\\mathcal\{P\}\(B\|\_\{\\mathcal\{S\}\}\)denote the polyhedron formed byB\|𝒮B\|\_\{\\mathcal\{S\}\}\. Thenℰ⁡\(B,Δ\)=⋃𝒮∈Δn𝒫⁡\(B\|𝒮\)\\mathcal\{E\}\(B,\\Delta\)=\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\_\{n\}\}\\mathcal\{P\}\(B\|\_\{\\mathcal\{S\}\}\)\. For𝒮∈Δj,n\\mathcal\{S\}\\in\\Delta\_\{j,n\}, the vertices of𝒮\\mathcal\{S\}also lie inPjP\_\{j\}, soB\|𝒮=Bj\|𝒮B\|\_\{\\mathcal\{S\}\}=B^\{j\}\|\_\{\\mathcal\{S\}\}\. Therefore

ℰ⁡\(B,Δ\)=⋃𝒮∈Δn𝒫⁡\(B\|𝒮\)=⋃j∈\{1,2\}⋃𝒮∈Δj,n𝒫⁡\(Bj\|𝒮\)=ℰ⁡\(B1,Δ1\)∪ℰ⁡\(B2,Δ2\)\.\\mathcal\{E\}\(B,\\Delta\)=\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\_\{n\}\}\\mathcal\{P\}\(B\|\_\{\\mathcal\{S\}\}\)=\\bigcup\_\{j\\in\\\{1,2\\\}\}\\bigcup\_\{\\mathcal\{S\}\\in\\Delta\_\{j,n\}\}\\mathcal\{P\}\(B^\{j\}\|\_\{\\mathcal\{S\}\}\)\\\\ =\\mathcal\{E\}\(B^\{1\},\\Delta\_\{1\}\)\\cup\\mathcal\{E\}\(B^\{2\},\\Delta\_\{2\}\)\.
\(Relaxed\.\)SinceB□B\_\{\\square\}replacesL,UL,Uwith the affine functionsL□,U□L\_\{\\square\},U\_\{\\square\}, the lower and upper surfaces ofℰ⁡\(B□,Δ□\)\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\)areL□,U□L\_\{\\square\},U\_\{\\square\}onconv​\(P□\)=conv​\(P\)\\textbf\{conv\}\(P\_\{\\square\}\)=\\textbf\{conv\}\(P\)independently ofΔ□\\Delta\_\{\\square\}\. Hence

ℰ\(B□,Δ□\)=\{\(𝐱,y\)∈ℝn×ℝ∣𝐱∈conv\(P\),L□\(𝐱\)≤y≤U□\(𝐱\)\},\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\)=\\\{\(\\mathbf\{x\},y\)\\in\\mathbb\{R\}^\{n\}\\times\\mathbb\{R\}\\mid\\mathbf\{x\}\\in\\textbf\{conv\}\(P\),\\\\ L\_\{\\square\}\(\\mathbf\{x\}\)\\leq y\\leq U\_\{\\square\}\(\\mathbf\{x\}\)\\\},and analogously

ℰ\(B□j,Δ□j\)=\{\(𝐱,y\)∣𝐱∈conv\(Pj\),L□j\(𝐱\)≤y≤U□j\(𝐱\)\}\.\\mathcal\{E\}\(B\_\{\\square\}^\{j\},\\Delta\_\{\\square\}^\{j\}\)=\\\{\(\\mathbf\{x\},y\)\\mid\\mathbf\{x\}\\in\\textbf\{conv\}\(P\_\{j\}\),\\\\ L\_\{\\square\}^\{j\}\(\\mathbf\{x\}\)\\leq y\\leq U\_\{\\square\}^\{j\}\(\\mathbf\{x\}\)\\\}\.SincePj⊆PP\_\{j\}\\subseteq P,bLj=minp∈Pj⁡\(L⁡\(p\)−𝐚L⋅p\)≥minp∈P⁡\(L⁡\(p\)−𝐚L⋅p\)=bLb\_\{L\}^\{j\}=\\min\_\{p\\in P\_\{j\}\}\(L\(p\)\-\\mathbf\{a\}\_\{L\}\\cdot p\)\\geq\\min\_\{p\\in P\}\(L\(p\)\-\\mathbf\{a\}\_\{L\}\\cdot p\)=b\_\{L\}\. A symmetric argument yieldsbUj≤bUb\_\{U\}^\{j\}\\leq b\_\{U\}\. Combined withconv​\(Pj\)⊆conv​\(P\)\\textbf\{conv\}\(P\_\{j\}\)\\subseteq\\textbf\{conv\}\(P\), this givesℰ⁡\(B□j,Δ□j\)⊆ℰ⁡\(B□,Δ□\)\\mathcal\{E\}\(B\_\{\\square\}^\{j\},\\Delta\_\{\\square\}^\{j\}\)\\subseteq\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\)forj∈\{1,2\}j\\in\\\{1,2\\\}, henceℰ⁡\(B□1,Δ□1\)∪ℰ⁡\(B□2,Δ□2\)⊆ℰ⁡\(B□,Δ□\)\\mathcal\{E\}\(B\_\{\\square\}^\{1\},\\Delta\_\{\\square\}^\{1\}\)\\cup\\mathcal\{E\}\(B\_\{\\square\}^\{2\},\\Delta\_\{\\square\}^\{2\}\)\\subseteq\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\)\.

For strict containment, supposebLj\>bLb\_\{L\}^\{j\}\>b\_\{L\}for somej∈\{1,2\}j\\in\\\{1,2\\\}\(the casebUj<bUb\_\{U\}^\{j\}<b\_\{U\}is symmetric\)\. Pick𝐱∗\\mathbf\{x\}^\{\*\}in the interior ofconv​\(Pj\)\\textbf\{conv\}\(P\_\{j\}\)and lety∗=L□​\(𝐱∗\)y^\{\*\}=L\_\{\\square\}\(\\mathbf\{x\}^\{\*\}\)\. Then\(𝐱∗,y∗\)∈ℰ⁡\(B□,Δ□\)\(\\mathbf\{x\}^\{\*\},y^\{\*\}\)\\in\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\), with the lower\-bound inequality holding by construction and the upper\-bound inequality sinceL□≤L≤U≤U□L\_\{\\square\}\\leq L\\leq U\\leq U\_\{\\square\}onPPgivesL□≤U□L\_\{\\square\}\\leq U\_\{\\square\}onconv​\(P\)\\textbf\{conv\}\(P\)by affinity\. Buty∗<L□j​\(𝐱∗\)y^\{\*\}<L\_\{\\square\}^\{j\}\(\\mathbf\{x\}^\{\*\}\)rules out\(𝐱∗,y∗\)∈ℰ⁡\(B□j,Δ□j\)\(\\mathbf\{x\}^\{\*\},y^\{\*\}\)\\in\\mathcal\{E\}\(B\_\{\\square\}^\{j\},\\Delta\_\{\\square\}^\{j\}\), and𝐱∗\\mathbf\{x\}^\{\*\}being interior toconv​\(Pj\)\\textbf\{conv\}\(P\_\{j\}\)rules out𝐱∗∈conv​\(Pj′\)\\mathbf\{x\}^\{\*\}\\in\\textbf\{conv\}\(P\_\{j^\{\\prime\}\}\)forj′≠jj^\{\\prime\}\\neq j\. Therefore\(𝐱∗,y∗\)∈ℰ⁡\(B□,Δ□\)∖\(ℰ⁡\(B□1,Δ□1\)∪ℰ⁡\(B□2,Δ□2\)\)\(\\mathbf\{x\}^\{\*\},y^\{\*\}\)\\in\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\)\\setminus\\big\(\\mathcal\{E\}\(B\_\{\\square\}^\{1\},\\Delta\_\{\\square\}^\{1\}\)\\cup\\mathcal\{E\}\(B\_\{\\square\}^\{2\},\\Delta\_\{\\square\}^\{2\}\)\\big\), so the union is a proper subset ofℰ⁡\(B□,Δ□\)\\mathcal\{E\}\(B\_\{\\square\},\\Delta\_\{\\square\}\)\. ∎

#### B\.2\.3Proposition 1

##### Statement\.

Let𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}have a BART relaxation at each RAIL node and a LiRPA relaxation at each nonlinear node in everyπ\(t\)\\pi^\{\(t\)\}\. Then any RAIL evaluation of𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}over𝐈×𝐄T\\mathbf\{I\}\\times\\mathbf\{E\}^\{T\}produces linear bounds on𝐱t\\mathbf\{x\}\_\{t\}that, when concretized, sound\-overapproximateτ𝒟​\(𝐈\)t\\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\mathbf\{I\}\)\_\{t\}for everyt∈\[0\.\.T\]t\\in\[0\.\.T\]\.

###### Proof\.

By[Definition3](https://arxiv.org/html/2609.16298#Thmdefinition3), the timettsubgraph of𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}realizes𝑛𝑒𝑥𝑡𝒟\\mathit\{next\}^\{\\mathcal\{D\}\}as a function of\(xt,ϵt\)\(x\_\{t\},\\epsilon\_\{t\}\), and chaining the subgraphs through state nodesx1,…,xTx\_\{1\},\\ldots,x\_\{T\}realizesτ𝒟\\mathit\{\\tau\}^\{\\mathcal\{D\}\}on𝐈×𝐄T\\mathbf\{I\}\\times\\mathbf\{E\}^\{T\}\.

BART relaxations at enclosure nodes are sound by[Theorem1](https://arxiv.org/html/2609.16298#Thmtheorem1), LiRPA relaxations at nonlinear nodes in eachπ\(t\)\\pi^\{\(t\)\}are sound by[Proposition3](https://arxiv.org/html/2609.16298#Thmproposition3), and the affine layer is exact\. Composition of per\-node linear bounds through the graph yields linear bounds onxtx\_\{t\}\(the LiRPA framework, applied to the directed acyclic structure of𝒢T𝒟\\mathcal\{G\}^\{\\mathcal\{D\}\}\_\{T\}\([Xu et al\. 2020a](https://arxiv.org/html/2609.16298#bib.bib20)\)\)\. Concretization of these bounds over𝐈×𝐄T\\mathbf\{I\}\\times\\mathbf\{E\}^\{T\}yields a set𝐱^t⊇𝐱t=τ𝒟​\(𝐈\)t\\hat\{\\mathbf\{x\}\}\_\{t\}\\supseteq\\mathbf\{x\}\_\{t\}=\\mathit\{\\tau\}^\{\\mathcal\{D\}\}\(\\mathbf\{I\}\)\_\{t\}for everyt∈\[0\.\.T\]t\\in\[0\.\.T\]\. ∎

#### B\.2\.4Proposition 2

##### Statement\.

Let𝐗^0,…,𝐗^T\\hat\{\\mathbf\{X\}\}\_\{0\},\\ldots,\\hat\{\\mathbf\{X\}\}\_\{T\}satisfy𝐗^t⊇𝐗t\\hat\{\\mathbf\{X\}\}\_\{t\}\\supseteq\\mathbf\{X\}\_\{t\}for allt∈\[0\.\.T\]t\\in\[0\.\.T\]\. If𝐗^t∩𝐀⁡\(t\)=∅\\hat\{\\mathbf\{X\}\}\_\{t\}\\cap\\mathbf\{A\}\(t\)=\\emptysetfor allttand𝐗^t∗⊆𝐆\\hat\{\\mathbf\{X\}\}\_\{t^\{\*\}\}\\subseteq\\mathbf\{G\}for somet∗∈\[0\.\.T\]t^\{\*\}\\in\[0\.\.T\], then𝒟\\mathcal\{D\}is safe\.

###### Proof\.

For eacht∈\[0\.\.T\]t\\in\[0\.\.T\],𝐗t⊆𝐗^t\\mathbf\{X\}\_\{t\}\\subseteq\\hat\{\\mathbf\{X\}\}\_\{t\}, so𝐗t∩𝐀⁡\(t\)⊆𝐗^t∩𝐀⁡\(t\)=∅\\mathbf\{X\}\_\{t\}\\cap\\mathbf\{A\}\(t\)\\subseteq\\hat\{\\mathbf\{X\}\}\_\{t\}\\cap\\mathbf\{A\}\(t\)=\\emptyset, satisfying \([3](https://arxiv.org/html/2609.16298#Sx2.E3)\)\. Similarly,𝐗t∗⊆𝐗^t∗⊆𝐆\\mathbf\{X\}\_\{t^\{\*\}\}\\subseteq\\hat\{\\mathbf\{X\}\}\_\{t^\{\*\}\}\\subseteq\\mathbf\{G\}, satisfying \([2](https://arxiv.org/html/2609.16298#Sx2.E2)\)\. ∎

## Appendix CExperimental Setup

### C\.1Benchmarks

We evaluate all tools on the nine ARCH\-COMP 2025 AINNCS benchmarks\([Manzanas Lopez et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib14)\)\. The benchmarks were originally specified in continuous time\. Following the guidance of the organizers, we obtain a discrete\-time neural feedback system by forward Euler integration with stepδ\\delta\. For each benchmark we give a brief description, the tuple⟨m,n,𝐈,𝐅,𝐄,𝐮,B,δ,T,𝐆,𝐀⟩\\langle m,n,\\mathbf\{I\},\\mathbf\{F\},\\mathbf\{E\},\\mathbf\{u\},B,\\delta,T,\\mathbf\{G\},\\mathbf\{A\}\\rangle, and the reach\-avoid specification\. Where the controller acts on preprocessed features \(e\.g\. relative distances\) or outputs \(e\.g\.π⁡\(𝐱\)−10\\pi\(\\mathbf\{x\}\)\-10\), we fold these transforms into𝐮\\mathbf\{u\}, so that𝐮:ℝn→ℝm\\mathbf\{u\}:\\mathbb\{R\}^\{n\}\\to\\mathbb\{R\}^\{m\}maps the full state to the applied control andBBrecords only which coordinates the control drives\.

##### Adaptive Cruise Control \(ACC\)\.

An ego vehicle tracks a set speed while maintaining a safe distance from a lead vehicle that brakes abruptly\. The state𝐱=\(xl,vl,al,xe,ve,ae\)\\mathbf\{x\}=\(x\_\{l\},v\_\{l\},a\_\{l\},x\_\{e\},v\_\{e\},a\_\{e\}\)collects the position, velocity, and acceleration of the lead \(ll\) and ego \(ee\) vehicles\. We haven=6n=6,m=1m=1, and

𝐅⁡\(𝐱\)=\(vl,al,−2​al−4−u​vl2,ve,ae,−2​ae−u​ve2\),\\mathbf\{F\}\(\\mathbf\{x\}\)=\\bigl\(v\_\{l\},\\;a\_\{l\},\\;\-2a\_\{l\}\-4\-uv\_\{l\}^\{2\},\\;v\_\{e\},\\;a\_\{e\},\\;\-2a\_\{e\}\-uv\_\{e\}^\{2\}\\bigr\),with drag coefficientu=10−4u=10^\{\-4\}and the constant lead decelerationac,l=−2a\_\{c,l\}=\-2folded into the third component\. The controller output enters the ego acceleration throughB=\(0,0,0,0,0,2\)⊤B=\(0,0,0,0,0,2\)^\{\\top\}\. The controller𝐮\\mathbf\{u\}is a five\-layer network of2020ReLU units per layer whose fixed affine input layer forms the features\(vset,Tgap,ve,xl−xe,vl−ve\)\(v\_\{\\text\{set\}\},T\_\{\\text\{gap\}\},v\_\{e\},x\_\{l\}\-x\_\{e\},v\_\{l\}\-v\_\{e\}\)from the state, with constantsvset=30v\_\{\\text\{set\}\}=30andTgap=1\.4T\_\{\\text\{gap\}\}=1\.4\. The remaining components are

𝐈=\[90,110\]×\[32,32\.2\]×\{0\}×\[10,11\]×\[30,30\.2\]×\{0\},\\mathbf\{I\}=\[90,110\]\\times\[32,32\.2\]\\times\\\{0\\\}\\times\[10,11\]\\times\[30,30\.2\]\\times\\\{0\\\},𝐄=\{0\}6\\mathbf\{E\}=\\\{0\\\}^\{6\},δ=0\.1\\delta=0\.1, andT=50T=50\(a55s window\)\.𝐆=ℝ6\\mathbf\{G\}=\\mathbb\{R\}^\{6\}and𝐀⁡\(t\)=\{𝐱:xl−xe<10\+1\.4​ve\}\\mathbf\{A\}\(t\)=\\\{\\mathbf\{x\}:x\_\{l\}\-x\_\{e\}<10\+1\.4\\,v\_\{e\}\\\}\.

##### TORA\.

A cart on a frictionless surface is stabilized by a rotational actuator\. The state𝐱=\(x1,x2,x3,x4\)\\mathbf\{x\}=\(x\_\{1\},x\_\{2\},x\_\{3\},x\_\{4\}\)collects the cart position, velocity, actuator angle, and angular velocity\. We haven=4n=4,m=1m=1, and

𝐅\(𝐱\)=\(x2,−x1\+0\.1sinx3,x4,0\)\.\\mathbf\{F\}\(\\mathbf\{x\}\)=\\bigl\(x\_\{2\},\\;\-x\_\{1\}\+0\.1\\sin x\_\{3\},\\;x\_\{4\},\\;0\\bigr\)\.The control enters the actuator throughB=\(0,0,0,1\)⊤B=\(0,0,0,1\)^\{\\top\}, and𝐄=\{0\}4\\mathbf\{E\}=\\\{0\\\}^\{4\}\. The benchmark provides three controllers, giving instances TORA 1–3 in[Table1](https://arxiv.org/html/2609.16298#Sx4.T1)\. TORA 1 \(*remain*\) uses a network with three hidden layers of100100ReLU units and a linear output, with𝐮=π⁡\(𝐱\)−10\\mathbf\{u\}=\\pi\(\\mathbf\{x\}\)\-10,δ=1\\delta=1,T=20T=20,𝐈=\[0\.6,0\.7\]×\[−0\.7,−0\.6\]×\[−0\.4,−0\.3\]×\[0\.5,0\.6\]\\mathbf\{I\}=\[0\.6,0\.7\]\\times\[\-0\.7,\-0\.6\]\\times\[\-0\.4,\-0\.3\]\\times\[0\.5,0\.6\],𝐆=ℝ4\\mathbf\{G\}=\\mathbb\{R\}^\{4\}, and𝐀⁡\(t\)=\{𝐱:𝐱∉\[−2,2\]4\}\\mathbf\{A\}\(t\)=\\\{\\mathbf\{x\}:\\mathbf\{x\}\\notin\[\-2,2\]^\{4\}\\\}\. TORA 2 \(*reach\-sigmoid*\) and TORA 3 \(*reach\-tanh*\) use networks with three hidden layers of2020units, the former with sigmoid activations and𝐮=22​π​\(𝐱\)−11\\mathbf\{u\}=22\\pi\(\\mathbf\{x\}\)\-11, the latter with ReLU activations and a tanh output and𝐮=11​π​\(𝐱\)\\mathbf\{u\}=11\\pi\(\\mathbf\{x\}\)\. The remaining parameters areδ=0\.5\\delta=0\.5,T=10T=10,𝐈=\[−0\.77,−0\.75\]×\[−0\.45,−0\.43\]×\[0\.51,0\.54\]×\[−0\.3,−0\.28\]\\mathbf\{I\}=\[\-0\.77,\-0\.75\]\\times\[\-0\.45,\-0\.43\]\\times\[0\.51,0\.54\]\\times\[\-0\.3,\-0\.28\],𝐆=\{𝐱:x1∈\[−0\.1,0\.2\],x2∈\[−0\.9,−0\.6\]\}\\mathbf\{G\}=\\\{\\mathbf\{x\}:x\_\{1\}\\in\[\-0\.1,0\.2\],\\,x\_\{2\}\\in\[\-0\.9,\-0\.6\]\\\}, and𝐀≡∅\\mathbf\{A\}\\equiv\\emptyset\.

##### Unicycle\.

A unicycle model of a car drives on a plane\. The state𝐱=\(x1,x2,x3,x4\)\\mathbf\{x\}=\(x\_\{1\},x\_\{2\},x\_\{3\},x\_\{4\}\)collects the planar position, heading, and speed\. We haven=4n=4,m=2m=2, and

𝐅\(𝐱\)=\(x4cosx3,x4sinx3,0,0\)\.\\mathbf\{F\}\(\\mathbf\{x\}\)=\\bigl\(x\_\{4\}\\cos x\_\{3\},\\;x\_\{4\}\\sin x\_\{3\},\\;0,\\;0\\bigr\)\.The controls drive the heading and speed throughB=\(00000110\)B=\\begin\{pmatrix\}0&0\\\\ 0&0\\\\ 0&1\\\\ 1&0\\end\{pmatrix\}, and𝐄=\{0\}3×10−4​\[−1,1\]\\mathbf\{E\}=\\\{0\\\}^\{3\}\\times 10^\{\-4\}\[\-1,1\]perturbs the speed\. The controller is a single hidden layer of500500ReLU units with𝐮i=π​\(𝐱\)i−20\\mathbf\{u\}\_\{i\}=\\pi\(\\mathbf\{x\}\)\_\{i\}\-20,δ=0\.2\\delta=0\.2,T=50T=50,𝐈=\[9\.5,9\.55\]×\[−4\.5,−4\.45\]×\[2\.1,2\.11\]×\[1\.5,1\.51\]\\mathbf\{I\}=\[9\.5,9\.55\]\\times\[\-4\.5,\-4\.45\]\\times\[2\.1,2\.11\]\\times\[1\.5,1\.51\],𝐆=\[−0\.6,0\.6\]×\[−0\.2,0\.2\]×\[−0\.06,0\.06\]×\[−0\.3,0\.3\]\\mathbf\{G\}=\[\-0\.6,0\.6\]\\times\[\-0\.2,0\.2\]\\times\[\-0\.06,0\.06\]\\times\[\-0\.3,0\.3\], and𝐀≡∅\\mathbf\{A\}\\equiv\\emptyset\.

##### Single Pendulum\.

An inverted pendulum is stabilized by a torque at its pivot\. The state𝐱=\(x1,x2\)=\(θ,θ˙\)\\mathbf\{x\}=\(x\_\{1\},x\_\{2\}\)=\(\\theta,\\dot\{\\theta\}\)collects the angle and angular velocity\. We haven=2n=2,m=1m=1, and

𝐅\(𝐱\)=\(x2,2sinx1\)\.\\mathbf\{F\}\(\\mathbf\{x\}\)=\\bigl\(x\_\{2\},\\;2\\sin x\_\{1\}\\bigr\)\.For parametersmp=L=0\.5m\_\{p\}=L=0\.5,c=0c=0,g=1g=1, the gravity term isg/L=2g/L=2and the torque enters the angular acceleration throughB=\(0,8\)⊤B=\(0,8\)^\{\\top\}with gain1/\(mp​L2\)=81/\(m\_\{p\}L^\{2\}\)=8\. The controller is a ReLU network with two hidden layers of2525units\. The remaining components are𝐄=\{0\}2\\mathbf\{E\}=\\\{0\\\}^\{2\},δ=0\.05\\delta=0\.05,T=20T=20,𝐈=\[1\.0,1\.175\]×\[0\.0,0\.2\]\\mathbf\{I\}=\[1\.0,1\.175\]\\times\[0\.0,0\.2\],𝐆=ℝ2\\mathbf\{G\}=\\mathbb\{R\}^\{2\}, and𝐀⁡\(t\)=\{𝐱:θ∉\[0,1\]\}\\mathbf\{A\}\(t\)=\\\{\\mathbf\{x\}:\\theta\\notin\[0,1\]\\\}fort∈\[10,20\]t\\in\[10,20\]and∅\\emptysetotherwise\.

##### Airplane\.

A simplified six\-degree\-of\-freedom airplane model has state𝐱=\(sx,sy,sz,vx,vy,vz,ϕ,θ,ψ,r,p,q\)\\mathbf\{x\}=\(s\_\{x\},s\_\{y\},s\_\{z\},v\_\{x\},v\_\{y\},v\_\{z\},\\phi,\\theta,\\psi,r,p,q\)of position, velocity, Euler angles, and body rates\. We haven=12n=12andm=6m=6\(three forces and three moments\);𝐅\\mathbf\{F\}andBBare the equations of motion of\([Manzanas Lopez et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib14), eq\. 10–12\), with parametersma=Ix=Iy=Iz=1m\_\{a\}=I\_\{x\}=I\_\{y\}=I\_\{z\}=1,Ix​z=0I\_\{xz\}=0,g=1g=1\. The controller is a ReLU network with three hidden layers of100100,100100, and2020units\. Withδ=0\.1\\delta=0\.1andT=20T=20, the initial set fixessx=sy=sz=r=p=q=0s\_\{x\}=s\_\{y\}=s\_\{z\}=r=p=q=0and\[vx,vy,vz,ϕ,θ,ψ\]∈\[0,1\]6\[v\_\{x\},v\_\{y\},v\_\{z\},\\phi,\\theta,\\psi\]\\in\[0,1\]^\{6\}, and the specification requiressy∈\[−1,1\]s\_\{y\}\\in\[\-1,1\]andϕ,θ,ψ∈\[−1,1\]\\phi,\\theta,\\psi\\in\[\-1,1\]throughout\.

##### Attitude Control\.

The attitude of a rigid body is controlled through three torques, with state𝐱=\(ω,ψ\)∈ℝ3×ℝ3\\mathbf\{x\}=\(\\omega,\\psi\)\\in\\mathbb\{R\}^\{3\}\\times\\mathbb\{R\}^\{3\}of angular velocity and Rodrigues parameters\. Heren=6n=6,m=3m=3,𝐄=\{0\}6\\mathbf\{E\}=\\\{0\\\}^\{6\}, and the angular\-velocity dynamics areω˙=\(0\.25​\(u0\+ω2​ω3\),0\.5​\(u1−3​ω1​ω3\),u2\+2​ω1​ω2\)\\dot\{\\omega\}=\(0\.25\(u\_\{0\}\+\\omega\_\{2\}\\omega\_\{3\}\),\\,0\.5\(u\_\{1\}\-3\\omega\_\{1\}\\omega\_\{3\}\),\\,u\_\{2\}\+2\\omega\_\{1\}\\omega\_\{2\}\)with the controls entering throughBB; theψ˙\\dot\{\\psi\}block is the kinematics of\([Manzanas Lopez et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib14), Sec\. V\)\. The controller has three hidden layers of6464units with sigmoid activations and a linear output,δ=0\.1\\delta=0\.1, andT=30T=30\. From the initial set of\([Manzanas Lopez et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib14)\)the specification requires avoiding the unsafe box given there:𝐆=ℝ6\\mathbf\{G\}=\\mathbb\{R\}^\{6\}and𝐀\\mathbf\{A\}is that box for alltt\.

##### Quadrotor\.

A quadrotor with twelve states \(position, velocity, attitude, body rates\) is controlled by three torques\. We haven=12n=12,m=3m=3,𝐄=\{0\}12\\mathbf\{E\}=\\\{0\\\}^\{12\}, with𝐅\\mathbf\{F\}andBBthe dynamics of\([Manzanas Lopez et al\. 2025](https://arxiv.org/html/2609.16298#bib.bib14), eq\. 12–16\)\. The controller has three hidden layers of6464units with sigmoid activations and a linear output,δ=0\.1\\delta=0\.1, andT=50T=50\. The initial set hasx1,…,x6∈\[−0\.4,0\.4\]x\_\{1\},\\ldots,x\_\{6\}\\in\[\-0\.4,0\.4\]andx7,…,x12=0x\_\{7\},\\ldots,x\_\{12\}=0, and the reach specification stabilizes the altitude,𝐆=\{𝐱:x3∈\[0\.94,1\.06\]\}\\mathbf\{G\}=\\\{\\mathbf\{x\}:x\_\{3\}\\in\[0\.94,1\.06\]\\\},𝐀≡∅\\mathbf\{A\}\\equiv\\emptyset\.

##### 2D Spacecraft Docking\.

A deputy spacecraft docks with a chief under linear Clohessy\-Wiltshire relative dynamics,𝐱=\(sx,sy,s˙x,s˙y\)\\mathbf\{x\}=\(s\_\{x\},s\_\{y\},\\dot\{s\}\_\{x\},\\dot\{s\}\_\{y\}\)\. Heren=4n=4,m=2m=2,𝐄=\{0\}4\\mathbf\{E\}=\\\{0\\\}^\{4\},

𝐅⁡\(𝐱\)=\(s˙x,s˙y,3​η2​sx\+2​η​s˙y,−2​η​s˙x\),\\mathbf\{F\}\(\\mathbf\{x\}\)=\\bigl\(\\dot\{s\}\_\{x\},\\;\\dot\{s\}\_\{y\},\\;3\\eta^\{2\}s\_\{x\}\+2\\eta\\dot\{s\}\_\{y\},\\;\-2\\eta\\dot\{s\}\_\{x\}\\bigr\),withη=0\.001027\\eta=0\.001027, and the controls enter the accelerations throughBBscaled by1/ms1/m\_\{s\},ms=12m\_\{s\}=12\. The controller has two hidden layers of256256units with tanh activations and a linear output,δ=1\\delta=1, andT=40T=40\. From the initial set\[70,106\]2×\[−0\.28,0\.28\]2\[70,106\]^\{2\}\\times\[\-0\.28,0\.28\]^\{2\}the specification is the velocity\-limit constraint∥\(s˙x,s˙y\)∥≤0\.2\+2​η​∥\(sx,sy\)∥\\lVert\(\\dot\{s\}\_\{x\},\\dot\{s\}\_\{y\}\)\\rVert\\leq 0\.2\+2\\eta\\lVert\(s\_\{x\},s\_\{y\}\)\\rVert, encoded as𝐀\\mathbf\{A\}for alltt\.

##### Navigation\.

A robot navigates to a goal while avoiding an obstacle,𝐱=\(x,y,θ,ν\)\\mathbf\{x\}=\(x,y,\\theta,\\nu\)\. We haven=4n=4,m=2m=2,𝐄=\{0\}4\\mathbf\{E\}=\\\{0\\\}^\{4\},

𝐅⁡\(𝐱\)=\(ν​cos⁡θ,ν​sin⁡θ,0,0\),B=\(00001001\)\.\\mathbf\{F\}\(\\mathbf\{x\}\)=\\bigl\(\\nu\\cos\\theta,\\;\\nu\\sin\\theta,\\;0,\\;0\\bigr\),\\quad B=\\begin\{pmatrix\}0&0\\\\ 0&0\\\\ 1&0\\\\ 0&1\\end\{pmatrix\}\.The two controllers \(each a ReLU network with two hidden layers of6464units and a tanh output, a standard one and an adversarially trained robust one\) give instances Navigation 1 and 2\. Withδ=0\.2\\delta=0\.2andT=30T=30, the initial set is\[2\.9,3\.1\]2×\{0\}×\{0\}\[2\.9,3\.1\]^\{2\}\\times\\\{0\\\}\\times\\\{0\\\}, and the reach\-avoid specification has𝐆=\{𝐱:x,y∈\[−0\.5,0\.5\]\}\\mathbf\{G\}=\\\{\\mathbf\{x\}:x,y\\in\[\-0\.5,0\.5\]\\\}and𝐀\(t\)=\{𝐱:x∈\[1,2\],y∈\[1,2\]\}\\mathbf\{A\}\(t\)=\\\{\\mathbf\{x\}:x\\in\[1,2\],\\,y\\in\[1,2\]\\\}\.

### C\.2Baselines

Every tool analyzes the same discrete\-time system\. For a benchmark tuple⟨m,n,𝐈,𝐅,𝐄,𝐮,B,δ,T,𝐆,𝐀⟩\\langle m,n,\\mathbf\{I\},\\mathbf\{F\},\\mathbf\{E\},\\mathbf\{u\},B,\\delta,T,\\mathbf\{G\},\\mathbf\{A\}\\rangle, the shared plant is the explicit\-Euler map

𝐱k\+1=𝐱k\+δ⁡\(𝐅⁡\(𝐱k\)\+B​𝐮​\(𝐱k\)\+ϵk\),ϵk∈𝐄,\\mathbf\{x\}\_\{k\+1\}=\\mathbf\{x\}\_\{k\}\+\\delta\\bigl\(\\mathbf\{F\}\(\\mathbf\{x\}\_\{k\}\)\+B\\,\\mathbf\{u\}\(\\mathbf\{x\}\_\{k\}\)\+\\mathbf\{\\epsilon\}\_\{k\}\\bigr\),\\quad\\mathbf\{\\epsilon\}\_\{k\}\\in\\mathbf\{E\},and each baseline is specialized to that map using its own set representation\. Three of the five participants \(CORA, immrax, CROWN\-Reach\) are continuous\-time tools in their ARCH\-COMP form, and we modify them to run on the discrete\-time map\. The continuous\-time machinery that exists solely to enclose a continuous flow, and therefore has no discrete counterpart, is dropped, and every other knob is left at the tool’s own competition value\. CORA needs no such removal, sincenonlinearSysDTis a native discrete\-time class; immrax needs none either, sinceevolution="discrete"is a first\-class mode; only CROWN\-Reach requires a source modification, described below\.

##### OvertPoly

\([Akinwande et al\. 2026a](https://arxiv.org/html/2609.16298#bib.bib1)\)\(v0\.1\.1, commit7743bc2\) is the combinatorial solver whose grid\-based enclosure of the dynamicsclipperalso adopts\. It encodes the closed loop over the horizon as a single mixed\-integer program: the piecewise\-linear enclosure of each nonlinear dynamics term contributes binary piece\-selection variables, and the𝖱𝖾𝖫𝖴\\mathsf\{ReLU\}controller contributes binary activation variables\. We run it on Julia 1\.10\.9 with Gurobi 13\.0\.2 through JuMP, at the solver’s default settings with logging suppressed, setting no optimality gap, thread cap, or time limit\. The tool is already discrete\-time, so no modification is required\.

##### OVERTVerify

\([Sidrane et al\. 2022](https://arxiv.org/html/2609.16298#bib.bib17)\)\(commit96c4d95\) is a distinct combinatorial tool that shares OvertPoly’s overapproximation of univariate dynamics but differs in the MILP encoding and in how the reachable set is queried\. It is likewise natively discrete\-time and runs on the same Julia and Gurobi versions with default solver settings\.

##### Controller restrictions in the combinatorial solvers\.

Both MILP encodings require a piecewise\-linear controller, which they realize as a big\-M encoding of𝖱𝖾𝖫𝖴\\mathsf\{ReLU\}activations\. This accounts for seven of the eightUcells in[Table1](https://arxiv.org/html/2609.16298#Sx4.T1), whose controllers use sigmoid or tanh activations\. The eighth, Airplane, has a𝖱𝖾𝖫𝖴\\mathsf\{ReLU\}controller, but atn=12n=12andm=6m=6the resulting encoding is too large for either tool to handle\.clipperadopts the same grid\-based enclosure of the dynamics but relaxes the controller with LiRPA rather than encoding it, and so places no restriction on its activations\.

##### CORA

\([Kochdumper et al\. 2023](https://arxiv.org/html/2609.16298#bib.bib12)\)\(v2026\.1\.0, commit904a444\) is pinned as a submodule and kept pristine\. We build the Euler plant as anonlinearSysDT, compose the controller withneurNetContrSys, and run reach, specification check, and CORA’s own recursive initial\-set splitting\. We do not call itsverifyentry point, whosesimulateRandomstage can return a falsifying trajectory before any splitting occurs and would report falsification time in place of set computation time\. Set\-representation options are taken per benchmark from CORA’s own ARCH\-COMP scripts, though options which have no discrete counterpart are not set\.

##### immrax

\([Harapanahalli, Jafarpour, and Coogan 2024](https://arxiv.org/html/2609.16298#bib.bib9)\)\(commitaf79191\) performs mixed\-monotone interval reachability in JAX, bounding the controller with CROWN throughjax\_verify\. It required no modification: discrete evolution is a first\-class mode and the mixed\-monotone embedding has a discrete branch, so the shared Euler map is expressed directly as an immrax system and rolled out over the horizon\. The only code we wrote is an adapter, including a converter from ONNX to immrax’s network format, validated against our own controller loader to within10−410^\{\-4\}\. Analysis options match immrax’s published neural\-network configuration, and where a benchmark warrants initial\-set partitioning we use immrax’s own pipeline: its documented15×1515\\times 15position grid on the Navigation instances, and a two\-cell heading split on Unicycle mirroring the partitionclipperuses there\.

##### CROWN\-Reach

\([Manzanas Lopez et al\. 2024](https://arxiv.org/html/2609.16298#bib.bib13);[Verified\-Intelligence 2024](https://arxiv.org/html/2609.16298#bib.bib18)\)\(commit7b90f30\) bounds the controller with LiRPA and propagates the plant as a Taylor model through Flow∗\. It is the only participant with no discrete\-time mode, and the only one whose source we changed, through three tracked patches against a pinned submodule\. The substantive patch replaces Flow∗’s continuous flowpipe integration with the shared Euler map applied directly to the Taylor model, which drops the a\-priori Picard enclosure and the flow remainder; both exist only to enclose the interior of an integration step, and discrete\-map Taylor\-model reachability is a standard construction\. Taylor\-model conservatism is untouched, as remainder growth and wrapping across steps remain and the tool keeps its own order and remainder settings\. The remaining patches disable the sampling\-based falsifier and add configurations for the instances CROWN\-Reach does not ship; every reachability option is the shipped ARCH\-COMP value\.

##### Configuration audit\.

Because untuned baselines are the obvious threat to the timing and tightness comparisons, we audited every option our harness sets against the value used by each tool’s own competition scripts\. CROWN\-Reach was already running its shipped configurations verbatim, and immrax matched its published configuration everywhere except Unicycle, where we then gave it the same heading splitclipperuses\. CORA was running one global default where its scripts tune per benchmark, which left its verdicts unchanged but inflated its reported volumes; every CORA row in[Table1](https://arxiv.org/html/2609.16298#Sx4.T1)was regenerated under the per\-benchmark configuration\. The one remaining gap is ACC, which we run at a lower zonotope order than CORA’s script specifies because that value crashes CORA partway through the horizon\.

### C\.3Implementation and Compute

All AINNCS experiments were run on a single workstation with an AMD Ryzen 9 7950X CPU \(16 cores, 32 threads\), 64 GB of RAM, and an NVIDIA GeForce RTX 3060 GPU with 12 GB of VRAM \(driver 580\.159\.03\), running Ubuntu 24\.04\.4 LTS\.clipperis implemented in Python 3\.12\.13 against PyTorch 2\.8\.0 with CUDA 12\.6,auto\_LiRPA0\.7\.0, and NumPy 2\.3\.5\. The environment is pinned by apixi\.lockfile that will be released with the source code\. The image\-based experiments of[AppendixD](https://arxiv.org/html/2609.16298#A4)were run separately on an NVIDIA H100 80 GB GPU and took120120GPU\-hours in total\. Enclosure\-slope optimization runs for 50 gradient steps; the relaxation ablation of[Table2](https://arxiv.org/html/2609.16298#Sx5.T2)holds this budget fixed across all three relaxations\.

Across the AINNCS benchmarks,muniselects enclosure refinements exclusively and no neuron split is taken\. Their controllers are small relative to the dynamics relaxation, and so a refinement always scores higher on the shared scale\. This is because the bulk of the bound\-sensitive relaxation error comes from the plant\. For example, on the unicycle benchmark with 500 neurons, we only encounter 7 “unstable” neurons during the initial concrete reachability pass, and neuron splitting is not beneficial there\.

## Appendix DImage\-Based Neural Feedback Systems

The AINNCS benchmark suite is limited to systems with small, state\-based controllers\. This favors tools with control\-native abstractions, thoughclipperremains competitive regardless\. To further highlight the benefits of our approach, we evaluateclipperon the advanced emergency braking system of[Cai, Fan, and Bak \(2025\)](https://arxiv.org/html/2609.16298#bib.bib4), which uses a image based controller\.

### D\.1The Advanced Emergency Braking System

The state is the distance to a stopped obstacle and the ego velocity,𝐱=\(d,v\)∈\[0,60\]×\[0,30\]\\mathbf\{x\}=\(d,v\)\\in\[0,60\]\\times\[0,30\], and the plant is linear,d\+=d−v​δd^\{\+\}=d\-v\\deltaandv\+=v−a​δv^\{\+\}=v\-a\\deltawithδ=0\.05\\delta=0\.05and a braking decelerationaaaffine in the controller output\. The perception system is replaced by a GAN conditioned ondd, carrying four latent variables bounded by10−210^\{\-2\}in magnitude and redrawn at every control step\. The network maps\(d,z,v\)\(d,z,v\)to a braking force through a generator and a controller composed into one convolutional network\. The specification requires the vehicle to stop beforeddreaches zero\.

### D\.2Inconclusive Instances

[Cai, Fan, and Bak \(2025\)](https://arxiv.org/html/2609.16298#bib.bib4)partition the state space into a100×100100\\times 100grid and prune it with50005000simulations per cell, then prove surviving cells safe by unrollingmmcontrol steps into a single composed network, bounding it withα,β\\alpha,\\beta\-CROWN, and re\-abstracting the result back to grid cells\. Coverage grows withmm, but so does the composed network, andm=3m=3is the ceiling they report\. On the2020Hz convolutional controller this leaves38683868cells \(38\.7%38\.7\\%of the space\), that are neither falsified by simulation, nor proven safe at anymmthey can reach \([Table4](https://arxiv.org/html/2609.16298#A4.T4)\)\.

### D\.3Reducing Inconclusive Cells

clippertargets these cells directly and does not re\-run the verificed/falsified cells\. We discuss the three routes close a cell, and[Table4](https://arxiv.org/html/2609.16298#A4.T4)reports how many cells each one settles\.

##### Kinematic lemma\.

We can exploit two facts about the benchmark to resolve inconclusive cells without network analysis\. The first is that the controller’s output layer clamps outputs to\[0,1\]\[0,1\]\. The second is that the velocity dynamics are affine, so every step sheds at least the speed the drag term alone removes\. A cell is therefore safe whenever its clearance exceeds the distance it could travel under the floor set by the most adversarial controller\. By construction, the worst case control is zero, and we can evaluate the floor in microseconds\.

##### Concrete reachability\.

One step of the composed network and plant is bounded withclipperfrom a state box and the latent box, giving a box that contains the true one\-step image, and iterating this yields a certified tube\. A cell closes when the velocity box falls to zero with clearance maintained throughout, or when clearance is maintained through the step bound the kinematic lemma floor supplies\.

##### Symbolic reachability\.

When that is not sufficient,clipperbounds the unrolled composition from the failing step back to the cell in a single backward pass, carrying one latent symbol per step and re\-boxing nowhere in between\. Every intermediate pre\-activation interval is intersected with the one the concrete pass computed for the same node, so the joint bound is no looser than the concrete bound it replaces, and we report the better of the two at each step\.

We branch on input and interior state nodes\. We expect the cells that remain to need branching on the controller’s activations alongside these routes, an actionclippersupports but whichmunidoes not select on any system reported here\.

Table 4:The2020Hz convolutional configuration of[Cai, Fan, and Bak \(2025\)](https://arxiv.org/html/2609.16298#bib.bib4)and the part of its inconclusive bandclipperresolves\. Counts are cells of their100×100100\\times 100grid, and their reported cost for this configuration is374374GPU\-hours normalized to a single machine\. The three routes overlap, so the rows attributing cells to them need not sum to the total resolved\.Cells in the state space10,00010\{,\}000Unsafe by simulation34633463Proven safe,11\-step00Proven safe,22\-step384384Proven safe,33\-step26692669Inconclusive after33\-step38683868Settled by the kinematic lemma1105Settled by concrete reachability44Settled by symbolic reachability9Resolved byclipper\(★\\bigstar\)1116Left inconclusive2752