CoChat
Sign Up
PreprintCited by 43Logic, programming, and type systemsSoftware Engineering ResearchSoftware Testing and Debugging Techniques

Clover: Closed-Loop Verifiable Code Generation

Open access
Sun, Chuyue, Sheng, Ying, Padon, Oded, Barrett, Clark·2023·arXiv
DOI 10.48550/arxiv.2310.17807arXiv 2310.17807
Open this paper in CoChat — free accountOpen PDF

Abstract

The use of large language models for code generation is a rapidly growing trend in software development. However, without effective methods for ensuring the correctness of generated code, this trend could lead to undesirable outcomes. In this paper, we introduce a new approach for addressing this challenge: the Clover paradigm, short for Closed-Loop Verifiable Code Generation, which uses consistency checking to provide a strong filter for incorrect code. Clover performs consistency checks among code, docstrings, and formal annotations. The checker is implemented using a novel integration of formal verification tools and large language models. We provide a theoretical analysis to support our thesis that Clover should be effective at consistency checking. We also empirically investigate its performance on a hand-designed dataset (CloverBench) featuring annotated Dafny programs at a textbook level of difficulty. Experimental results show that for this dataset: (i) LLMs are reasonably successful at automatically generating formal specifications; and (ii) our consistency checker achieves a promising acceptance rate (up to 87%) for correct instances while maintaining zero tolerance for adversarial incorrect ones (no false positives). Clover also discovered 6 incorrect programs in the existing human-written dataset MBPP-DFY-50.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2310.17807

Cites

1 of 1 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs.

    “However, generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs.”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Sun et al., 2023

    Appendix A.4.5 attributes GPT-4’s difficulty with current Dafny syntax to likely limited training data, supporting the data-scarcity point in that specific setting. The Introduction identifies the need for human expertise in writing formal specifications as the main obstacle; it says the proof step can often be automated, so it does not support formal-proof complexity as the obstacle claimed. (LLM, conf=0.86)

    Experimental — accuracy not yet measured

  • An alternative paradigm integrates language models with languages that offload proving to automated reasoning tools (e.g., SMT), including Dafny and F*.

    “An alternative paradigm integrates language models with languages that offload proving to automated reasoning tools (e.g., SMT), including Dafny (Leino, 2010;Sun et al., 2023;Loughridge et al., 2024) and F* (Swamy et al., 2016;Chakraborty et al., 2024).”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Sun et al., 2023

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

  • Do Users Write More Insecure Code with AI Assistants?

    Perry, N., Srivastava, M., Kumar, D., & Boneh, D. (2022) · arXiv · cited 2×

    “Results suggest that developers with access to AI assistants write more insecure code, while at the same time having higher confidence in their code [52].”
    Background

Flagged first, then by citations

