Learning Interestingness in Automated Mathematical Theory Formation

AI summary

Overview

Research area: Artificial intelligence for mathematics — specifically reinforcement learning environments and program synthesis for automated mathematical theory formation, combining symbolic production rules, an SMT-based theorem prover, and LLM-driven evolutionary search.

Technical level: Intermediate to Advanced. Readers need comfort with Markov decision processes, intrinsic vs. extrinsic reward, evolutionary program synthesis, and basic number theory / finite field terminology. The paper is written so that the high-level narrative is accessible, but the MDP formalism and production rule definitions are technical.

Scope (one sentence): The paper introduces Fermat, a reinforcement learning environment for open-ended mathematical theory formation, and EvoAbstract, an LLM-based evolutionary algorithm with abstraction learning that synthesizes interpretable "interestingness" measures to guide concept discovery in elementary number theory and finite fields.

What This Paper Is About

Most AI-for-mathematics systems solve predefined problems, while human mathematicians build theories through an open-ended cycle of defining concepts, conjecturing properties, and proving or refuting them. The bottleneck in that open-ended cycle is search guidance: the space of possible definitions and conjectures is combinatorially vast, and most paths lead to trivial mathematics, so human mathematicians rely on an intuitive sense of "interestingness." This paper builds a formal RL environment for the full theory-formation loop and then treats the discovery of an interestingness heuristic as a learnable problem, searching for it as an interpretable Python program.

Key Contributions

1. Fermat, an RL environment for theory formation. The paper formalizes mathematical theory formation as a Markov Decision Process (𝒮, 𝒜, 𝒯, ℛ). States are directed knowledge graphs of definitions, conjectures, and theorems; actions are symbolic production rules for producing definitions, producing conjectures, and proving or disproving; the environment generalizes the earlier symbolic system HR. Fermat is implemented in Python and released at github.com/trishullab/Fermat.

2. Interestingness framed as intrinsic reward. The paper defines an interestingness measure as a function ℐ(m, S) scoring a mathematical entity m in the context of the current theory S, and connects it to RL by setting the intrinsic reward of a transition equal to the score of the newly generated entity. The learning objective is to find the measure ℐ* that maximizes expected cumulative extrinsic reward, i.e., discovery of ground-truth entities.

3. EvoAbstract, an LLM-driven evolutionary program synthesis algorithm with abstraction learning. EvoAbstract extends the FunSearch approach with a periodic abstraction phase in which an LLM analyzes high-scoring programs, extracts reusable subroutines, and stores them in a per-island abstraction library that conditions later mutations. The design goal is interpretable, modular interestingness programs.

4. Empirical evaluation in two mathematical domains. The authors curate ground-truth benchmarks in elementary number theory and over 𝔽₂₇, compare EvoAbstract and FunSearch against random, hand-coded HR measures, and one-shot GPT-4o sampling, and analyze both the learned measures and the theories they generate.

Main Findings

• Evolutionary search dominates static baselines. The best measure discovered by FunSearch averaged (10.23, 22.41, 11.34) ground-truth entities per episodic rollout on (succ_zero_eq, arithmetic_base, ff_27), versus 4.68 (2.25), 4.44 (2.23), and 2.33 (1.20) for the random policy.

• EvoAbstract helps most on arithmetic_base but plateaus elsewhere. EvoAbstract averaged 23.98 (10.50) on arithmetic_base, slightly above FunSearch's 22.41 (2.68) but with higher variance. On succ_zero_eq it scored 9.62 (2.97) versus 10.23 (1.70) for FunSearch, and on ff_27 it scored 9.82 (4.83) versus 11.34 (4.09). On ff_27 and succ_zero_eq, EvoAbstract finds better solutions quicker but its progress slows, an effect the authors attribute to abstraction "lock-in."

• Random and novelty measures perform worst. Random and novelty exhibit roughly equivalent scores. Parsimony's inefficacy likely stems from limited discriminative power, since most generated definitions involve few inputs.

• Comprehensibility is the strongest hand-coded measure. It scored 8.23 (2.84), 8.55 (3.22), and 5.38 (1.89) across the three settings. The paper notes it alone cannot scale to more complex entities due to combinatorial expansion of the action space.

