Case study: proving sqrt(2) irrational with LPTP and an LLM
作者: Fred Mesnard, Étienne Payet, Wim Vanhoof
分类: cs.LO, cs.AI, cs.SC
发布日期: 2026-07-23
备注: In Proceedings ICLP 2026, arXiv:2607.17707
期刊: EPTCS 450, 2026, pp. 67-80
DOI: 10.4204/EPTCS.450.5
💡 一句话要点
利用LPTP和LLM证明根号2的无理性
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 逻辑编程 自动化证明 大型语言模型 数学证明 自然推理
📋 核心要点
- 核心问题：现有方法在证明数学命题时缺乏自动化和可读性，尤其是在逻辑编程环境中。
- 方法要点：通过结合LPTP和LLM，利用自然推理的可读性来生成和验证数学证明。
- 实验或效果：最终生成的证明不仅完整且经过LPTP的严格检查，展示了LLM在数学证明中的潜力。
📝 摘要（中文）
本文展示了与大型语言模型（LLM）的互动，旨在逻辑编程（LP）背景下证明根号2不是有理数。我们从一些基本的纯逻辑编程谓词定义开始，依赖于逻辑程序定理证明器（LPTP）系统来陈述和证明逻辑程序的性质。由于LPTP的证明语言基于自然推理，证明过程可读性强。我们在LPTP中勾勒了证明根号2无理性的常规证明，并描述了与LLM的互动，最终得到了一个完整的形式证明，该证明部分由LLM生成，完全由LPTP进行证明检查。
🔬 方法详解
问题定义：本文旨在解决在逻辑编程环境中证明根号2无理性的问题。现有方法往往缺乏自动化和可读性，难以有效生成和验证数学证明。
核心思路：论文的核心思路是结合逻辑程序定理证明器（LPTP）与大型语言模型（LLM），利用LLM生成初步证明，然后通过LPTP进行验证，以确保证明的严谨性和可读性。
技术框架：整体架构包括两个主要模块：首先，使用LPTP定义逻辑程序和相关谓词；其次，利用LLM生成证明的初步草稿，最后通过LPTP进行全面的证明检查。
关键创新：最重要的技术创新点在于将LLM与逻辑程序定理证明器结合，形成了一种新的证明生成和验证机制。这种方法在可读性和自动化方面优于传统的证明方法。
关键设计：在设计过程中，重点关注了自然推理的可读性，确保生成的证明不仅正确而且易于理解。同时，LPTP的证明检查机制确保了最终结果的严谨性。
🖼️ 关键图片
📊 实验亮点
实验结果表明，结合LLM与LPTP的证明生成方法有效提高了证明的自动化程度和可读性。最终生成的证明经过LPTP的严格检查，确保了其完整性和正确性，展示了LLM在数学证明中的实际应用潜力。
🎯 应用场景
该研究的潜在应用领域包括教育、自动化定理证明和数学研究等。通过提高数学证明的自动化程度和可读性，能够帮助学生更好地理解复杂的数学概念，同时也为研究人员提供了新的工具来探索更复杂的数学命题。
📄 摘要（原文）
We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of the square root of 2. Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.