ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908804344446976 |
|---|---|
| author | Baksys, Mantas Zetzsche, Stefan Bouissou, Olivier Delmas, Remi Kong, Soonho Holden, Sean B. |
| author_facet | Baksys, Mantas Zetzsche, Stefan Bouissou, Olivier Delmas, Remi Kong, Soonho Holden, Sean B. |
| contents | Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust, yet for safety-critical applications, formal verification provides the only true guarantees through machine-checked proofs. However, verified code remains scarce compared to mainstream languages or mathematical theorem proving, limiting LLM capabilities in this domain. We present ATLAS, an automated pipeline that synthesizes verified programs to address this data bottleneck. Applied to the TACO dataset of Python solutions to LeetCode-style problems, ATLAS generates 2.7K verified Dafny programs, each with high-quality specifications and machine-checked proofs. Through task decomposition, we extract 19K training examples. Fine-tuning Qwen 2.5 7B Coder on this data improves performance from 32.4% to 56.9% on DafnyBench and from 15.8% to 65.8% on DafnySynthesis, demonstrating that synthetic data generation is a viable path to scaling LLM capabilities for formal verification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_10173 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis Baksys, Mantas Zetzsche, Stefan Bouissou, Olivier Delmas, Remi Kong, Soonho Holden, Sean B. Software Engineering Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust, yet for safety-critical applications, formal verification provides the only true guarantees through machine-checked proofs. However, verified code remains scarce compared to mainstream languages or mathematical theorem proving, limiting LLM capabilities in this domain. We present ATLAS, an automated pipeline that synthesizes verified programs to address this data bottleneck. Applied to the TACO dataset of Python solutions to LeetCode-style problems, ATLAS generates 2.7K verified Dafny programs, each with high-quality specifications and machine-checked proofs. Through task decomposition, we extract 19K training examples. Fine-tuning Qwen 2.5 7B Coder on this data improves performance from 32.4% to 56.9% on DafnyBench and from 15.8% to 65.8% on DafnySynthesis, demonstrating that synthetic data generation is a viable path to scaling LLM capabilities for formal verification. |
| title | ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2512.10173 |