{"id":"4bda6b4d-3793-4766-81e2-49b055373067","arxiv_id":"2412.19985","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The 2024 VNN-COMP report documents that GPU-accelerated linear bound propagation with branch-and-bound, led by α,β-CROWN, dominated both the regular and extended tracks.","lead":"This report summarizes the 2024 International Verification of Neural Networks Competition, detailing the rules, eight participating tools, twenty benchmarks, and final rankings. It provides the community's annual snapshot of which neural network verification approaches work best on standardized hardware.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The ranking trusts unverified UNSAT answers: the scoring protocol only validates counterexamples, so an unsound 'UNSAT' is awarded points; the paper's own Marabou/Gurobi footnote shows this failure mode is real, leaving α,β-CROWN's win conditional on external soundness checks.","rationale":"The reader's weakest assumption correctly identifies the scoring protocol's treatment of UNSAT answers as the load-bearing point. The competition's central data are the scores in Tables 6 and 7, and those scores are built from per-instance verdicts. SAT verdicts are externally validated via counterexample checking, but UNSAT verdicts are only trusted by default. The report itself provides a concrete instance of unsound UNSAT behavior (Marabou on ViT, Section 3.3 footnote), proving the failure mode is not hypothetical. Since the winning tool's margin over PyRAT in the regular track is about 199 points out of 1200, and a single undetected wrong UNSAT costs 160 points relative to a correct SAT answer, only a handful of unsound UNSAT results could change the ranking. The concern is not an attack on the organizers, who were transparent about artifacts and limitations; rather, it is a precise condition that must hold for the empirical conclusion to be trustworthy. The paper's own future-work list includes more rigorous soundness evaluation, reinforcing that the condition is not yet satisfied. An independent re-verification of the default-trusted UNSAT instances would directly settle whether α,β-CROWN's first-place finish is an artifact of the protocol or a genuine state-of-the-art result. The reader's CONDITIONAL verdict is therefore appropriate, and no change to it is needed.","tokens_in":85408,"tokens_out":6701,"duration_ms":61620,"concrete_test":"Using the public per-instance result CSVs and scoring scripts, select every instance where α,β-CROWN returned UNSAT and no other tool produced a valid counterexample (the default-trusted UNSAT set). Re-run these instances with an independent complete verifier that either proves UNSAT with a machine-checkable certificate or returns a valid counterexample, following the hidden-counterexample methodology of reference [91]; validate any counterexample with onnxruntime as in Section 2. Then recompute Tables 6 and 7 with -150 points for each wrong UNSAT. If α,β-CROWN still ranks first in both tracks, the central claim survives; if not, the competition conclusion is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2's scoring rule gives 10 points for a 'correct hold' whenever a tool reports UNSAT and no participant produces a valid counterexample; the burden of proof is placed only on SAT claims. UNSAT answers are therefore accepted on faith when no other tool disputes them. The report itself documents that this faith can be misplaced: the Section 3.3 footnote states that Marabou's competition version was unsound on ViT benchmarks because Gurobi could report 'Infeasible' where counterexamples exist. That unsoundness was discovered only because another team investigated, not by the scoring protocol. The central conclusion—Tables 6 and 7, α,β-CROWN first in both tracks—relies on hundreds of default-trusted UNSAT results (e.g., 194 on NN4Sys, 84 on ViT, 40 on LSNC, and 81 across the two ml4acopf benchmark tables) where no other tool produced a counterexample. If even a few of these are actually SAT, the -150 penalty per wrong result would reduce α,β-CROWN's benchmark scores, potentially changing the normalized totals and the ranking. Section 6 itself lists 'more rigorous soundness evaluation' as a future improvement, acknowledging the gap. Thus the empirical claim is conditional on an unverified soundness assumption.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper reports the rules, benchmarks, participating tools, and results of VNN-COMP 2024, the fifth iteration of the International Verification of Neural Networks Competition. It describes the scoring protocol, the two-track setup (regular and extended), the 8 participating tools, and the benchmark suite, and it presents detailed instance-level results. The central conclusion is that the best-performing tools converge to GPU-enabled linear bound propagation methods using a branch-and-bound framework, with α,β-CROWN achieving first place in both the regular track (Table 6, score 1200.0) and the extended track (Table 7, score 900.0).","tokens_in":85700,"tokens_out":5553,"duration_ms":51291,"significance":"If the results are accepted, this paper provides a valuable community resource: a reproducible, standardized evaluation pipeline, an openly available set of benchmarks and results, and a snapshot of the state of the art in neural network verification as of 2024. The paper is transparent about known issues, including Marabou's unsoundness on ViT benchmarks and the output-format penalties for NeuralSAT and CORA, and it makes raw results and scoring scripts publicly available. The main limitation is that the scoring protocol trusts UNSAT answers without independent soundness validation, which makes the reported ranking conditional on the soundness of the participating tools.","major_comments":[{"comment":"The scoring protocol awards 'correct hold' points to any tool that reports UNSAT when no participating tool produces a valid counterexample within the timeout. This means an unsound UNSAT answer is awarded points and is never penalized unless another tool happens to find a counterexample. The paper itself documents this failure mode in the Section 3.3 footnote: Marabou's competition version was unsound on the ViT benchmarks because Gurobi could report 'Infeasible' where counterexamples exist. Since the central ranking in Tables 6 and 7 relies on large numbers of default-trusted UNSAT results (e.g., 194 in NN4Sys, 84 in ViT, 40 in LSNC), a few undetected false UNSATs would incur -150-point penalties and could change the normalized benchmark scores and the overall ranking. The paper should either validate a sample of UNSAT results with an independent complete verifier or a soundness-focused benchmark, or explicitly state in the abstract and conclusion that the ranking is conditional on the soundness of the reported UNSAT answers.","section":"Section 2, Instance score"},{"comment":"The abstract states that VNN-COMP 2024 had '12 regular and 8 extended benchmarks,' but the extended track results in Appendix A.2 contain nine scored benchmark tables: cctsdb-yolo-2023, collins-aerospace-benchmark, lsnc, ml4acopf-2023, ml4acopf-2024, traffic-signs-recognition-2023, vggnet16-2023, vit-2023, and yolo-2023. The ml4acopf benchmark is split into two scored tables, which suggests nine scored benchmarks unless the paper explicitly defines ml4acopf as a single benchmark with two sub-benchmarks. This inconsistency should be resolved by correcting the count or clarifying the benchmark definition.","section":"Abstract and Section 5.2"},{"comment":"The main text Table 6 reports NeuralSAT with a score of 0 in the regular track, while Appendix B Table 35 reports NeuralSAT with a score of 1113.1 after fixing output-format issues. The 'Update' note mentions this, but the main text and abstract do not indicate which result set is the official ranking, and the two sets differ substantially in the lower half of the table. The paper should explicitly designate one set of results as the official scores and explain the implications for the reported rankings, so that readers are not left to choose between two inconsistent tables.","section":"Section 5.1 and Appendix B"}],"minor_comments":[{"comment":"The section heading 'T erminology' has an erroneous space and should read 'Terminology.'","section":"Section 2, heading"},{"comment":"The abstract contains 'the The 7th International Symposium on AI Verification'; remove the duplicate 'The.'","section":"Abstract"},{"comment":"The phrase 'propagate stes through all linear layers' should be 'propagate sets through all linear layers.'","section":"Section 3.5, nnenum description"},{"comment":"The phrase 'the rool runs on the wide-range of benchmarks' should be 'the tool runs on the wide range of benchmarks.'","section":"Section 3.7, NeuralSAT description"},{"comment":"The paper reports results for the Collins Aerospace, CCTSDB, Metaroom, and yolo benchmarks but states that their descriptions are not yet available; this should be marked as a temporary omission and the descriptions should be added before final publication.","section":"Section 4.17"}],"recommendation":"major_revision","confidential_remarks":"The author list includes several competition organizers who are also tool developers (e.g., Brix is affiliated with the α,β-CROWN team, Wu with Marabou, Bak with nnenum, and Johnson with NNV). This is typical for competition reports and is disclosed, but it makes the soundness-validation issue in the scoring protocol particularly important: the first-place result could be seen as favoring a tool that reports UNSAT aggressively, so an independent check of a sample of UNSAT answers would substantially strengthen the report's credibility."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a solid annual competition report, the strongest part being its transparency—public artifacts, detailed per-instance tables, and an appendix that corrects scoring after tool-format fixes. The headline conclusion (α,β-CROWN wins both tracks, GPU bound propagation with BaB leads) is supported by the scores. But the report is a record of a competition, not a soundness certification. The scoring rule trusts UNSAT answers unless another tool produces a counterexample, and the paper's own Marabou footnote demonstrates that unsound UNSAT is not hypothetical. That's a real limitation, and I'd weight it about as heavily as the reader does—serious but not disqualifying, because the report flags it and the field understands rankings are conditional.\n\nWhat's new: the 2024 datasets (cGAN, LinearizeNN, LSNC, ml4acopf, safeNLP, traffic signs), the per-benchmark scores, and the updated results in Appendix B. The format is familiar from prior years, but the empirical data are new and the artifacts are public, so the results are independently checkable. That's worth real credit.\n\nWhere it's soft: first, the abstract says 8 extended benchmarks while the results score 9 (ml4acopf is split into two). Small but sloppy for a citable report. Second, Section 4.17 admits no descriptions for four benchmarks—Collins Aerospace, CCTSDB, Metaroom, yolo—which limits the reader's ability to interpret those results. Both are minor and fixable.\n\nThe stress-test's worry about UNSAT-trust is legitimate but should be stated precisely: the competition is not designed to prove soundness of every tool, only to compare performance on a fixed benchmark set. The Marabou case shows the failure mode is real, but it was caught by cross-tool investigation, not by the scoring protocol. The report even flags 'more rigorous soundness evaluation' as future work, which is the right call. For α,β-CROWN's win specifically, the margin over PyRAT is large enough that a handful of wrong UNSATs wouldn't flip the ranking; the bigger risk is on benchmarks where only one tool solved many instances (e.g., NN4Sys), but even there the score difference is substantial.\n\nWho it's for: verification researchers who want the year's state-of-the-art snapshot, tool developers choosing where to compete next, and anyone building on these benchmarks. It's not a methods paper and doesn't need to be. I'd send it to peer review—the transparency and reproducibility outweigh the minor inconsistencies. A serious referee should ask for the benchmark count fix and the missing descriptions, but the core is solid.","headline":"A transparent, reproducible competition record whose top-ranking conclusion is plausible but rests on a scoring convention that trusts UNSAT—a limitation the authors themselves acknowledge.","tokens_in":86184,"tokens_out":3573,"would_cite":true,"duration_ms":34851,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Neural-network verifiers are converging on GPU-accelerated linear bound propagation wrapped in branch-and-bound, the 2024 VNN-COMP results show.","keywords":["neural network verification","VNN-COMP 2024","adversarial robustness","bound propagation","branch-and-bound","formal verification benchmarks","GPU acceleration"],"falsifier":"Rerun the 2024 benchmark suite with an independent ground truth—for example, by seeding hidden counterexamples that participants cannot see, or by cross-checking every UNSAT verdict with a different complete solver family—and check whether any tool's UNSAT answers on contested instances are wrong; if even one is wrong, the affected scores and rankings change.","tokens_in":85241,"feed_emoji":"🤖","tokens_out":3860,"duration_ms":41213,"temperature":0.7,"pith_summary":"This report argues that the field of neural-network verification is converging on a single winning recipe: GPU-accelerated linear bound propagation inside a branch-and-bound loop. The evidence comes from the fifth annual VNN-COMP, where eight teams competed on twelve regular and eight extended benchmarks under standardized formats, equal-cost hardware, and an automated evaluation pipeline. The α,β-CROWN tool placed first in both the regular track (1200.0 points) and the extended track (900.0 points), with the abstract-interpretation tool PyRAT second in both. The report's central conclusion is that the best-performing tools seem to converge to this design, and that standardization and automation are lowering the barrier for practitioners.","feed_headline":"Neural-network verifiers converge on one winning recipe","feed_subtitle":"VNN-COMP 2024's top tools share a GPU-accelerated branch-and-bound design; α,β-CROWN takes both tracks.","key_machinery":"The mechanism that carries the argument is the pair (branch-and-bound, linear bound propagation): a complete search splits the verification problem into subproblems by branching on unstable ReLU neurons or input regions, while affine lower and upper bounds are propagated through the network, tightened by gradient-based optimization, split constraints, and cutting planes, with GPUs making the propagation fast enough to scale to large networks. The competition's scoring protocol—10 points per correct verdict, -150 per incorrect verdict, zero for timeouts, and per-benchmark normalization to 100—is the measurement device that turns raw tool outputs into the rankings.","core_discovery":"The competition data show that the top verifiers now cluster around a single algorithmic family: complete branch-and-bound search whose bound-tightening engine is a GPU-optimized linear bound propagator. α,β-CROWN, the winner of both scored tracks, combines CROWN-style affine bound propagation with α-CROWN's joint optimization of intermediate and final bounds, β-CROWN's per-neuron split constraints, cutting planes from GCP-CROWN and BICCOS, and branching for general nonlinearities via GenBaB. The runner-up, PyRAT, uses abstract-interpretation domains on CPU and GPU with its own branch-and-bound heuristics. The report presents per-benchmark scores, cactus plots, and counts of verified and falsified instances to support the conclusion that this convergence is real, while also documenting format-related scoring issues that changed several tools' standings.","pith_inferences":["If the trend continues, competition rankings will increasingly be decided by engineering details—GPU utilization, cut management, branching heuristics—rather than by the choice of the core algorithm family.","The scoring protocol's burden-of-proof rule could be probed directly: a tool that silently returns UNSAT on hard instances where all competitors time out would be rewarded, so a dedicated soundness benchmark with hidden counterexamples would complement the current leaderboard.","The convergence suggests that incomplete verifiers, such as plain abstract interpretation without branch-and-bound, will keep losing ground on hard benchmarks but may remain attractive for easy instances where low latency matters more.","The same bound-propagation engine that wins verification competitions is also used for certified training, so progress in the competition is likely to feed back into training verifiably robust models."],"forward_implications":["If the convergence holds, future verifier development will focus on making bound propagation tighter and faster, and on branching strategies, rather than on entirely new algorithm families.","The success of α,β-CROWN, whose code is openly available, means the state of the art is reproducible and can be adopted by practitioners and researchers.","Large and architecturally rich networks—Vision Transformers, VGGNet-16, generative models, neural Lyapunov controllers—are now within reach of complete verification on standard cloud hardware.","The documented format-related penalties and soundness issues (e.g., Marabou's unsound UNSAT on ViT benchmarks) show that scoring and soundness checking need more rigorous treatment in future editions.","The standardized ONNX/VNN-LIB pipeline and automated evaluation process reduce the overhead of comparing verification tools, making the competition useful beyond the participants."],"supporting_citations":[{"why":"Supplies the branch-and-bound formulation that unifies complete neural-network verification and underpins the winning tools.","marker":"[17]"},{"why":"Introduces automatically derived linear bound propagation (auto LiRPA), the GPU-accelerated engine at the core of α,β-CROWN.","marker":"[83]"},{"why":"Adds per-neuron split constraints to bound propagation, the key to making branch-and-bound efficient in α,β-CROWN.","marker":"[74]"},{"why":"Provides general cutting planes that tighten bounds and contribute to the winning tool's scalability.","marker":"[86]"},{"why":"Extends branch-and-bound to general nonlinearities, enabling the ViT and Lyapunov-stability benchmarks.","marker":"[58]"},{"why":"Describes Marabou, a competing complete solver whose performance and soundness issues are directly compared in the results.","marker":"[38]"},{"why":"Describes nnenum, a star-set reachability tool that serves as a representative of the alternative method family.","marker":"[10]"},{"why":"Describes PyRAT, the second-place abstract-interpretation tool that shows non-bound-propagation approaches remain competitive.","marker":"[48]"},{"why":"Defines the VNN-LIB specification format that standardizes all competition benchmarks.","marker":"[22]"},{"why":"Reports the prior VNN-COMP 2022 iteration whose benchmark design and lessons this edition extends and compares against.","marker":"[54]"}],"fun_headline_variants":["VNN-COMP 2024: One algorithm family dominates","α,β-CROWN sweeps VNN-COMP with branch-and-bound","Top verifiers converge on GPU-accelerated B&B","VNN-COMP 2024: 8 teams, one winning recipe","Branch-and-bound wins again in VNN-COMP 2024"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The scoring system trusts a tool's proof of safety (UNSAT) whenever no participating tool produces a valid counterexample within the timeout, so a tool that falsely reports \"safe\" on instances where everyone else times out would be awarded points for a wrong answer.","fun_headline_variants_meta":{"raw":{"variants":["VNN-COMP 2024: One algorithm family dominates","α,β-CROWN sweeps VNN-COMP with branch-and-bound","Top verifiers converge on GPU-accelerated B&B","VNN-COMP 2024: 8 teams, one winning recipe","Branch-and-bound wins again in VNN-COMP 2024"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000759,"raw_usage":{"total_tokens":3355,"prompt_tokens":912,"completion_tokens":2443,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":528,"completion_tokens_details":{"reasoning_tokens":2350}},"tokens_in":528,"tokens_out":2443,"duration_ms":16976,"temperature":1.0,"reasoning_tokens":2350,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T23:41:49.802551+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Rerun the 2024 benchmark suite with an independent ground truth—for example, by seeding hidden counterexamples that participants cannot see, or by cross-checking every UNSAT verdict with a different complete solver family—and check whether any tool's UNSAT answers on contested instances are wrong; if even one is wrong, the affected scores and rankings change.","supporting_citations":[{"cited_title":"A unified view of piecewise linear neural network verification","cited_arxiv_id":null,"evidence_quote":"Supplies the branch-and-bound formulation that unifies complete neural-network verification and underpins the winning tools."},{"cited_title":"Automatic perturbation analysis for scalable certified robustness and beyond","cited_arxiv_id":null,"evidence_quote":"Introduces automatically derived linear bound propagation (auto LiRPA), the GPU-accelerated engine at the core of α,β-CROWN."},{"cited_title":"General cutting planes for bound-propagation-based neural network verification","cited_arxiv_id":null,"evidence_quote":"Provides general cutting planes that tighten bounds and contribute to the winning tool's scalability."},{"cited_title":"The marabou framework for ver- ification and analysis of deep neural networks","cited_arxiv_id":null,"evidence_quote":"Describes Marabou, a competing complete solver whose performance and soundness issues are directly compared in the results."},{"cited_title":"Supporting standardiza- tion of neural networks verification with vnnlib and coconet","cited_arxiv_id":null,"evidence_quote":"Defines the VNN-LIB specification format that standardizes all competition benchmarks."}],"review_version":1}