ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Soonho Kong, Sean B. Holden

TL;DR
ATLAS is an automated pipeline that synthesizes verified programs, generating thousands of machine-checked proofs to enhance large language models' ability to produce correct, verified code for safety-critical applications.
Contribution
The paper introduces ATLAS, a novel automated system that creates verified code and training data, significantly improving LLM performance in formal verification tasks.
Findings
Generated 2.7K verified Dafny programs with proofs
Improved LLM performance on verification benchmarks
Demonstrated synthetic data's effectiveness for scaling verification capabilities
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMachine Learning in Materials Science · Logic, programming, and type systems · Scientific Computing and Data Management
