主要证据
- IsarStep: a Benchmark for High-level Mathematical ReasoningS1 · 主要研究来源 · 论文 · 2020-06-13
- IsarStep: a Benchmark for High-level Mathematical Reasoning — ICLR 2021S1 · 主要研究来源 · 论文
- IsarStep code, dataset and HAT resourcesS1 · 主要研究来源 · 代码仓库
IsarStep 以人工 Isabelle 证明建立高层数学推理基准
IsarStep 将声明式 Isar 证明转换为序列到序列样本，并移除其中的中间命题。任务要求模型重建连接前后证明状态的语义桥梁；作者评测了 Transformer 类基线，并设计面向长证明上下文的分层架构。
发生了什么？
Wenda Li、Lei Yu、Yuhuai Wu 与 Lawrence C. Paulson 提出 IsarStep：一个从 Isabelle Archive of Formal Proofs 中抽取的 benchmark，要求模型根据周围证明上下文预测缺失的中间命题，覆盖本科与研究级数学及计算机科学形式化内容。
为什么重要？
该 benchmark 将部分学习式定理证明研究从低层动作预测推进到真实证明语料上的可读中间推理。它与同期形式数学预训练研究一起，为后来的 LLM 时代之前从成熟证明助手数学库学习可复用数学表示与证明步骤提供了重要试验场。
重要性说明：IsarStep 从人工编写的 Isabelle 证明中构建大规模非合成 benchmark，并把评测重点放在恢复缺失的中间命题，而不只是预测低层 tactic。它推动“在真实形式数学中生成高层证明步骤”成为独立学习问题，早于后来语言模型定理证明系统对类似路线的扩展。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 神经序列模型被训练和评测，用于根据证明上下文预测缺失的形式命题；底层 Isabelle 证明、benchmark 抽取和评测协议由人类编写或研究者设计。
- 人类贡献
- 研究者抽取并处理 Isabelle 证明语料、定义缺失命题任务与数据划分、设计序列到序列及分层 Transformer 基线，并在留出证明上评估模型泛化能力。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- isarstep, isabelle
- 机构
- university-of-cambridge
- 数学问题
- high-level-mathematical-reasoning, missing-proposition-generation
- 方法
- sequence-to-sequence-learning, hierarchical-transformer, proof-corpus-mining, benchmarking
全部来源与工件
- IsarStep: a Benchmark for High-level Mathematical ReasoningS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- IsarStep: a Benchmark for High-level Mathematical Reasoning — ICLR 2021S1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- IsarStep code, dataset and HAT resourcesS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-15
验证历史
- 2020-06-13 · 论文已发布 · E2 · 研究记录
arXiv 研究记录确认了 IsarStep 任务、源自 Isabelle 的数据集以及论文报告的神经序列模型实验。
- 2026-09-15 · 论文已发布 · E3 · 可检查工件
公开 IsarStep 仓库提供代码，并链接已发布的数据集、分层 Transformer 实现与测试集。E3 表示 artifact 可直接检查，并不代表论文报告的全部结果已获得独立复现。
更正
当前没有记录的更正。