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

摘要

AI智能体使代码生产成本迅速下降，但生成程序的质量保障未跟上。形式验证提供最强保证，但AI模型使用验证感知语言的能力受制于人类书写样例的稀缺。为解决该数据稀缺，我们提出Formal Disco：一个协调LLM工作者的分布式系统，可轻松应用于大规模开放式合成数据生成。我们在三类工作者之间共享任务与程序：“发起者”阅读开源仓库的随机README与文档片段、勾画相关的经验证程序；“修复者”接受编译器与验证器反馈尝试解决问题；“扩展者”拿可用程序提议扩展补丁。Formal Disco记录所有智能体轨迹，既用于从更强模型的初始蒸馏，也用于自我改进。我们提出合成程序生成的最大熵原则，并经迭代SFT做熵最大化，学习生成日益多样的程序。我们发布Dafny、Verus与Frama-C三种语言的大型合成经验证程序数据集，并为验证相关任务微调开源模型——常匹敌或超过Claude Opus 4.5。

Formal Disco：形式验证程序的可扩展开放式生成：论文配图 — 图 1：正式迪斯科概述。该系统以分布式议程为中心，大语言模型的工作人员在其中协作完成任务并存储对象——主要是正在编写、扩展和修复的合成程序。发起者工作人员使用给定的验证感知语言绘制初始程序，包括规范和证明，从开源存储库中采样的自述文件以及编程语言参考中的片段和示例中获取想法。程序可能会编译或验证失败；然后，修复者工人会编写补丁来尝试修复错误。工作程序的复杂性因扩展器工作人员编写的补丁而增加。由此产生的合成程序既可以用于自我改进底层的大语言模型，也可以为下游任务生成训练数据。