主要证据
- miniCTX: Neural Theorem Proving with (Long-)ContextsS1 · 主要研究来源 · 论文 · 2024-08-05
- miniCTX evaluation repositoryS1 · 主要研究来源 · 代码仓库
miniCTX 测试定理证明器使用长篇、未见项目上下文的能力
该基准从真实 Lean 项目和教材中抽取定理，并提供提取新项目上下文的工具。
发生了什么？
miniCTX 引入带有可达数万 token 仓库上下文的 Lean 定理证明任务，并显示利用上下文的方法明显优于只看 proof state 的基线。
为什么重要？
它更接近实际证明 Agent 在大型形式化代码库中工作的真实条件。
重要性说明：miniCTX 把评测推进到仓库级定理证明：所需定义与引理存在于长篇、训练时未见的上下文中。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 模型在证明过程中必须从长篇项目上下文中检索并利用相关定义与引理。
- 人类贡献
- 研究者构建基准与 ntp-toolkit，用于提取上下文感知的定理证明数据。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- minictx, ntp-toolkit, lean
- 机构
- carnegie-mellon-university
- 数学问题
- repository-level-theorem-proving
- 方法
- long-context, retrieval, benchmarking
全部来源与工件
- miniCTX: Neural Theorem Proving with (Long-)ContextsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- miniCTX evaluation repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2024-08-05 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。