Primary evidence
- Reinforcement Learning of Theorem ProvingS1 · Primary research · Paper · 2018-05-19
- Reinforcement Learning of Theorem Proving — NeurIPS 2018S1 · Primary research · Paper
Reinforcement learning guides large-scale automated theorem-proving search
The system repeatedly performs proof-search simulations, turns successful and failed attempts into learning signals, and retrains guidance used in subsequent searches.
What happened?
Cezary Kaliszyk, Josef Urban, Henryk Michalewski and Mirek Olšák introduced a connection-style theorem prover whose Monte Carlo simulations were guided by reinforcement learning from previous proof attempts. The paper reported that its strongest trained configuration solved more than 40% more previously unseen problems than a baseline prover under the same inference budget.
The system repeatedly performs proof-search simulations, turns successful and failed attempts into learning signals, and retrains guidance used in subsequent searches. The approach was evaluated over a large formal-mathematics problem corpus, emphasizing learned search control rather than theorem-specific handwritten heuristics.
Why it matters
The work showed that theorem proving could be organized as an iterative learning-and-search loop at substantial corpus scale. This helped connect automated theorem proving with modern reinforcement-learning methodology and supplied historical context for later self-improving and interactive proof-search agents.
Significance rationale: Reinforcement Learning of Theorem Proving established a prominent large-scale route in which an automated prover improves search guidance from its own previous proof attempts rather than relying primarily on hand-built domain heuristics. It helped make reinforcement learning over broad formal-theorem corpora a concrete AI4Math research program before later proof-assistant-native RL systems.
Historical context
Earlier developments
Later developments
—
Related milestones
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Autonomous primary role
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- The learned policy guided proof-search simulations and was updated from prior proof attempts; the automated prover carried out the search and produced successful formal derivations without human step-by-step tactic selection.
- Human contribution
- Researchers designed the connection-style prover, reinforcement-learning loop, search features, training/evaluation corpus and experimental protocol.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- rl-theorem-prover
- Organizations
- university-of-innsbruck
- Problems
- automated-theorem-proving
- Methods
- reinforcement-learning, monte-carlo-search, connection-tableaux, proof-search
Sources & artifacts
- Reinforcement Learning of Theorem ProvingS1 · Primary research · Paper · accessed 2026-09-15
- Reinforcement Learning of Theorem Proving — NeurIPS 2018S1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 2018-05-19 · Paper released · E2 · Research record
The arXiv and NeurIPS research records establish the reinforcement-learning proof-search algorithm and the reported large-corpus evaluation. The Chronicle does not record a directly inspectable proof artifact or independent replay for this event, so formal assurance remains `none`.
Corrections
No corrections recorded.