{"id":"49858e08-1c1a-490d-98ed-751d5e5243e2","arxiv_id":"2501.13023","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A new training method uses scaled hybrid zonotopes to turn exact ReLU reachability into a differentiable loss, enabling verified avoidance of non-convex unsafe sets.","lead":"The authors propose training ReLU neural networks to avoid unsafe regions by computing the exact image of a non-convex input set with scaled hybrid zonotopes and using a differentiable collision loss. The method is demonstrated for forward-invariant control and black-box reach-avoid planning, with a MILP check providing the final safety guarantee.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Exact-image construction (3) depends on an uncertified hypercube radius a; if any pre-activation leaves [-a,a], the final MILP verifies an under-approximate Q and can issue a false safety certificate.","rationale":"The reader's weakest assumption and this stress-test converge on the same point: the final MILP is only an independent certificate if Q is the true image intersection. The paper states the a condition but does not certify it; because a is fixed while weights evolve, this is not a one-time choice. This is more load-bearing than concerns about training convergence or the LP surrogate, because it can turn a verified 'safe' result into an unsafe one. A corrected version should compute an adaptive bound (e.g., maintain pre-activation bounds after each update) or at least verify post-training that all pre-activations lie inside [-a,a]. If the proposed check passes for all experiments, the central claim would be supported; if it fails for any, the reported safety guarantees need to be withdrawn or re-derived with a sufficient a. The central idea of Theorem 6 is otherwise coherent, so the appropriate disposition remains conditional on this exactness certificate.","tokens_in":14743,"tokens_out":14995,"duration_ms":160315,"concrete_test":"For each final network reported in Table I and Sec. VI, compute tight per-neuron pre-activation bounds over the input set Z (e.g., with a sound verifier such as alpha-beta-CROWN or an exact hybrid-zonotope backward preimage). If any bound exceeds the a value used in that experiment (50, 1000, or 40), re-run the MILP check (14) with an enlarged a. If any reported 'safe' network changes from verified empty to nonempty, the exactness assumption is false and the corresponding safety certificate is invalid.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section II-B defines H_n as the ReLU graph over the hypercube {-a <= x <= a} and says '(3) holds as long as a is large enough.' The safety certificate is only valid if Y_d from (3) is the exact graph of the whole input set Z. If any pre-activation v_i lies outside [-a,a], that part of Z is absent from Y_d, so the computed collision set Q = P_d ∩ U is a strict subset of the true collision set. The terminal MILP (14) then certifies emptiness of this under-approximation, so 'Q empty' can hold while the true network image still intersects U. The experiments fix a=50, a=1000, and a=40 by hand, with no computation of pre-activation bounds and no check after training. Since weights are updated during training, an a that was large enough initially can become insufficient. This assumption therefore underpins the 'provably-safe' claim in every reported result.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a training method for ReLU networks that drives the image of a non-convex input set out of collision with a non-convex unsafe region. The key construction is a scaled hybrid zonotope (SHZ), which scales a user-selected subset of continuous generator bounds by a factor r. Theorem 6 states that the collision set Q is empty if and only if the optimal scaling r* in MILP (15) is greater than 1, giving a loss l = 1 - r*. To make the loss differentiable, the paper solves an LP relaxation (16) with a log-barrier term and uses KKT differentiation. Training alternates with an independent MILP check (14) that certifies Q is empty. Experiments benchmark scalability up to 240 neurons against the authors' prior work [15], and two applications are presented: training a forward-invariant controller for a double integrator with a non-convex safe set, and a reach-avoid plan for a black-box drifting vehicle.","tokens_in":14979,"tokens_out":8989,"duration_ms":99332,"significance":"If the exactness assumptions are certified, the paper makes a meaningful contribution: it is, to my knowledge, the first training method that uses exact hybrid-zonotope reachability for non-convex input and unsafe sets, with representation complexity linear in the number of neurons and a final safety certificate from an independent MILP rather than from the training loss itself. The SHZ scaling idea is elegant, and the theoretical core (Corollary 3, Proposition 5, Theorem 6) is simple and correct under its stated assumptions. The numerical comparison with [15] is appropriate, and the two control demonstrations show practical potential. The main caveat is that the advertised 'exact' and 'provably-safe' claims rest on an unverified hypercube radius a, so the guarantee as presented is not yet fully demonstrated.","major_comments":[{"comment":"The exact-image construction (3) is valid only when the hypercube radius a is large enough to contain every pre-activation value of the network. The paper states this without proof and fixes a=50, a=1000, and a=40 by hand, with no check before or after training. Because the weights are updated during training, an initially sufficient a can cease to be sufficient. If any pre-activation leaves [-a,a], the computed Q in (3) is a strict subset of the true collision set, and the verification MILP (14) can certify emptiness of an under-approximation, yielding a false safety certificate. Please add a certified bound on all pre-activations for the final network (and ideally during training), or otherwise demonstrate that the selected a values are sufficient in each experiment.","section":"Section II-B, Eq. (5); Sections V-A, VI-A, VI-B"},{"comment":"The equivalence 'Q is empty if and only if r* > 1' presumes that the MILP (15) has an optimal solution. If Q is empty and no finite r makes Q_r = SHZ(Q,r,nr) nonempty, then (15) is infeasible and r* is undefined, so the theorem as stated is not universally valid. The paper should either prove feasibility for the constructed Q (for example, from the structure of ReLU reachable sets) or explicitly handle the infeasible case, which would itself certify safety. This matters because the proposed loss function requires r* to be computable.","section":"Theorem 6, Eq. (15)"},{"comment":"The paper states that for a small enough mu, the condition l~ < 0 is sufficient for Q to be empty. This is an asymptotic statement in the limit mu -> 0, but the experiments use mu = 0.1 and no quantitative bound is given for that value. Since the final certificate is obtained from the independent MILP (14), this does not invalidate the reported safety results, but the paper should be explicit that the sufficiency is asymptotic and not certified at the implemented mu.","section":"Section IV-C, Eq. (16)"}],"minor_comments":[{"comment":"The objective contains the expression '1ln(' which should presumably be '1^T ln('; please clarify the notation.","section":"Eq. (16)"},{"comment":"There are two typos: 'to to tackle' in Problem 1 and 'belive' in the Conclusion.","section":"Problem 1 and Conclusion"},{"comment":"Each experiment was run only once, so the reported training times should be presented as indicative rather than as statistically robust measurements; adding repetitions or error bars would strengthen the comparison.","section":"Table I"},{"comment":"The discussion of why nr = 5 is preferred over nr = 9 is useful, but a short explanation of how nr was selected would improve reproducibility, given the observed sensitivity to this hyperparameter.","section":"Section VI-A"},{"comment":"The hybrid zonotope defining the safe set Xt is displayed with large matrices that are difficult to parse; consider reformatting or referring the reader to a figure with a clearer visualization.","section":"Eq. (18)"}],"recommendation":"major_revision","confidential_remarks":"The paper's own limitations section acknowledges hyperparameter sensitivity and the inability to verify solvability, but it does not mention the unverified hypercube radius a, which is the most serious gap for the 'provably-safe' claim. I would ask the authors to add a certification step for a and to fix the existence assumption in Theorem 6. The comparison to [15] is against the authors' prior work, which is acceptable, though an external baseline would strengthen the novelty claim. The paper fits the scope of cs.LG."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe core idea is solid: scaled hybrid zonotopes give a differentiable way to measure collision between a ReLU network's image and a non-convex unsafe set, and the LP relaxation with KKT-based gradients makes it trainable. The experiments show a dramatic speedup over [15], and the authors are upfront about the main limitations. But the paper's headline claim—'provably-safe'—rests on an assumption that is never certified.\n\nSection II-B defines the ReLU graph over the hypercube [-a,a]^n and says (3) holds as long as a is large enough. That's true, but the paper never checks that the hand-picked values (a=50, 1000, 40) actually bound every pre-activation value during or after training. Weights move during training; an a that was fine initially can become too small. If that happens, the computed reachable set is an under-approximation of the true network image, and the final MILP (14) certifies emptiness of that under-approximation. A false positive is possible: the MILP says 'no collision' while the true image still intersects the unsafe region. This is a soundness gap in the safety certificate, not a minor implementation detail.\n\nWhat is genuinely new here is the scaled hybrid zonotope itself and the way it enables parameterized scaling of non-convex polytopic sets. Theorem 6 is correct, and the final verification is independent of the loss, which keeps the circularity burden low. The empirical comparison with [15] is fair, and the authors noticeably avoid overclaiming: they acknowledge hyperparameter sensitivity, the absence of a solvability check, and the restriction to fully connected ReLU networks.\n\nThe fix is straightforward: compute interval bounds on pre-activations to certify a, or automatically enlarge a during training and re-certify before declaring success. I would also like to see multiple seeds and a clarification of the timing columns in Table I. The LP relaxation's dependence on μ is a training-efficiency issue, not a safety issue, since the MILP check is used during training.\n\nThis paper deserves a serious referee. It is a genuine step forward for verification-based training, and the core method is likely salvageable with an explicit certificate for a. I would encourage the editor to send it out with a request for careful treatment of that assumption.","headline":"A genuinely useful method for non-convex safety certification that currently ships without a certificate for its hypercube bound.","tokens_in":15482,"tokens_out":4392,"would_cite":true,"duration_ms":53130,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T07","90C11"],"pacs":[],"model":"deepseek-v4-flash","headline":"A training loss derived from hybrid-zonotope reachability drives the exact image of a ReLU network out of collision with a non-convex unsafe region, with an independent MILP check certifying safety.","keywords":["safe neural network training","hybrid zonotopes","scaled hybrid zonotopes","ReLU networks","reachability analysis","mixed-integer linear programming","forward invariance","reach-avoid"],"falsifier":"For any network the method reports as safe, compute the exact range of pre-activation values over the input set; if any value exceeds the chosen bound $a$, the exact-image formula is invalid and an independent MILP on the true image could reveal a collision, settling whether the certificate is real.","tokens_in":14553,"feed_emoji":"🛡️","tokens_out":8403,"duration_ms":85063,"temperature":0.7,"pith_summary":"This paper proposes a training method that makes a ReLU neural network provably avoid an unsafe region for an entire non-convex input set, not just for sampled points. The central device is the scaled hybrid zonotope, a set representation obtained by adding one optimization variable that shrinks or grows a hybrid zonotope's continuous generators. The authors show that the image of the scaled input set through the network stays a scaled hybrid zonotope, so checking whether the image collides with an unsafe set reduces to a mixed-integer linear program whose optimal value is greater than one exactly when there is no collision. Training minimizes a convex-relaxed surrogate loss; once that loss becomes negative, the exact image is guaranteed collision-free, and an independent MILP verifies the guarantee. The method is demonstrated on networks up to 240 neurons, a forward-invariant controller for a non-convex safe set, and safe reach-avoid plans for a black-box drifting vehicle.","feed_headline":"A new loss provably keeps ReLU networks out of unsafe regions","feed_subtitle":"It computes the network's exact image of a non-convex input set, then trains until a MILP verifies zero collision.","key_machinery":"Scaled hybrid zonotope: a hybrid zonotope whose first $n_r$ continuous-generator coefficients are constrained by $\\|(z_c)_{1:n_r}\\|_\\infty \\le r$ instead of $\\|z_c\\|_\\infty \\le 1$, so $r$ parameterizes a nested family of polytopic sets ($r<1$ shrinks, $r>1$ grows). The paper proves that the operations used to propagate a set through a ReLU network—Cartesian products, intersections with hyperplanes, affine maps, and intersections—commute with this scaling, so the exact graph and image of the scaled input set are obtained from the same matrices as the unscaled image. The emptiness-check MILP optimizes $r$, and an LP relaxation makes the optimum differentiable through KKT conditions, which is how the safety signal reaches the network weights.","core_discovery":"The paper's central claim is Theorem 6: for a collision set $Q$ formed by intersecting the exact image of an input set with an unsafe region, $Q$ is empty if and only if the optimal scaling factor $r^*$ of the MILP (15) is strictly greater than 1. Consequently the scalar $\\ell = 1 - r^*$ is a certificate of safety whenever it is negative. Because an MILP optimum is not differentiable, the paper replaces $r^*$ with the optimum of an LP relaxation with log-barrier regularization; for a small barrier parameter the relaxed value is no larger than $r^*$, so a negative surrogate loss is a sufficient condition for $Q$ to be empty. The paper thereby converts a verification problem into a loss function that can be minimized by backpropagation while retaining an independent mixed-integer feasibility check as the final safety certificate.","pith_inferences":["The parameterized scaling idea transfers to any exact set-based layer representation whose constraints are linear in bounded continuous coefficients, so the same $r$-based loss could be built for activation functions beyond ReLU once such representations exist.","In the black-box reach-avoid application, the formal guarantee applies to the learned trajectory model plus a sampled error bound; the physical robot's safety is only as strong as that error estimate, which is not itself certified.","The optimal $r^*$ can be read as a safety margin: how much the input set would need to shrink before its image touches the unsafe set. Used online, it could serve as a safety-distance estimate for re-planning or for ranking candidate controllers, not just as a training loss."],"forward_implications":["If the surrogate loss drops below zero, the exact image of the input set is guaranteed to be disjoint from the unsafe region, with the guarantee checked by an independent MILP rather than by sampling.","Non-convex input sets and non-convex unsafe regions can be handled exactly, removing a restriction of earlier verification-based training methods that only treated convex sets.","The reachable-set representation grows linearly in the number of neurons, so training remains practical for networks of a few hundred neurons and for long time horizons that would make time-stepped methods expensive.","The same loss can produce forward-invariant controllers for non-convex safe sets and safe reach-avoid policies for black-box dynamical systems, because the loss integrates with standard optimizers and additional objective terms."],"supporting_citations":[{"why":"Proves that hybrid zonotopes exactly represent ReLU network images, grounding the exact image computation in equation (3).","marker":"[6]"},{"why":"Defines hybrid zonotopes and their closed set operations used throughout the reachable-set construction.","marker":"[17]"},{"why":"Provides the hybrid-zonotope graph of a ReLU activation over a hypercube, supplying equation (5) and the complexity counts.","marker":"[20]"},{"why":"Is the prior constrained-zonotope training method whose scaling-based emptiness check this work adapts and outperforms in the benchmarks.","marker":"[15]"},{"why":"Supplies KKT differentiation of the LP relaxation, which makes the emptiness loss backpropagatable.","marker":"[28]"},{"why":"Is the interior-point LP solver used to evaluate the relaxed emptiness check and its gradient.","marker":"[29]"},{"why":"Represents the prior certified-invariant-polytope training approach limited to convex sets, the limitation this method removes.","marker":"[11]"},{"why":"Supplies the black-box reach-avoid problem setup and the comparison baseline used in the application demo.","marker":"[34]"}],"fun_headline_variants":["Hybrid zonotope reachability makes ReLU training provably safe","Train ReLU nets with exact collision check via MILP","Provable safe training: non-convex reachability via MILP loss","Backprop through a scaled hybrid zonotope for safe ReLU training","MILP-verified safety loss for training ReLU networks"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The reachable set is guaranteed exact only if the hypercube bound used to encode each ReLU is large enough to contain every pre-activation value the network produces, and the paper does not certify that its hand-picked values (50, 1000, and 40) are sufficient for the experiments.","fun_headline_variants_meta":{"raw":{"variants":["Hybrid zonotope reachability makes ReLU training provably safe","Train ReLU nets with exact collision check via MILP","Provable safe training: non-convex reachability via MILP loss","Backprop through a scaled hybrid zonotope for safe ReLU training","MILP-verified safety loss for training ReLU networks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000587,"raw_usage":{"total_tokens":2777,"prompt_tokens":983,"completion_tokens":1794,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":599,"completion_tokens_details":{"reasoning_tokens":1703}},"tokens_in":599,"tokens_out":1794,"duration_ms":15697,"temperature":1.0,"reasoning_tokens":1703,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T16:31:09.503289+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For any network the method reports as safe, compute the exact range of pre-activation values over the input set; if any value exceeds the chosen bound $a$, the exact-image formula is invalid and an independent MILP on the true image could reveal a collision, settling whether the certificate is real.","supporting_citations":[{"cited_title":"Hybrid zonotopes exactly represent ReLU neural networks,","cited_arxiv_id":null,"evidence_quote":"Proves that hybrid zonotopes exactly represent ReLU network images, grounding the exact image computation in equation (3)."},{"cited_title":"Hybrid zonotopes: A new set representation for reachability analysis of mixed logical dynamical systems,","cited_arxiv_id":null,"evidence_quote":"Defines hybrid zonotopes and their closed set operations used throughout the reachable-set construction."},{"cited_title":"Backward reachability analysis of neural feedback systems using hybrid zonotopes,","cited_arxiv_id":null,"evidence_quote":"Provides the hybrid-zonotope graph of a ReLU activation over a hypercube, supplying equation (5) and the complexity counts."},{"cited_title":"Two-Stage Predict+ Optimize for MILPs with Unknown Parameters in Constraints,","cited_arxiv_id":null,"evidence_quote":"Supplies KKT differentiation of the LP relaxation, which makes the emptiness loss backpropagatable."},{"cited_title":"Interior point solving for lp-based pre- diction+ optimisation,","cited_arxiv_id":null,"evidence_quote":"Is the interior-point LP solver used to evaluate the relaxed emptiness check and its gradient."},{"cited_title":"Guaranteed Reach-Avoid for Black-Box Systems through Narrow Gaps via Neural Network Reachability","cited_arxiv_id":"2409.13195","evidence_quote":"Supplies the black-box reach-avoid problem setup and the comparison baseline used in the application demo."}],"review_version":1}