用大模型将形式化证明转为自然语言，提升可读性。
Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
- 通过大模型将形式化步骤转化为口语化描述
- 在本科教材和Lean证明库上均生成高质量自然语言证明
- 适合数学教育、形式化验证领域研究者使用
本文提出一种自然语言翻译方法，用于机器可验证的形式化证明。该方法利用大模型的非形式化（将形式语言证明步骤口语化）与摘要能力，将形式化证明转化为自然语言。评估中，该方法应用于基于本科教材自然语言证明生成的形式化证明数据集，并对比生成结果与原始自然语言证明的质量。此外，还展示了该方法在现有Lean证明库上的应用效果，能够输出高度可读且准确的自然语言证明。
原文摘要 · Abstract (English)
This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and summarization capabilities of LLMs. For evaluation, it was applied to formal proof data created in accordance with natural language proofs taken from an undergraduate-level textbook, and the quality of the generated natural language proofs was analyzed in comparison with the original natural language proofs. Furthermore, we will demonstrate that this method can output highly readable and accurate natural language proofs by applying it to existing formal proof library of the Lean proof assistant.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。