Pith. sign in

REVIEW 3 major objections 5 minor 12 cited by

The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results

T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Neural-network verifiers are converging on GPU-accelerated linear bound propagation wrapped in branch-and-bound, the 2024 VNN-COMP results show.

desk verdict 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. read the letter →

arxiv 2412.19985 v1 pith:QBLB452D submitted 2024-12-28 cs.LG cs.AI

Christopher Brix , Stanley Bak , Taylor T. Johnson , Haoze Wu This is my paper · ORCID
classification cs.LGcs.AI
keywords neuralnetworkverificationVNN-COMP2024adversarialrobustnessboundpropagationbranch-and-boundformalbenchmarksGPUacceleration
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

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).

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 (3)
  1. [Section 2, Instance score] 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.
  2. [Abstract and Section 5.2] 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.
  3. [Section 5.1 and Appendix B] 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.
minor comments (5)
  1. [Section 2, heading] The section heading 'T erminology' has an erroneous space and should read 'Terminology.'
  2. [Abstract] The abstract contains 'the The 7th International Symposium on AI Verification'; remove the duplicate 'The.'
  3. [Section 3.5, nnenum description] The phrase 'propagate stes through all linear layers' should be 'propagate sets through all linear layers.'
  4. [Section 3.7, NeuralSAT description] The phrase 'the rool runs on the wide-range of benchmarks' should be 'the tool runs on the wide range of benchmarks.'
  5. [Section 4.17] 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.

Circularity Check

1 steps flagged · score 2.0 of 10

The UNSAT scoring rule makes part of the ranking an agreement score; the central conclusion is otherwise empirical and not circularly derived.

  1. self definitional [Section 2, 'Instance score' paragraph, and Tables 6/7 in Section 5]
    "However, the ground truth for any given instance is generally not known a priori. In the case of disagreement between tools, we, therefore, place the burden of proof on the tool claiming that a specification is violated, i.e. that a counterexample can be found, and deem it correct exactly if it produces a valid counterexample."

    Combined with the preceding bullet ('Correct hold (property proven): 10 points'), this rule awards UNSAT points whenever a tool reports UNSAT and no participating tool produces a valid counterexample. Thus the 'correct hold' counts feeding the normalized scores in Tables 6 and 7 are, by construction, counts of uncontradicted UNSAT reports rather than independently established property truth. The UNSAT component of the ranking therefore measures agreement among the particular set of participants, not an external ground truth. The paper itself documents the failure mode: the Section 3.3 footnote reports that Marabou's competition version returned 'Infeasible' on ViT benchmarks where counterexamples are expected, and Section 6 lists 'more rigorous soundness evaluation' as future work.

full rationale

This is a competition summary built from empirical runs, not a mathematical derivation, so most of its content is self-contained measurement rather than circular reasoning. The one definitional coupling is the UNSAT scoring rule: without an external oracle, a 'correct hold' is operationally identical to 'UNSAT report with no counterexample produced by any participant,' making part of the score self-referential. This is transparently acknowledged in the paper, which states that ground truth is not known a priori, and the paper explicitly flags soundness gaps in the ViT benchmark section ('this version of the benchmark may not be able to reflect soundness issues in verifiers') and in the future-work list. The self-citations in tool descriptions (e.g., the alpha,beta-CROWN method papers) are descriptive rather than load-bearing: the rankings are computed from actual runs, not from those citations. The SAT half of the results is independently checked through counterexample validation, so the central empirical content does not reduce to a fitted parameter or a self-citation chain. Overall, the circularity is mild and localized to the definition of UNSAT correctness, warranting a score of 2.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The report is an empirical competition summary; it introduces no free parameters or new entities. Its claims rest on the scoring protocol and on the correctness of the evaluation pipeline.

assumptions (2)
  • domain assumption Ground truth is determined by the burden-of-proof rule: a SAT claim is correct iff it produces a valid counterexample; UNSAT claims are accepted when no counterexample is found.
    This is the scoring rule in Section 2; it assumes that the absence of counterexamples among participating tools implies the property is truly UNSAT, which can fail if a tool is unsound.
  • domain assumption Counterexample outputs are validated using onnxruntime; missing or differing outputs in counterexample files are discarded and only inputs are used.
    Section 2 (Scoring) states that all outputs in counterexample files were discarded and evaluation was based solely on inputs and onnxruntime-computed outputs; this assumes onnxruntime correctly computes the network behavior.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results." pith.science (2026). https://pith.science/paper/QBLB452D

@misc{pith2026241219985,
  author       = {Pith},
  title        = {Pith review of: The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QBLB452D}},
  note         = {Machine review of arXiv:2412.19985}
}
read the original abstract

