通过对证明步骤的非形式化化及证明结构的递归概述实现形式证明的自然语言翻译
计算与语言
2025-09-15 v1
摘要
本文提出了一种用于机器可验证形式证明的自然语言翻译方法，利用大语言模型的非形式化化（将形式语言证明步骤 verbalization）和概述能力。为进行评估，该方法被应用于根据自然语言证明（取自大学水平教材）创建的形式证明数据，并分析生成的自然语言证明质量与原自然语言证明的对比。此外，我们将展示该方法能够输出高可读性和高准确性的自然语言证明，通过将其应用于现有的 Lean 证明助手形式证明库。
引用
@article{arxiv.2509.09726,
title = {Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure},
author = {Seiji Hattori and Takuya Matsuzaki and Makoto Fujiwara},
journal= {arXiv preprint arXiv:2509.09726},
year = {2025}
}
备注
Submitted to INLG 2025 (accepted)