Research map / Multi-agent systems and games / Human-AI and goal-conditioned

Learning Formal Mathematics From Intrinsic Motivation

NeurIPS 2024 · Multi-agent systems and games › Human-AI and goal-conditioned · approach: Imitation and skill learning · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Minimo jointly trains a randomly initialized small transformer to conjecture valid propositions via constrained type-directed decoding and to prove them with MCTS in the Peano environment, using hindsight relabeling to self-improve from only the axioms.

Problem

Training formal mathematical reasoning agents without human-written theorems or problems, starting only from the axioms of a domain in dependent type theory, where successful proofs are sparse and conjectures must be both valid and provable-but-hard.

Approach

Sample well-formed conjectures by construction using a completion engine (Synchromesh-style constrained semantic decoding with type-directed synthesis) from a randomly initialized LM, use the same LM as policy and value for MCTS in Peano, and apply hindsight relabeling to proof search trees to extract both prover and conjecturer training data from failed searches.

Key results

• In Groups, average proof length on generated conjectures rose from 2.67 steps in iteration 1 to 5 steps by iteration 4; longest proofs grew from 4 to 9 steps.
• Agents trained with hindsight relabeling keep producing harder provable conjectures, whereas without hindsight training collapses toward easy conjectures (e.g., 0 = 0).
• Success on human-written theorems (Kleene's book and Natural Number Game) increases across training iterations, with four propositional logic theorems proved only after the final iteration.

Measured effects reported in the paper

Surprising findings

• Without hindsight relabeling, the proven-conjecture ratio in arithmetic sharply increases because the conjecturer generates mostly trivial statements such as 0 = 0.
• Generating false conjectures can still be beneficial, since hard conjectures that fail to be proven still yield useful training data for the prover.

Limitations

• The fixed library means the agent cannot accumulate lemmas, so cut-free proofs grow exponentially and harder conjectures are mainly longer statements.
• Action enumeration in Peano becomes slow with large libraries; no premise selection is used.
• Evaluation is small-scale, limited to three axiomatic domains and 10 NNG plus 35 textbook theorems.

Experimental setup

Datasets: self-generated conjectures in Peano (propositional logic, arithmetic, groups axioms) Kleene Introduction to Metamathematics Theorem 41 (35 statements, evaluation) Lean Natural Number Game levels (10 levels, evaluation)

Benchmarks: Kleene Theorem 41 propositional logic statements Lean Natural Number Game levels (10)

Metrics: proof log-likelihood as difficulty success rate within 2000 MCTS expansions fraction of proven conjectures per batch average proof length

Baselines: initial random policy (policy 0) agents trained without hindsight relabeling

Builds on: Synchromesh constrained semantic decoding Hindsight Experience Replay AlphaZero Peano

Closest papers by meaning

• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics (ICML 2026 · similarity 0.87)
• ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.87)
• LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.86)
• Learning Interestingness in Automated Mathematical Theory Formation (NeurIPS 2025 · similarity 0.86)
• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.86)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving (ICML 2025 · similarity 0.86)