发生了什么？
INT 引入不等式定理证明基准，提供理论上可无限生成定理与证明的生成器、六类受控泛化设置，以及用于训练和评测证明 Agent 的快速序列与图接口。
为什么重要？
它较早为学习式定理证明中的核心问题提供了受控试验场：证明器能否超越训练阶段见过的定理形态和证明模式进行迁移。
重要性说明：INT 不再只用总体证明成功率评价定理证明器，而是借助定理生成器系统构造不同分布偏移，把受控泛化能力作为核心评测对象，并提供轻量级学习式证明研究环境。
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
如何理解这些标签？ →
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式证明 Agent 在生成的定理证明环境中训练与评测；基准本身是研究者设计的评测产物。
- 人类贡献
- 研究者设计不等式公理、定理生成器、六类泛化设置、交互接口、基线和评测协议。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- int-benchmark
- 机构
- university-of-toronto, vector-institute
- 数学问题
- inequality-theorem-proving
- 方法
- theorem-generation, benchmarking, systematic-generalization, graph-neural-networks, transformers
