论文提出定理「有趣度」指标,27B 模型超越前沿模型预测证明难度
Pascallisch · x · 2026-09-26
NYU Julia Kempe 团队发布论文《Learning to Discover Interesting Mathematics》,探讨 AI 自动定理证明如何真正推动数学前沿——目标不是产出无穷堆砌的真定理,而是让 AI 发现数学并把每个发现建为下一个发现的基础。核心贡献:
- 将定理的内在有趣度定义为「证明长度/陈述长度」之比,并证明该指标与定理下游效用的外在度量强相关;
- 以「给定前提条件下证明的难度」为计算这些指标的关键原语,训练出一个 27B 模型,其预测证明难度的准确率超过前沿通用大模型;
- 按该指标优化后,模型产出的定理更有趣,且与 Mathlib 形式库的大量或完全重叠率从 91.9% 降至 30.6%,表明生成了更多分布外的新数学;
- 系统可生成候选定理、挑选最有趣者,并迭代扩展一个自我增长、机器可验证的数学库,为排序猜想、指导证明搜索提供可量化的实用信号。
所属事件:研究提出定理「有趣度」指标，LLM 自主发现有趣数学(2 条相关)→
「漫话AGI」频道最新
- AI 生成内容很吓人？我们早活在人类 slop 时代了 — enggirlfriend · 2026-09-26
- 评论：强制企业移除安全限制的 AI 政策，与「独裁 AI」威胁模型何异？ — menhguin · 2026-09-26
- Reddit 热议：前沿模型研发本质是「生成一晚再筛选」的 SD 流程 — wreck_of_u · 2026-09-26
- MIT 劳动经济学家 Stansbury 用 Messy Jobs 框架教未来职场 — soumitrashukla9 · 2026-09-26
- 剑桥 AI 安全教授反驳:十年前沿经验者与外行有本质区别 — DavidSKrueger · 2026-09-26
- AI 圈热议:做游戏开发或是当下最有价值的事之一 — repligate · 2026-09-26