主要证据
- An In-Context Learning Agent for Formal Theorem-ProvingS1 · 主要研究来源 · 论文 · 2023-10-06
- COPRA repositoryS1 · 主要研究来源 · 代码仓库
COPRA 将通用大模型转化为有状态的形式证明搜索 Agent
Agent 在每一步提出战术、在证明助手中执行，将错误或新的目标写回下一轮提示，并维护搜索历史以支持回溯。该架构展示了无需针对任务专门微调，也能把前沿通用模型封装为证明导向 Agent。
发生了什么？
COPRA 将 GPT-4 置于带证明环境反馈、检索和回溯机制的有状态循环中；论文报告其明显优于 few-shot GPT-4，并在 Lean miniF2F 上与微调证明器竞争，同时还能处理 Coq 任务。
为什么重要？
COPRA 把证明助手变成 LLM Agent 的交互环境，提前体现了后来形式数学 Agent 中核心的“生成—执行—观察—修订”循环。
重要性说明：COPRA 是较早明确采用 Agent 结构的定理证明系统之一：通用大模型反复在 Lean 或 Coq 中行动，读取证明助手反馈并维护可回溯的搜索状态，而不是一次性生成答案。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号, 混合
- AI 贡献
- GPT-4 提出战术并推进证明搜索，Lean 或 Coq 对每个被接受的证明动作进行机械检查。
- 人类贡献
- 研究者设计 Agent 状态、检索、回溯与提示协议，选择基准并构建与证明助手之间的接口。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- copra, gpt-4, lean, coq
- 机构
- university-of-texas-at-austin
- 数学问题
- minif2f, compcert
- 方法
- agentic-proof-search, in-context-learning, backtracking, retrieval, proof-assistant-feedback
全部来源与工件
- An In-Context Learning Agent for Formal Theorem-ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- COPRA repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-10
验证历史
- 2023-10-06 · 论文已发布 · E2 · 研究记录
作者公开论文，说明 Agent 设计以及 Lean 与 Coq 评测。
- 2023-10-06 · 论文已发布 · E3 · 可检查工件
代码与实验基础设施通过公开 COPRA 仓库提供。
更正
当前没有记录的更正。