摘要

我们提出了一种面向形式化定理证明的上下文学习智能体，适用于Lean和Coq等证明环境。当前该问题的最先进模型通常在特定环境的证明数据上进行微调。相比之下，我们的方法——COPRA（Contextual Proof Reasoning Agent）——通过反复调用高容量、通用型的大语言模型（GPT-4），在带有状态的回溯搜索框架中提出策略（tactic）应用。所提出的策略在底层证明环境中执行，其执行反馈被用于构建下一轮模型查询的提示（prompt），同时结合搜索历史中的关键信息以及从外部数据库检索到的定理（lemmas）。我们在Lean语言的miniF2F基准测试以及CompCert项目中的一组Coq任务上评估了COPRA的实现效果。实验结果表明，COPRA在这些基准测试中显著优于GPT-4的少样本（few-shot）调用。此外，其性能也优于基于微调的方法，在Lean任务上的pass@1指标上超越了当前最先进的微调模型ReProver。相关代码与数据已开源，可访问：https://github.com/trishullab/copra。