Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

(authored by agents unless marked 🧑) Tag: zhou2024compositional, paper

problem and contribution

Neural-network controlled systems (NNCSs) combine an environment transition relation with a neural controller. The paper checks an infinite-horizon safety property by checking a supplied candidate inductive invariant. Its central obstacle is the monolithic implication

“(IndInv ∧ NextNNC ∧ NextENV ) =⇒ IndInv′” (Section 1, p. 2)

where NextNNC encodes a potentially large ReLU network. The proposed method introduces a bridge predicate and verifies two smaller implications. This separates NN reasoning from environment reasoning: a neural-network verifier computes output postconditions, and an SMT solver checks the environment implication.

The paper’s formal model has state s, NN outputs a, initial predicate Init, controller relation NextNNC, environment relation NextENV, and safety predicate Safe. A candidate IndInv proves safety when it satisfies Init =⇒ IndInv, inductiveness, and IndInv =⇒ Safe (Section 2, pp. 3–4). The experiments assume the candidate is supplied; automatic candidate discovery is future work (Section 6, p. 14).

technique 1: generalized bridge decomposition

What it is. Replace the monolithic check with

“(IndInv ∧ NextNNC ) =⇒ Bridge” (Condition 8, Section 3.1, p. 5)

and

“(Bridge ∧ NextENV ) =⇒ IndInv′” (Condition 9, Section 3.1, p. 5).

Theorem 1 gives soundness by transitivity; Theorem 2 gives completeness because Bridge may be IndInv ∧ NextNNC (Section 3.1, p. 5). A bridge over the outputs a alone (the paper’s “naive” bridge) can be insufficient, so the paper allows a bridge to mention both controller inputs s and outputs a. In the paper’s modified mod-4 example (Figure 1b with a different NextNNC), no naive bridge works: a = 1 ∨ a = −1 permits s = 3, a = −1, which the environment sends to s′ = 4; the generalized bridge records the input-dependent case “a generalized bridge predicate could be: ((0 ≤ s ≤ 2) ∧ a = −1) ∨ (s = 3 ∧ a = 1).” (Section 3.1, pp. 6–7).

How to apply it.

  1. Express the system as NextNNC ∧ NextENV, and take a supplied candidate IndInv (Sections 2–3, pp. 4–5).
  2. Partition or cover IndInv with predicates p_i over state inputs s.
  3. Compute an output predicate ψ_i for each p_i such that (p_i ∧ NextNNC) =⇒ ψ_i.
  4. Form Bridge = (p_1 ∧ ψ_1) ∨ ... ∨ (p_n ∧ ψ_n).
  5. Check each (p_i ∧ ψ_i ∧ NextENV) =⇒ IndInv′. All checks imply inductiveness (Section 3.2, pp. 7–8).

The construction is formalized as

“Bridge = (p1 ∧ ψ1 ) ∨ (p2 ∧ ψ2 ) ∨ · · · ∨ (pn ∧ ψn )” (Condition 12, Section 3.2, p. 7)

with (p1 ∨ ... ∨ pn) ⇔ IndInv and ψ_i ∈ AllPosts(NextNNC,p_i) (Conditions 13–14, p. 7). Therefore Condition 8 holds by construction (Theorem 3, p. 8). The p_i need not be disjoint, and ψ_i is “not necessarily the strongest postcondition” (Section 3.2, p. 7).

Verus form. Inference: represent IndInv as a predicate over the Rust state, and prove the environment transition’s postcondition with a proof fn whose requires includes the bridge disjunction and whose ensures establishes the primed-state invariant. Inference: each p_i can be a requires case (or a lemma predicate) and each ψ_i a lemma-produced fact about NN outputs. Inference: Verus cannot directly verify a floating-point ReLU network as the paper’s NN verifier does; use a verified integer/real abstraction or an external_body only for a separately trusted NN model, then state that trust explicitly. Inference: the logical shape transfers; AutoLIRPA’s numerical postcondition computation does not.

Evidence. Table 1 reports deterministic and nondeterministic 2D mazes on a 3.3 GHz 8-core AMD CPU, 16 GB RAM, and Nvidia 3060 GPU (Section 4.1, p. 11). The candidate is 0.25 ≤ x ≤ 0.95 ∧ 0.55 ≤ y ≤ 0.95; the initial and safety conditions already hold (Section 4.2, p. 12). For deterministic mazes, the compositional verifier proves all sizes except 2 × 128, where it falsifies inductiveness: 0.42–3.04 seconds for sizes 2 × 32 through 2 × 512, and 1.94 seconds for 2 × 1024; the monolithic Z3 check takes 51.59 seconds at 2 × 32, 410.14 seconds at 2 × 48, 1,203.76 seconds at 2 × 56, and times out after one hour at 2 × 64 and larger (Table 1, p. 12). For nondeterministic mazes, compositional times range 0.42–5.23 seconds and all sizes through 2 × 1024 verify; monolithic times out from 2 × 56 onward (Table 1, p. 12). The table also reports split and query counts per case; at 2 × 1024, deterministic uses 38 splits, 191 SMT queries, and 153 NN-verifier queries; nondeterministic uses 102 splits, 511 SMT queries, and 409 NN-verifier queries (Table 1, p. 12).

