{"id":"fe31019a-67b4-44bb-861c-7dc0da131aeb","arxiv_id":"2505.03643","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"BURNS computes sound underapproximate backward reachable sets for discrete-time nonlinear neural feedback loops using mixed-integer linear programming, enabling goal-reaching verification.","lead":"This paper presents BURNS, an algorithm that computes guaranteed-safe starting regions for nonlinear systems controlled by neural networks, proving that any state in those regions will reach a goal within a fixed number of steps. It encodes the system as mixed-integer linear programs and certifies the regions as true underapproximations.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Missing semantics for backward reachable sets of the multivalued overapproximation \\hat f makes Lemmas IV.6–IV.7 and Theorem IV.8 unproven; under the natural existential reading of the MILP encoding, the claimed underapproximation property is false.","rationale":"The reader's weakest assumption identifies the same load-bearing gap: the paper never defines backward reachable sets for the multivalued overapproximation \\hat f, and Lemmas IV.6–IV.7 are valid only under a for-all-branches semantics that is never stated. This is the single most important obstruction to the central claim because Theorem IV.8 depends directly on those lemmas. The concern is not merely stylistic: under the existential semantics that the MILP encoding naturally suggests, the claimed underapproximation is false, as shown by the two-branch example. The issue is addressable by adding an explicit definition and rewriting the proof of Lemma IV.7, so the appropriate verdict remains CONDITIONAL rather than a rejection. I agree with the reader that the weak proof is the primary concern; the numerical demonstration and the algorithmic idea appear plausible, but the paper cannot be accepted as a rigorous verification result without fixing this semantic gap.","tokens_in":11591,"tokens_out":15937,"duration_ms":177152,"concrete_test":"Ask the authors to state explicitly the definition of R_{\\hat f}^{(-t)}(G) for multivalued \\hat f. Then perform the finite-state check: define f(a)=b, f(b)=c, f(c)=0, \\hat f(a)={b,c}, \\hat f(b)=c, \\hat f(c)=0, and G={c}. Compute R_{\\hat f}^{(-1)}(G) and R_f^{(-1)}(G) under the stated definition. If the definition is existential, the inclusion fails because a is in the \\hat f-backward set but not the f-backward set. If the definition is universal, the inclusion holds, but the authors must then reconcile the MILP encoding, which uses a single feasible branch per solution, with universal branch quantification.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Definition III.1 defines the backward reachable set only for a single-valued function f, via equality trajectories. Lemmas IV.6 and IV.7 then use the notation R_{\\hat f}^{(-t)}(G) without ever defining it for the multivalued \\hat f. This is not cosmetic. Under existential semantics, where x belongs to the backward reachable set if some branch of \\hat f reaches G, the claimed inclusion is false. For example, take states a,b,c with f(a)=b, f(b)=c, and \\hat f(a)={b,c}, \\hat f(b)=c. Then \\hat f overapproximates f, but for G={c} we have a in R_{\\hat f}^{(-1)}(G) while a is not in R_f^{(-1)}(G), so R_{\\hat f}^{(-1)}(G) is not a subset of R_f^{(-1)}(G). Under universal semantics, where all branches must reach G, the inclusion holds, but the paper never states this semantics. The proof of Lemma IV.7 silently relies on the universal reading by restricting the domain to X=R_f^{(-1)}(G); that restriction is harmless only under universal semantics. The MILP encoding in Section IV-A, however, selects a single feasible assignment of binary variables, which is the existential reading, and the paper never connects that encoding to the universal property needed for soundness. Theorem IV.8 therefore rests on an undefined and ambiguous notion.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces BURNS, an algorithm for underapproximate backward reachable set computation for discrete-time nonlinear neural feedback loops, using an overapproximation of the dynamics combined with mixed-integer linear programming. The algorithm samples points in the true backward reachable set, computes maximal norm balls centered at those points via MILPs, and unions the balls to form per-step underapproximations. The paper claims soundness of this construction, uses the resulting sets to check goal-reaching properties, and presents a 2-D navigation example with an ablation over the number of samples. The central idea is plausible and the numerical demonstration is a useful first step, but the current manuscript has several load-bearing gaps in the formal development, most importantly an undefined semantics for backward reachability of the multivalued abstraction and a proof step that relies on a vacuous lemma. These issues are repairable but require substantive rewriting of Section IV-D and the associated optimization encoding.","tokens_in":11886,"tokens_out":7364,"duration_ms":76039,"significance":"If the soundness gaps are fixed, the paper addresses a real gap in the literature: underapproximate backward reachability for nonlinear neural feedback loops, which is the right tool for certifying reach properties. The algorithmic structure, based on OVERT-style overapproximation followed by MILP-based norm-ball maximization, is sensible and the numerical example shows nontrivial coverage of the backward reachable set. The paper is also transparent about its scalability limitation and does not overclaim experimental generality. The main contribution is conditional on a precise semantics for the multivalued abstraction and a correct proof of the inclusion R_hat-f^{-t}(G) ⊆ R_f^{-t}(G); with those fixed, the work would be a meaningful advance in learning-enabled system verification.","major_comments":[{"comment":"Definition III.1 defines the k-step backward reachable set only for a single-valued function f. Lemmas IV.6 and IV.7 and Theorem IV.8 use the notation R_hat-f^{(-t)}(G) for the multivalued overapproximation hat-f without defining it. This is not cosmetic. Under the existential semantics, where x is included if some branch of hat-f reaches G, the claimed inclusion is false: for f(a)=b, f(b)=c, and hat-f(a)={b,c}, hat-f(b)=c, with G={c}, we have a ∈ R_hat-f^{(-1)}(G) but a ∉ R_f^{(-1)}(G). Under universal semantics, where all branches must reach G, the inclusion can hold, but the paper never states this semantics. Moreover, the MILP encoding in Section IV-A selects a single feasible assignment of binary variables, which corresponds to the existential reading, and the paper never shows that this encoding enforces the universal property needed for soundness. Please define the semantics explicitly, state which one the proofs use, and adapt the optimization encoding and proofs accordingly.","section":"Section IV-D, Lemmas IV.6 and IV.7"},{"comment":"Lemma IV.6 is vacuous as stated. Its hypothesis that Z={f(x)|x∈X} implies R_f^{(-1)}(Z)=X, so the conclusion R_hat-f^{(-1)}(Z)⊆R_f^{(-1)}(Z) reduces to the trivial inclusion R_hat-f^{(-1)}(Z)⊆X. In Lemma IV.7 the lemma is invoked with Z=G and X=R_f^{(-1)}(G), but G is generally not the image of f over X, so the lemma does not apply. Consequently the base case and the inductive step of Lemma IV.7, and therefore Theorem IV.8, are not established. A correct proof must either generalize Lemma IV.6 to arbitrary target sets under the universal semantics or provide a different induction argument.","section":"Section IV-D, Lemma IV.6 and Lemma IV.7"},{"comment":"The encoding of x∉Ball via the max-over-halfspaces construction replaces the complement of a closed ball, {x : ||x||>r}, with {x : ||x||≥r}. A point on the boundary of a ball is therefore treated as being outside the union of balls even though it belongs to the union. If the optimization finds such a boundary point, it is not a genuine counterexample to Xs⊆Q. The paper's statement that using ≥ constraints 'actually enforces P⊂Q rather than P⊆Q but a stricter guarantee is acceptable' is not accurate: the check remains a sufficient condition only if the 'no point found' outcome is the one used to conclude the property holds, and the possibility of a false positive should be stated precisely.","section":"Section IV-F, eq. (10)"},{"comment":"The theorem statement says Algorithm 1 produces a valid underapproximation of the 'k-step backward reachable set,' but Algorithm 1 actually computes, for each t=1,...,k, a separate underapproximation of R_f^{(-t)}(G) and does not form a single underapproximation of R_f^{(-k)}(G) unless k is the final step. The statement should be rephrased as: for each t∈{1,...,k}, Algorithm 1 produces a valid underapproximation of the t-step backward reachable set of G. This is a logical clarification of the central claim and should be fixed in the next revision.","section":"Theorem IV.8 and Algorithm 1"}],"minor_comments":[{"comment":"The proof says constraint (3d) is x0∉G, but the optimization problem in eq. (3) states x0∉intG. Please correct the proof to use the actual constraint and explain whether the intended argument requires x0∉G or x0∉intG.","section":"Lemma IV.5, part b"},{"comment":"The proof refers to 'theorem III.1' when it means Definition III.1; the same reference error appears in the proof of Lemma IV.6 and in the proof of Lemma IV.5, which refers to 'theorem IV.5' instead of Lemma IV.5.","section":"Section IV-D, proof of Lemma IV.6"},{"comment":"The proof of Lemma IV.4 cites 'theorem II.1' but no such theorem is stated; it should cite Lemma IV.4 itself or the relevant closure property from the preliminaries.","section":"Section IV-A, Lemma IV.4 proof"},{"comment":"The text says 'Sobel sequence' and 'global sobel sampler' in Algorithms 1 and 2; the correct name is the Sobol sequence. Please fix the spelling.","section":"Section V"},{"comment":"The text refers to 'theorem III.2 and theorem III.3' but these are Definitions III.2 and III.3 in the problem statement; please correct the cross-references.","section":"Section IV-F"},{"comment":"The volume-fraction estimates are computed by Monte Carlo sampling rather than by exact integration; the caption and text should state that these are estimates so that the reader does not overinterpret the reported coverage values.","section":"Section V, Table I"}],"recommendation":"major_revision","confidential_remarks":"The main concern is the undefined semantics of multivalued backward reachability and the resulting gap in Lemmas IV.6-IV.7. I believe the authors can fix this within the manuscript's scope by defining universal backward reachability and by either proving that the MILP encoding enforces it or modifying the encoding to do so. The vacuousness of Lemma IV.6 is also fixable with a more careful induction. I therefore recommend major revision rather than rejection. There is no indication of any circularity or inappropriate reliance on fitted parameters in the derivation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper tackles a real gap: underapproximate backward reachability for nonlinear neural feedback loops. The algorithmic idea is sensible: overapproximate the closed-loop dynamics with a piecewise-linear multivalued map, then grow norm balls around sampled points by solving MILPs that, in effect, search for a trajectory that exits the goal set. The numerical example is well chosen and the coverage numbers are encouraging. The inclusion-checking reduction in Section IV-F is also a nice piece of work.\n\nThat said, the soundness proof has a serious hole. The paper never defines the backward reachable set for the multivalued overapproximation \\hat f. Lemmas IV.6 and IV.7 use that notation as if it were self-explanatory, but the claim only holds under a universal ('all branches reach the goal') semantics. Under the natural existential reading, the claimed inclusion is simply false, as the stress-test counterexample shows. The proof of Lemma IV.7 also misapplies Lemma IV.6 by taking Z=G and X=R_f^{(-1)}(G), which does not satisfy the lemma's hypotheses. And in Lemma IV.5's proof, constraint (3d) is misstated as x0 not in G instead of x0 not in int G—minor by itself, but indicative of sloppiness around the boundary cases.\n\nHere is the nuance: the algorithm itself may be sound under the right interpretation. The MILP feasibility check asks whether there exists a branch of \\hat f that takes a point outside the goal's interior. If no such branch exists for points in a ball, then all branches of the overapproximation stay in the goal, which is exactly a universal guarantee. The paper's proofs do not capture this, and the exposition does not say it. So I think the flaw is in the proof and the formalization, not necessarily in the algorithm. But as written, Theorem IV.8 is unproven.\n\nOther soft spots: no code is provided, and the evaluation is a single 2D benchmark, which limits confidence in scalability claims. The related work comparison to [14] seems accurate, though.\n\nBottom line: this is a solid idea that deserves a real referee and major revision. The authors need to define the semantics of \\hat f's backward reachable sets, rewrite Lemmas IV.6 and IV.7 with the universal reading, and connect the MILP encoding to that semantics explicitly. If they do that, the paper would be a useful contribution to the verification community. I would not cite the current version in my own work, but I would cite a corrected version. Worth bringing to a reading group as a case study in how a plausible algorithm can be let down by an underspecified proof.","headline":"A genuinely useful algorithm for underapproximate backward reachability of nonlinear neural feedback loops, but the soundness proof has a serious undefined-semantics gap that needs to be fixed before the paper can be accepted as a rigorous verification result.","tokens_in":12402,"tokens_out":7560,"would_cite":false,"duration_ms":70122,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68T07","90C11","93B03"],"pacs":[],"model":"deepseek-v4-flash","headline":"Underapproximate backward reachability makes goal-reaching verification sound for nonlinear neural feedback loops.","keywords":["underapproximate backward reachability","neural feedback loops","goal-reaching verification","mixed-integer linear programming","nonlinear discrete-time systems","neural network verification","reachability analysis"],"falsifier":"Build a one-step system where the true map sends $x$ to a point outside the goal, while the overapproximation $\\hat f$ also contains a spurious branch sending the same $x$ into the goal. The algorithm would include $x$ in its 'underapproximate' backward reachable set of the goal, yet $x$ is not in the true backward reachable set, directly contradicting Theorem IV.8 on that instance.","tokens_in":11340,"feed_emoji":"🎯","tokens_out":8408,"duration_ms":72963,"temperature":0.7,"pith_summary":"The paper introduces BURNS, an algorithm for computing underapproximate backward reachable sets of discrete-time nonlinear systems whose controller is a fixed neural network. Underapproximate backward reachable sets are the right tool for goal-reaching verification: if the starting set of states is contained in the computed union of norm balls, then every state in the starting set will reach the goal within $k$ steps, with no false alarms. The algorithm overapproximates the nonlinear closed-loop dynamics by a piecewise-linear multi-valued function, encodes that abstraction as a mixed-integer linear program, and solves a sequence of optimization problems to grow norm balls until they touch the boundary of the true backward reachable set. The paper proves the resulting union of balls is a valid underapproximation and demonstrates on a 2-D robot navigation example that the approach can check candidate starting sets in under a tenth of a second.","feed_headline":"Neural control loops get sound goal-reaching checks","feed_subtitle":"BURNS underapproximates backward reachable sets via MILPs, soundly proving when start states reach the goal.","key_machinery":"The load-bearing object is the underapproximate backward reachable set, represented as a union of $p$-norm balls and computed ball-by-ball through mixed-integer linear programming. The mechanism that makes this tractable is a double approximation: the nonlinear plant $f(x, \\mathrm{NN}(x))$ is first overapproximated by a multi-valued piecewise-linear function $\\hat f$ built from max/min functions and ReLU activations, each encodable exactly with mixed-integer linear constraints; then, for a sampled center $x_d$, the algorithm solves an optimization problem that maximizes the ball radius subject to the constraint that the terminal state of the $k$-step trajectory leaves the interior of the goal set (opt. prob. 3). The proof that the resulting ball is boundary-coincident with the true backward reachable set guarantees the ball is the largest sound ball centered at $x_d$, and an induction argument (Lemma IV.7) extends the guarantee to all $k$ time steps.","core_discovery":"The paper claims that Algorithm 1 produces a valid underapproximation of the $k$-step backward reachable set of a goal set $G$. Concretely, the algorithm outputs a collection of $p$-norm balls whose union is a subset of the true set of states that reach $G$ within $k$ steps under the closed-loop dynamics $f_{\\mathrm{cl}}(x) = f(x, \\mathrm{NN}(x))$. Because the computed set is an underapproximation, checking that a starting polytope $X_s$ lies inside the union of balls is a sound proof of the goal-reaching specification: every state in $X_s$ is guaranteed to enter $G$ within $k$ steps. The soundness argument combines two pieces: each norm ball is constructed as the largest ball centered at a sampled point that stays inside the true backward reachable set (a boundary-coincident subset), and replacing the true dynamics by a multi-valued overapproximation preserves the underapproximation property over multiple time steps. The numerical example shows that with 25 samples per timestep the union of balls covers roughly $90\\%$ to $96\\%$ of the true backward reachable set at early timesteps, while the goal-reaching checks themselves take under $0.1$ seconds.","pith_inferences":["The computed norm balls are reusable certificates: once a per-step backward reachable set is stored, checking many candidate starting sets costs only one small MILP each, which could make the method practical for runtime monitoring.","The boundary-coincidence construction is not tied to norm balls in principle; the same largest-container-inside-the-set logic should work with ellipsoids or zonotopes, provided their enclosing constraints can be encoded, opening the door to richer underapproximate set families.","The volume-fraction table suggests a direct way to grade a neural controller's verifiability: the coverage of the true backward reachable set measures how far the current policy is from being certified for a given goal, which could drive counterexample-guided policy improvement.","A remaining gap between theory and practice is the sampling of centers: the soundness proof assumes a center is in the true backward reachable set, while the implementation obtains it by rejection sampling; replacing that with a method that can certify membership would close the gap."],"forward_implications":["Goal-reaching properties for nonlinear neural feedback loops become soundly checkable offline: a candidate starting polytope is contained in the union of balls, or a counterexample point is found, via a single MILP.","The volume-fraction estimates used in the paper give a quantitative, tunable measure of verification strength: increasing the number of sampled centers trades computation time for tighter coverage of the true backward reachable set.","Because the method only requires a piecewise-linear overapproximation of the dynamics and piecewise-linear activations in the controller, it applies to any nonlinear discrete-time system for which such an abstraction can be constructed, not only the neural-feedback-loop setting.","The numerical results show solve time growing steeply with the horizon, so the practical frontier is scaling the MILP, which the paper suggests addressing with hybrid-symbolic reachability techniques."],"supporting_citations":[{"why":"Supplies the mixed-integer linear encoding of ReLU and max/min functions that turns the piecewise-linear abstraction into a MILP.","marker":"[19]"},{"why":"Supplies the piecewise-linear overapproximation technique used to abstract the nonlinear dynamics into the multi-valued function.","marker":"[18]"},{"why":"Provides the nonlinear 2-D robot navigation dynamics and goal set used in the numerical demonstration.","marker":"[14]"},{"why":"Established underapproximate backward reachability for linear neural feedback loops, the property class this paper generalizes to nonlinear systems.","marker":"[12]"},{"why":"Provides the bounding procedure used during encoding to bound the controller network's intermediate values.","marker":"[21]"},{"why":"Defines the symbolic reachability analysis formulation the algorithm adopts, and is cited as the basis for the hybrid-symbolic extension to longer horizons.","marker":"[13]"},{"why":"Motivates the view of neural network preimages as backward reachable sets, which the paper adapts to multi-timestep closed-loop dynamics.","marker":"[17]"}],"fun_headline_variants":["BURNS proves neural control reaches its goals","Sound goal verification for neural feedback loops","Underapproximate reachability checks neural loop goals","BURNS: sound backward reachability for neural control","Neural loop goal checks made sound with BURNS"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof that replacing the true dynamics with the overapproximation preserves the underapproximation relies on an unstated rule: a point counts as reaching the goal only if every branch allowed by the overapproximation reaches it; if the opposite rule is used, the claim is false.","fun_headline_variants_meta":{"raw":{"variants":["BURNS proves neural control reaches its goals","Sound goal verification for neural feedback loops","Underapproximate reachability checks neural loop goals","BURNS: sound backward reachability for neural control","Neural loop goal checks made sound with BURNS"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000232,"raw_usage":{"total_tokens":1471,"prompt_tokens":905,"completion_tokens":566,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":521,"completion_tokens_details":{"reasoning_tokens":493}},"tokens_in":521,"tokens_out":566,"duration_ms":5172,"temperature":1.0,"reasoning_tokens":493,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T23:47:20.631830+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a one-step system where the true map sends $x$ to a point outside the goal, while the overapproximation $\\hat f$ also contains a spurious branch sending the same $x$ into the goal. The algorithm would include $x$ in its 'underapproximate' backward reachable set of the goal, yet $x$ is not in the true backward reachable set, directly contradicting Theorem IV.8 on that instance.","supporting_citations":[{"cited_title":"Verifying Inverse Model Neural Networks","cited_arxiv_id":"2202.02429","evidence_quote":"Supplies the piecewise-linear overapproximation technique used to abstract the nonlinear dynamics into the multi-valued function."},{"cited_title":"Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,","cited_arxiv_id":null,"evidence_quote":"Provides the nonlinear 2-D robot navigation dynamics and goal set used in the numerical demonstration."},{"cited_title":"Reachability analysis of neural feedback loops,","cited_arxiv_id":null,"evidence_quote":"Established underapproximate backward reachability for linear neural feedback loops, the property class this paper generalizes to nonlinear systems."},{"cited_title":"Fast and effective robustness certification,","cited_arxiv_id":null,"evidence_quote":"Provides the bounding procedure used during encoding to bound the controller network's intermediate values."},{"cited_title":"Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,","cited_arxiv_id":null,"evidence_quote":"Defines the symbolic reachability analysis formulation the algorithm adopts, and is cited as the basis for the hybrid-symbolic extension to longer horizons."},{"cited_title":"PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks","cited_arxiv_id":"2408.09262","evidence_quote":"Motivates the view of neural network preimages as backward reachable sets, which the paper adapts to multi-timestep closed-loop dynamics."}],"review_version":1}