Case study: solving P-99 with LPTP and an LLM

📄 arXiv: 2607.21196v1 📥 PDF

作者: Fred Mesnard, Thierry Marianne, Étienne Payet, Wim Vanhoof

分类: cs.LO, cs.AI

发布日期: 2026-07-23

备注: In Proceedings ICLP 2026, arXiv:2607.17707

期刊: EPTCS 450, 2026, pp. 209-222

DOI: 10.4204/EPTCS.450.17

💡 一句话要点

利用LPTP和LLM解决P-99问题的案例研究

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: Prolog 大型语言模型 逻辑程序 形式化验证 自动化编程 LPTP 代码生成 实验研究

📋 核心要点

  1. 现有的Prolog问题解决方法往往依赖于人工编码，效率低且容易出错。
  2. 本文提出通过大型语言模型Claude生成Prolog代码，并利用LPTP进行形式化验证，提升了代码生成的可靠性。
  3. 实验结果显示，Claude成功生成了大量逻辑程序和测试，且所有生成的代码均通过了验证，证明了该方法的有效性。

📝 摘要（中文）

《九十九个Prolog问题（P-99）》是一组著名的Prolog练习。本文通过提示大型语言模型（LLM）Claude，成功解决了前33个问题。我们生成了Prolog代码和测试文件，运行测试并验证其通过情况，随后使用逻辑程序定理证明器（LPTP）对类型、可达性、终止性、唯一性、存在性及功能正确性进行了形式化证明。我们的研究展示了从非正式的英文规范出发，通过LLM生成代码的实验过程，并确保生成代码的可靠性。Claude共生成了58个逻辑过程、508个测试和257个引理，总计11800行证明。我们手动检查了每个生成文件，确保了代码和证明的准确性。本文详细描述了这一实验，以便感兴趣的读者能够复现。

🔬 方法详解

问题定义：本文旨在解决P-99中的Prolog问题，现有方法主要依赖人工编码，效率低且容易出错，缺乏自动化和可靠性验证。

核心思路：通过利用大型语言模型Claude，从非正式的英文规范出发生成Prolog代码，并使用LPTP进行形式化验证，以确保生成代码的正确性和可靠性。

技术框架：整体流程包括三个主要阶段：首先是从英文规范生成Prolog代码，其次是生成测试文件并运行测试，最后使用LPTP进行形式化证明，验证代码的各项属性。

关键创新：本研究的创新在于结合了LLM的生成能力与LPTP的验证能力，实现了从自然语言到形式化证明的自动化过程，显著提高了Prolog代码的生成和验证效率。

关键设计：在参数设置上，Claude生成了58个逻辑过程、508个测试和257个引理，确保了生成的代码和证明的全面性和准确性。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

实验结果表明，Claude成功生成了58个逻辑程序和508个测试，所有生成的代码均通过了LPTP的验证，证明了该方法在生成和验证Prolog代码方面的有效性和可靠性。

🎯 应用场景

该研究的潜在应用领域包括自动化程序生成、教育领域的编程教学以及形式化验证等。通过结合LLM与逻辑证明工具，可以在多个领域实现更高效的代码生成和验证，推动智能编程的发展。

📄 摘要（原文）

Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By solved we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem Prover). Hence our approach is an experiment in vibe-coding/vericoding of P-99. It is a vibe-coding experiment because we started from informal specifications written in English and let Claude generate the Prolog code. It also fits within vericoding because the LLM proved reliability guarantees on the generated Prolog code. Claude wrote 58 logic procedures, 508 tests, 257 lemmas for a total of 11800 proof lines. We manually checked each file generated by the LLM. We checked the Prolog code, ran the tests, examined the logical statements generated by Claude and proof-checked Claude's proofs with LPTP. This paper describes this experiment and provides the main details so that it can be reproduced by the interested reader.