主要证据
- Learning to Prove Theorems by Learning to Generate TheoremsS1 · 主要研究来源 · 论文 · 2020-02-17
- Learning to Prove Theorems by Learning to Generate Theorems — NeurIPS 2020S1 · 主要研究来源 · 论文
- MetaGen code and reproduction repositoryS1 · 主要研究来源 · 代码仓库
MetaGen 学习生成合成定理与证明，用于训练定理证明器
该系统从既有形式数学中学习，生成额外的定理—证明对，再把合成语料反馈到证明器训练中，而不是仅依赖稀缺的人工证明轨迹。
发生了什么？
MetaGen 训练神经生成器合成带有证明的 Metamath 定理，并用这些生成样本改进神经定理证明器；作者报告其在所用 Metamath 评测上取得当时领先的自动定理证明表现。
为什么重要？
它较早确立了面向形式数学的神经数据生成路线，并与后来利用证明产物、合成形式化和自训练的数据管线形成历史上的连续技术脉络。
重要性说明：MetaGen 将学习式生成合成形式定理与证明发展为神经定理证明中的实用数据增强路线，用于缓解人工形式证明数据稀缺，并提升 Metamath 真实任务上的证明器表现。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 实质性支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式生成器产生合成形式定理—证明对，学习式证明器再利用扩充后的语料训练并搜索目标定理的证明。
- 人类贡献
- 研究者设计生成器—证明器训练循环、形式数据管线与评测；Metamath 库提供人工编写的形式语料和证明检查器。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- metagen, metamath
- 机构
- princeton-university
- 数学问题
- —
- 方法
- synthetic-theorem-generation, synthetic-proof-generation, data-augmentation, neural-theorem-proving
全部来源与工件
- Learning to Prove Theorems by Learning to Generate TheoremsS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Learning to Prove Theorems by Learning to Generate Theorems — NeurIPS 2020S1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- MetaGen code and reproduction repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2020-02-17 · 论文已发布 · E2 · 研究记录
arXiv 研究记录公开了合成定理与证明生成方法及其报告的 Metamath 定理证明结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
Chronicle 补入 NeurIPS 2020 同行评议记录以及作者公开的 MetaGen 仓库。E3 表示存在可检查研究产物，并不等同于对所报告性能主张的独立验证。
更正
当前没有记录的更正。