Primary evidence
- Mathematical Reasoning via Self-supervised Skip-tree TrainingS1 · Primary research · Paper · 2020-06-08
- Mathematical Reasoning via Self-supervised Skip-tree Training — ICLR 2021S1 · Primary research · Paper
Skip-tree training brings structure-aware self-supervision to formal mathematical reasoning
Rather than masking only a flat token span, skip-tree training removes a subtree from a structured mathematical expression and trains a model to reconstruct it, encouraging representations that reflect the compositional structure of formal mathematics.
What happened?
The authors introduced the skip-tree pretraining task for formal mathematical expressions and reported that skip-tree-trained models outperformed standard skip-sequence training on tasks including type inference, missing-assumption prediction and equality completion, while also producing conjectures evaluated for provability and usefulness.
Why it matters
The work helped establish self-supervised pretraining on formal mathematical corpora as a distinct route to reusable reasoning representations before later large-scale formal-math language models and proof-oriented pretraining pipelines.
Significance rationale: Skip-tree training was an early structure-aware self-supervised objective for formal mathematics, showing that language-model pretraining over mathematical expression trees could support several downstream reasoning tasks and useful conjecture generation.
Historical context
Earlier developments
—
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Computation only
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Language models learn representations from self-supervised reconstruction of formal expressions and are evaluated on mathematical reasoning and conjecture-generation tasks.
- Human contribution
- Researchers designed the skip-tree objective, downstream tasks, formal-mathematics corpus processing and evaluation methodology.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- skip-tree
- Organizations
- google-research
- Problems
- —
- Methods
- self-supervised-learning, skip-tree-training, formal-math-pretraining, conjecture-generation
Sources & artifacts
- Mathematical Reasoning via Self-supervised Skip-tree TrainingS1 · Primary research · Paper · accessed 2026-09-11
- Mathematical Reasoning via Self-supervised Skip-tree Training — ICLR 2021S1 · Primary research · Paper · accessed 2026-09-11
- Google at ICLR 2021S2 · Official institutional · Official announcement · accessed 2026-09-11
Verification history
- 2020-06-08 · Paper released · E2 · Research record
The Chronicle records the method and reported results from the arXiv research record, later accepted at ICLR 2021; no directly inspectable public implementation artifact is recorded here.
Corrections
No corrections recorded.