• One-shot GPT-4o underperforms the hand-coded measures. GPT-4o scored 5.26 (1.11), 6.46 (1.98), and 2.36 (0.40), only slightly better than the random baseline overall, and was outperformed by the comprehensibility measure alone. The paper attributes this to GPT-4o measures rewarding construction depth and connectivity, which assigns disproportionately high interestingness to initial but irrelevant entities, causing a cascading drift away from the ground-truth set.

• A larger starting theory helps. Starting from arithmetic_base generally leads to greater rewards than starting from succ_zero_eq or ff_27.

• Learned measures rediscover and refine HR-style features. On succ_zero_eq, the best EvoAbstract program uses numerous abstractions identified in earlier phases. It generates applicability-like measures (e.g., compute_example_balance), refines prior abstractions (e.g., calculate_uniqueness_score_v2), finds measures distinct from HR baselines (e.g., calculate_rule_diversity_score), and generalizes construction patterns (e.g., adjust_score_by_node_type). The FunSearch best program uses similar components but fewer of them, integrated more directly and with a less modular structure.

• What the generated theories contain. From succ_zero_eq, the agent develops addition, multiplication, divisibility, and the tau function, and makes progress toward conjecturing the reflexivity of divisibility. From arithmetic_base, it discovers powers and primality along with more complex function compositions. In 𝔽₂₇, it discovers concepts such as ff_sum_three_times but cannot find the conjecture that char(𝔽₂₇) = 3, which requires further rule applications.

• Failure modes. The best-performing measures can still be suboptimal, assigning overly high interestingness to equals and producing redundant or vacuous statements. The agent had difficulty discovering many ground-truth conjectures, which the authors suggest is due to the limited number of correct ways to specify a conjecture compared to a definition.

• Reported limitations. The policy template exposes only a subset of the complete action space at any step; "bottleneck" entities such as primality must be discovered to continue, but once primality is discovered the knowledge graph becomes prohibitively large and obstructs valuable actions involving it; and Fermat does not exploit symmetries in entities, leading to representational redundancy. Exhaustive equivalence checking between definitions was found computationally intractable with Z3 as theories grow.

Methodology in Plain English

The authors start by writing down mathematical theory building as a game an agent can play. The agent's "board" is a graph of the definitions, conjectures, and theorems discovered so far. Its legal moves are a fixed set of production rules inherited from the HR system: nine rules for making new definitions (including Exists, Specialize, Compose, MapIterate, ForAll, Match, Negate, Size, and Constant) and four rules for making conjectures (Implication, Equivalence, Nonexistence, and Exclusivity), plus actions to prove or disprove a conjecture. Each entity carries three things: a symbolic definition in Fermat's domain-specific language, an executable Python interpretation that returns True, False, or Unknown, and cached positive and negative examples. Conjectures are compiled to SMT-LIB and handed to the Z3 theorem prover in the number theory setting; finite field reasoning uses a custom Python prover.

Because the extrinsic reward — one point for discovering a concept from the curated ground-truth list — is sparse, the agent needs a heuristic to decide what is worth pursuing. That heuristic, the interestingness measure, is treated as the thing being learned. The authors search over Python programs, using an evolutionary loop: an LLM proposes mutated candidate programs conditioned on a template and high-performing parents, and candidates are scored by actually running them as policies inside Fermat for multiple rollouts. Diversity is maintained with an island model.

EvoAbstract adds a second LLM role. Every few iterations, a separate LLM examines the best programs on each island, identifies reusable subroutines, and proposes them as new functions. These are filtered for validity and uniqueness and stored in an abstraction library for that island, which the mutation LLM can then use as building blocks. This is meant to make search more modular and the resulting programs more readable.

