用大模型自动生成并验证33个逻辑编程题的代码与证明。
Case study: solving P-99 with LPTP and an LLM
- 从英文描述出发，让大模型生成Prolog代码和测试用例。
- 生成58个逻辑函数、508个测试用例，完成257个定理证明共1.18万行。
- 人工验证代码正确性与形式化证明，可复现的可信编码实验。
九十九个Prolog问题（P-99）是一组著名的Prolog练习题。我们仅通过提示大语言模型（LLM）就解决了前33个问题。使用的是Anthropic的Claude模型。所谓解决，指生成Prolog代码与测试文件，运行测试验证通过，并使用逻辑程序定理证明器LPTP对类型、原子性、终止性、唯一性、存在性及部分函数正确性进行形式化证明。该方法是一次‘直觉编码’（vibe-coding）与‘验证编码’（vericoding）的结合实验：从非形式化的英文说明开始，由大模型生成代码；同时确保生成代码具备可靠性保障。Claude共生成58个逻辑过程、508个测试用例、257个引理，总计11800行证明。我们手动检查了每一份生成文件：核对Prolog代码、执行测试、审查逻辑陈述，并用LPTP逐项验证证明。本文详细描述该实验过程，提供可复现的完整细节。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。