基于推理的LLM自动定理证明

自动化定理证明是形式化方法的基础，最近的趋势是将大语言模型（LLM）和证明助手集成起来形成有效的证明代理。虽然现有的证明智能体显示出有希望的性能，但它们在高层规划和自我批评中没有充分利用现代 LLM 的推理能力。我们认为，证明Agent不仅应该制定策略，还应该对证明计划进行战略性推理，并批判性地评估自己的建议。本文介绍了 ReCent-Prover，这是一种以推理为中心、基于 LLM 的 Rocq 证明代理，它解决了当前系统中的两个关键限制。首先，我们通过反射进行验证，使 LLM 能够在反射发现潜在错误时仔细检查其生成的策略并综合失败摘要，从而更早地过滤掉可能被误用的策略。其次，我们提出带有规划的检索，它以 LLM 生成的证明计划而不是子目标相似性为检索条件，检索与预期证明策略一致的引理和证明。这两种技术都会增加 LLM 的调用次数。然而，当在 CoqStoq 基准上进行评估时，即使在相同的 LLM 调用预算下，ReCent-Prover 的已证明定理数量比之前最先进的技术也实现了 22.58% 的相对改进，这表明我们以推理为中心的设计显着增强了自动化定理证明能力。