⏶9
StepFun-Formalizer：通过知识-推理融合释放LLM的自动形式化潜力
发表
由 
Yutong Wu 提交
Yutong Wu 提交作者: Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, 
Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu摘要
自动形式化旨在将自然语言的数学陈述翻译成形式语言。虽然大型语言模型（LLMs）加速了这一领域的进展，但现有方法仍然存在准确性低的问题。我们确定了有效自动形式化的两个关键能力：全面掌握形式语言领域知识，以及自然语言问题理解和非形式到形式对齐的推理能力。没有前者，模型无法识别正确的形式对象；没有后者，模型难以解释现实世界语境并将其精确映射到形式表达式。为了解决这些不足，我们引入了 ThinkingF，一个数据合成和训练管道，可以提升这两种能力。首先，我们构建了两个数据集：一个通过提炼和选择富含形式知识的大规模示例，另一个通过生成由专家设计的模板指导的非形式到形式推理轨迹。然后，我们使用这些数据集应用 SFT 和 RLVR，以进一步融合和完善这两种能力。由此产生的 7B 和 32B 模型既展现出全面的形式知识，又具备强大的非形式到形式推理能力。值得注意的是，StepFun-Formalizer-32B 在 FormalMATH-Lite 上达到了 40.5% 的 SOTA BEq@1 分数，在 ProverBench 上达到了 26.7% 的 SOTA BEq@1 分数，超越了所有先前的通用和专用模型。
自动形式化旨在将自然语言数学语句翻译成形式语言。尽管大型语言模型加速了该领域的进展，但现有方法仍然存在准确性低的问题。我们确定了有效自动形式化的两项关键能力：对形式语言领域知识的全面掌握，以及自然语言问题理解和非形式-形式对齐的推理能力。没有前者，模型无法识别正确的形式对象；没有后者，它难以解释现实世界的上下文并将其精确映射为形式表达式。为了弥补这些差距，我们引入了 ThinkingF，一个数据合成和训练管道，可以同时提高这两种能力。首先，我们构建了两个数据集：一个通过提炼和选择富含形式知识的大规模示例，另一个通过专家设计的模板生成非形式到形式的推理轨迹。然后，我们使用这些数据集应用 SFT 和 RLVR，以进一步融合和完善这两种能力。最终的 7B 和 32B 模型展示了全面的形式知识和强大的非形式到形式推理能力。值得注意的是，StepFun-Formalizer-32B 在 FormalMATH-Lite 上取得了 40.5% 的 SOTA BEq@1 分数，在 ProverBench 上取得了 26.7% 的 SOTA BEq@1 分数，超越了所有之前的通用和专用模型。