---
title: "DafnyBench: A Benchmark for Formal Software Verification (2024)"
description: "The benchmark offers a much larger and harder baseline for measuring how well AI can verify software. 41 references, cited by 9 papers here."
authors: ["Chloe Loughridge", "Qinyi Sun", "Seth Ahrenbach", "Federico Cassano", "Chuyue Sun", "Ying Sheng", "Anish Mudide", "Md Rakib Hossain Misu", "Nada Amin", "Max Tegmark"]
year: 2024
venue: "arXiv:2406.08467"
source: "https://arxiv.org/abs/2406.08467"
doi: "10.48550/arxiv.2406.08467"
arxiv: "2406.08467"
licence: "CC BY 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/loughridge-2024-dafnybench-benchmark-formal-software-verification/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/loughridge-2024-dafnybench-benchmark-formal-software-verification/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/12/) / DafnyBench: A Benchmark for Formal Software Verification

# DafnyBench: A Benchmark for Formal Software Verification

**Authors:** Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, [Federico Cassano](https://md.research.elamur.ai/free/en/authors/federico-cassano/), [Chuyue Sun](https://md.research.elamur.ai/free/en/authors/chuyue-sun/), [Ying Sheng](https://md.research.elamur.ai/free/en/authors/ying-sheng/), Anish Mudide, [Md Rakib Hossain Misu](https://md.research.elamur.ai/free/en/authors/md-rakib-hossain-misu/), Nada Amin and [Max Tegmark](https://md.research.elamur.ai/free/en/authors/max-tegmark/) · **Year:** 2024 · **Venue:** arXiv:2406.08467 · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2406.08467) · [PDF](https://arxiv.org/pdf/2406.08467v1) · [DOI 10.48550/arxiv.2406.08467](https://doi.org/10.48550/arxiv.2406.08467) · [arXiv 2406.08467](https://arxiv.org/abs/2406.08467) · [OpenAlex](https://openalex.org/W4399657810)

**Citations:** 6 citations (OpenAlex, 2026-10-14) · [9](https://md.research.elamur.ai/free/en/papers/loughridge-2024-dafnybench-benchmark-formal-software-verification/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Formal verification can mathematically guarantee that code meets its specification, but it demands a lot of expert effort. The authors argue that AI could automate this work, as it has for theorem proving. Progress, however, is held back by a lack of training and evaluation data: before this work, the largest benchmarks, Clover and dafny-synthesis, held only a few hundred programs combined. DafnyBench addresses this gap with 782 standalone Dafny programs (about 53,000 lines) drawn from deduplicated GitHub code, Clover and dafny-synthesis.

The main task, fill_hints, removes every assert and invariant annotation and asks an LLM to restore enough hints for the Dafny verifier to succeed. The model may not alter preconditions or postconditions or disable verification. Claude 3 Opus achieved the best result at roughly 68%. Feedback from error messages brought only modest gains, and success fell as programs got longer. The benchmark offers a much larger and harder baseline for measuring how well AI can verify software.

## Key points
- **Dataset composition:** 556 programs come from GitHub, 62 from Clover and 164 from dafny-synthesis.
  - The GitHub portion started from about 15,000 files, which shrank to about 5,000 after minhash deduplication.
  - Only files that verified under Dafny 4.3.0 and contained ensures, assert or invariant clauses were kept.
- **Program complexity:** On average, each program has 2.12 methods, 1.03 functions and 1.40 lemmas, so it is more complex than Clover's single-method examples.
- **Success rates with up to 10 attempts (temperature 0.3):**

  | Model | Success |
  |---|---|
  | Claude 3 Opus | 67.8% |
  | GPT-4 Turbo | 59.8% |
  | GPT-4o | 59.3% |
  | GPT-3.5 Turbo | 44.0% |
  | CodeLlama-7b-Instruct-hf | 28.0% |
  | No-LLM baseline (Dafny verifies without hints) | 26.9% |

- **Effect of retries:** The best models solved about 54% of programs on the first attempt. Retries with error feedback levelled off near 65% after roughly five attempts, which suggests models make limited use of Dafny's error messages.
- **Validity rules:** An attempt fails if it modifies requires/ensures statements or uses {:verify false} or assume false. To avoid data contamination, models should not be trained on the GitHub repositories listed in the paper.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 567 works · 335,189 citations
- [Massachusetts Institute of Technology](https://md.research.elamur.ai/free/en/universities/massachusetts-institute-of-technology/) — University, Cambridge, United States · 274 works · 82,013 citations
- [Harvard University](https://md.research.elamur.ai/free/en/universities/harvard-university/) — University, Cambridge, United States · 137 works · 45,850 citations
- [Northeastern University](https://md.research.elamur.ai/free/en/universities/northeastern-university/) — University, Boston, United States · 70 works · 7,342 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works · [💻 Software](https://md.research.elamur.ai/free/en/shelves/computer-science/software/) · 150 works

🧭 Topics (2): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works · [📏 Evaluation & benchmarks](https://md.research.elamur.ai/free/en/topics/evaluation-benchmarks/) · 1,394 works

## Cite

Cite as: Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin and Max Tegmark. 2024. DafnyBench: A Benchmark for Formal Software Verification. arXiv:2406.08467.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{loughridge2024dafnybench,
  title = {{DafnyBench: A Benchmark for Formal Software Verification}},
  author = {Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin and Max Tegmark},
  year = {2024},
  doi = {10.48550/arxiv.2406.08467},
  eprint = {2406.08467},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2406.08467}
}
```

- [← previous Beyond Correlation: Interpretable Evaluation of Machine Translation Metrics](https://md.research.elamur.ai/free/en/papers/perrella-2024-beyond-correlation-interpretable-evaluation-machine/)
- [next → DARES: Dataset for Arabic Readability Estimation of School Materials](https://md.research.elamur.ai/free/en/papers/haj-2024-dares-dataset-arabic-readability-estimation/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/12/)

## References

41 references, 17 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. [Sparks of artificial general intelligence: Early experiments with gpt-4](https://md.research.elamur.ai/free/en/papers/bubeck-2023-sparks-artificial-general-intelligence-early/). arXiv preprint arXiv:2303.12712, 2023.
2. Anthropic. The claude 3 model family: Opus, sonnet, haiku. Technical report, Anthropic, 2024. [find](https://scholar.google.com/scholar?q=Anthropic%2E+The+claude+3+model+family%3A+Opus%2C+sonnet%2C+haiku%2E+Technical+report%2C+Anthropic%2C+2024%2E)
3. Gemini Team, Rohan Anil, Sebastian Borgeaud, Yonghui Wu, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M Dai, Anja Hauth, et al. [Gemini: a family of highly capable multimodal models](https://md.research.elamur.ai/free/en/papers/gemini-team-2023-gemini-family-highly-capable-multimodal/). arXiv preprint arXiv:2312.11805, 2023.
4. European Space Agency. Flight 501 failure, 1996. URL [https://esamultimedia.esa.int/docs/esa-x-1819eng.pdf](https://esamultimedia.esa.int/docs/esa-x-1819eng.pdf). Accessed: 2024-06-04. [↗](https://esamultimedia.esa.int/docs/esa-x-1819eng.pdf)
5. Heartbleed. The heartbleed bug. [https://heartbleed.com/](https://heartbleed.com/), 2024. Accessed: 2024-06-04. [↗](https://heartbleed.com/)
6. Wikipedia contributors. Shellshock (software bug). [https://en.wikipedia.org/wiki/](https://en.wikipedia.org/wiki/) Shellshock_(software_bug), 2024. Accessed: 2024-06-04. [↗](https://en.wikipedia.org/wiki/)
7. Stanislas Polu and Ilya Sutskever. [Generative Language Modeling for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv, September 2020. doi: 10.48550/arXiv.2009.03393.
8. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. [HyperTree Proof Search for Neural Theorem Proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). arXiv, May 2022. doi: 10.48550/arXiv.2205.11491.
9. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. [Clover: Closed-loop verifiable code generation](https://md.research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/). In ICLR 2024 Conference, 2024. URL [https://openreview.net/forum?id=](https://openreview.net/forum?id=) oSuVEv4X7w. [↗](https://openreview.net/forum?id=)
10. Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. [Towards ai-assisted synthesis of verified dafny methods](https://md.research.elamur.ai/free/en/papers/misu-2024-ai-assisted-synthesis-verified-dafny/). Proc. ACM Softw. Eng., 1(FSE), 2024. doi: 10.1145/ 3643763. URL https://doi.org/10.1145/3643763. [↗](https://doi.org/10.1145/3643763)
11. K Rustan M Leino. Program Proofs. MIT Press, 2023. [find](https://scholar.google.com/scholar?q=K+Rustan+M+Leino%2E+Program+Proofs%2E+MIT+Press%2C+2023%2E)
12. Kaiyu Yang and Jia Deng. [Learning to prove theorems via interacting with proof assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/), 2019.
13. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. [Leandojo: Theorem proving with retrieval-augmented language models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/), 2023.
14. Pisa: Isabelle proofs dataset. [https://aitp-conference.org/2021/abstract/paper_](https://aitp-conference.org/2021/abstract/paper_) 17.pdf, 2021. [↗](https://aitp-conference.org/2021/abstract/paper_)
15. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. [Naturalproofs: Mathematical theorem proving in natural language](https://md.research.elamur.ai/free/en/papers/welleck-2021-naturalproofs-mathematical-theorem-proving-natural/). In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021. URL [https://openreview.ne…](https://openreview.ne…) [↗](https://openreview.ne…)
16. Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. Mining the archive of formal proofs. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, pages 3–17, Cham, 2015. Springer International Pu… [find](https://scholar.google.com/scholar?q=Jasmin+Christian+Blanchette%2C+Maximilian+Haslbeck%2C+Daniel+Matichuk%2C+and+Tobias+Nipkow%2E+Mining+the+archive+of+formal+proofs%2E+In+Manfred+Kerber%2C+Jacques+Carette%2C+Cezary+Kaliszyk%2C+Florian+Rabe%2C+and+Volker)
17. Dan Hendrycks, Steven Basart, Saurav Kadavath, Mantas Mazeika, Akul Arora, Ethan Guo, Collin Burns, Samir Puranik, Horace He, Dawn Song, and Jacob Steinhardt. [Measuring coding challenge competence with apps](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-coding-challenge-competence-apps/). arXiv preprint arXiv:2105.09938, 2021.
18. Qinkai Zheng, Xiao Xia, Xu Zou, Yuxiao Dong, Shan Wang, Yufei Xue, Zihan Wang, Lei Shen, Andi Wang, Yang Li, Teng Su, Zhilin Yang, and Jie Tang. Codegeex: A pre-trained model for code generation with multilingual evaluations on humaneval-x, 2023. [find](https://scholar.google.com/scholar?q=Qinkai+Zheng%2C+Xiao+Xia%2C+Xu+Zou%2C+Yuxiao+Dong%2C+Shan+Wang%2C+Yufei+Xue%2C+Zihan+Wang%2C+Lei+Shen%2C+Andi+Wang%2C+Yang+Li%2C+Teng+Su%2C+Zhilin+Yang%2C+and+Jie+Tang%2E+Codegeex%3A+A+pre%2Dtrained+model+for+code+generation+with+)
19. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. [Evaluating large language models trained on code](https://md.research.elamur.ai/free/en/papers/chen-2021-evaluating-large-language-models-trained/), 2021.
20. Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, and Charles Sutton. [Program synthesis with large language models](https://md.research.elamur.ai/free/en/papers/austin-2021-program-synthesis-large-language-models/), 2021.
21. Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, Karthik Narasimhan, et al. [Swe-bench: Can language models resolve real-world github issues?](https://md.research.elamur.ai/free/en/papers/jimenez-2024-swe-bench-can-language-models/), 2023.
22. Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando Solar-Lezama, Koushik Sen, and Ion Stoica. [Livecodebench: Holistic and contamination free evaluation of large language models for code](https://md.research.elamur.ai/free/en/papers/jain-2024-livecodebench-holistic-contamination-free-evaluation/). arXiv preprint, 2024.
23. OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, Irwan Bello, Ja… — [GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/)
24. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — [Language Models are Few-Shot Learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/)
25. Code llama: Fine-tuning llama for code generation. [https://huggingface.co/Phind/](https://huggingface.co/Phind/) Phind-CodeLlama-34B-v2, 2022. [↗](https://huggingface.co/Phind/)
26. Steve Klabnik and with contributions from the Rust Community Carol Nichols. The Rust Programming Language. No Starch Press, second edition, 2021. URL [https://doc.rust-lang.org/stable/book/](https://doc.rust-lang.org/stable/book/). [↗](https://doc.rust-lang.org/stable/book/)
27. XAI-ORG. Grok-1 Model on Hugging Face. [https://huggingface.co/xai-org/grok-1](https://huggingface.co/xai-org/grok-1), 2024. Accessed: 2024-06-05. [↗](https://huggingface.co/xai-org/grok-1)
28. David Brandfonbrener, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Jianang Yang, Simon Henniger, William E. Byrd, Robert Zinkov, and Nada Amin. Verified multi-step synthesis using large language models and monte carlo tree search, 2023. [find](https://scholar.google.com/scholar?q=David+Brandfonbrener%2C+Sibi+Raja%2C+Tarun+Prasad%2C+Chloe+Loughridge%2C+Federico+Cassano%2C+Jianang+Yang%2C+Simon+Henniger%2C+William+E%2E+Byrd%2C+Robert+Zinkov%2C+and+Nada+Amin%2E+Verified+multi%2Dstep+synthesis+using+larg)
29. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. [A survey on deep learning for theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/). arXiv preprint arXiv:2404.09939, 2024.
30. Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263–288, 2009. URL [http://xavierleroy.org/](http://xavierleroy.org/) publi/Clight.pdf. [↗](http://xavierleroy.org/)
31. Nicholas D Matsakis and Felix S Klock II. The rust language. In ACM SIGAda Ada Letters, volume 34, pages 103–104. ACM, 2014. [find](https://scholar.google.com/scholar?q=Nicholas+D+Matsakis+and+Felix+S+Klock+II%2E+The+rust+language%2E+In+ACM+SIGAda+Ada+Letters%2C+volume+34%2C+pages+103%E2%80%93104%2E+ACM%2C+2014%2E)
32. The Coq Development Team. The Coq reference manual – release 8.19.0. [https://coq.inria.fr/doc/V8.19.0/refman](https://coq.inria.fr/doc/V8.19.0/refman), 2024. [↗](https://coq.inria.fr/doc/V8.19.0/refman)
33. DANIL ANNENKOV, MIKKEL MILO, JAKOB BOTSCH NIELSEN, and BAS SPITTERS. Extracting functional programs from Coq, in Coq. Journal of Functional Programming, 32:e11, 2022. doi: 10.1017/S0956796822000077. — [doi:10.1017/s0956796822000077](https://doi.org/10.1017/s0956796822000077) [find](https://scholar.google.com/scholar?q=DANIL+ANNENKOV%2C+MIKKEL+MILO%2C+JAKOB+BOTSCH+NIELSEN%2C+and+BAS+SPITTERS%2E+Extracting+functional+programs+from+Coq%2C+in+Coq%2E+Journal+of+Functional+Programming%2C+32%3Ae11%2C+2022%2E+doi%3A+10%2E1017%2FS0956796822000077%2E+%E2%80%94)
34. Design Automation Standards Committee and Automatic Test Program Generation Subcommittee. Ieee standard for vhdl language reference manual. IEEE Std 1076-2019, pages 1–673, 2019. doi: 10.1109/IEEESTD.2019.8938196. — [doi:10.1109/ieeestd.2019.8938196](https://doi.org/10.1109/ieeestd.2019.8938196) [find](https://scholar.google.com/scholar?q=Design+Automation+Standards+Committee+and+Automatic+Test+Program+Generation+Subcommittee%2E+Ieee+standard+for+vhdl+language+reference+manual%2E+IEEE+Std+1076%2D2019%2C+pages+1%E2%80%93673%2C+2019%2E+doi%3A+10%2E1109%2FIEEESTD%2E)
35. Donald Thomas and Philip Moorby. The Verilog Hardware Description Language. Springer Publishing Company, Incorporated, 5th ed. edition, 2008. ISBN 0387849300. [find](https://scholar.google.com/scholar?q=Donald+Thomas+and+Philip+Moorby%2E+The+Verilog+Hardware+Description+Language%2E+Springer+Publishing+Company%2C+Incorporated%2C+5th+ed%2E+edition%2C+2008%2E+ISBN+0387849300%2E)
36. Adam Procter, William L. Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. Semantics driven hardware design, implementation, and verification with rewire. In Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM, LCTES’15, Ne… — [doi:10.1145/2670529.2754970](https://doi.org/10.1145/2670529.2754970) [find](https://scholar.google.com/scholar?q=Adam+Procter%2C+William+L%2E+Harrison%2C+Ian+Graves%2C+Michela+Becchi%2C+and+Gerard+Allwein%2E+Semantics+driven+hardware+design%2C+implementation%2C+and+verification+with+rewire%2E+In+Proceedings+of+the+16th+ACM+SIGPLA)
37. Xun Li, Mohit Tiwari, Jason K. Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, and Ben Hardekopf. Caisson: a hardware description language for secure information flow. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, page 109… — [doi:10.1145/1993498.1993512](https://doi.org/10.1145/1993498.1993512) [find](https://scholar.google.com/scholar?q=Xun+Li%2C+Mohit+Tiwari%2C+Jason+K%2E+Oberg%2C+Vineeth+Kashyap%2C+Frederic+T%2E+Chong%2C+Timothy+Sherwood%2C+and+Ben+Hardekopf%2E+Caisson%3A+a+hardware+description+language+for+secure+information+flow%2E+In+Proceedings+of+t)
38. Wikipedia contributors. Jaccard index — wikipedia, the free encyclopedia. [https://en.wikipedia.org/wiki/Jaccard_index](https://en.wikipedia.org/wiki/Jaccard_index), 2024. Accessed: 2024-03-27. [↗](https://en.wikipedia.org/wiki/Jaccard_index)
39. Wikipedia contributors. N-gram — Wikipedia, the free encyclopedia. wikipedia.org/wiki/N-gram, 2024. Accessed: 2024-03-27. https://en. [find](https://scholar.google.com/scholar?q=Wikipedia+contributors%2E+N%2Dgram+%E2%80%94+Wikipedia%2C+the+free+encyclopedia%2E+wikipedia%2Eorg%2Fwiki%2FN%2Dgram%2C+2024%2E+Accessed%3A+2024%2D03%2D27%2E+https%3A%2F%2Fen%2E)
40. Chenghao Mou, Chris Ha, Kenneth Enevoldsen, and Peiyuan Liu. Chenghaomou/text-dedup: Reference snapshot, September 2023. URL https://doi.org/10.5281/zenodo.8364980. — [doi:10.5281/zenodo.8364980](https://doi.org/10.5281/zenodo.8364980) [↗](https://doi.org/10.5281/zenodo.8364980)
41. Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark Barrett, and Ying Sheng. Efficiently programming large language models using sglang, 2023. [find](https://scholar.google.com/scholar?q=Lianmin+Zheng%2C+Liangsheng+Yin%2C+Zhiqiang+Xie%2C+Jeff+Huang%2C+Chuyue+Sun%2C+Cody+Hao+Yu%2C+Shiyi+Cao%2C+Christos+Kozyrakis%2C+Ion+Stoica%2C+Joseph+E%2E+Gonzalez%2C+Clark+Barrett%2C+and+Ying+Sheng%2E+Efficiently+programming+)

*Updated 3 November 2026*