Language agents, which use a large language model (LLM) capable of in-context learning to interact with an external environment, have recently emerged as a promising approach to control tasks. We present the first language-agent approach to formal theorem-proving. Our method, COPRA, uses a high-capacity, black-box LLM (GPT-4) as part of a policy for a stateful backtracking search. During the search, the policy can select proof tactics and retrieve lemmas and definitions from an external database. Each selected tactic is executed in the underlying proof framework, and the execution feedback is used to build the prompt for the next policy invocation. The search also tracks selected information from its history and uses it to reduce hallucinations and unnecessary LLM queries. 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 one-shot invocations of GPT-4, as well as state-of-the-art models fine-tuned on proof data, at finding correct proofs quickly. Our code and data are available at https://github.com/trishullab/copra.

翻译：语言智能体利用具备上下文学习能力的大语言模型（LLM）与外部环境交互，近来已成为控制任务领域一种颇具前景的方法。我们首次提出将语言智能体应用于形式定理证明。该方法名为COPRA，采用高容量黑盒LLM（GPT-4）作为带状态回溯搜索策略的组成部分。在搜索过程中，该策略可选取证明策略，并从外部数据库检索引理与定义。每个被选取的策略均在底层证明框架中执行，其执行反馈被用于构建下一次策略调用的提示。搜索过程中还会追踪历史中的选定信息，以减少模型幻觉和不必要的LLM查询。我们在面向Lean的miniF2F基准测试及Compcert项目中面向Coq的任务集上评估了COPRA的实现。实验表明，COPRA在快速找到正确证明方面显著优于单次调用的GPT-4以及基于证明数据微调的最先进模型。我们的代码与数据已开源至 https://github.com/trishullab/copra。