NeurIPS 论文提出 prover-conjecturer 自博弈定理证明理论框架
StanfordAILab · x · 2026-11-09
斯坦福 AI 实验室转发 Thomas Chen 与 Zhiyuan Li 的 NeurIPS 2026 海报论文《A Theoretical Framework for Self-Play Theorem Proving Algorithms》(arXiv:2606.01861)。
- 背景:Dong & Ma (2025) 提出双智能体自博弈训练——prover 负责证明定理,conjecturer 生成新定理作为课程,实证上让 LLM 在形式化定理证明中自我改进。
- 理论框架:将定理集合建模为图(节点为定理、边连接语义相近的定理),并引入刻画已训练 prover 保证与 conjecturer 对图结构访问能力的基本假设。
- 核心结论:若定理图连接性良好,基于可逆随机游走的 conjecturing 算法即可使已证明定理集合指数级增长。
- 改进算法:针对实证中 conjecturer 倾向生成人为复杂、非根本性定理的问题,提出定理训练分布的多样性度量,并通过计算相邻定理间的扩散相似度来局部最大化多样性,改进猜想生成。
作者将在悉尼 NeurIPS 2026 Poster Session 2(周二 5-8pm,Hall 1-4)展示。
「研究」频道最新
- 作者自曝失误：METR 报告公开版对 AI R&D 加速判定表述不清 — ShakeelHashim · 2026-11-09
- 哲学家挑战「大脑即计算机」：意识源于脑干而非皮层 — AnnaCiaunica · 2026-11-09
- 回应 Sutton 之争：软归纳偏置加上规模化反而更强 — irinarish · 2026-11-09
- CSProfKGD 开放 24 个交互式计算机视觉可视化合集 — CSProfKGD · 2026-11-09
- 每日可视化:Hough Transform 直线检测的投票几何 — CSProfKGD · 2026-11-09
- Brian Armstrong 倡议科研像开源:每个实验一个可复现的 repo — alishbaimran_ · 2026-11-09