{"id":"3127d5d7-e1ce-4dca-8d54-b2204a953e82","arxiv_id":"2505.00963","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"ABONN orders branch-and-bound sub-problems by a counterexample potentiality score and reports speedups of up to 15.2x on MNIST and 24.7x on CIFAR-10 over a naive branch-and-bound baseline.","lead":"This paper presents ABONN, a neural network verifier that uses Monte-Carlo tree search to decide which sub-problems of a branch-and-bound proof tree to explore first. A smart generalist might read it because verification speed is a bottleneck for deploying neural networks in safety-critical systems.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Alg. 1 never propagates found counterexamples or completed subtrees to the root, so the stated termination conditions R(ε)=±∞ cannot fire on multi-level trees; the central speedup claim rests on behavior the pseudocode does not implement.","rationale":"The reader's CONDITIONAL verdict is driven by an underspecified heuristic (p_min) and missing baselines. My stress-test found a more severe, structural problem: as printed, Alg. 1 cannot propagate terminal rewards to the root, making the termination conditions unreachable on any tree deeper than one split. Even if the implementation secretly performs back-propagation, the paper's central algorithmic description does not support its completeness/early-termination claim, and the experiments cannot be interpreted as validating the stated method. This is not a disagreement with community consensus; it is an internal inconsistency. I credit the paper for a complete evaluation setup and a public code link, and I acknowledge that the released implementation may differ from the pseudocode. However, the burden is on the authors to present the algorithm they actually evaluate. If a corrected back-propagation is added and the code is confirmed to match, the paper would move back toward CONDITIONAL/ACCEPT; in its current form, the central claim is not supported. I therefore recommend REJECT rather than CONDITIONAL, because the missing propagation is a correctness defect in the main algorithm, not a missing baseline or a tunable definition.","tokens_in":20981,"tokens_out":6388,"duration_ms":73168,"concrete_test":"Run ABONN on a two-layer ReLU network with a known counterexample requiring depth-2 splitting (root false alarm, child false alarm, counterexample at grandchild). Instrument R(root), R(child), and R(grandchild) after each MCTS-BAB call. If R(root) remains finite negative while R(grandchild)=+∞ and the loop exits only by timeout, the termination flaw is confirmed. Additionally, inspect the released code for an implicit ancestor update after Line 14; if present, revise Alg. 1 to show it and rerun Table II to ensure the reported speedups correspond to the printed algorithm.","verdict_should_be":"REJECT","load_bearing_attack":"The central claim that ABONN is a complete verification algorithm that can terminate early with false on finding a counterexample, or true after visiting all sub-problems, depends on the root reward R(ε) becoming +∞ or −∞. In Alg. 1, rewards are updated only in the expansion branch: Line 20 sets R(Γ) to the max of its newly created children and Line 21 adds those children to T(Γ). The recursive call in Line 14 is followed by no back-propagation statement; after MCTS-BAB returns from a descendant, the ancestor rewards are not recomputed. Consequently, once the root has been expanded, R(ε) is fixed to the initial max over its children. A counterexample found in a grandchild updates R(grandchild) and then R(child), but not R(ε); a fully certified leaf sets R(leaf)=−∞ but again only the immediate parent is updated. The while-loop termination checks in Lines 5–7 therefore cannot fire on any nontrivial tree, and the algorithm would run to timeout even after solving the problem. This is an internal inconsistency between the prose claim of back-propagation 'until the root node' and the printed algorithm. The same listing also uses |T(Γ)| as if it were a visit count in the UCB1 term (Line 13), although T is a set of nodes and is never incremented per visit. The underspecified p_min heuristic is secondary; even if p_min were defined, the search would still not terminate as written.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes ABONN, a branch-and-bound (BaB) verification algorithm for ReLU neural networks that explores the BaB tree in a Monte-Carlo tree search (MCTS) style. It introduces a heuristic called 'counterexample potentiality' that combines the depth of a subproblem with a value p̂ returned by an approximated verifier, and uses a UCB1-style selection rule to prioritize subproblems that are more likely to contain a real counterexample. The authors claim that ABONN remains complete (it can return 'true' after visiting all subproblems) and can terminate early with 'false' upon finding a counterexample. Experiments on 552 verification problems over MNIST and CIFAR-10 report speedups of up to 15.2× and 24.7× over a naive BaB baseline, with additional comparisons against αβ-Crown and studies of the hyperparameters λ and c.","tokens_in":21310,"tokens_out":5140,"duration_ms":51034,"significance":"If the approach works as claimed, it addresses a real bottleneck of BaB-based neural network verification: the order in which subproblems are explored can have a large effect on efficiency, especially on harder CIFAR-10 problems. The paper is clearly written, the problem is well motivated, and the authors make their code and data publicly available. The separation of results for violated and certified instances (RQ3) is a useful sanity check. However, the central algorithmic description in Algorithm 1 has a termination-related inconsistency that calls into question whether the printed algorithm is the one that produced the reported results; the significance can only be assessed after this is resolved.","major_comments":[{"comment":"The back-propagation described in the prose is not implemented in the pseudocode. In Algorithm 1, R(Γ) is updated only at Line 20, which executes when a node's children are first expanded. The recursive call at Line 14 is followed by no update to the rewards of ancestor nodes. Consequently, if a real counterexample is found at depth ≥ 2, the value +∞ is propagated to the parent of the leaf but not to R(ε), the root's reward. Similarly, when all leaves of a deep subtree are verified (JΓK = −∞), the value −∞ is not propagated to the root. The termination checks in Lines 5–7 (R(ε) = ±∞) therefore cannot fire on any tree of depth greater than one, and the algorithm would run to timeout even after the verification problem has been solved. This is an internal inconsistency between the prose claim that rewards are propagated 'until the root node' and the printed algorithm, and it undermines both the completeness claim and the early-termination claim.","section":"§IV-B, Algorithm 1 (Lines 10–21)"},{"comment":"The UCB1 selection term uses |T(Γ)| and |T(Γ·a)| as visit counts, but T is defined as a set of nodes (T(ε) is initialized to {ε} at Line 3, and Line 21 adds newly expanded nodes to the set of the parent). The size of a subtree is not the number of times a node has been visited, and no visit counter is ever incremented anywhere in the algorithm. Thus the exploration term c√(2 ln|T(Γ)|/|T(Γ·a)|) is not a UCB1 term in any standard sense; it is unclear what quantity the algorithm actually optimizes when selecting a child. This is load-bearing because the core efficiency claim rests on the MCTS-style exploration strategy.","section":"§IV-B, Algorithm 1, Line 13"},{"comment":"The quantity p_min (written as p̂_min in the definition) is never defined. The counterexample potentiality JΓK is defined as λ·depth(Γ)/K + (1−λ)·p̂/p_min in the fallback case, and this value is the reward used throughout the MCTS search (Lines 2 and 18 of Algorithm 1). Without knowing how p_min is computed (e.g., the minimum over all subproblems, a fixed constant, or a network-dependent normalization), the reward values, and hence the search order and all reported speedups, are not reproducible. This must be specified before the experimental results can be meaningfully interpreted.","section":"§IV-A, Definition 1"},{"comment":"The hyperparameters λ and c are tuned on the same 552 benchmark problems on which the overall results in RQ1 are reported. The heatmaps in Figure 5 show that the number of solved problems varies by as much as 22 between parameter settings (e.g., for λ=0.0 vs λ=1.0 with c=0.2 in Figure 5c). Since the default λ=0.5 and c=0.2 are selected based on this same set, the reported average speedups may be optimistically biased. The authors should either evaluate on a separate test split, or report the sensitivity in a way that shows the conclusions are robust across a plausible range of parameter choices.","section":"§V-B, RQ2 (Figures 5a–5c)"}],"minor_comments":[{"comment":"Line 20 uses 'arg max' but should be 'max': the intent is to set R(Γ) to the maximum of the children's potentialities, not to return the argument that achieves the maximum.","section":"§IV-B, Algorithm 1, Line 20"},{"comment":"The notation is inconsistent: the prose and the reader's understanding refer to p_min, while the displayed formula uses p̂_min. Please unify the notation and explain the sign conventions, since p̂ is negative in the fallback case and p_min may be negative as well.","section":"§IV-A, Definition 1"},{"comment":"The paper says that 'after visiting all the sub-problems, it can still manage to verify the problem,' but the algorithm as written has no mechanism to detect that all subproblems have been visited independently of the reward propagation. This is related to Major Comment 1; even after fixing back-propagation, a separate completeness condition (e.g., an explicit queue or a check that the tree has no expanded-but-unverified nodes) should be stated.","section":"General"}],"recommendation":"major_revision","confidential_remarks":"The reported code is available online, so it may be that the implementation correctly performs back-propagation and visit counting; if so, the pseudocode must be corrected to match the implementation. The current Algorithm 1, however, cannot terminate with a nontrivial verdict, and this is a load-bearing issue that cannot be waved away. The hyperparameter tuning on the test set is also a concern that should be addressed in the revision. The paper's idea is interesting, and with a corrected algorithm and a more careful evaluation protocol it could be a useful contribution to the BaB verification literature."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing you should know: this paper’s central idea is solid and the CIFAR-10 numbers are impressive, but Algorithm 1 as printed does not do what the prose promises. The prose says rewards are propagated 'until the root node'; the pseudocode only updates the immediate parent after expansion. So a counterexample found three levels down updates that node and its parent, but not the root, and the termination check R(ε)=±∞ can never fire on any tree with more than one split. That is a load-bearing flaw. If the implementation actually back-propagates (as standard MCTS would), the fix is a one-line loop, but as written the algorithm is incomplete.\n\nWhat is genuinely new: using MCTS with a counterexample-potentiality reward to order BaB sub-problem visits is not in the cited branching-heuristic literature, and it is orthogonal to ReLU selection. The reward combining depth and verifier value is a reasonable prior. The empirical results on CIFAR-10 are strong: ABONN solves 106/115 on CIFAR-10BASE versus 27 for naive BaB and 32 for αβ-Crown, with much lower average time. That is a useful practical gain.\n\nSoft spots, in order: (1) the missing back-propagation in the pseudocode, which is the big one; (2) p_min in Definition 1 is never defined, so the potentiality is underspecified; (3) hyperparameters λ and c appear to be selected on the same benchmark suite they are evaluated on, with no separate validation split reported; (4) no variance or confidence intervals are given; (5) a greedy best-first baseline that would isolate the effect of the UCB1 exploration term is absent. The completeness argument itself is fine: if every leaf is certified, the conjunction proves the property, and valid counterexamples are checked.\n\nThe stress-test note is correct about the back-propagation issue; it is not a manufactured concern. The paper needs a corrected algorithm, an explicit back-propagation block, a definition of p_min, and a cleaner evaluation protocol. With those, it would be a worthwhile contribution to the verification community. Without them, the speedups are hard to reproduce or trust.\n\nFor you: if you work on BaB verification, this is worth a reading-group slot and worth citing once the algorithm is fixed. I'd send it to peer review; the idea is important enough to merit referee time even though the current writeup has a serious bug. Recommend major revision.","headline":"The MCTS-guided tree exploration is a real improvement on CIFAR-10, but the printed algorithm has a load-bearing back-propagation bug that must be fixed before the results can be trusted.","tokens_in":21818,"tokens_out":3979,"would_cite":true,"duration_ms":39265,"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":"Branch-and-bound verification becomes faster when the sub-problem tree is explored in an order biased toward sub-problems likely to contain a real counterexample, with speedups up to 24.7x reported on CIFAR-10.","keywords":["neural network verification","branch and bound","Monte-Carlo tree search","counterexample potentiality","adversarial robustness","complete verification","ReLU networks","MCTS"],"falsifier":"On a held-out set of violated CIFAR-10 properties, compute each explored sub-problem's counterexample potentiality and record whether it actually contains a valid counterexample; if, among negative-margin sub-problems, higher potentiality does not correspond to a higher rate of valid counterexamples, the ranking mechanism at the core of ABONN is not doing the work the speedups require.","tokens_in":20812,"feed_emoji":"🧠","tokens_out":12041,"duration_ms":107286,"temperature":0.7,"pith_summary":"Branch-and-bound (BaB) verification of neural networks normally visits sub-problems in a fixed, breadth-first order, ignoring whether a sub-problem is likely to contain a real counterexample. This paper proposes ABONN, an MCTS-style traversal that scores every BaB sub-problem by counterexample potentiality—a blend of how deeply the problem has been split and how far the approximate verifier says it is from being satisfied—and always moves next to the most promising child, while retaining occasional exploration of less-visited branches via UCB1. Because a real counterexample can terminate verification immediately, this ordering lets ABONN refute violated specifications much sooner; if no counterexample exists, completeness is preserved because the whole tree is eventually visited. On 552 MNIST and CIFAR-10 verification problems, ABONN reports speedups up to 15.2x on MNIST and 24.7x on CIFAR-10, and solves substantially more CIFAR-10 instances than either a breadth-first BaB baseline or a strong complete-verifier baseline within a 1000-second budget.","feed_headline":"Adaptive BaB search speeds neural-net verification 24.7x","feed_subtitle":"MCTS-style exploration targets sub-problems likely to contain counterexamples, solving far more CIFAR-10 cases.","key_machinery":"The central object is the counterexample potentiality \\(J\\Gamma K\\) of a sub-problem \\(\\Gamma\\), defined as \\(-\\infty\\) when the approximate verifier reports a positive margin, \\(+\\infty\\) when the returned counterexample is valid, and otherwise \\(\\$\\lambda$\\frac{\\operatorname{depth}(\\Gamma)}{K}+(1-\\$\\lambda$)\\frac{\\hat{p}}{\\hat{p}_{\\min}}\\), where \\(\\$\\lambda$\\in[0,1]\\) weighs the two attributes, \\(K\\) is the number of ReLU neurons, and \\(\\hat{p}\\) is the verifier's negative margin. This reward is used by an MCTS-style traversal: parent rewards are back-propagated as the maximum over children, and UCB1 selects the child \\(a\\) maximizing \\(R(\\Gamma\\cdot a)+c\\sqrt{2\\ln|T(\\Gamma)|/|T(\\Gamma\\cdot a)|}\\). The machinery carries the argument because it changes nothing about the verifier or the splitting rule; it changes only the order in which sub-problems are visited, so any speedup is attributable to exploration order and completeness remains intact.","core_discovery":"The paper's central claim is that the order in which a complete BaB verifier expands its sub-problem tree is itself a source of inefficiency, and that an order biased toward sub-problems likely to contain a real counterexample makes the same verification pipeline faster without sacrificing soundness or completeness. The paper introduces counterexample potentiality as a reward signal: a sub-problem whose approximate verifier returns a positive margin is marked impossible, one whose returned counterexample validates is marked solved, and all others get a weighted score of depth and negative margin. ABONN uses this reward inside a Monte-Carlo tree search with UCB1 selection, so it exploits promising branches but still probes under-visited ones. If a counterexample is found early, the problem is decided false; if the whole tree is exhausted without one, the problem is decided true. The evaluation attributes the gains to this adaptive order, especially on violated CIFAR-10 properties, and shows that the balance parameters matter, with \\(\\$\\lambda$=0.5\\) and \\(c=0.2\\) performing best in their experiments.","pith_inferences":["If counterexample potentiality is as predictive as the reported speedups suggest, the same ranking could serve as an adversarial-attack heuristic on its own, since attack algorithms also want to reach a real counterexample quickly.","A testable refinement is to define \\(\\hat{p}_{\\min}\\) scale-invariantly, since the current definition leaves the score's normalization unspecified; this would make the ordering more portable across networks.","An ablation that separately reports time-to-first-counterexample and number of nodes visited would make the mechanism more transparent and could isolate whether the gains come from visiting fewer sub-problems or from implicitly changing the split sequence.","Because certified-case gains appeared on one convolutional model, explicitly studying how traversal order interacts with ReLU selection could yield further improvements by coupling potentiality with branching decisions."],"forward_implications":["On violated CIFAR-10 properties, ABONN solves 67 to 106 instances per model within the 1000-second budget, versus 23 to 27 for the breadth-first BaB baseline, making complete verification practical for more unsafe networks.","Because ABONN is orthogonal to the ReLU-selection heuristic, the same adaptive order can be layered on top of improved branching strategies, so the speedups should compose with future splitting rules.","On the harder CIFAR-10 model, certified safe properties are also verified faster than by the baseline, suggesting the adaptive order helps the underlying split heuristic obtain tighter bounds.","The hyperparameter study implies a tunable exploration/exploitation trade-off: \\(\\lambda=0.5\\) and \\(c=0.2\\) give the best average time on the tested benchmarks, while pure exploitation is competitive when the potentiality score is reliable."],"supporting_citations":[{"why":"Defines the branch-and-bound verification framework that ABONN adapts; the naive breadth-first version serves as the main baseline.","marker":"[10]"},{"why":"Supplies the Monte-Carlo tree search and UCB1 selection rule that ABONN uses to choose which BaB sub-problem to visit next.","marker":"[11]"},{"why":"Provides the state-of-the-art complete verifier used as a second baseline in the experiments.","marker":"[13]"},{"why":"Provides the ReLU-selection heuristic that ABONN calls when a node must be split.","marker":"[14]"},{"why":"Provides the abstract-domain approximated verifier that returns the margin \\(\\hat{p}\\) and a candidate counterexample for each sub-problem.","marker":"[7]"},{"why":"Provides the fast robustness-certification method also used as the approximated verifier AppVer.","marker":"[16]"},{"why":"Defines the benchmark suite from which the 552 MNIST and CIFAR-10 verification problems are drawn.","marker":"[3]"}],"fun_headline_variants":["MCTS-guided BaB tree search speeds neural net verification 24.7x","Adaptive branching order boosts BaB verification 24.7x","Counterexample-aware tree exploration accelerates NN verification 24.7x","ABONN: prioritize likely counterexamples for faster verification"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the counterexample potentiality score—a weighted combination of tree depth and the verifier's negative margin \\(\\hat{p}\\)—really ranks sub-problems by how likely they are to contain a genuine counterexample; the paper asserts this correlation rather than deriving or validating it, and the normalizing constant \\(\\hat{p}_{\\min}\\) is never defined.","fun_headline_variants_meta":{"raw":{"variants":["MCTS-guided BaB tree search speeds neural net verification 24.7x","Adaptive branching order boosts BaB verification 24.7x","Counterexample-aware tree exploration accelerates NN verification 24.7x","ABONN: prioritize likely counterexamples for faster verification"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000485,"raw_usage":{"total_tokens":2455,"prompt_tokens":1067,"completion_tokens":1388,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":683,"completion_tokens_details":{"reasoning_tokens":1312}},"tokens_in":683,"tokens_out":1388,"duration_ms":12046,"temperature":1.0,"reasoning_tokens":1312,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:31:15.597757+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"On a held-out set of violated CIFAR-10 properties, compute each explored sub-problem's counterexample potentiality and record whether it actually contains a valid counterexample; if, among negative-margin sub-problems, higher potentiality does not correspond to a higher rate of valid counterexamples, the ranking mechanism at the core of ABONN is not doing the work the speedups require.","supporting_citations":[{"cited_title":"A survey of Monte Carlo tree search methods,","cited_arxiv_id":null,"evidence_quote":"Supplies the Monte-Carlo tree search and UCB1 selection rule that ABONN uses to choose which BaB sub-problem to visit next."},{"cited_title":"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,","cited_arxiv_id":null,"evidence_quote":"Provides the state-of-the-art complete verifier used as a second baseline in the experiments."},{"cited_title":"Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis","cited_arxiv_id":null,"evidence_quote":"Provides the ReLU-selection heuristic that ABONN calls when a node must be split."},{"cited_title":"An abstract domain for certifying neural networks,","cited_arxiv_id":null,"evidence_quote":"Provides the abstract-domain approximated verifier that returns the margin \\(\\hat{p}\\) and a candidate counterexample for each sub-problem."},{"cited_title":"Fast and effective robustness certification,","cited_arxiv_id":null,"evidence_quote":"Provides the fast robustness-certification method also used as the approximated verifier AppVer."}],"review_version":1}