Pith. sign in

REVIEW 64 references

Proof-Carrying Neuro-Symbolic Code

T0 review · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read The paper defines proof-carrying neuro-symbolic code, a research program for delivering neural-network-containing software with formal safety proofs, and reviews early tools and challenges.

arxiv 2504.12031 v1 pith:GY5PMSYZ submitted 2025-04-16 cs.PL cs.AIcs.LO

Ekaterina Komendantskaya This is my paper · ORCID
classification cs.PLcs.AIcs.LO
keywords codeneuro-symbolicproof-carryingareachallengesconceptexplainsfaces
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

Proof-carrying code is an old idea from programming languages: ship a program together with a proof that it behaves correctly. This paper asks what that idea means when part of the program is a neural network. It calls the answer 'proof-carrying neuro-symbolic code'. The paper walks through a simple self-driving scenario. A car has a neural controller that decides how much to brake. To prove the car will not crash, three kinds of facts are needed: the neural network itself satisfies a property like 'it brakes strongly enough', that property still holds after the network's inputs and outputs are translated into real-world values, and the whole control loop is safe. The paper presents this as three lemmas that together give a safety proof.

The rest of the paper lists three challenges. First, existing proof assistants like Agda are good at high-level proofs but bad at verifying neural networks; specialized solvers like Marabou are the opposite. A compiler called Vehicle tries to connect the two. Second, if you trust a neural network solver, you need evidence you can check independently; the paper describes a proof checker for Marabou that was itself verified in the interactive prover Imandra. Third, specifications written in logic must be turned into loss functions for training, which requires a theory of differentiable logics. The paper reports early progress and open issues.

This is not a paper with a new theorem or experiment. It is an invited talk written as a position piece. Its value is in naming a research area and showing that existing tools already cover parts of it.

Extended reading notes

Core claim

In Section 2 the paper states: 'writing proof-carrying neuro-symbolic code amounts to writing a program s(u◦f◦e) and completing a proof as in equations (1) - (3).' If correct, neuro-symbolic programs can be delivered with end-to-end safety proofs by discharging three lemmas: a network property Ξ, a solution property Φ, and a program property Ψ.

Load-bearing premise

The framework assumes that for any neuro-symbolic program s(u◦f◦e) and any desired property Ψ, there exist a network property Ξ and a solution property Φ such that the three lemmas (1)-(3) hold, in particular the lifting lemma ∀g. Ξ(g) ⇒ Φ(u◦g◦e). Section 2 introduces this decomposition as the definition of proof-carrying neuro-symbolic code, but the paper does not prove the lemmas for the car example or identify conditions on e, u, and s under which the decomposition is complete. If the decomposition is not generally achievable, the framework only applies to specially structured programs.

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.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The paper introduces no free parameters and makes no quantitative predictions. Its argument rests on background mathematics (e.g., Farkas lemma, properties of fuzzy logics) and on published verified tools (Vehicle, Imandra-based Marabou proof checker, Coq formalization of differentiable logics). The main structural assumption is the three-lemma decomposition itself, which is proposed as the definition of the new concept. The term 'proof-carrying neuro-symbolic code' is listed as an invented conceptual entity; it has no falsifiable handles beyond the eventual success of the research program.

assumptions (3)
  • domain assumption For any neuro-symbolic program s(u◦f◦e) and property Ψ, there exist Ξ and Φ such that lemmas (1)-(3) hold.
    This is the defining framework of the paper (Section 2), but it is not proven to be generally applicable; it is the structure that the research agenda assumes can always be constructed.
  • domain assumption Neural network solvers such as Marabou are sound and can produce proof certificates; the Imandra-based checker is correct.
    Section 4.2 relies on published results [25,36] that the proof checker is certified; the paper does not re-verify them. Since these references have artifacts, the support is external but assumed.
  • domain assumption Robustness and similar universal properties cannot be learned from data alone and require formal specification.
    Section 3 uses this premise to argue for proof-carrying code; it is an argument based on the need for universal quantification over inputs not in the data set.
invented entities (1)
  • proof-carrying neuro-symbolic code (term/framework)
    purpose: To name and unify the research program of verifying neuro-symbolic programs with end-to-end formal proofs.
    The term is a conceptual label introduced in this paper; it does not come with falsifiable predictions or mechanisms beyond the eventual success of the research program.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Proof-Carrying Neuro-Symbolic Code." pith.science (2026). https://pith.science/paper/GY5PMSYZ

