{"id":"4a07e285-1cb2-4dc4-bfa7-feb5b282b6f0","arxiv_id":"2608.13118","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"SABRE verifies global robustness of ReLU networks by branch-and-bound splitting of relational neurons, guided by a dual-formulation selection heuristic.","lead":"This paper introduces SABRE, a branch-and-bound verifier that splits relational neurons, the differences between two network executions, to prove global robustness properties of neural networks. It reports that relational splitting with a dual-based neuron selection strategy outperforms individual-neuron splitting baselines across 817 verification instances on five benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The printed ReLU relaxation in §IV-A is unsound as written; without an artifact audit or soundness proof, every verified-instance claim rests on an unverified encoding.","rationale":"The paper is an empirical branch-and-bound system for relational verification of neural networks. Its central claim requires two things: that the DiffPoly/RaVeN abstraction is a sound over-approximation of the relational semantics, and that the implementation faithfully encodes that abstraction in the LP of Eq. 3. The strongest evidence is the public artifact and the 817-instance evaluation, but the paper gives no soundness theorem and the printed ReLU constraint in Section IV-A is not a valid over-approximation as written: for a ReLU with input range [l,u] and u>0, the feasible set excludes positive outputs, which is unsound in the unsafe direction. This is not a cosmetic typo because the same constraint pattern appears in Appendix A and because Appendix C's derivation is explicitly partial, so the dual formulation and Table I cannot be checked against the printed primal. The reader's weakest assumption identifies exactly this gate, and I agree with it. I would keep the CONDITIONAL verdict rather than escalate to REJECT because the artifact is publicly available and a single code inspection or root-LP comparison can settle whether the implementation contains the standard ReLU bound; if it does, the paper's main empirical conclusion may still be valid after correcting the writeup. Secondary issues, such as the counterexample check in Algorithm 1 comparing the full output vector instead of the ℓ-th output dimension, reinforce the need for an artifact audit but do not replace the primary soundness concern.","tokens_in":26580,"tokens_out":13251,"duration_ms":120769,"concrete_test":"Fetch the Zenodo artifact (DOI 10.5281/zenodo.21536550), locate the ReLU upper-bound constraint in the ApxVerRel implementation, and check whether it is (u-l)y - u x + u l <= 0 (with the u x term present) or the printed simplified form (u-l)y <= 0. Then, as a decisive numerical check, take the first ACAS Xu instance from Table IV, re-solve the root LP with the corrected standard ReLU bound, and compare the certified interval and verdict with the artifact's output. If the result changes, the implementation follows the unsound printed equation and the experimental claims are invalid; if the result is identical, the printed formula is only a typo and the central claim can be evaluated on the code. Independently, re-derive Appendix C Eq. 31 from Eq.","verdict_should_be":"UNCHANGED","load_bearing_attack":"To certify global robustness, the LP in Eq. 3 must contain a sound over-approximation of each ReLU. The printed ConstReLU upper bound is (u-l)y - (ul-lu) <= 0, i.e., (u-l)y <= 0, hence y <= 0 whenever u > l. This excludes all positive ReLU outputs and is not an over-approximation; a solver using it could certify properties that are actually false. The same pattern appears in Appendix A Eq. 13. Appendix C does not repair this: it derives only one representative case, asserts the rest 'analogously', and the resulting dual coefficients in Table I cannot be independently checked against the printed primal. No machine-checked proof or independent implementation audit is supplied, so the 817-instance evaluation is meaningful only if the artifact silently deviates from the paper. If the code follows the printed inequality, the central claim collapses; if it follows the standard (u-l)y - u x + u l <= 0 inequality, the paper needs a correction but may stand. The soundness of the LP encoding is therefore the load-bearing gate for the paper's claims.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes SABRE, a branch-and-bound framework for relational verification of neural networks, targeting global robustness properties. Unlike prior BaB-based relational verifiers that split individual neurons, SABRE splits relational neurons (differences between corresponding neurons of two network copies) and selects which relational neuron to split using a dual-formulation-based heuristic adapted from BaBSR. The verification bound is computed by a linear program that encodes the individual and relational ReLU constraints of the DiffPoly domain. The authors evaluate SABRE on 817 instances across ACAS Xu, MNIST, CIFAR, and GTSRB, comparing against the RaVeN approximation verifier, individual-neuron splitting baselines (ClasIS and DualIS), and a random-selection ablation (RandRS). They report that relational splitting solves more instances, explores fewer sub-problems, achieves lower time ratios, and certifies larger perturbation radii on most benchmarks, with an advantage that increases as the relational perturbation grows.","tokens_in":26815,"tokens_out":9703,"duration_ms":92989,"significance":"If the framework is sound, the paper is a meaningful step for relational verification: it adapts the well-known BaB paradigm to the relational setting by splitting relational neurons, and it provides an efficient, dual-based selection rule. The evaluation is extensive (five benchmarks, several baselines, ablations, and a statistical comparison), the artifact is publicly available, and the method introduces no fitted parameters. The central ideal of the paper is plausible and the empirical claims, if backed by a correct implementation, would be useful to the neural network verification community. However, the soundness of the whole verification pipeline depends on the printed ReLU relaxation constraints and on the control flow of the BaB algorithm; as printed, both have load-bearing problems that must be fixed before the results can be trusted.","major_comments":[{"comment":"The printed upper-bound ReLU constraint is unsound. The inequality (x_upper - x_lower)y - (x_upper*x_lower - x_lower*x_upper) <= 0 reduces to (x_upper - x_lower)y <= 0, i.e., y <= 0, which is not a sound over-approximation of ReLU(x) for intervals crossing zero. The standard constraint is (x_upper - x_lower)y - x_upper*x + x_upper*x_lower <= 0. The same garbled pattern appears in Appendix A Eq. (13) and in the primal constraints of Appendix C, Eqs. (20)-(21). Since these constraints define the LP in Eq. (3) from which certified bounds and counterexample validation are derived, this is a load-bearing soundness issue. The equations must be corrected, and the authors should state clearly, or demonstrate by an artifact audit, that the implementation uses the corrected constraints rather than the printed ones.","section":"§IV-A, Eq. (3), ConstReLU; also Appendix A Eq. (13) and Appendix C Eq. (20)-(21)"},{"comment":"The branch condition in line 8 is not the standard \"not verified\" condition. As printed, it checks whether the lower bound is greater than δ or the upper bound is less than -δ, i.e., whether the interval is in definite violation on one side. The correct non-verification test is whether the upper bound exceeds δ or the lower bound is below -δ. Moreover, the pseudocode has no explicit action for a subproblem whose bounds are already within [-δ, δ]: the function simply falls off the end without returning, and no branch is marked solved. This makes the control flow, and hence termination and completeness of the BaB loop, ambiguous as written. Please correct the condition and specify what happens for verified subproblems, and be explicit about which symbols are lower and upper bounds.","section":"Algorithm 1, line 8"},{"comment":"The definition of s# is inconsistent with the reported numbers. The text says that for all BaB-based approaches, s# counts only instances additionally solved beyond RaVeN, because all BaB methods invoke RaVeN first. But Table III reports SABRE s# values such as 67 on ACAS Xu, while RaVeN solves 42 of 230 instances; if s# were only the additional solves, the entry would be 25 (or the table would need a separate total-solved column). The same ambiguity affects Tables IV, VI, and VIII. Please define s# unambiguously (total solved vs. additional solved) and make all tables and prose consistent, since this metric underlies the paper's central empirical claims.","section":"§V-A, Table III and metric definitions"}],"minor_comments":[{"comment":"The derivation in Appendix C covers only one representative case and states that the remaining cases follow analogously. For a paper whose core algorithmic contribution is the dual-based selection rule, Table I should be derivable from the printed primal constraints; please either expand the derivation for all cases or provide a script that generates the table from the corrected constraints.","section":"Appendix C, Eqs. (30)-(31) and Table I"},{"comment":"There are several typographical and notation issues: 'a branch-and-bound' appears as 'abranch-and-bound'; the tool name is inconsistently written as SaBRe, SABRE, and SABRE; and the use of upper and lower bars in Eq. (2), Algorithm 1, and Table I is not always visually distinct in the text. These make it unnecessarily hard to check the soundness of the presented constraints.","section":"Throughout"},{"comment":"Example 1 refers to Fig. 2b for quantitative bound refinements, but the figure caption says the bounds were solved by Gurobi following the approach in §IV; the text does not state the network architecture or the exact specification. Please provide the network definition and the property so the example is reproducible without the repository.","section":"§III-B, Example 1 and Fig. 2"},{"comment":"The paragraph on CIFAR states that the CIFAR model has significantly more unstable ReLU neurons, but Table VII reports only the two networks used in RQ3; a direct comparison of unstable-ReLU counts for the CIFAR models in RQ2 would make the argument more concrete.","section":"§V-B, RQ2"}],"recommendation":"major_revision","confidential_remarks":"The paper is potentially publishable after revision, but the printed ReLU relaxation and the BaB control flow must be corrected first. I would ask the authors to confirm, ideally by a small artifact audit or a machine-checkable certificate, that the implementation uses the standard sound upper-bound inequality rather than the unsound one printed in Eqs. (3), (13), (20), and (21). If the implementation already uses the correct constraint, the paper may stand after a careful revision; if not, the empirical claims are not supported."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear [name],\n\nThe paper is worth your time. The core idea—branching on relational neurons rather than individual ReLUs in a BaB verifier for global robustness, with a dual-based selection heuristic—is a genuine extension of the BaB line into hyperproperties. The evaluation is serious: 817 instances across five benchmarks, comparisons against RaVeN, RABBit-style splitting, and an ablation of the selection strategy. The results are consistent enough that the method is likely doing something right.\n\nWhat it does well: the empirical story is unusually complete. RQ4 shows the selection heuristic matters—random relational splitting is much worse. RQ5 shows SABRE certifies larger radii on many instances. The code and data are posted. That's real evidence.\n\nSoft spots, in order of importance. First, the printed ReLU upper-bound constraint in §IV-A and Appendix A is, taken literally, not a sound over-approximation. The notation is so garbled in the text that I suspect a rendering problem, but the authors need to write the standard (u-l)y <= u*x - l*u explicitly. Without that, the LP in Eq. 3 cannot be checked, and the whole soundness argument rests on the code silently matching the intended formula. Second, Algorithm 1 line 8 branches only on definite violation, not on 'not verified'; the condition and the comment disagree. That's a typo, but in a verification paper, pseudocode typos are exactly what a referee should catch. Third, Appendix C derives only one case of the dual and says the rest are analogous; Table I is a lot to take on faith. None of this makes me think the method is wrong—the underlying DiffPoly domain is published and the implementation is available—but the paper as written does not let a reader verify the derivation.\n\nThe CIFAR results go against the main trend, and the explanation (more unstable ReLUs) is plausible but post hoc. I'd want a bit more on that.\n\nOverall: the contribution is incremental but useful. If the authors fix the notation and pseudocode, and ideally confirm the artifact matches the intended equations, this is a solid conference paper. I'd send it to peer review.\n\nBest,","headline":"Solid incremental contribution to relational neural network verification; the core idea is plausible and the evaluation is strong, but the paper needs typo and notation fixes before the soundness claims are checkable.","tokens_in":27309,"tokens_out":5135,"would_cite":true,"duration_ms":42641,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Relational neuron splitting certifies global robustness faster","keywords":["neural network verification","relational verification","global robustness","branch and bound","relational neurons","dual formulation","abstraction refinement","ReLU networks"],"falsifier":"Implement the second ReLU constraint in Section IV-A exactly as printed for one neuron with pre-activation bounds $[-1,1]$. If the printed formula indeed simplifies to $y\\le0$, then at $x=1$ the LP permits $y=0$ while the true ReLU output is $1$, showing the bound is unsound and that the implementation must use a different formula.","tokens_in":1561,"feed_emoji":"🛡️","tokens_out":3329,"duration_ms":93715,"temperature":0.7,"pith_summary":"This paper claims that relational verification of neural networks—checking properties that compare two runs of the same network, such as global robustness—can be made far more effective by branch-and-bound splitting of relational neurons, the symbolic differences between corresponding neurons in the two runs, rather than splitting individual neurons. It builds a verifier, SABRE, that repeatedly splits the problem by constraining the sign of one relational neuron's pre-activation, making the ReLU difference exact on each branch and thereby tightening the output-difference bound. To pick which relational neuron to split, it extends Lagrangian-dual selection to the two-copy relational setting, scoring each candidate in constant time. On 817 instances across ACAS Xu, MNIST, CIFAR, and GTSRB, the paper reports that relational splitting outperforms individual-splitting baselines in solved instances and verification efficiency on most benchmarks, and that dual-based selection reliably beats random selection.","feed_headline":"Relational neuron splitting certifies global robustness faster","feed_subtitle":"Branching on differences between two network runs solves more verification instances than branching on single neurons.","key_machinery":"The central object is the relational neuron, the difference $\\Delta y^{(i)}_j = y^{(i)}_j - \\hat y^{(i)}_j$ between the outputs of the same neuron in two network copies; its pre-activation difference $\\Delta x^{(i)}_j$ is what gets split. The key mechanism is that after a sign split, the ReLU difference for that neuron is no longer over-approximated but exact on each branch. Selection uses the Lagrangian dual of the linear program that computes relational bounds: the dual objective decomposes into per-neuron terms, so splitting a relational neuron changes only the dual variables and coefficients attached to that index, and the expected bound improvement can be estimated by comparing the dual objective before and after the split in constant time.","core_discovery":"The central claim is that branching directly on the difference between two network inferences exploits the relational structure of the problem. The paper defines relational neurons $\\Delta y^{(i)}_j = y^{(i)}_j - \\hat y^{(i)}_j$ and, at each branch-and-bound step, selects one unstable relational neuron and splits its pre-activation into $\\Delta x^{(i)}_j \\le 0$ and $\\Delta x^{(i)}_j \\ge 0$, making the ReLU difference exact on both branches. A small worked example shows this tightens the output-difference bound more than splitting an individual neuron. The reported experiments confirm the advantage on most benchmarks, with one notable reversal: on CIFAR at small relational input distances, individual splitting solves more instances, which the authors attribute to the high number of unstable ReLUs in that model.","pith_inferences":["The same dual-scored relational split could be applied to other relational properties—universal adversarial perturbations, Lipschitz bounds, or pair-level fairness—wherever the specification constrains the difference between two executions.","A hybrid switching between relational and individual splits, using the same dual score, could close the CIFAR small-$\n\\varepsilon$ gap; the paper itself notes the dual formulation already contains terms for both kinds of neurons.","Because solved counts only count instances the base verifier fails on, a direct comparison on instances solvable at the root would quantify how often branching is unnecessary."],"forward_implications":["Relational specifications like global robustness become practically verifiable on large networks: the paper reports many more solved instances than individual-splitting baselines on ACAS Xu, MNIST-F, MNIST-C, and GTSRB.","The dual-based selection rule is load-bearing: replacing it with random selection lowers solved instances on every benchmark, e.g., from 67 to 44 on ACAS Xu and from 33 to 9 on GTSRB.","Relational splitting is not universally dominant: on CIFAR at small relational perturbations, individual splitting solves more instances, linked to a larger number of unstable ReLUs.","Branch-and-bound keeps verification sound regardless of the split heuristic, so the reported gains are improvements in completeness and efficiency, not a relaxation of soundness."],"supporting_citations":[{"why":"Supplies the relational convex abstraction and bound-propagation rules that the branch-and-bound loop invokes as its base verifier.","marker":"[12]"},{"why":"Supplies the branch-and-bound template and the Lagrangian-dual selection scheme that the paper extends to relational neurons.","marker":"[7]"},{"why":"Defines the global-robustness property and the twin-network encoding that motivates the two-inference verification formulation.","marker":"[11]"},{"why":"Represents the earlier relational branch-and-bound style that splits individual neurons, which the paper adapts as a baseline.","marker":"[17]"},{"why":"Introduces the convex-outer-polytope dual perspective that the per-neuron split-impact estimate relies on.","marker":"[24]"}],"fun_headline_variants":["Branch on neuron differences for faster network proofs","Relational splitting sharpens robustness verification","Splitting difference neurons beats single-neuron cuts","New BaB strategy certifies global robustness quicker"],"cache_read_input_tokens":29568,"weakest_assumption_plain":"The method returns sound certificates only if the relational ReLU over-approximation from the base verifier is faithfully encoded in the linear program; the printed version of the ReLU upper-bound constraint in Section IV-A looks garbled—it simplifies to $y\\le0$—so the implementation must rely on the intended, unprinted formula.","fun_headline_variants_meta":{"raw":{"variants":["Branch on neuron differences for faster network proofs","Relational splitting sharpens robustness verification","Splitting difference neurons beats single-neuron cuts","New BaB strategy certifies global robustness quicker"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000159,"raw_usage":{"total_tokens":1234,"prompt_tokens":959,"completion_tokens":275,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":575,"completion_tokens_details":{"reasoning_tokens":218}},"tokens_in":575,"tokens_out":275,"duration_ms":2903,"temperature":1.0,"reasoning_tokens":218,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T16:25:44.134525+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Implement the second ReLU constraint in Section IV-A exactly as printed for one neuron with pre-activation bounds $[-1,1]$. If the printed formula indeed simplifies to $y\\le0$, then at $x=1$ the LP permits $y=0$ while the true ReLU output is $1$, showing the bound is unsound and that the implementation must use a different formula.","supporting_citations":[{"cited_title":"Input-relational verification of deep neural networks,","cited_arxiv_id":null,"evidence_quote":"Supplies the relational convex abstraction and bound-propagation rules that the branch-and-bound loop invokes as its base verifier."},{"cited_title":"Efficient global robustness certifi- cation of neural networks via interleaving twin-network encoding,","cited_arxiv_id":null,"evidence_quote":"Defines the global-robustness property and the twin-network encoding that motivates the two-inference verification formulation."},{"cited_title":"Relational verification leaps forward with RABBit,","cited_arxiv_id":null,"evidence_quote":"Represents the earlier relational branch-and-bound style that splits individual neurons, which the paper adapts as a baseline."},{"cited_title":"Provable defenses against adversarial examples via the convex outer adversarial polytope,","cited_arxiv_id":null,"evidence_quote":"Introduces the convex-outer-polytope dual perspective that the per-neuron split-impact estimate relies on."}],"review_version":1}