This report summarizes the 5th International Verification of Neural Networks Competition (VNN-COMP 2024), held as a part of the 7th International Symposium on AI Verification (SAIV), that was collocated with the 36th International Conference on Computer-Aided Verification (CAV). VNN-COMP is held annually to facilitate the fair and objective comparison of state-of-the-art neural network verification tools, encourage the standardization of tool interfaces, and bring together the neural network verification community. To this end, standardized formats for networks (ONNX) and specification (VNN-LIB) were defined, tools were evaluated on equal-cost hardware (using an automatic evaluation pipeline based on AWS instances), and tool parameters were chosen by the participants before the final test sets were made public. In the 2024 iteration, 8 teams participated on a diverse set of 12 regular and 8 extended benchmarks. This report summarizes the rules, benchmarks, participating tools, results, and lessons learned from this iteration of this competition.

Figures

Figures reproduced from arXiv: 2412.19985 by the authors.

Figure 1
Figure 1. Accuracy Efficient Architecture for GTSRB and Belgium dataset [PITH_FULL_IMAGE:figures/full_fig_p018_1.png] view at source ↗
Figure 4
Figure 4. Generic approach to generating the NLP verification pipelines [18, 19] deployed to obtain the safeNLP benchmark. to train the neural network to be robust on them. The problem was that each of the existing approaches [36, 34, 77, 89, 75, 42, 25, 61, 14] used parts of this pipeline in different ways, which made it difficult to compare or audit the results. In [18, 19], we made a generic implementation of this pipeline… view at source ↗
Figure 5
Figure 5. Cactus Plot for All Instances (Regular Track). [PITH_FULL_IMAGE:figures/full_fig_p024_5.png] view at source ↗
Figures from the paper (24 more)
Figure 6
Figure 6. Figure 6: Cactus Plot for All Instances (Extended Track). [PITH_FULL_IMAGE:figures/full_fig_p025_6.png]
Figure 7
Figure 7. Figure 7: Cactus Plot for acasxu 2023. 35 [PITH_FULL_IMAGE:figures/full_fig_p035_7.png]
Figure 8
Figure 8. Figure 8: Cactus Plot for cgan 2023. 36 [PITH_FULL_IMAGE:figures/full_fig_p036_8.png]
Figure 9
Figure 9. Figure 9: Cactus Plot for cifar100. 37 [PITH_FULL_IMAGE:figures/full_fig_p037_9.png]
Figure 10
Figure 10. Figure 10: Cactus Plot for collins rul cnn 2023. 38 [PITH_FULL_IMAGE:figures/full_fig_p038_10.png]
Figure 11
Figure 11. Figure 11: Cactus Plot for cora. 39 [PITH_FULL_IMAGE:figures/full_fig_p039_11.png]
Figure 12
Figure 12. Figure 12: Cactus Plot for dist shift 2023. 40 [PITH_FULL_IMAGE:figures/full_fig_p040_12.png]
Figure 13
Figure 13. Figure 13: Cactus Plot for linearizenn. 41 [PITH_FULL_IMAGE:figures/full_fig_p041_13.png]
Figure 14
Figure 14. Figure 14: Cactus Plot for metaroom 2023. 42 [PITH_FULL_IMAGE:figures/full_fig_p042_14.png]
Figure 15
Figure 15. Figure 15: Cactus Plot for nn4sys 2023. 43 [PITH_FULL_IMAGE:figures/full_fig_p043_15.png]
Figure 16
Figure 16. Figure 16: Cactus Plot for safenlp. 44 [PITH_FULL_IMAGE:figures/full_fig_p044_16.png]
Figure 17
Figure 17. Figure 17: Cactus Plot for tinyimagenet [PITH_FULL_IMAGE:figures/full_fig_p045_17.png]
Figure 18
Figure 18. Figure 18: Cactus Plot for tllverifybench 2023. 46 [PITH_FULL_IMAGE:figures/full_fig_p046_18.png]
Figure 19
Figure 19. Figure 19: Cactus Plot for cctsdb yolo 2023. 47 [PITH_FULL_IMAGE:figures/full_fig_p047_19.png]
Figure 20
Figure 20. Figure 20: Cactus Plot for collins aerospace benchmark. [PITH_FULL_IMAGE:figures/full_fig_p048_20.png]
Figure 21
Figure 21. Figure 21: Cactus Plot for lsnc. 49 [PITH_FULL_IMAGE:figures/full_fig_p049_21.png]
Figure 22
Figure 22. Figure 22: Cactus Plot for ml4acopf 2023. 50 [PITH_FULL_IMAGE:figures/full_fig_p050_22.png]
Figure 23
Figure 23. Figure 23: Cactus Plot for ml4acopf 2024. 51 [PITH_FULL_IMAGE:figures/full_fig_p051_23.png]
Figure 24
Figure 24. Figure 24: Cactus Plot for traffic signs recognition 2023. [PITH_FULL_IMAGE:figures/full_fig_p052_24.png]
Figure 25
Figure 25. Figure 25: Cactus Plot for vggnet16 2023. 53 [PITH_FULL_IMAGE:figures/full_fig_p053_25.png]
Figure 26
Figure 26. Figure 26: Cactus Plot for vit 2023. 54 [PITH_FULL_IMAGE:figures/full_fig_p054_26.png]
Figure 27
Figure 27. Figure 27: Cactus Plot for yolo 2023. 55 [PITH_FULL_IMAGE:figures/full_fig_p055_27.png]
Figure 28
Figure 28. Figure 28: Cactus Plot for All Instances (Regular Track). [PITH_FULL_IMAGE:figures/full_fig_p057_28.png]
Figure 29
Figure 29. Figure 29: Cactus Plot for All Instances (Extended Track). [PITH_FULL_IMAGE:figures/full_fig_p057_29.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 12 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. IoUCert: Robustness Verification for Anchor-based Object Detectors

    cs.LG 2026-03 conditional novelty 7.0 of 10

    IoUCert derives exact IoU bounds over anchor-offset boxes via a coordinate transformation and uses them to formally verify single-object SSD, YOLOv2, and YOLOv3 models under brightness, contrast, and motion-blur pertu...

  2. Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

    eess.SY 2025-07 conditional novelty 7.0 of 10

    A dL/dGL-based method that verifies infinite-horizon safety of neural network controllers under bounded finite-precision perturbations and synthesizes sound mixed-precision fixed-point implementations.

  3. Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification

    cs.LG 2025-06 conditional novelty 7.0 of 10

    Semidefinite relaxation for deep ReLU verification suffers from 'interior-point vanishing' as depth increases, and removing layer-wise bound constraints mitigates it.

  4. SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming

    cs.LG 2025-06 reject novelty 7.0 of 10

    SDP-CROWN's deep-network integration is unsound: the per-layer L2 ball is centered at the linear network's preactivation instead of the actual forward preactivation, allowing invalid robustness certificates.

  5. Branch and Bound for Relational Verification of Neural Networks

    cs.LG 2026-08 conditional novelty 6.0 of 10

    SABRE verifies global robustness of ReLU networks by branch-and-bound splitting of relational neurons, guided by a dual-formulation selection heuristic.

  6. Learning Lookahead Lemmas for Neural Network Verification

    cs.LG 2026-07 conditional novelty 6.0 of 10

    A lookahead-based inprocessing framework derives implication lemmas over ReLU phases and vivifies boolean cuts, solving up to 34% more unsatisfiable instances in Marabou and α-β-CROWN.

  7. Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification

    cs.LO 2025-12 conditional novelty 6.0 of 10

    A DQfD-trained ReLU-splitting policy modestly improves Marabou's average verification time on ACAS Xu, but not the number of iterations as claimed.

  8. Efficient Certified Reasoning for Binarized Neural Networks

    cs.LG 2025-06 unverdicted novelty 6.0 of 10

    A native BNN-aware solver and proof-checking pipeline certifies 99% of qualitative and 86% of quantitative robustness queries, with 9x and 218x speedups over prior certified baselines.

  9. Neural Network Verification for Gliding Drone Control: A Case Study

    cs.RO 2025-05 conditional novelty 6.0 of 10

    A case study shows that combining Marabou/Vehicle with CORA can partially verify neural-network controllers for Alsomitra-inspired gliders, but practical guarantees remain out of reach.

  10. A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification

    cs.AI 2025-02 conditional novelty 6.0 of 10

    Probabilistic NeSy robustness can be verified approximately by compiling neural and symbolic parts into one arithmetic graph and running interval bound propagation, with an NPPP-completeness result for the exact version.

  11. SAIL: Sound Abstract Interpreters with LLMs

    cs.PL 2025-11 reject novelty 5.0 of 10

    SAIL synthesizes globally sound abstract transformers for neural-network operators by combining LLM generation with syntactic validation, SMT-based soundness checking, and cost-guided iterative refinement.

  12. Neural Network Verification is a Programming Language Challenge

    cs.PL 2025-01 conditional novelty 4.0 of 10

    Neural network verification's hardest open problems are reframed as programming language design challenges, with a unified dependently typed language proposed as the ideal solution.

Reference graph

Works this paper leans on

92 extracted references · 66 canonical work pages · cited by 12 Pith papers

  1. [1]

    https://www.kaggle.com/datasets/shazaelmorsh/ trafficsigns

    Belgian Traffic Sign Database. https://www.kaggle.com/datasets/shazaelmorsh/ trafficsigns. Accessed: March 25th, 2023

    2023

  2. [2]

    https://www.kaggle.com/datasets/dmitryyemelyanov/ chinese-traffic-signs

    Chinese Traffic Sign Database. https://www.kaggle.com/datasets/dmitryyemelyanov/ chinese-traffic-signs . Accessed: March 25th, 2023

    2023

  3. [3]

    https://https://cora.in.tum.de//

    CORA: A Tool for Continuous Reachability Analysis . https://https://cora.in.tum.de//. Accessed: October 15th, 2024

    2024

  4. [4]

    https://www.kaggle.com/datasets/ meowmeowmeowmeowmeow/gtsrb-german-traffic-sign?datasetId=82373&language=Python

    German Traffic Sign Recognition Benchmark. https://www.kaggle.com/datasets/ meowmeowmeowmeowmeow/gtsrb-german-traffic-sign?datasetId=82373&language=Python . Accessed: March 25th, 2023

    2023

  5. [5]

    https://pyrat-analyzer.com/

    PyRAT Analyzer website. https://pyrat-analyzer.com/. Accessed: December 20th, 2024

    2024

  6. [6]

    Risk-graded safety for handling medical queries in conver- sational ai

    Gavin Abercrombie and Verena Rieser. Risk-graded safety for handling medical queries in conver- sational ai. In Proceedings of the 2nd Conference of the Asia-Pacific Chapter of the Association for Computational Linguistics and the 12th International Joint Conference on Natural Language Processing, pages 234–243, 2022

    2022

  7. [7]

    An introduction to CORA 2015

    Matthias Althoff. An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH) , pages 120–151, 2015

    2015

  8. [8]

    Verification of Neural Network Control Systems in Continuous Time , page 100–115

    Ali ArjomandBigdeli, Andrew Mata, and Stanley Bak. Verification of Neural Network Control Systems in Continuous Time , page 100–115. Springer Nature Switzerland, 2024

    2024

