案例研究：使用LPTP和大语言模型证明√2是无理数
Case study: proving sqrt(2) irrational with LPTP and an LLM
浏览论文内容
中文总结 AI 辅助
该研究在逻辑编程环境下，从基本谓词定义出发，借助LPTP系统，简述√2无理数的证明并与LLM交互，最终获得由LLM部分生成、LPTP完全验证的完整形式证明。
中文摘要 AI 辅助
我们展示了在逻辑编程（LP）环境中与大语言模型（LLM）交互以证明√2不是有理数的过程。我们从一些基本的纯逻辑编程谓词定义开始，依靠逻辑程序定理证明器（LPTP）系统来陈述和证明逻辑程序的属性。由于LPTP的证明语言基于自然演绎，证明是人类可读的。在案例研究中，我们在LPTP中简述了证明√2无理数的常见证明，然后描述与LLM的交互，最终得到一个由LLM部分生成、LPTP完全验证的完整形式证明。
英文摘要
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.
发表机构
- LIM, université de La Réunion（留尼汪大学LIM实验室）
- Université de Namur（那慕尔大学）
机构由 AI 辅助整理，请以论文原文为准。
