Formal Disco：可扩展的形式化验证程序开放式生成

针对形式化验证语言数据稀缺问题，本文提出 Formal Disco，一种基于 LLM 的分布式多智能体系统。该系统协调“发起者”、“修复者”和“扩展者”三类智能体，通过开源文档 sketch 程序、利用编译器反馈修复错误及扩展功能，大规模生成合成数据。系统记录生成轨迹用于模型蒸馏与自我改进，并提出最大熵原则，通过迭代监督微调提升程序多样性。实验在 Dafny 等语言上生成大量数据集，微调后的开源模型性能媲美顶级闭源模型，突破了形式化推理领域的数据壁垒。