主要证据
- Proof Artifact Co-training for Theorem Proving with Language ModelsS1 · 主要研究来源 · 论文 · 2021-02-11
- PACT LeanStep proof-artifact extraction codeS1 · 主要研究来源 · 代码仓库
PACT 利用证明产物扩展语言模型定理证明
该方法从内核级证明项中提取自监督目标，并与 tactic prediction 一起训练。
发生了什么？
PACT 使用 Lean 证明产物对 Transformer 定理证明器进行协同训练，将留出定理的证明成功率从 32% 提升至 48%。
为什么重要？
它说明形式数学库中可学习的信息远多于表层的下一步 tactic 标签，为后续大规模形式证明训练提供了基础。
重要性说明：PACT 将证明项衍生的自监督数据用于缓解神经定理证明中的数据稀缺问题，形成了重要的训练路线。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 实质性支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 语言模型利用 tactic 标签和证明产物目标共同学习的表示来预测证明步骤。
- 人类贡献
- 研究者设计证明产物训练目标、接入 Lean 并构建评测设置。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- pact, lean
- 机构
- openai
- 数学问题
- —
- 方法
- proof-artifact-cotraining, transformer, tactic-prediction
全部来源与工件
- Proof Artifact Co-training for Theorem Proving with Language ModelsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- PACT LeanStep proof-artifact extraction codeS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2021-02-11 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。