Research map / Reinforcement learning / Visual and representation RL
Learning Interestingness in Automated Mathematical Theory Formation
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.
Introduces Fermat, an RL environment for symbolic mathematical theory formation, and EvoAbstract, an LLM-driven evolutionary program synthesis method with abstraction learning that evolves programmatic interestingness measures.
Problem
Automating open-ended mathematical theory formation requires guiding search over a combinatorially vast space of definitions and conjectures, which depends on a notion of interestingness that prior systems hard-coded.
Approach
Model theory formation (definitions, conjectures, proofs via Z3) as an MDP, and learn interestingness measures as Python programs via LLM-driven evolution augmented with an abstraction library of reusable subroutines extracted from high-scoring programs.
Key results
- Best EvoAbstract/FunSearch measures discover on average 10.23, 22.41, and 11.34 ground-truth entities per rollout on succ_zero_eq, arithmetic_base, and ff_27 respectively.
- On arithmetic_base EvoAbstract reaches 23.98 ground-truth entities on average, slightly above FunSearch, but with higher variance.
- One-shot GPT-4o measures perform only slightly better than the random policy and are beaten by the comprehensibility HR measure.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add abstraction learning to evolutionary program synthesis (ablation) | FunSearch · arithmetic_base | ground-truth entities per episodic roll-out: 23.98 | Helped |
| Add abstraction learning to evolutionary program synthesis (ablation) | FunSearch · succ_zero_eq and ff_27 | ground-truth entities per episodic roll-out | Mixed |
| Use evolutionary program synthesis rather than static HR measures or one-shot GPT-4o measures | Fermat theory formation · succ_zero_eq, arithmetic_base, and ff_27 | ground-truth entities per episodic roll-out: 10.23, 22.41, 11.34 | Helped |
| Use one-shot GPT-4o-generated measures instead of evolutionary program synthesis | Fermat theory formation · three starting theories | ground-truth entities discovered | Hurt |
Surprising findings
- One-shot GPT-4o interestingness measures barely outperform a random policy, assigning high interest to initial but irrelevant entities.
- EvoAbstract's abstraction phase speeds early progress but leads to abstraction lock-in, plateauing below FunSearch on succ_zero_eq and ff_27.
Limitations
- Policy template exposes only a subset of the action space, limiting scalability to complex objects.
- Redundant representations and lack of equivalence checking make the knowledge graph grow intractably; primality becomes a bottleneck.
- Learned measures can still assign high interestingness to uninteresting entities such as equals, producing redundant statements.
Experimental setup
Datasets: ground truth set of 180 number theory concepts/theorems from an introductory number theory textbook 67 ground truth entities over F_27
Benchmarks: Fermat number theory ground-truth set (succ_zero_eq, arithmetic_base) Fermat F_27 ground-truth set (ff_27)
Metrics: average extrinsic reward (ground-truth entities discovered p
Baselines: Random policy HR measures (novelty, parsimony, productivity, applicability, comprehensibility) One-shot GPT-4o FunSearch
Builds on: FunSearch HR Z3
Closest papers by meaning
- Learning Formal Mathematics From Intrinsic Motivation (NeurIPS 2024 · similarity 0.86)
- A Matter of Interest: Understanding Interestingness Judgments of Math Problems in Humans and Language Models (NeurIPS 2026 · similarity 0.86)
- MathSmith: Towards Extremely Hard Mathematical Reasoning by Forging Synthetic Problems with a Reinforced Policy (AAAI 2026 · similarity 0.85)
- Unsupervised Discovery of Formulas for Mathematical Constants (NeurIPS 2024 · similarity 0.84)
- MARGE: Improving Math Reasoning with Guided Exploration (ICML 2025 · similarity 0.84)
- Subgoal-based Demonstration Learning for Formal Theorem Proving (ICML 2024 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.