发表机构
LIM, université de La Réunion; Université de Namur（留尼汪大学LIM实验室; 那慕尔大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究以九十九个Prolog问题（P-99）为对象，借助向语言模型Claude提问，生成Prolog代码及测试文件，再用LPTP进行验证，完成了前三十三个问题的解决，介绍了具体过程与细节，为他人重现实验提供便利。
AI 中文摘要
九十九个Prolog问题（P-99）是一组著名的Prolog练习。我们仅通过向语言模型（大语言模型，LLM）提问就解决了前三十三个问题，使用的是Anthropic公司的Claude。解决问题意味着生成Prolog代码和测试文件，运行测试并检查是否通过，然后用LPTP（逻辑程序定理证明器）正式证明类型、基元性、终止性、唯一性、存在性，有时还包括功能正确性。因此，我们的方法是对P-99进行氛围编码/验证编码的实验。这是一个氛围编码实验，因为我们从用英语编写的非正式规范开始，让Claude生成Prolog代码。它也符合验证编码，因为LLM对生成的Prolog代码证明了可靠性保证。Claude编写了58个逻辑程序、508个测试、257个引理，总共11800行证明。我们手动检查了LLM生成的每个文件，包括检查Prolog代码、运行测试、检查Claude生成的逻辑语句并用LPTP对Claude的证明进行校验。本文描述了这个实验并提供了主要细节，以便感兴趣的读者能够重现它。
英文摘要
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.
CommentsIn Proceedings ICLP 2026, arXiv:2607.17707
Journal refEPTCS 450, 2026, pp. 209-222
