ProofBridge：基于联合嵌入的自然语言证明自动形式化
计算机科学中的逻辑
2026-03-31 v3 人工智能
摘要
将人类编写的数学定理和证明从自然语言(NL)翻译成像 Lean 4 这样的形式语言(FL)，一直是 AI 的重要挑战之一。大多数最先进方法要么专注于 NL-to-FL 定理-only 自动形式化，要么专注于从 FL 定理进行 FL 证明合成。实际中，对定理与证明的自动形式化仍需要人工介入，正如 AlphaProof 在 2024 年 IMO 中所展现的银牌成绩所示，问题陈述被手动翻译后才能进行自动证明合成。我们提出了 ProofBridge，一个统一的框架，用于自动将整个 NL 定理和证明翻译成 Lean 4。其核心是一个联合嵌入模型，在共享语义空间中对齐 NL 和 FL(NL-FL) 定理+证明对，实现语义相关 FL 示例的跨模态检索，以指导翻译。ProofBridge 集成了检索增强微调与迭代证明修复，利用 Lean 的类型检查器和语义等价反馈，确保语法正确性和语义忠实性。实验表明，ProofBridge 在强基线(包括 GPT-5、Gemini-2.5、Kimina-Prover、DeepSeek-Prover)上显著改进了证明自动形式化，我们的检索增强方法在语义正确性(SC，通过证明双向等价)和类型正确性(TC，通过类型检查定理+证明)方面带来显著提升，尤其在 miniF2F-Test-PF 数据集上，SC 提升了 31.14%，TC 提升了 1.64%。
引用
@article{arxiv.2510.15681,
title = {ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings},
author = {Prithwish Jana and Kaan Kale and Ahmet Ege Tanriverdi and Cruise Song and Sriram Vishwanath and Vijay Ganesh},
journal= {arXiv preprint arXiv:2510.15681},
year = {2026}
}
备注
Published as a conference paper at the 14th International Conference on Learning Representations (ICLR 2026), Rio de Janeiro, Brazil, April 23-27, 2026