ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
summary
ATLAS is an automated pipeline that converts Python contest problems into complete Dafny programs by generating a fixed method signature, synthesizing specifications and test cases, then implementing and proving against them using a compiler-feedback loop with staged self-correction. The pipeline produces about 2.7K verified Dafny programs and extracts over 19K training examples plus error-correction traces. Fine-tuning Qwen 2.5 7B Coder on this data yields large gains (+23pp on DafnyBench, +50pp on DafnySynthesis).
AI-written summary · about
chapters (11)
- 0:00ATLAS introduction
- 1:08Dataset and pipeline
- 3:34Pipeline stages example
- 5:42Python spec challenges
- 7:27Overly restrictive specs
- 9:16Compiler feedback results
- 10:39Metadata analysis
- 12:01Fine-tuning approach
- 13:49Benchmark evaluation
- 14:31Conclusion and future
- 15:13Q&A
related talks
22mTowards Automated Verification of LLM-Synthesized C Programs
39mTraining AI To Code Using The Largest Code Dataset (Project CodeNet)
38mAutomatically Synthesising Programs that We Can Trust
41m"Do What I Mean": The History of AI and Program Synthesis- 39mTraining AI To Code Using The Largest Code Dataset (Project CodeNet)
54mA World Without Programmers?
26mDSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines
01h 16mCoding Agents: New opportunities for formal methods?