@misc{pith2026250412031,
  author       = {Pith},
  title        = {Pith review of: Proof-Carrying Neuro-Symbolic Code},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GY5PMSYZ}},
  note         = {Machine review of arXiv:2504.12031}
}
read the original abstract

This invited paper introduces the concept of "proof-carrying neuro-symbolic code" and explains its meaning and value, from both the "neural" and the "symbolic" perspectives. The talk outlines the first successes and challenges that this new area of research faces.

Figures

Figures reproduced from arXiv: 2504.12031 by the authors.

Figure 1
Figure 1. Example of a cyber-physical system with a neural controller (given by the left￾most car) written in the syntax of the Differentiable Dynamic Logic [29,53,58]. 2 What is Proof-Carrying Neuro-Symbolic Code? Consider a purely symbolic program s(·), whose completion requires computing a complex, unknown function H : P → R that maps objects in the problem input space P to those in the problem output space R. Given an emb… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

64 extracted references · 41 canonical work pages

  1. [1]

    In: Gurfinkel, A., Ganesh, V

    Abate,A.,Giacobbe,M.,Roy,D.:Stochasticomega-regularverificationandcontrol with supermartingales. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Ver- ification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14683, pp. 395–419. Springer (2024). https://do...

    work page doi:10.1007/978-3-031-65633-0_ 2024

  2. [2]

    Available athttps://github

    Affeldt, R., Bruni, A., Bertot, Y., Cohen, C., Kerjean, M., Mahboubi, A., Rouh- ling, D., Roux, P., Sakaguchi, K., Stone, Z., Strub, P.Y., Théry, L.: Analysis li- brary compatible with mathematical components. Available athttps://github. com/math-comp/analysis (2017), latest version: 1.8.0 (2024-12-19)

    work page 2017

  3. [3]

    In: Bertot, Y., Kutsia, T., Norrish, M

    Affeldt, R., Bruni, A., Komendantskaya, E., Ślusarz, N., Stark, K.: Taming Dif- ferentiable Logics with Coq Formalisation. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 309, pp. 4:1–4:19. Schloss Dagstuhl – Leibniz-Zent...

    doi:10.4230/lipics.itp.2024.4 2024

  4. [4]

    In: 30th International Conference on Types for Proofs and Programs TYPES 2024–Abstracts

    Affeldt, R., Bruni, A., Roux, P., Saikawa, T.: Yet another formal theory of probabil- ities (with an application to random sampling). In: 30th International Conference on Types for Proofs and Programs TYPES 2024–Abstracts. p. 11 (2024)

    work page 2024

  5. [5]

    Affeldt, R., Cohen, C.: Measure construction by extension in dependent type theory with application to integration. J. Autom. Reason. 67(3), 28 (2023). https://doi.org/10.1007/S10817-023-09671-5, https://doi.org/10. 1007/s10817-023-09671-5

    doi:10.1007/s10817-023-09671-5 2023

  6. [6]

    In: Bertot, Y., Kutsia, T., Norrish, M

    Affeldt, R., Stone, Z.: A comprehensive overview of the lebesgue differentiation theorem in coq. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th Interna- tional Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia. LIPIcs, vol. 309, pp. 5:1–5:19. Schloss Dagstuhl - Leibniz- Zentrum für Informatik (2024). https://...

    work page doi:10.4230/lipics.itp.2024.5 2024

  7. [7]

    ARIA grant (2024)

    Atkey, R., Capucci, M., Komendantskaya, E., Mardare, R.: Quantitative predicate logic as a foundation for verified ml. ARIA grant (2024)

    work page 2024

  8. [8]

    Annals of Pure and Ap- plied Logic 147(1), 23–47 (2007)

    Baaz, M., Preining, N., Zach, R.: First-order gödel logics. Annals of Pure and Ap- plied Logic 147(1), 23–47 (2007). https://doi.org/https://doi.org/10.1016/ j.apal.2007.03.001, https://www.sciencedirect.com/science/article/pii/ S016800720700019X

    work page 2007

