Toward Automated, Contamination-free Dafny Benchmark Generation
Recently, Large Language Models (LLMs) have been widely applied to code generation, and recent studies have explored their ability to produce programs in verification languages, including Dafny. Although several benchmarks have been proposed to assess LLM performance in generating Dafny code, existing datasets suffer from several limitations, including no clear verification goals, limited diversity in verification complexity, potential contamination, and heavy reliance on manually collected examples that are publicly available online. In this work, we introduce TACoDafny, an automated pipeline for constructing Dafny verification benchmarks directly from task descriptions sourced from online programming repositories. As a preliminary result, we successfully generated 76 Dafny programs with verifiable properties derived from the task descriptions of the first 200 LeetCode problems. Our pipeline not only enables large-scale benchmark generation, but also facilitates the creation of additional verifiable Dafny code that can be leveraged to train models to further improve their verification capabilities.
Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:00 - 18:00 | |||
16:00 18mTalk | ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis Dafny Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services, Soonho Kong Amazon Web Services, Remi Delmas Amazon Web Services Pre-print | ||
16:18 18mTalk | A benchmark for vericoding: formally verified program synthesis Dafny Sergiu Bursuc Beneficial AI Foundation, Theodore Ehrenborg Beneficial AI Foundation, Shaowei Lin Beneficial AI Foundation, Lăcrămioara Aștefănoaei Beneficial AI Foundation, Ionel Emilian Chiosa MIT, Jure Kukovec Beneficial AI Foundation, Alok Singh Beneficial AI Foundation, Oliver Butterley Beneficial AI Foundation, Adem Bizid MIT, Quinn Dougherty Beneficial AI Foundation, Miranda Zhao MIT, Max Tan MIT, Max Tegmark Massachusetts Institute of Technology Pre-print File Attached | ||
16:36 18mTalk | DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Dafny Pre-print | ||
16:54 18mTalk | MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification Dafny Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services Pre-print | ||
17:12 18mTalk | Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs Dafny Valentina Wu Faculdade de Engenharia, Universidade do Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, Alexandre Abreu University of Porto & INESC TEC | ||
17:30 18mTalk | Toward Automated, Contamination-free Dafny Benchmark Generation Dafny Changjie Wang KTH Royal Institute of Technology, Mariano Scazzariello RISE Research Institutes of Sweden, Dejan Kostic KTH Royal Institute of Technology, Marco Chiesa KTH Royal Institute of Technology Pre-print | ||
17:48 12mDay closing | Day closing Dafny | ||