Formal Disco: 형식적으로 검증된 프로그램의 확장 가능하고 개방형 생성 시스템

Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

인공지능 에이전트의 성능이 향상됨에 따라 코드 생성 비용은 빠르게 감소하고 있지만, 생성된 프로그램의 품질 보장은 그 속도를 따라가지 못하고 있습니다. 형식적 검증은 가장 강력한 수준의 보장을 제공하지만, AI 모델이 검증을 고려한 언어를 사용하도록 하는 것은 해당 언어로 작성된 프로그램 예제의 부족으로 인해 어려움을 겪고 있습니다. 이러한 데이터 부족 문제를 해결하기 위해, 우리는 LLM 기반 작업자를 조정하는 분산 시스템인 Formal Disco를 제안합니다. 이 시스템은 대규모의 개방형 합성 데이터 생성에 쉽게 적용될 수 있습니다. Formal Disco는 세 가지 유형의 작업자(

The cost of producing code is rapidly diminishing with increasingly capable AI agents, while quality assurance of generated programs has not kept pace. Formal verification provides the strongest possible guarantees, but the ability of AI models to work with verification-aware languages is hindered by the scarcity of human-written examples of programs in those languages. To tackle this prevalent data scarcity issue, we propose Formal Disco: a distributed system for coordination of LLM-based workers that can be easily applied to open-ended synthetic data generation at scale. We use Formal Disco to share tasks and programs between three classes of workers: "initiators", which read random READMEs from open-source repositories and documentation snippets to sketch a related verified program, "fixers" which take compiler and verifier feedback and attempt to resolve issues, and "extenders" that take working programs and propose patches to expand them. Formal Disco records all agent-generated traces and uses them both for initial distillation from a stronger model as well as self-improvement. We also propose a principle of maximum entropy for synthetic program generation, and use entropy maximization via iterative supervised fine-tuning to learn to generate increasingly diverse programs over time. We release large datasets of synthetic verified programs in three languages - Dafny, Verus, and Frama-C -, and fine-tune open models for verification-relevant tasks, often matching or exceeding the performance of Claude Opus 4.5. Overall, our work offers a path to create synthetic data at scale for formal reasoning domains and overcome the long-standing data barrier.