主要证据
- Reinforcement Learning of Theorem ProvingS1 · 主要研究来源 · 论文 · 2018-05-19
- Reinforcement Learning of Theorem Proving — NeurIPS 2018S1 · 主要研究来源 · 论文
强化学习用于引导大规模自动定理证明搜索
该系统反复执行证明搜索模拟，把成功与失败的尝试转化为学习信号，并重新训练后续搜索所使用的引导策略。方法在大型形式数学问题语料上进行评测，重点是学习式搜索控制，而非针对具体定理手写启发式规则。
发生了什么？
Cezary Kaliszyk、Josef Urban、Henryk Michalewski 与 Mirek Olšák 提出一种 connection-style 定理证明器，使用从此前证明尝试中学习的强化学习策略引导蒙特卡洛模拟。论文报告称，在相同推理预算下，最强训练配置在此前未见问题上比基线证明器多解决超过 40% 的问题。
为什么重要？
该工作展示了定理证明可以在相当规模的语料上组织为“学习—搜索—再学习”的迭代循环，推动自动定理证明与现代强化学习方法结合，并为后来的自我改进式和交互式证明搜索智能体提供历史前序。
重要性说明：Reinforcement Learning of Theorem Proving 建立了一条具有代表性的大规模路线：自动证明器从此前的证明尝试中学习搜索引导，而不是主要依赖人工编写的领域启发式。它在后续证明助手原生强化学习系统出现之前，推动面向大规模形式定理语料的强化学习成为具体的 AI4Math 研究方向。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 自主主导
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式策略引导证明搜索模拟，并根据此前证明尝试持续更新；自动证明器执行搜索并产生成功的形式推导，不需要人类逐步选择证明动作。
- 人类贡献
- 研究者设计 connection-style 证明器、强化学习循环、搜索特征、训练与评测语料以及实验协议。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- rl-theorem-prover
- 机构
- university-of-innsbruck
- 数学问题
- automated-theorem-proving
- 方法
- reinforcement-learning, monte-carlo-search, connection-tableaux, proof-search
全部来源与工件
- Reinforcement Learning of Theorem ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- Reinforcement Learning of Theorem Proving — NeurIPS 2018S1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2018-05-19 · 论文已发布 · E2 · 研究记录
arXiv 与 NeurIPS 研究记录确认了强化学习证明搜索算法及论文报告的大规模语料评测。Chronicle 当前未记录可直接检查的证明 artifact 或独立 replay，因此 formal assurance 保持为 `none`。
更正
当前没有记录的更正。