TheoremForge：用低预算Agentic工作流扩展形式化数据合成

形式数学中Agentic工作流的高成本阻碍了大规模数据合成，加剧了开源语料的稀缺。为此，我们提出TheoremForge，一个经济高效的形式化数据合成管线，它将形式化过程分解为五个子任务：陈述形式化、证明生成、前提选择、证明纠错和证明草拟。通过实施解耦抽取策略（Decoupled Extraction Strategy），该工作流能从整体失败的轨迹中回收有效的训练信号，有效利用被浪费的计算。在2,000题基准上的实验表明，TheoremForge实现了12.6%的验证通过率（Verified Rate），超过8.6%的基线，且使用Gemini-3-Flash时每条成功轨迹的平均成本仅为0.481美元。关键在于，与标准过滤相比，我们的策略使证明生成的数据产量提升1.6倍。这些结果确立了TheoremForge作为构建数据飞轮以训练未来专家模型的可扩展框架。我们的代码发布于 https://github.com/timechess/TheoremForge。