Research works printed but not linked: 77

  1. Rajeev Alur et al. "Syntax-guided synthesis". In: Formal Methods in Computer- Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 2013, pp. 1-8. url: https://ieeexplore.ieee.org/document/ 6679385/.
  2. Jacob Austin et al. "Program Synthesis with Large Language Models". In: CoRR abs/2108.07732 (2021). arXiv: 2108.07732. url: https://arxiv. org/abs/2108.07732. · arXiv
  3. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfia- bility. Vol. 185. IOS press, 2009.
  4. Matthew Bowers et al. "Top-Down Synthesis for Library Learning". In: Proc. ACM Program. Lang. 7.POPL (2023), pp. 1182-1213. doi: 10.1145/ 3571234. url: https://doi.org/10.1145/3571234. · DOI · Paper page
  5. David Brandfonbrener et al. "Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search". In: arXiv preprint arXiv:2402.08147 (2024). · arXiv
  6. Sébastien Bubeck et al. "Sparks of artificial general intelligence: Early experiments with gpt-4". In: arXiv preprint arXiv:2303.12712 (2023). · arXiv
  7. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. "KLEE: Unas- sisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs". In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. Ed. by Richard Draves and Robbert van Re- nesse. USENIX Association, 2008, pp. 209-224. url: http://www.usenix. org/events/osdi08/tech/full%5C_papers/cadar/cadar.pdf.
  8. Cristian Cadar and Koushik Sen. "Symbolic execution for software testing: three decades later". In: Commun. ACM 56.2 (2013), pp. 82-90. doi: 10.1145/2408776.2408795. url: https://doi.org/10.1145/2408776. 2408795. · DOI
  9. Yiannis Charalambous et al. "A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verifica- tion". In: CoRR abs/2305.14752 (2023). doi: 10 . 48550 / arXiv . 2305 . 14752. arXiv: 2305.14752. url: https://doi.org/10.48550/arXiv. 2305.14752. · DOI
  10. Swarat Chaudhuri et al. "Neurosymbolic Programming". In: Found. Trends Program. Lang. 7.3 (2021), pp. 158-243. doi: 10.1561/2500000049. url: https://doi.org/10.1561/2500000049. · DOI
  11. Bei Chen et al. "CodeT: Code Generation with Generated Tests". In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. url: https:// openreview.net/pdf?id=ktrw68Cmu9c.
  12. Bei Chen et al. "Codet: Code generation with generated tests". In: arXiv preprint arXiv:2207.10397 (2022). · arXiv
  13. Mark Chen et al. "Evaluating Large Language Models Trained on Code". In: CoRR abs/2107.03374 (2021). arXiv: 2107 . 03374. url: https : / / arxiv.org/abs/2107.03374. · arXiv
  14. Xinyun Chen et al. "Teaching large language models to self-debug". In: arXiv preprint arXiv:2304.05128 (2023). · arXiv
  15. Zhoujun Cheng et al. "Binding Language Models in Symbolic Languages". In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. url: https://openreview.net/pdf?id=lH1PV42cbF.
  16. Aakanksha Chowdhery et al. "PaLM: Scaling Language Modeling with Pathways". In: CoRR abs/2204.02311 (2022). doi: 10 . 48550 / arXiv . 2204 . 02311. arXiv: 2204 . 02311. url: https : / / doi . org / 10 . 48550 / arXiv.2204.02311. · DOI · Paper page
  17. Berkeley R. Churchill et al. "Semantic program alignment for equivalence checking". In: Proceedings of the 40th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019.
  18. Ed. by Kathryn S. McKinley and Kathleen Fisher. ACM, 2019, pp. 1027-1040. doi: 10.1145/3314221.3314596. url: https://doi.org/10.1145/3314221.3314596. · DOI · Paper page
  19. Karl Cobbe et al. "Training Verifiers to Solve Math Word Problems". In: CoRR abs/2110.14168 (2021). arXiv: 2110.14168. url: https://arxiv. org/abs/2110.14168. · arXiv
  20. Domenico Cotroneo et al. "Vulnerabilities in AI Code Generators: Explor- ing Targeted Data Poisoning Attacks". In: CoRR abs/2308.04451 (2023). doi: 10 . 48550 / arXiv . 2308 . 04451. arXiv: 2308 . 04451. url: https : //doi.org/10.48550/arXiv.2308.04451. · DOI
  21. Yangruibo Ding et al. "TRACED: Execution-aware Pre-training for Source Code". In: arXiv preprint arXiv:2306.07487 (2023). · arXiv
  22. Kevin Ellis et al. "DreamCoder: bootstrapping inductive program synthe- sis with wake-sleep library learning". In: PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Imple- mentation, Virtual Event, Canada, June 20-25, 2021.
  23. Ed. by Stephen N. Freund and Eran Yahav. ACM, 2021, pp. 835-850. doi: 10.1145/3453483. 3454080. url: https://doi.org/10.1145/3453483.3454080. · DOI · Paper page
  24. Robert W. Floyd. "Assigning Meanings to Programs". In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathe- matics. American Mathematical Society, 1967, pp. 19-32.
  25. Sayontan Ghosh et al. "SpecNFS: A Challenge Dataset Towards Extract- ing Formal Models from Natural Language Specifications". In: Proceedings of the Thirteenth Language Resources and Evaluation Conference, LREC 2022, Marseille, France, 20-25 June 2022.
  26. Ed. by Nicoletta Calzolari et al. European Language Resources Association, 2022, pp. 2166-2176. url: https://aclanthology.org/2022.lrec-1.233.
  27. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. "Program Syn- thesis". In: Found. Trends Program. Lang. 4.1-2 (2017), pp. 1-119. doi: 10.1561/2500000010. url: https://doi.org/10.1561/2500000010. · DOI
  28. Christopher Hahn et al. "Formal Specifications from Natural Language". In: CoRR abs/2206.01962 (2022). doi: 10 . 48550 / arXiv . 2206 . 01962. arXiv: 2206 . 01962. url: https : // doi . org /10 . 48550 / arXiv. 2206 . 01962. · DOI
  29. James Hendler. "Understanding the limits of AI coding". In: Science 379.6632 (2023), pp. 548-548.
  30. Dan Hendrycks et al. "Measuring Coding Challenge Competence With APPS". In: Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual. Ed. by Joaquin Vanschoren and Sai-Kit Ye- ung. 2021. url: https://datasets-benchmarks-proceedings.neurips. cc/paper/2021/hash/c24cd76e1ce41366a4bbe8a49b02a028-Abstract- round2.html.
  31. C. A. R. Hoare. "An Axiomatic Basis for Computer Programming". In: Commun. ACM 12.10 (1969), pp. 576-580. doi: 10.1145/363235.363259. url: http://doi.acm.org/10.1145/363235.363259. · DOI
  32. Jeevana Priya Inala et al. "Fault-Aware Neural Code Rankers". In: NeurIPS. 2022. url: http://papers.nips.cc/paper%5C_files/paper/2022/ hash/5762c579d09811b7639be2389b3d07be-Abstract-Conference.html.
  33. Darren Key, Wen-Ding Li, and Kevin Ellis. "I Speak, You Verify: To- ward Trustworthy Neural Program Synthesis". In: CoRR abs/2210.00848 (2022). doi: 10 . 48550 / arXiv . 2210 . 00848. arXiv: 2210 . 00848. url: https://doi.org/10.48550/arXiv.2210.00848. · DOI
  34. James C. King. "Symbolic Execution and Program Testing". In: Com- mun. ACM 19.7 (1976), pp. 385-394. doi: 10.1145/360248.360252. url: https://doi.org/10.1145/360248.360252. · DOI
  35. Yuhang Lai et al. "DS-1000: A Natural and Reliable Benchmark for Data Science Code Generation". In: International Conference on Machine Learn- ing, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 18319-18345. url: https://proceedings.mlr.press/v202/ lai23b.html.
  36. Andrea Lattuada et al. Verus: Verifying Rust Programs using Linear Ghost Types (extended version). 2023. arXiv: 2303.05491 [cs.LO]. · arXiv
  37. K Rustan M Leino. "Dafny: An automatic program verifier for functional correctness". In: International conference on logic for programming artifi- cial intelligence and reasoning. Springer. 2010, pp. 348-370.
  38. Yifei Li et al. "On the Advance of Making Language Models Better Rea- soners". In: CoRR abs/2206.02336 (2022). doi: 10.48550/arXiv.2206. 02336. arXiv: 2206.02336. url: https://doi.org/10.48550/arXiv. 2206.02336. · DOI
  39. Yujia Li et al. "Competition-level code generation with alphacode". In: Science 378.6624 (2022), pp. 1092-1097.
  40. Chang Liu et al. "Towards General Loop Invariant Generation via Co- ordinating Symbolic Execution and Large Language Models". In: arXiv preprint arXiv:2311.10483 (2023). · arXiv
  41. Jiawei Liu et al. "Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation". In: CoRR abs/2305.01210 (2023). doi: 10.48550/arXiv.2305.01210. arXiv: 2305.01210. url: https://doi.org/10.48550/arXiv.2305.01210. · DOI · Paper page
  42. Aman Madaan et al. "Self-refine: Iterative refinement with self-feedback". In: Advances in Neural Information Processing Systems 36 (2024).
  43. Zohar Manna and Richard Waldinger. "Knowledge and reasoning in pro- gram synthesis". In: Artificial intelligence 6.2 (1975), pp. 175-208.
  44. Zohar Manna and Richard J Waldinger. "Toward automatic program syn- thesis". In: Communications of the ACM 14.3 (1971), pp. 151-165.
  45. Md Rakib Hossain Misu et al. "Towards AI-Assisted Synthesis of Verified Dafny Methods". In: arXiv preprint arXiv:2402.00247 (2024). · arXiv
  46. Nausheen Mohammed et al. "Enabling Memory Safety of C Programs using LLMs". In: arXiv preprint arXiv:2404.01096 (2024). · arXiv
  47. Rajdeep Mondal et al. "What do LLMs need to Synthesize Correct Router Configurations?" In: Proceedings of the 22nd ACM Workshop on Hot Top- ics in Networks. 2023, pp. 189-195.
  48. Theo X Olausson et al. "Is Self-Repair a Silver Bullet for Code Genera- tion?" In: The Twelfth International Conference on Learning Representa- tions. 2023.
  49. OpenAI. "GPT-4 Technical Report". In: CoRR abs/2303.08774 (2023). doi: 10 . 48550 / arXiv . 2303 . 08774. arXiv: 2303 . 08774. url: https : //doi.org/10.48550/arXiv.2303.08774. · DOI · Paper page
  50. Liangming Pan et al. "Automatically correcting large language models: Surveying the landscape of diverse self-correction strategies". In: arXiv preprint arXiv:2308.03188 (2023). · arXiv
  51. Hammond Pearce et al. "Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions". In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 2022, pp. 754-768. doi: 10.1109/SP46214.2022.9833571. url: https://doi.org/10.1109/SP46214.2022.9833571. · DOI · Paper page
  52. Kexin Pei et al. "Can Large Language Models Reason about Program Invariants?" In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 27496-27520. url: https://proceedings.mlr.press/v202/pei23a. html.
  53. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. "Program synthesis from polymorphic refinement types". In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Im- plementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016.
  54. Ed. by Chandra Krintz and Emery D. Berger. ACM, 2016, pp. 522-538. doi: 10 . 1145 / 2908080 . 2908093. url: https : / / doi . org / 10 . 1145 / 2908080.2908093. · DOI
  55. Gabriel Ryan et al. "Code-Aware Prompting: A study of Coverage Guided Test Generation in Regression Setting using LLM". In: arXiv preprint arXiv:2402.00097 (2024). · arXiv
  56. Gustavo Sandoval et al. "Lost at C: A User Study on the Security Im- plications of Large Language Model Code Assistants". In: 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023.
  57. Ed. by Joseph A. Calandrino and Carmela Troncoso. USENIX Association, 2023. url: https://www.usenix.org/conference/usenixsecurity23/ presentation/sandoval.
  58. William Saunders et al. "Self-critiquing models for assisting human evalu- ators". In: arXiv preprint arXiv:2206.05802 (2022). · arXiv
  59. Freda Shi et al. "Natural Language to Code Translation with Execution". In: Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022.
  60. Ed. by Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang. Association for Computational Linguistics, 2022, pp. 3533-3546. doi: 10.18653/v1/2022.emnlp-main.231. url: https://doi.org/10. 18653/v1/2022.emnlp-main.231. · DOI
  61. Kensen Shi et al. "CrossBeam: Learning to Search in Bottom-Up Program Synthesis". In: The Tenth International Conference on Learning Represen- tations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. url: https://openreview.net/forum?id=qhC8mr2LEKq.
  62. Chuyue Sun, Christopher Hahn, and Caroline Trippel. "Towards Improv- ing Verification Productivity with Circuit-Aware Translation of Natural Language to SystemVerilog Assertions". In: First International Workshop on Deep Learning-aided Verification. 2023.
  63. Abhishek Udupa et al. "TRANSIT: specifying protocols with concolic snip- pets". In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013.
  64. Ed. by Hans-Juergen Boehm and Cormac Flanagan. ACM, 2013, pp. 287-296. doi: 10 . 1145 / 2491956 . 2462174. url: https : / / doi . org / 10 . 1145 / 2491956.2462174. · DOI
  65. Priyan Vaithilingam, Tianyi Zhang, and Elena L. Glassman. "Expecta- tion vs. Experience: Evaluating the Usability of Code Generation Tools Powered by Large Language Models". In: CHI '22: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022 -5 May 2022, Extended Abstracts. Ed. by Simone D. J. Barbosa et al. ACM, 2022, 332:1-332:7. doi: 10 . 1145 / 3491101 . 3519665. url: https://doi.org/10.1145/3491101.3519665. · DOI · Paper page
  66. Richard J Waldinger and Richard CT Lee. "PROW: A step toward au- tomatic program writing". In: Proceedings of the 1st international joint conference on Artificial intelligence. 1969, pp. 241-252.
  67. Xuezhi Wang et al. "Self-consistency improves chain of thought reasoning in language models". In: arXiv preprint arXiv:2203.11171 (2022). · arXiv
  68. Jason Wei et al. "Chain-of-Thought Prompting Elicits Reasoning in Large Language Models". In: NeurIPS. 2022. url: http://papers.nips.cc/ paper%5C_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4- Abstract-Conference.html.
  69. Cheng Wen et al. "Enchanting program specification synthesis by large language models using static analysis and program verification". In: arXiv preprint arXiv:2404.00762 (2024). · arXiv
  70. Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating Large Language Models in Automated Program Verification. 2023. arXiv: 2310. 04870 [cs.FL].
  71. Frank F. Xu, Bogdan Vasilescu, and Graham Neubig. "In-IDE Code Gener- ation from Natural Language: Promise and Challenges". In: ACM Trans. Softw. Eng. Methodol. 31.2 (2022), 29:1-29:47. doi: 10 . 1145 / 3487569. url: https://doi.org/10.1145/3487569. · DOI · Paper page
  72. Pengcheng Yin and Graham Neubig. "A Syntactic Neural Model for General- Purpose Code Generation". In: Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, Vancouver, Canada, July 30 -August 4, Volume 1: Long Papers. Ed. by Regina Barzi- lay and Min-Yen Kan. Association for Computational Linguistics, 2017, pp. 440-450. doi: 10.18653/v1/P17-1041. url: https://doi.org/10. 18653/v1/P17-1041. · DOI · Paper page
  73. Pengcheng Yin et al. "Natural Language to Code Generation in Interactive Data Science Notebooks". In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023.
  74. Ed. by Anna Rogers, Jor- dan L. Boyd-Graber, and Naoaki Okazaki. Association for Computational Linguistics, 2023, pp. 126-173. doi: 10 . 18653 / v1 / 2023 . acl -long . 9. url: https://doi.org/10.18653/v1/2023.acl-long.9. · DOI
  75. Eric Zelikman et al. "Parsel: A (de-) compositional framework for algorith- mic reasoning with language models". In: arXiv preprint arXiv:2212.10561 (2023). · arXiv
  76. Tianyi Zhang et al. "Coder Reviewer Reranking for Code Generation". In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Pro- ceedings of Machine Learning Research. PMLR, 2023, pp. 41832-41846. url: https://proceedings.mlr.press/v202/zhang23av.html.
  77. Baishun Zhou and Gangyi Ding. "Survey of intelligent program synthe- sis techniques". In: International Conference on Algorithms, High Per- formance Computing, and Artificial Intelligence (AHPCAI 2023). Ed. by Sandeep Saxena and Cairong Zhao. Vol. 12941. International Society for Optics and Photonics. SPIE, 2023, 129414G. doi: 10.1117/12.3011627. url: https://doi.org/10.1117/12.3011627. · DOI

Cited by

Sorted by citations

Authors
Sun, C., Sheng, Y., Padon, O., & Barrett, C.
Affiliations
  • Stanford University (US)
  • VMware (United States) (US)
Corresponding author
Sun, Chuyue
ORCID
Venue
arXiv
Publisher
arXiv
Published
2023
Pages
134-155
ISSN
0302-9743 (ISSN-L)
DOI
10.48550/arxiv.2310.17807
arXiv
2310.17807
OpenAlex
W4400675892
Cited by
43
References
1
Citations by year
2026: 16 · 2025: 22 · 2024: 5
FWCI
12.71
Type
conference paper
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • Lecture notes in computer science (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Information Systems › Software Engineering Research
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords
large language models, code generation, consistency checking, formal verification, Dafny, formal specification, docstrings, program correctness

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review