2025/12/11 by Mantas Baksys, Baksys, Mantas, Stefan Zetzsche +8
Computer Science · Decision Sciences · Materials Science · #FOS: Computer and information sciences #Logic, programming, and type systems #Machine Learning in Materials Science #Scientific Computing and Data Management #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2512.10173
openalex publication_date 2025/12/11 · openalex created_date 2025/12/13 · openalex updated_date 2026/07/28
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.