Evaluation uses three starting configurations of the initial knowledge graph: succ_zero_eq (zero, successor, equality), arithmetic_base (zero, one, two, addition, multiplication, divides, ≤ , and equality), and ff_27 (zero, one, and generators of 𝔽₂₇). Each measure is scored by running 64 episodes with a 60-second timeout and averaging the extrinsic reward. EvoAbstract was configured with 4 islands, 64 generations, 16 i.i.d. rollouts per function evaluation, 2 programs sampled per iteration, an abstraction phase every 8 iterations sampling at most two abstractions per island, and GPT-4o-mini for both the evolutionary and abstraction LLM roles; each configuration was run 4 times and averaged.

Why This Matters

Impact on research. This is one of the few recent efforts to formalize the entire open-ended theory-formation loop — synthesizing new definitions, not just new problems — as a trainable RL problem, and it reframes mathematical "interestingness" from a hand-coded heuristic into an object of automated program synthesis. The finding that the synthesized measures are interpretable programs (rather than opaque networks) matters because it lets researchers inspect why a measure drives discovery. The negative results are also informative: one-shot LLM prompting of measures underperforms even a simple hand-coded measure, and abstraction can cause premature convergence.

Real-world applications (potential, not reported as deployments in the paper):

• Assisting mathematicians and graduate students with hypothesis generation in domains where concept spaces are large and hand-curated heuristics do not transfer.
• Automated curriculum or lemma-selection guidance inside interactive theorem provers and proof assistants, where a sparse reward signal is the central difficulty.
• Formal verification and program-analysis workflows, where derived predicates, invariants, and conjectures must be proposed before they can be checked.
• Educational tooling that can reconstruct, step by step, the concept hierarchy of an introductory number theory course — the paper's ground truth is drawn from an introductory number theory textbook.

Industry relevance. The techniques generalize beyond mathematics to any setting with sparsely rewarded, open-ended search over symbolic objects and a need for interpretable scoring functions: automated scientific discovery, program synthesis, and reward design for RL agents in large combinatorial spaces. The open-sourced Fermat environment gives labs a reusable benchmark harness.

Future Directions

• Richer policy templates and action exposure. The current template exposes only a subset of the full action space at each step, which limits scalability to more complex mathematical objects requiring long, ordered sequences of actions.
• Resolving bottleneck entities. Entities like primality must be discovered to continue toward a richer theory, but once discovered they blow up the knowledge graph and obstruct useful actions. Better state pruning or entity management is needed.
• Exploiting symmetries. Fermat does not yet exploit symmetries in entities, causing representational redundancy; exhaustive equivalence checking was found computationally intractable with Z3 as theories grow, so more scalable redundancy suppression is an open problem.
• Larger compute budgets. The authors call for further FunSearch and EvoAbstract experiments with heavy compute budgets to test whether evolutionary methods can produce significant discoveries in these domains, and note the abstraction "lock-in" as a diversity problem to address.
• Better conjecture discovery. Recovering ground-truth conjectures proved harder than recovering definitions, which the authors attribute to the narrower space of correct conjecture specifications.

Target Audience

This paper is most valuable to automated-reasoning and AI-for-math researchers, particularly those working on theorem proving, conjecture generation, theory exploration, and program synthesis; to RL researchers interested in intrinsic motivation, reward learning, and sparse-reward symbolic domains; and to mathematically trained readers curious about how machine learning systems might construct — rather than merely solve — mathematical theories. Practitioners building educational or proof-assistant tooling that needs interpretable heuristics will also find the EvoAbstract design and the negative baseline results directly useful.

Authors’ abstract

We take two key steps in automating the open-ended discovery of new mathematical theories, a grand challenge in artificial intelligence. First, we introduce $\emph{FERMAT}$, a reinforcement learning (RL) environment that models concept discovery and theorem-proving using a set of symbolic actions, opening up a range of RL problems relevant to theory discovery. Second, we explore a specific problem through $\emph{FERMAT}$: automatically scoring the $\emph{interestingness}$ of mathematical objects. We investigate evolutionary algorithms for synthesizing nontrivial interestingness measures. In particular, we introduce an LLM-based evolutionary algorithm that features function abstraction, leading to notable improvements in discovering elementary number theory and finite fields over hard-coded baselines. We open-source the $\emph{FERMAT}$ environment at this URL(https://github.com/trishullab/Fermat).