用低成本代理流程批量生成可验证的数学定理数据
TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow
- 将形式化过程拆解为五步任务，通过解耦策略回收失败轨迹中的有效信号
- 在2000题基准上达成12.6%验证率，成本仅0.481美元/成功轨迹
- 适合想构建数学推理数据飞轮的研究者或工具开发者
形式化数学中代理工作流的高成本限制了大规模数据合成，加剧了开源语料库的稀缺。为此，我们提出《TheoremForge》——一种低成本的形式化数据合成流水线，将形式化过程分解为五个子任务：命题形式化、证明生成、前提选择、证明修正和证明草图。通过实现解耦提取策略，该流程从全局失败轨迹中恢复有效训练信号，充分利用被浪费的计算资源。在包含2000个问题的基准测试中，TheoremForge以每条成功轨迹平均0.481美元的成本（使用Gemini-3-Flash）实现了12.6%的验证率，超过8.6%的基线水平。关键的是，该策略使证明生成的数据产出率提升了1.6倍，相较于标准过滤方法。这些结果确立了TheoremForge作为构建未来专家模型数据飞轮的可扩展框架。代码已开源。
原文摘要 · Abstract (English)
The high cost of agentic workflows in formal mathematics hinders large-scale data synthesis, exacerbating the scarcity of open-source corpora. To address this, we introduce \textbf{TheoremForge}, a cost-effective formal data synthesis pipeline that decomposes the formalization process into five sub-tasks, which are \textit{statement formalization}, \textit{proof generation}, \textit{premise selection}, \textit{proof correction} and \textit{proof sketching}. By implementing a \textit{Decoupled Extraction Strategy}, the workflow recovers valid training signals from globally failed trajectories, effectively utilizing wasted computation. Experiments on a 2,000-problem benchmark demonstrate that TheoremForge achieves a Verified Rate of 12.6\%, surpassing the 8.6\% baseline, at an average cost of only \textbf{\$0.481} per successful trajectory using Gemini-3-Flash. Crucially, our strategy increases data yield by \textbf{1.6$\times$} for proof generation compared to standard filtering. These results establish TheoremForge as a scalable framework for constructing a data flywheel to train future expert models. Our code is available \href{https://github.com/timechess/TheoremForge}{here}.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。