# Learning Conjecturing from Scratch

arXiv: https://arxiv.org/abs/2503.01389 · HTML: https://mlsanity.com/paper/2503.01389/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 43 references that are in the map.
- First posted on arXiv 3 Mar 2025.

## Builds on (most cited first, 16 of 16)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Attention-Based Models for Speech Recognition](https://mlsanity.com/paper/1506.07503/) (2015)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [Can Neural Networks Learn Symbolic Rewriting?](https://mlsanity.com/paper/1911.04873/) (2019)
- [Stateful Premise Selection by Recurrent Neural Networks](https://mlsanity.com/paper/2004.08212/) (2020)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [Alien Coding](https://mlsanity.com/paper/2301.11479/) (2023)
- [Learning Program Synthesis for Integer Sequences from Scratch](https://mlsanity.com/paper/2202.11908/) (2022)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Template-Based Conjecturing for Automated Induction in Isabelle/HOL](https://mlsanity.com/paper/2212.11151/) (2022)
- [Faster Smarter Induction in Isabelle/HOL](https://mlsanity.com/paper/2009.09215/) (2020)
- [A Mathematical Benchmark for Inductive Theorem Provers](https://mlsanity.com/paper/2304.02986/) (2023)

## Built on by (most cited first, 3 of 3)

- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [IntSeqBERT: Learning Arithmetic Structure in OEIS via Modulo-Spectrum Embeddings](https://mlsanity.com/paper/2603.05556/) (2026)

## Abstract (arXiv)

We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP systems because they require a combination of inductive and arithmetical reasoning. Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the correspondence between the problems solved so far and the induction predicates useful for them, (ii) using the trained neural system to generate many new induction predicates for the problems, (iii) fast runs of the z3 prover attempting to prove the problems using the generated predicates, (iv) using heuristics such as predicate size and solution speed on the proved problems to choose the best predicates for the next iteration of training. The algorithm discovers on its own many interesting induction predicates, ultimately solving 5565 problems, compared to 2265 problems solved by CVC5, Vampire or Z3 in 60 seconds.