Show all 92 references
  1. [9]

    Execution-guided overapproximation (ego) for improving scalability of neural network verification, 2020

    Stanley Bak. Execution-guided overapproximation (ego) for improving scalability of neural network verification, 2020

    2020

  2. [10]

    nnenum: Verification of relu neural networks with optimized abstraction refinement

    Stanley Bak. nnenum: Verification of relu neural networks with optimized abstraction refinement. In NASA Formal Methods Symposium , pages 19–36. Springer, 2021

    2021

  3. [11]

    The second international verification of neural networks competition (vnn-comp 2021): Summary and results, 2021

    Stanley Bak, Changliu Liu, and Taylor Johnson. The second international verification of neural networks competition (vnn-comp 2021): Summary and results, 2021

    2021

  4. [12]

    Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, and Taylor T. Johnson. Improved geometric path enumeration for verifying ReLU neural networks. In 32nd International Conference on Computer- Aided Verification (CA V), July 2020

    2020

  5. [13]

    Patient and consumer safety risks when using conversational assistants for medical information: an observational study of siri, alexa, and google assistant

    Timothy W Bickmore, Ha Trinh, Stefan Olafsson, Teresa K O’Leary, Reza Asadi, Nathaniel M Rickles, and Ricardo Cruz. Patient and consumer safety risks when using conversational assistants for medical information: an observational study of siri, alexa, and google assistant. Jour...

    2018

  6. [14]

    Fast and precise certification of transformers

    Gregory Bonaert, Dimitar I Dimitrov, Maximilian Baader, and Martin Vechev. Fast and precise certification of transformers. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , pages 466–481, 2021

    2021

  7. [15]

    Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international verification of neural networks competition (vnn-comp 2023): Summary and results. 2023

    2023

  8. [16]

    Johnson, and Changliu Liu

    Christopher Brix, Mark Niklas M¨ uller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (vnn-comp), 2023

    2023

  9. [17]

    A unified view of piecewise linear neural network verification

    Rudy Bunel, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. A unified view of piecewise linear neural network verification. Advances in Neural Information Processing Systems, 2018

    2018

  10. [18]

    Antonio: Towards a systematic method for gener- ating nlp benchmarks for verification

    Marco Casadio, Luca Arnaboldi, Matthew L Daggitt, Omri Isac, Tanvi Dinkar, Daniel Kienitz, Verena Rieser, and Ekaterina Komendantskaya. Antonio: Towards a systematic method for gener- ating nlp benchmarks for verification. In Proceedings of the 6th Workshop on Formal , volume ...

    2023

  11. [19]

    Nlp verification: Towards a general method- 29 VNN-COMP 2024 Report C

    Marco Casadio, Tanvi Dinkar, Ekaterina Komendantskaya, Luca Arnaboldi, Omri Isac, Matthew L Daggitt, Guy Katz, Verena Rieser, and Oliver Lemon. Nlp verification: Towards a general method- 29 VNN-COMP 2024 Report C. Brix, S. Bak, T. Johnson, H. Wu ology for certifying robustnes...

    2024 arXiv

  12. [20]

    Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli

    Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli. Neural network robustness as a verification property: A principled case study. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th Interna- t...

    2022

  13. [21]

    Gonzalez, Ion Stoica, and Eric P

    Wei-Lin Chiang, Zhuohan Li, Zi Lin, Ying Sheng, Zhanghao Wu, Hao Zhang, Lianmin Zheng, Siyuan Zhuang, Yonghao Zhuang, Joseph E. Gonzalez, Ion Stoica, and Eric P. Xing. Vicuna: An open-source chatbot impressing gpt-4 with 90%* chatgpt quality, March 2023

    2023

  14. [22]

    Supporting standardiza- tion of neural networks verification with vnnlib and coconet

    Stefano Demarchi, Dario Guidotti, Luca Pulina, and Armando Tacchella. Supporting standardiza- tion of neural networks verification with vnnlib and coconet. In Nina Narodytska, Guy Amir, Guy Katz, and Omri Isac, editors, Proceedings of the 6th Workshop on Formal Methods for ML-...

    2023

  15. [23]

    Never2: Learning and verification of neural networks

    Stefano Demarchi, Dario Guidotti, Luca Pulina, and Armando Tacchella. Never2: Learning and verification of neural networks. Soft Computing , 2024

    2024

  16. [24]

    An image is worth 16x16 words: Transformers for image recognition at scale

    Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, et al. An image is worth 16x16 words: Transformers for image recognition at scale. In International Con...

    2020

  17. [25]

    Cert-rnn: Towards certifying the robustness of recurrent neural networks

    Tianyu Du, Shouling Ji, Lujia Shen, Yao Zhang, Jinfeng Li, Jie Shi, Chengfang Fang, Jianwei Yin, Raheem Beyah, and Ting Wang. Cert-rnn: Towards certifying the robustness of recurrent neural networks. CCS, 21(2021):15–19, 2021

    2021

  18. [26]

    A DPLL(T) Framework for Verifying Deep Neural Networks, 2023

    Hai Duong, Linhan Li, ThanhVu Nguyen, and Matthew Dwyer. A DPLL(T) Framework for Verifying Deep Neural Networks, 2023. arXiv, 25 pages

    2023

  19. [27]

    Harnessing neuron stability to improve dnn verification

    Hai Duong, Dong Xu, ThanhVu Nguyen, and Matthew B Dwyer. Harnessing neuron stability to improve dnn verification. Proceedings of the ACM on Software Engineering , 1(FSE):859–881, 2024

    2024

  20. [28]

    Reciph: Relational coefficients for input partitioning heuristic

    Serge Durand, Augustin Lemesle, Zakaria Chihani, Caterina Urban, and Fran¸ cois Terrier. Reciph: Relational coefficients for input partitioning heuristic. In 1st Workshop on Formal Verification of Machine Learning (WFVML 2022) , 2022

    2022

  21. [29]

    Formal Methods use for Learning Assurance (ForMuLA)

    EASA and Collins Aerospace. Formal Methods use for Learning Assurance (ForMuLA). Technical report, April 2023

    2023

  22. [30]

    Fast BATLLNN: fast box analysis of two- level lattice neural networks

    James Ferlez, Haitham Khedr, and Yasser Shoukry. Fast BATLLNN: fast box analysis of two- level lattice neural networks. In Ezio Bartocci and Sylvie Putot, editors, HSCC ’22: 25th ACM International Conference on Hybrid Systems: Computation and Control, Milan, Italy, May 4 - 6, ...

    2022

  23. [31]

    On the effectiveness of interval bound propagation for training verifiably robust models

    Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715 , 2018

    arXiv

  24. [32]

    The rua-robot dataset: Helping avoid chatbot deception by detecting user questions about human or non-human identity

    David Gros, Yu Li, and Zhou Yu. The rua-robot dataset: Helping avoid chatbot deception by detecting user questions about human or non-human identity. In Proceedings of the 59th An- nual Meeting of the Association for Computational Linguistics and the 11th International Joint C...

    2021

  25. [33]

    pynever: A framework for learning and verification of neural networks

    Dario Guidotti, Luca Pulina, and Armando Tacchella. pynever: A framework for learning and verification of neural networks. In Automated Technology for Verification and Analysis: 19th Inter- national Symposium, ATV A 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Procee...

    2021

  26. [34]

    Achieving verified robustness to symbol sub- 30 VNN-COMP 2024 Report C

    Po-Sen Huang, Robert Stanforth, Johannes Welbl, Chris Dyer, Dani Yogatama, Sven Gowal, Krishnamurthy Dvijotham, and Pushmeet Kohli. Achieving verified robustness to symbol sub- 30 VNN-COMP 2024 Report C. Brix, S. Bak, T. Johnson, H. Wu stitutions via interval bound propagation...

    2024

  27. [35]

    Binarized Neural Networks

    Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El-Yaniv, and Yoshua Bengio. Binarized Neural Networks. Advances in Neural Information Processing Systems , 29, 2016

    2016

  28. [36]

    Certified robustness to adversar- ial word substitutions

    Robin Jia, Aditi Raghunathan, Kerem G¨ oksel, and Percy Liang. Certified robustness to adversar- ial word substitutions. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Pro...

    2019

  29. [37]

    Reluplex: An efficient smt solver for verifying deep neural networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pages 97–117. Springer, 2017

    2017

  30. [38]

    The marabou framework for ver- ification and analysis of deep neural networks

    Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji´ c, et al. The marabou framework for ver- ification and analysis of deep neural networks. In International Conference on Computer Ai...

    2019

  31. [39]

    Katz, Anthony L

    Sydney M. Katz, Anthony L. Corso, Christopher A. Strong, and Mykel J. Kochenderfer. Verifica- tion of image-based neural network controllers using generative models, 2021

    2021

  32. [40]

    Benchmark: remaining useful life predictor for aircraft equipment

    Dmitrii Kirov and Simone Fulvio Rollini. Benchmark: remaining useful life predictor for aircraft equipment. In International Conference on Bridging the Gap between AI and Reality , pages 299–

  33. [41]

    Formal verification of a neural network based prognostics system for aircraft equipment

    Dmitrii Kirov, Simone Fulvio Rollini, Luigi Di Guglielmo, and Darren Cofer. Formal verification of a neural network based prognostics system for aircraft equipment. In International Conference on Bridging the Gap between AI and Reality , pages 225–240. Springer, 2023

    2023

  34. [42]

    Popqorn: Quantifying robustness of recurrent neural networks

    Ching-Yun Ko, Zhaoyang Lyu, Lily Weng, Luca Daniel, Ngai Wong, and Dahua Lin. Popqorn: Quantifying robustness of recurrent neural networks. In International Conference on Machine Learning, pages 3468–3477. PMLR, 2019

    2019

  35. [43]

    Open- and closed- loop neural network verification using polynomial zonotopes

    Niklas Kochdumper, Christian Schilling, Matthias Althoff, and Stanley Bak. Open- and closed- loop neural network verification using polynomial zonotopes. In NASA Formal Methods , pages 16–36, 2023

    2023

  36. [44]

    Set-based training for neural network verifi- cation

    Lukas Koller, Tobias Ladner, and Matthias Althoff. Set-based training for neural network verifi- cation. arXiv preprint arXiv:2401.14961 , 2024

    2024 arXiv

  37. [45]

    Eu artificial intelligence act: The european approach to ai, 2021

    Mauritz Kop. Eu artificial intelligence act: The european approach to ai, 2021

    2021

  38. [46]

    The case for learned index structures

    Tim Kraska, Alex Beutel, Ed H Chi, Jeffrey Dean, and Neoklis Polyzotis. The case for learned index structures. In Proceedings of the 2018 International Conference on Management of Data , 2018

    2018

  39. [47]

    Automatic abstraction refinement in neural network verifi- cation using sensitivity analysis

    Tobias Ladner and Matthias Althoff. Automatic abstraction refinement in neural network verifi- cation using sensitivity analysis. In Proc. of the Int. Conf. on Hybrid Systems: Computation and Control (HSCC), pages 1–13, 2023

    2023

  40. [48]

    Neural Network Verification with PyRAT

    Augustin Lemesle, Julien Lehmann, and Le Gall Tristan. Neural Network Verification with PyRAT. arXiv preprint arXiv:2410.23903 , 2024

    2024 arXiv

  41. [49]

    Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T. Johnson. NNV 2.0: The neural network verification tool. In 35th International Conference on Computer-Aided Verification (CA V), July 2023

    2023

  42. [50]

    Towards deep learning models resistant to adversarial attacks

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083 , 2017

    2017 arXiv

  43. [51]

    Towards deep learning models resistant to adversarial attacks

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In International Conference on Learning Representations, 2018. 31 VNN-COMP 2024 Report C. Brix, S. Bak, T. Johnson, H. Wu

    2018

  44. [52]

    Reachability analysis of a general class of neural ordinary differential equation

    Diego Manzanas Lopez, Patrick Musau, Nathaniel Hamilton, and Taylor Johnson. Reachability analysis of a general class of neural ordinary differential equation. In Proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022), ...

    2022

  45. [53]

    Evaluating the robustness of neural language models to input perturbations

    Milad Moradi and Matthias Samwald. Evaluating the robustness of neural language models to input perturbations. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 1558–1570, 2021

    2021

  46. [54]

    The third international verification of neural networks competition (vnn-comp 2022): Summary and results

    Mark Niklas M¨ uller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson. The third international verification of neural networks competition (vnn-comp 2022): Summary and results. arXiv preprint arXiv:2212.10376 , 2022

    2022 arXiv

  47. [55]

    Architecturing binarized neural networks for traffic sign recognition

    Andreea Postovan and M˘ ad˘ alina Era¸ scu. Architecturing binarized neural networks for traffic sign recognition. arXiv preprint arXiv:2303.15005 , 2023

    2023 arXiv

  48. [56]

    Sentence-BERT: Sentence embeddings using Siamese BERT- networks

    Nils Reimers and Iryna Gurevych. Sentence-BERT: Sentence embeddings using Siamese BERT- networks. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP- IJCNLP)...

    2019

  49. [57]

    Certified training with branch-and-bound: A case study on lyapunov-stable neural control

    Zhouxing Shi, Cho-Jui Hsieh, and Huan Zhang. Certified training with branch-and-bound: A case study on lyapunov-stable neural control. arXiv preprint arXiv:2411.18235 , 2024

    2024 arXiv

  50. [58]

    Neu- ral network verification with branch-and-bound for general nonlinearities

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Neu- ral network verification with branch-and-bound for general nonlinearities. arXiv preprint arXiv:2405.21063, 2024

    2024 arXiv

  51. [59]

    Fast certified robust training with short warmup

    Zhouxing Shi, Yihan Wang, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. Fast certified robust training with short warmup. Advances in Neural Information Processing Systems, 34:18335–18349, 2021

    2021

  52. [60]

    Robustness veri- fication for transformers

    Zhouxing Shi, Huan Zhang, Kai-Wei Chang, Minlie Huang, and Cho-Jui Hsieh. Robustness veri- fication for transformers. In International Conference on Learning Representations , 2019

    2019

  53. [61]

    Robustness veri- fication for transformers, 2020

    Zhouxing Shi, Huan Zhang, Kai-Wei Chang, Minlie Huang, and Cho-Jui Hsieh. Robustness veri- fication for transformers, 2020

    2020

  54. [62]

    Very deep convolutional networks for large-scale image recognition

    Karen Simonyan and Andrew Zisserman. Very deep convolutional networks for large-scale image recognition. arXiv preprint arXiv:1409.1556 , 2014

    2014 arXiv

  55. [63]

    Gagandeep Singh, Timon Gehr, Markus P¨ uschel, and Martin T. Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(POPL):41:1–41:30, 2019

    2019

  56. [64]

    Intriguing Properties of Neural Networks

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfel- low, and Rob Fergus. Intriguing Properties of Neural Networks. arXiv preprint arXiv:1312.6199 , 2013

    2013 arXiv

  57. [65]

    Xiao, and Russ Tedrake

    Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In ICLR, 2019

    2019

  58. [66]

    H. D. Tran, N. Pal, D. Lopez, P. Musau, X. Yang, W. Xiang L. Nguyen, S. Bak, , and T. T. Johnson. Verification of piecewise deep neural networks: A star set approach with zonotope pre-filter. Formal aspects of computing, 2021

    2021

  59. [67]

    Hoang-Dung Tran, Stanley Bak, Weiming Xiang, and Taylor T. Johnson. Verification of deep convolutional neural networks using imagestars. In 32nd International Conference on Computer- Aided Verification (CA V). Springer, July 2020

    2020

  60. [68]

    Johnson, and Xenofon Kout- soukos

    Hoang-Dung Tran, Feiyang Cei, Diego Manzanas Lopez, Taylor T. Johnson, and Xenofon Kout- soukos. Safety verification of cyber-physical systems with reinforcement learning control. In ACM SIGBED International Conference on Embedded Software (EMSOFT’19) . ACM, October 2019

    2019

  61. [69]

    Verification of recurrent neural networks using star reachability

    Hoang Dung Tran, SungWoo Choi, Tomoya Yamaguchi, Bardh Hoxha, and Danil Prokhorov. Verification of recurrent neural networks using star reachability. In The 26th ACM International 32 VNN-COMP 2024 Report C. Brix, S. Bak, T. Johnson, H. Wu Conference on Hybrid Systems: Computat...

    2024

  62. [70]

    Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. Star-based reachability analysis for deep neural networks. In 23rd International Symposium on Formal Methods (FM’19) . Springer International Publishing...

    2019

  63. [71]

    Hamilton, Diego Manzanas Lopez, Stanley Bak, and Taylor T

    Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Xiaodong Yang, Nathaniel P. Hamilton, Diego Manzanas Lopez, Stanley Bak, and Taylor T. Johnson. Robustness verification of seman- tic segmentation neural networks using relaxed reachability. In 33rd International Conference on Co...

    2021

  64. [72]

    Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson. NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In 32nd International Confe...

    2020

  65. [73]

    Attention is all you need

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. Advances in neural information processing systems, 30, 2017

    2017

  66. [74]

    Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624 , 2021

    2021 arXiv

  67. [75]

    Robustness-aware word embedding improves certi- fied robustness to adversarial word substitutions

    Yibin Wang, Yichen Yang, Di He, and Kun He. Robustness-aware word embedding improves certi- fied robustness to adversarial word substitutions. In Findings of the Association for Computational Linguistics: ACL 2023 , pages 673–687, 2023

    2023

  68. [76]

    Convex bounds on the softmax function with applications to robustness verification

    Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark Barrett, and Eitan Farchi. Convex bounds on the softmax function with applications to robustness verification. In International Conference on Artificial Intelligence and Statistics , pages 6853–6878. PMLR, 2023

    2023

  69. [77]

    Towards verified robustness under text deletion interven- tions

    Johannes Welbl, Po-Sen Huang, Robert Stanforth, Sven Gowal, Krishnamurthy Dj Dvijotham, Martin Szummer, and Pushmeet Kohli. Towards verified robustness under text deletion interven- tions. 2020

    2020

  70. [78]

    Scalable verification of gnn-based job schedulers

    Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh. Scalable verification of gnn-based job schedulers. 6(OOPSLA2), oct 2022

    2022

  71. [79]

    Marabou 2.0: a versatile formal analyzer of neural networks

    Haoze Wu, Omri Isac, Aleksandar Zelji´ c, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, et al. Marabou 2.0: a versatile formal analyzer of neural networks. In International Conference on Computer Aided Verification , pages 2...

    2024

  72. [80]

    Parallelization techniques for verifying neural networks

    Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett. Parallelization techniques for verifying neural networks. In # PLACEHOLDER PARENT METADATA V ALUE#, volume 1, pages 128–

  73. [81]

    Toward certified robustness against real- world distribution shifts

    Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George Pappas, Hamed Hassani, Corina Pasareanu, and Clark Barrett. Toward certified robustness against real- world distribution shifts. arXiv preprint arXiv:2206.03669 , 2022

    2022 arXiv

  74. [82]

    Efficient neural network analysis with sum-of-infeasibilities

    Haoze Wu, Aleksandar Zelji´ c, Guy Katz, and Clark Barrett. Efficient neural network analysis with sum-of-infeasibilities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 143–163. Springer, 2022

    2022

  75. [83]

    Automatic perturbation analysis for scalable certified robustness and beyond

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems , 33, 2020

    2020

  76. [84]

    Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations , 2021. 33 VNN...

    2021

  77. [85]

    Lyapunov- stable neural control for state and output feedback: A novel formulation

    Lujie Yang, Hongkai Dai, Zhouxing Shi, Cho-Jui Hsieh, Russ Tedrake, and Huan Zhang. Lyapunov- stable neural control for state and output feedback: A novel formulation. In Forty-first Interna- tional Conference on Machine Learning , 2024

    2024

  78. [86]

    General cutting planes for bound-propagation-based neural network verification

    Huan Zhang*, Shiqi Wang*, Kaidi Xu*, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for bound-propagation-based neural network verification. Advances in Neural Information Processing Systems (NeurIPS) , 2022

    2022

  79. [87]

    Efficient neural network robustness certification with general activation functions.Advances in Neural Information Processing Systems, 31:4939–4948, 2018

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions.Advances in Neural Information Processing Systems, 31:4939–4948, 2018

    2018

  80. [88]

    Lightweight Deep Network for Traffic Sign Classification

    Jianming Zhang, Wei Wang, Chaoquan Lu, Jin Wang, and Arun Kumar Sangaiah. Lightweight Deep Network for Traffic Sign Classification. Annals of Telecommunications, 75:369–379, 2020

    2020

  81. [89]

    Certified robustness to programmable transformations in lstms

    Yuhao Zhang, Aws Albarghouthi, and Loris D’Antoni. Certified robustness to programmable transformations in lstms. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 1068–1083, 2021

    2021

  82. [90]

    Scalable neural network ver- ification with branch-and-bound inferred cutting planes

    Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang. Scalable neural network ver- ification with branch-and-bound inferred cutting planes. In The Thirty-eighth Annual Conference on Neural Information Processing Systems , 2024

    2024

  83. [91]

    Testing neural network verifiers: A soundness benchmark with hidden counterexamples

    Xingjian Zhou, Hongji Xu, Andy Xu, Zhouxing Shi, Cho-Jui Hsieh, and Huan Zhang. Testing neural network verifiers: A soundness benchmark with hidden counterexamples. arXiv preprint arXiv:2412.03154, 2024. 34 VNN-COMP 2024 Report C. Brix, S. Bak, T. Johnson, H. Wu A Detailed Res...

    2024

  84. [137]

    TU Wien Academic Press, 2020

    2020

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.