ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
By: Mantas Baksys , Stefan Zetzsche , Olivier Bouissou and more
Potential Business Impact:
Creates code that checks itself for mistakes.
Large language models have shown potential for program verification, but progress is hindered by the scarcity of verified code for training. We present ATLAS, an automated pipeline that synthesizes verified programs at scale to address this data bottleneck. ATLAS generates complete Dafny programs with specifications, implementations, and proofs, producing 2.7K verified programs from which we extract over 19K training examples--more than 7 per verified program--by decomposing the synthesis process into multiple specialized tasks. Fine-tuning Qwen 2.5 7B Coder on this dataset produces substantial gains: +23 percentage points on DafnyBench and +50 percentage points on DafnySynthesis. These results demonstrate that synthetic verified code can effectively enhance LLM capabilities for formal verification.
Similar Papers
AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution
Software Engineering
Makes computer code write itself correctly.
Arrows of Math Reasoning Data Synthesis for Large Language Models: Diversity, Complexity and Correctness
Computation and Language
Teaches computers to solve math problems better.
A benchmark for vericoding: formally verified program synthesis
Software Engineering
Makes computer code work perfectly, every time.