Show all 64 references
  1. [9]

    Electronic Notes in Theoretical Informatics and Computer Sci- ence 3 (2023)

    Bacci, G., Mardare, R., Panangaden, P., Plotkin, G.: Propositional logics for the lawvere quantale. Electronic Notes in Theoretical Informatics and Computer Sci- ence 3 (2023)

    2023

  2. [10]

    In: Proc

    Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Bar- rett, C.: Flexible Proof Production in an Industrial-Strength SMT Solver. In: Proc. 11th Int. Joint Conference on A...

    2022

  3. [11]

    All about Proofs, Proofs for All55(1), 23–44 (2015)

    Barrett, C., de Moura, L., Fontaine, P.: Proofs in Satisfiability Modulo Theories. All about Proofs, Proofs for All55(1), 23–44 (2015)

    2015

  4. [12]

    Bourgain, J.: New classes of Lp-spaces, vol. 889. Springer (2006)

    2006

  5. [13]

    arXiv preprint arXiv:2406.04936 (2024)

    Capucci, M.: On quantifiers for quantitative reasoning. arXiv preprint arXiv:2406.04936 (2024)

    2024

  6. [14]

    Carlini, N.: A complete list of all (arxiv) adversarial example papers (2019)

    2019

  7. [15]

    In: Computer Aided Verification (CAV 2022)

    Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: A principled case study. In: Computer Aided Verification (CAV 2022). Lecture Notes in Computer Science, Springer (2022)

    2022

  8. [16]

    In: International conference on computer aided verification

    Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: a principled case study. In: International conference on computer aided verification. pp. 219–231. Springer (2022) 10 E. Komendantskaya

    2022

  9. [17]

    Foundations and Trends® in Programming Languages 7(3), 158–243 (2021)

    Chaudhuri, S., Ellis, K., Polozov, O., Singh, R., Solar-Lezama, A., Yue, Y.: Neu- rosymbolic programming. Foundations and Trends® in Programming Languages 7(3), 158–243 (2021). https://doi.org/10.1561/2500000049, http://dx.doi. org/10.1561/2500000049

    2021 doi

  10. [18]

    In: European Symposium on Programming Languages, ESOP 2025 (2025)

    Cordeiro, L., Daggitt, M., Girard, J., Isac, O., Johnson, T., Katz, G., Komen- dantskaya, E., Manino, E., Sinkarovs, A., Wu, H.: Neural network verification is a programming language challenge. In: European Symposium on Programming Languages, ESOP 2025 (2025)

    2025

  11. [19]

    In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

    Daggitt, M.L., Atkey, R., Kokke, W., Komendantskaya, E., Arnaboldi, L.: Com- piling higher-order specifications to smt solvers: How to deal with rejection con- structively. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 1...

    2023

  12. [20]

    Daggitt, M.L., Kokke, W., Atkey, R.: Efficient compilation of expressive problem space specifications to neural network solvers (2024), https://arxiv.org/abs/ 2402.01353

    2024

  13. [21]

    CoRRabs/2401.06379(2024)

    Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: Bridging the embedding gap in the verification of neuro-symbolic pro- grams. CoRRabs/2401.06379(2024). https://doi.org/10.48550/ARXIV.2401. 06379, https://doi.org/10.48550/arXiv.2401.06379

    2024 doi arXiv

  14. [22]

    arXiv preprint arXiv:2401.06379 (2024)

    Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: Bridging the embedding gap in the verification of neuro-symbolic pro- grams. arXiv preprint arXiv:2401.06379 (2024)

    2024 arXiv

  15. [23]

    In: Narodytska, N., Amir, G., Katz, G., Isac, O

    Daggitt, M.L., Kokke, W., Komendantskaya, E., Atkey, R., Arnaboldi, L., Slusarz, N., Casadio, M., Coke, B., Lee, J.: The vehicle tutorial: Neural network verifica- tion with vehicle. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceed- ings of the 6th Workshop on F...

    2023 doi

  16. [24]

    Dalrymple, D.: Safeguarded ai: constructing guaranteed safety (2024), programme Thesis

    2024

  17. [25]

    In: Submitted to ITP’25

    Desmartin, R., Isac, O., Komendantskaya, E., Stark, K., Passmore, G.O., Katz, G.: A certified proof checker for deep neural network verification in imandra. In: Submitted to ITP’25. https://doi.org/10.48550/arXiv.2405.10611 (2025)

    2025 doi arXiv

  18. [26]

    In: International Conference on Machine Learning

    Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.: Dl2: training and querying neural networks with logic. In: International Conference on Machine Learning. pp. 1931–1941. PMLR (2019)

    2019

  19. [27]

    In: Chaudhuri, K., Salakhutdinov, R

    Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.T.: DL2: training and querying neural networks with logic. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Ma- chine Learning, ICML 2019, 9-15 June 2...

    2019

  20. [28]

    Flinkow, T., Pearlmutter, B.A., Monahan, R.: Comparing differentiable logics for learning with logical constraints (2024),https://arxiv.org/abs/2407.03847

    2024 arXiv

  21. [29]

    In: CADE

    Fulton, N., et al.: KeYmaeraX: An axiomatic tactical theorem prover for hybrid systems. In: CADE. pp. 527–538 (2015). https://doi.org/10.1007/ 978-3-319-21401-6_36

    2015

  22. [30]

    Elsevier (2007) Proof-Carrying Neuro-Symbolic Code 11

    Galatos, N., Jipsen, P., Ono, T.K.H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier (2007) Proof-Carrying Neuro-Symbolic Code 11

    2007

  23. [31]

    In: Proc

    Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In: Proc. 39th IEEE Symposium on Security and Privacy (SP). pp. 3–18 (2018)

    2018

  24. [32]

    arXiv preprint arXiv:2206.03044 (2022)

    Girard-Satabin, J., Alberti, M., Bobot, F., Chihani, Z., Lemesle, A.: Caisar: A plat- form for characterizing artificial intelligence safety and robustness. arXiv preprint arXiv:2206.03044 (2022)

    2022 arXiv

  25. [33]

    In: Thirty-First International Joint Conference on Artificial Intelli- gence (IJCAI-22)

    Giunchiglia, E., Stoian, M.C., Lukasiewicz, T.: Deep learning with logical con- straints. In: Thirty-First International Joint Conference on Artificial Intelli- gence (IJCAI-22). pp. 5478–5485. International Joint Conferences on Artificial Intelligence Organization (7 2022).ht...

    2022 doi

  26. [34]

    In: McMillan, K.L., Middeldorp, A., Voronkov, A

    Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recogni- tion and lemma discovery in ACL2. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, S...

    2013

  27. [35]

    Ho, S., Fromherz, A., Protzenko, J.: Modularity, code specialization, and zero-cost abstractions for program verification. Proc. ACM Program. Lang.7(ICFP) (Aug 2023). https://doi.org/10.1145/3607844, https://doi.org/10.1145/3607844

    2023 doi

  28. [36]

    In: Proc

    Isac, O., Barrett, C., Zhang, M., Katz, G.: Neural Network Verification with Proof Production. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). pp. 38–48 (2022)

    2022

  29. [37]

    In: Proc

    Jia, K., Rinard, M.: Exploiting Verified Neural Networks via Floating Point Nu- merical Error. In: Proc. 28th Int. Static Analysis Symposium (SAS). pp. 191–205 (2021)

    2021

  30. [38]

    443–452 (07 2019)

    Katz, G., Huang, D., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D., Kochenderfer, M., Barrett, C.: The Marabou Framework for Verification and Analysis of Deep Neural Networks, pp. 443–452 (07 2019)

    2019

  31. [39]

    Courier Corporation (2014)

    Kazarinoff, N.D.: Analytic inequalities. Courier Corporation (2014)

    2014

  32. [40]

    Kokke, W., Komendantskaya, E., Kienitz, D., Atkey, R., Aspinall, D.: Neu- ral networks, secure by construction - an exploration of refinement types. In: d. S. Oliveira, B.C. (ed.) Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30...

    2020 doi

  33. [41]

    NeurIPS 2018 tutorial (2018), available athttps://adversarial-ml-tutorial.org/

    Kolter, Z., Madry, A.: Adversarial robustness—theory and practice. NeurIPS 2018 tutorial (2018), available athttps://adversarial-ml-tutorial.org/

    2018

  34. [42]

    In: Kaliszyk, C., Lüth, C

    Komendantskaya, E., Heras, J., Grov, G.: Machine learning in proof general: Interfacing interfaces. In: Kaliszyk, C., Lüth, C. (eds.) Proceedings 10th Inter- national Workshop On User Interfaces for Theorem Provers, UITP 2012, Bre- men, Germany, July 11th, 2012. EPTCS, vol. 11...

    2012 doi

  35. [43]

    Lemesle, A., Lehmann, J., Gall, T.L.: Neural network verification with pyrat (2024), https://arxiv.org/abs/2410.23903

    2024 arXiv

  36. [44]

    Communications of the ACM 52(7), 107–115 (2009) 12 E

    Leroy, X.: Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 107–115 (2009) 12 E. Komendantskaya

    2009

  37. [45]

    Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F.L., Ravaioli, U.J., Meng, B., Durling, M., Ganai, M., Shim, T., Katz, G., Barrett, C.: Formally verifying deep reinforcement learning controllers with lyapunov barrier certificates (2024), https://arxiv.org/abs/2405.14058

    2024 arXiv

  38. [46]

    Manginas, V., Manginas, N., Stevinson, E., Varghese, S., Katzouris, N., Paliouras, G., Lomuscio, A.: A scalable approach to probabilistic neuro-symbolic verification (2025), https://arxiv.org/abs/2502.03274

    2025 arXiv

  39. [47]

    Marulanda-Giraldo, J.M., Komendantskaya, E., Bruni, A., Affeldt, R., Capucci, M.: Quantifiers for quantitative logics in rocq: a new project description (2025), a draft

    2025

  40. [48]

    Metcalfe, G., Olivetti, N., Gabbay, D.M.: Proof theory for fuzzy logics, vol. 36. Springer Science & Business Media (2008)

    2008

  41. [49]

    Communications of the ACM54(9), 69–77 (2011)

    de Moura, L., Bjørner, N.: Satisfiability Modulo Theories: Introduction and Appli- cations. Communications of the ACM54(9), 69–77 (2011)

    2011

  42. [50]

    In: Proc

    Necula, G.: Proof-carrying code. In: Proc. 24th Symposium on Principles of Pro- gramming Languages (POPL). pp. 106–119 (1997)

    1997

  43. [51]

    CoRR abs/2412.17432 (2024)

    Neustroev, G., Giacobbe, M., Lukina, A.: Neural continuous-time supermartingale certificates. CoRR abs/2412.17432 (2024). https://doi.org/10.48550/ARXIV. 2412.17432, https://doi.org/10.48550/arXiv.2412.17432

    2024 doi arXiv

  44. [52]

    In: Proc

    Passmore, G., Cruanes, S., Ignatovich, D., Aitken, D., Bray, M., Kagan, E., Kani- shev, K., Maclean, E., Mometto, N.: The Imandra Automated Reasoning System (System Description). In: Proc. 10th Int. Joint Conf. Automated Reasoning (IJ- CAR). pp. 464–471 (2020)

    2020

  45. [53]

    Springer, Cham (2018)

    Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63588-0

    2018 doi

  46. [55]

    In: Piskac, R., Voronkov, A

    Slusarz, N., Komendantskaya, E., Daggitt, M.L., Stewart, R.J., Stark, K.: Logic of differentiable logics: Towards a uniform semantics of DL. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelli...

    2023 doi

  47. [56]

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks (2014)

    2014

  48. [57]

    Team, M.C.: Mathematical components library.https://github.com/math-comp/ math-comp (2007)

    2007

  49. [58]

    In: NeurIPS 2024 (2024), http://papers.nips.cc/paper_files/paper/2024/hash/ 031b5fd7d847f69ed33378a9a1117b4b-Abstract-Conference.html

    Teuber, S., Mitsch, S., Platzer, A.: Provably safe neural net- work controllers via differential dynamic logic. In: NeurIPS 2024 (2024), http://papers.nips.cc/paper_files/paper/2024/hash/ 031b5fd7d847f69ed33378a9a1117b4b-Abstract-Conference.html

    2024

  50. [59]

    Journal of the Operational Research Society (1996)

    Vanderbei, R.: Linear Programming: Foundations and Extensions. Journal of the Operational Research Society (1996)

    1996

  51. [60]

    Advances in Neural Information Processing Sys- tems 34, 29909–29921 (2021) Proof-Carrying Neuro-Symbolic Code 13

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Sys- tems 34, 29909–29921 (2021) Proof-Ca...

    2021

  52. [61]

    In: Proc

    Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komen- dantskaya, E., Katz, G., Barrett, C.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Proc. 36th ...

    2024

  53. [62]

    In: Computer Aided Verification (CAV) (2024)

    Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Computer ...

    2024

  54. [63]

    CoRR abs/2412.16075 (2024)

    Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., Song, D.: For- mal mathematical reasoning: A new frontier in AI. CoRR abs/2412.16075 (2024). https://doi.org/10.48550/ARXIV.2412.16075, https://doi.org/10. 48550/arXiv.2412.16075

    2024 doi arXiv

  55. [64]

    In: International Conference on Learning Representations (2021), https://api.semanticscholar.org/CorpusID:235613486

    Zombori,D.,Bánhelyi,B.,Csendes,T.,Megyeri,I.,Jelasity,M.:Foolingacomplete neural network verifier. In: International Conference on Learning Representations (2021), https://api.semanticscholar.org/CorpusID:235613486

    2021

  56. [406]

    Springer (2013).https://doi.org/10.1007/978-3-642-45221-5_27 , https: //doi.org/10.1007/978-3-642-45221-5_27

    2013 doi

Pith tools

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