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.

翻译：我们提出了一种面向Lean和Coq等环境的上下文学习智能体，用于形式化定理证明。当前针对该问题的最先进模型均需要在特定环境下的证明数据上进行微调。与此不同，我们的方法COPRA重复调用高容量、通用型大语言模型（GPT-4），使其在有状态的回溯搜索框架内提出战术应用建议。所提议的战术在底层证明环境中执行，执行反馈与搜索历史及外部数据库中检索到的引理等选定信息共同构成下一次模型查询的提示。我们在Lean平台的miniF2F基准测试和CompCert项目的Coq任务集上评估了COPRA的实现。实验表明，COPRA显著优于GPT-4的少样本调用方法。同时，该方法与基于微调的方法相比也表现优异，在pass@1指标上超越了Lean领域最先进的微调方法REPROVER。我们的代码和数据已开源至https://github.com/trishullab/copra。