带工具反馈的 Autoformalizer
人工智能
2025-10-09 v1
摘要
Autoformalization 通过将数学问题从自然语言翻译为形式语句来解决自动定理证明（ATP）数据稀缺的问题。近期研究努力从直接调用大型语言模型转向从零开始训练端到端的 formalizer 模型，取得了显著的进展。然而，现有的 formalizer 仍然难以持续生成满足语法有效性和语义一致性的有效语句。为此，我们提出了带工具反馈的 Autoformalizer（ATF），一种新方法，将语法和一致性信息作为工具集成到形式化过程中。通过集成 Lean 4 编译器进行语法校正，并采用多 LLM 评判法进行一致性验证，模型能够根据工具反馈自适应地细化生成的语句，从而提高语法有效性和语义一致性。ATF 的训练包括针对合成工具调用数据的 cold-start 阶段、提升形式化能力的 expert iteration 阶段，以及用于缓解无效修订的 Direct Preference Optimization。实验结果表明，ATF 在一系列基线 formalizer 模型上实现了显著的优势，其优越性能经人类评估进一步得到验证。随后分析表明，ATF 在推理规模方面表现出色。我们开源了 Numina-ATF，包含 75 万个合成形式语句的数据集，以推动 autoformalization 和 ATP 研究的进展。
引用
@article{arxiv.2510.06857,
title = {Autoformalizer with Tool Feedback},
author = {Qi Guo and Jianing Wang and Jianfei Zhang and Deyang Kong and Xiangzhou Huang and Xiangyu Xi and Wei Wang and Jingang Wang and Xunliang Cai and Shikun Zhang and Wei Ye},
journal= {arXiv preprint arXiv:2510.06857},
year = {2025}
}