主要证据
- Thor: Wielding Hammers to Integrate Language Models and Automated Theorem ProversS1 · 主要研究来源 · 论文 · 2022-05-22
Thor 将语言模型与自动定理证明器 Hammer 集成
该框架使用定理证明器 hammer 进行前提选择，其余证明决策由语言模型完成。
发生了什么？
Thor 将语言模型在 PISA 数据集上的成功率从 39% 提升到 57%，并以更少算力在 miniF2F 上达到当时领先方法水平。
为什么重要？
它体现了一条长期有效的设计原则：把符号工具用于可靠的结构化搜索，把学习模型用于需要生成与启发式判断的环节。
重要性说明：Thor 是较早明确采用神经符号分工的架构之一：语言模型把前提选择瓶颈交给传统自动定理证明器处理。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号, 混合
- AI 贡献
- 语言模型生成证明动作，自动定理证明器负责提供前提搜索支持。
- 人类贡献
- 研究者设计集成协议并在多个定理证明环境中进行评测。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-11
技术细节
- 系统
- thor
- 机构
- university-of-cambridge, microsoft-research
- 数学问题
- pisa, minif2f
- 方法
- hammer, premise-selection, language-model
全部来源与工件
- Thor: Wielding Hammers to Integrate Language Models and Automated Theorem ProversS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
验证历史
- 2022-05-22 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
更正
当前没有记录的更正。