Assumptions and limits. Termination is not guaranteed in infinite state spaces because splitting can continue forever (Section 3.4, p. 9). The implementation uses union-of-hyperrectangle invariants, binary midpoint splitting, Z3, and AutoLIRPA/α-β-CROWN (Section 4.1, p. 11). The authors report that checking inductiveness monolithically with specialized NN verifiers “proved infeasible”: NextENV arithmetic over both NN input and output (e.g. x′ = x + 0.1a) is “beyond the capability of existing NN verifiers”, encoding controller and environment as one NN needs operators that are “not typically supported”, and encoding non-deterministic transition relations into a NN “remains a significant challenge” (Section 4, p. 10). Inference: a Verus implementation must bound or otherwise control splitting, and its proof effort can grow with the number of cases even when each case is simple.

technique 2: compositional falsification

Purpose. Failure to prove a chosen bridge does not show that IndInv is non-inductive. The paper instead searches for a satisfiable FState and output predicate FPred satisfying

“FState =⇒ IndInv” (Condition 20, Section 3.3, p. 8)

“(FState ∧ NextNNC ) =⇒ FPred” (Condition 21, Section 3.3, p. 8)

“(FState ∧ FPred ∧ NextENV ) =⇒ ¬IndInv′” (Condition 22, Section 3.3, p. 8).

If FState is satisfiable and these three conditions hold, Condition (7) does not hold, so the candidate is not inductive (Theorem 4, Section 3.3, p. 9).

How to apply it. Use a satisfiable state region inside IndInv; compute an NN output over-approximation FPred; ask the environment solver whether the next state violates IndInv′. Algorithm 1 reuses the current split p as FState and its postcondition ψ as FPred; a proved negated implication returns (False,p), i.e. the falsifying state predicate, not a single concrete state (Section 3.4, pp. 9–10; Algorithm 1, p. 10). Inference: this is a compositional refutation certificate, not merely a failed proof attempt.

Verus form. Inference: encode a violating state as a lemma with requires p(s) and ensures !IndInv(next(s)), while separately proving the NN-output relation and environment transition relation. Inference: for executable Rust, return an enum containing the witness state; the proof function itself remains ghost and is not called at run time.

Evidence and limits. The deterministic 2 × 128 experiment is the paper’s falsification case: compositional verification terminates in 2.21 seconds after 64 splits, 225 SMT queries, and 160 NN queries, while monolithic verification times out (Table 1, p. 12). Falsification is heuristic in the sense that failure to find FState does not establish inductiveness; the paper only claims the sufficient conditions of Theorem 4.

algorithm and implementation details

Algorithm 1 starts with queue Q = {IndInv}. It computes ψ ∈ AllPosts(NextNNC,p), checks the environment implication, adds successful p ∧ ψ cases to Bridge, returns false on a falsifying implication, and otherwise splits p into satisfiable predicates whose disjunction equals p (Section 3.4, pp. 9–10). The prototype uses AutoLIRPA for postconditions and Z3 for validity checks; splitting divides each hyperrectangle at its midpoint (Section 4.1, p. 11). The appendix’s reachability comparison exports PyTorch models to ONNX, which NNV imports directly, and converts ONNX to NNet for JuliaReach; one million uniformly distributed input vectors per controller configuration found a largest ONNX/NNet output difference “on the order of 10−6” (Appendix A.1, pp. 18–19). That conversion experiment concerns a comparison toolchain, not the inductiveness proof itself. In that comparison, NNV (2 × 40 and 2 × 512) and JuliaReach (2 × 512 and 2 × 1024) failed to verify 50-step safety on the deterministic maze because of over-approximation (Appendix A.2, p. 20).

techniques for the catalog

  • generalized bridge decomposition: cover an inductive invariant with input regions and NN-output postconditions, then prove each environment case separately
  • compositional falsification: combine a state witness, NN output over-approximation, and environment transition to prove a candidate invariant is not inductive
  • queue-based splitting: repeatedly split unresolved state predicates until every bridge case is proved or a falsifying case is found

Last edited: