An In-Context Learning Agent for Formal Theorem-Proving

📄 arXiv: 2310.04353v5 📥 PDF

作者: Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, Swarat Chaudhuri

分类: cs.LG, cs.AI, cs.LO, cs.PL

发布日期: 2023-10-06 (更新: 2024-08-08)

🔗 代码/项目: GITHUB

💡 一句话要点

提出COPRA以解决形式定理证明中的学习效率问题

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

关键词: 形式定理证明 上下文学习 大型语言模型 状态回溯搜索 自动定理证明 程序验证 机器学习

📋 核心要点

  1. 现有方法在形式定理证明中依赖于环境特定的微调数据，限制了其通用性和效率。
  2. COPRA通过高容量的通用大型语言模型在状态回溯搜索中动态生成策略应用，提升了学习效率。
  3. 在miniF2F基准和CompCert项目的任务中，COPRA显著优于少量调用和微调方法，表现出更高的准确性。

📝 摘要（中文）

我们提出了一种用于形式定理证明的上下文学习代理，适用于Lean和Coq等环境。当前的最先进模型通常在特定环境的证明数据上进行微调，而我们的方案COPRA则通过高容量的通用大型语言模型（如GPT-4）在状态回溯搜索中反复请求策略应用。提出的策略在基础证明环境中执行，执行反馈用于构建下一次模型查询的提示，同时结合搜索历史和从外部数据库检索的引理信息。我们在miniF2F基准和CompCert项目的Coq任务上评估了COPRA的实现，结果显示其显著优于GPT-4的少量调用，并在pass@1指标上超越了Lean领域的微调方法ReProver。

🔬 方法详解

问题定义：本论文旨在解决形式定理证明中的学习效率问题，现有方法依赖于特定环境的微调数据，导致通用性不足和效率低下。

核心思路：COPRA的核心思路是利用高容量的通用大型语言模型（如GPT-4）在状态回溯搜索中动态生成策略应用，通过反馈循环不断优化模型的输入提示。

技术框架：COPRA的整体架构包括状态回溯搜索模块、策略生成模块和反馈整合模块。首先，模型在当前状态下生成策略，然后执行该策略并获取反馈，最后将反馈与历史信息结合，构建下一次查询的提示。

关键创新：COPRA的最大创新在于其不依赖于环境特定的微调数据，而是通过动态生成和反馈循环来提升学习效率，这与传统方法形成鲜明对比。

关键设计：在设计中，COPRA使用了高容量的GPT-4模型，并结合了外部数据库中的引理信息，确保生成的策略更加准确和有效。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在miniF2F基准和CompCert项目的任务中，COPRA的表现显著优于少量调用的GPT-4，并在pass@1指标上超越了当前最先进的微调方法ReProver，显示出更高的准确性和效率。

🎯 应用场景

该研究的潜在应用领域包括自动定理证明、形式验证和程序分析等。通过提高形式定理证明的效率，COPRA能够在软件验证和安全性分析等实际场景中发挥重要作用，推动相关领域的研究与应用发展。

📄 摘要（原文）

We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-specific proof data. By contrast, our approach, called COPRA, repeatedly asks a high-capacity, general-purpose large language model (GPT-4) to propose tactic applications from within a stateful backtracking search. Proposed tactics are executed in the underlying proof environment. Feedback from the execution is used to build the prompt for the next model query, along with selected information from the search history and lemmas retrieved from an external database. We evaluate our implementation of COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the CompCert project. On these benchmarks, COPRA significantly outperforms few-shot invocations of GPT-4. It also compares favorably against finetuning-based approaches, outperforming ReProver, a state-of-the-art finetuned approach for Lean, in terms of the pass@1 metric. Our code and data are available at https://github.com/trishullab/copra.