Skip-tree 将结构感知的自监督训练引入形式数学推理

Skip-tree 不只遮蔽扁平 token 序列,而是从结构化数学表达式中移除一个子树并要求模型重建,从而促使表示学习利用形式数学的组合结构。

发生了什么?

作者提出面向形式数学表达式的 skip-tree 预训练任务,并报告该方法在类型推断、缺失假设预测和等式补全等任务上优于标准 skip-sequence 训练,同时还能生成并按可证明性与可用性评估 conjecture。

为什么重要?

该工作在后续大规模形式数学语言模型与证明导向预训练管线出现之前,较早展示了在形式数学语料上进行自监督预训练、学习可复用推理表示的技术路线。

重要性说明:Skip-tree training 是较早面向形式数学结构设计的自监督目标之一,展示了对数学表达式树进行语言模型预训练可以支持多类下游推理任务,并生成具有可证明性和可用性的 conjecture。

历史脉络

主要证据

证据与状态一览

重要性
H2 · 领域里程碑
验证状态
论文已发布
证据等级
E2 · 研究记录
AI 角色
仅计算支持
形式保障
无形式保障

如何理解这些标签? →

贡献与验证

数学新颖性
工具性进展
接口
形式化, 符号
AI 贡献
语言模型通过对形式表达式进行自监督重建来学习表示,并在数学推理与 conjecture generation 任务上接受评测。
人类贡献
研究者设计 skip-tree 目标、下游任务、形式数学语料处理和评测方法。
验证状态
论文已发布 · E2 · 研究记录 · 无形式保障
最后审阅
2026-09-15

技术细节

系统
skip-tree
机构
google-research
数学问题
—
方法
self-supervised-learning, skip-tree-training, formal-math-pretraining, conjecture-generation

全部来源与工件

验证历史

  • 2020-06-08 · 论文已发布 · E2 · 研究记录

    Chronicle 根据 arXiv 研究记录及其后 ICLR 2021 接收记录记载该方法与报告结果;本记录目前未收录可直接检查的公开实现产物。

更正

当前没有记录的更正。