Learning Formal Mathematics From Intrinsic Motivation — part 1/5

Cleaned-text code points [0, 15778). Bibliography omitted here; source.md includes it.

# Learning Formal Mathematics From Intrinsic Motivation

###### Abstract

How did humanity coax mathematics from the æther? We explore the Platonic view that mathematics can be discovered from its axioms—a game of conjecture and proof. We describe Minimo (Mathematics from Intrinsic Motivation): an agent that jointly learns to pose challenging problems for itself ( conjecturing ) and solve them ( theorem proving ). Given a mathematical domain axiomatized in dependent type theory, we first combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our method guarantees well-formed conjectures by construction, even as we start with a randomly initialized model. We use the same model to represent a policy and value function for guiding proof search. Our agent targets generating hard but provable conjectures—a moving target, since its own theorem proving ability also improves as it trains. We propose novel methods for hindsight relabeling on proof search trees to significantly improve the agent’s sample efficiency in both tasks. Experiments on 3 axiomatic domains (propositional logic, arithmetic and group theory) demonstrate that our agent can bootstrap from only the axioms, self-improving in generating true and challenging conjectures and in finding proofs.

## 1 Introduction

Mathematical reasoning stands as a grand challenge for Artificial Intelligence (AI) research since the birth of the field [ 25 ] . Artificial agents capable of general mathematical reasoning have the potential to drastically impact both mathematics itself and areas where mathematical proof plays a key role, such as program and hardware verification [ 4 ] . While this goal has received significant attention from the AI community [ 22 , 46 , 30 , 42 ] , it still remains far from the breakthroughs that areas such as general game playing [ 36 ] , image [ 32 ] generation or protein folding [ 35 ] have witnessed.

Prior work has reflected two main visions of how AI might achieve general mathematical reasoning abilities. One such strategy is to leverage all of the available human-produced mathematical knowledge as a starting point [ 31 ] . This knowledge is encoded in source as varied as textbooks, online forums, academic papers, as well as formal proofs written in computer languages such as Lean, Isabelle, Coq or Metamath [ 2 ] . Large Language Models (LLMs) can ingest all such sources of knowledge in a unified manner, and provide a foundation for tasks in both formal and informal mathematics. Benchmarks of mathematical problem solving in natural language, such as GSM8k [ 10 ] and MATH [ 15 ] , have measured rapid progress over the years, but they remain limited to problems where the final answer is a number, due to the challenge of assessing the correctness of mathematical arguments written in natural language. This difficulty is not a challenge in formal theorem proving, where we can automatically verify the correctness of proofs in arbitrarily high-level mathematics. But benchmarks of formal theorem proving (such as minif2f [ 46 ] and LeanDojo [ 44 ] ), even with rapid advances in LLMs, have not yet witnessed the same breakthroughs. In fact, these benchmarks remain far from solved even though all of the theorems and problems in them are known mathematical facts, often already presented informally in publicly available training data.

An alternative vision of how AI might master mathematical reasoning sees mathematics through the lens of game playing, observing that the rules of the “game of mathematics” can be encoded in a variety of formal systems, such as dependent type theory, using a small set of axioms [ 24 ] . In principle, this can allows us to potentially borrow the successes of general game-playing agents, such as AlphaZero [ 36 ] , that have achieved remarkable success in mastering complex games entirely from experience. Notably, AlphaZero achieves super-human performance in a range of games without leveraging any human examples. Instead, it learns entirely from experience given only an environment where it can play the game by itself. If this approach could be transported to mathematics, it would bypass the dependency on human examples, and allow us to explore mathematical domains — both known and new, without distinction — by utilizing large scale compute and the potential of axioms to produce infinite data.

However, there is a crucial and often neglected difference between mathematics and traditional board games where game-playing AI has succeeded: mathematics is a game with intrinsic rewards [ 8 ] . Board games, such as Go or Chess, have a fixed starting configuration, and their rules determine the outcome of the game unequivocally. Mastering the game then amounts to learning a policy that optimizes for the extrinsic signal of winning. In theorem proving, a starting configuration is given by a theorem statement, and the correctness of a proof can be assessed objectively in a formal system. But the choice to work on a particular statement — a conjecture , before it is proved — is not given a priori by the rules of the game of mathematics. Instead, these goals come from the intrinsically motivated agents [ 8 , 34 ] who are playing the game. Thus, a key skill developed by human mathematicians is to decide which conjectures are worth considering. In stark contrast, current benchmarks of mathematical reasoning abilities, both formal [ 46 , 44 ] and informal [ 10 , 15 ] , all measure performance on an extrinsically defined set of problems, without space for further discovery.

In this paper, we make the first step towards creating intrinsically motivated mathematical agents by proposing Minimo — Mathematics from Intrinsic Motivation —, a method to jointly learn conjecturing and theorem proving, starting from nothing but the axioms of a given mathematical domain , represented in dependent type theory [ 12 ] . We borrow inspiration from the literature of intrinsic motivation in Reinforcement Learning (RL) [ 8 , 7 , 33 , 26 ] , where agents can learn from interacting with an environment even when no specific goals are given. Intrinsic motivation objectives have been instrumental for RL in hard exploration environments, where rewards are too sparse to seek directly [ 5 ] . The sparsity of rewards is also a major challenge in theorem proving, making this connection especially attractive. We thus define the objective of conjecturing as generating new problems that are challenging for the current agent but still provable within its given search budget. Since the agent also learns from the solutions it finds, the conjecturer has to continuously increase the difficulty of the problems it generates.

Minimo performs both conjecturing and proof search with a Transformer [ 40 ] language model (LM), which starts randomly initialized. To sample conjectures even from a model that starts with no prior knowledge, we combine methods from type-directed program synthesis and constrained generation from language models, enabling us to get valid conjectures by construction — concretely, conjectures are simply terms of type prop , the type of mathematical propositions in our type theory. Then, we perform proof search in the Peano environment [ 28 ] , which provides a finite action space for search in a dependent type theory, guiding search using the LM as a policy and value function. When a proof is found, proof search generates training data for improving the policy and values; it also provides data to improve conjecturing, since we then know how hard the problem was. We use this to alternate between conjecturing and theorem proving, in a self-improving loop. However, successful proofs are sparse. We thus adapt the idea of hindsight relabeling [ 1 ] to reinterpret failed trajectories as successful ones by rewriting their goals a posteriori. This significantly accelerates learning, allowing us to extract hundreds of new (true) conjectures, and their proofs, even from failed proof searches. In this way, even unprovable conjectures can be highly useful for the agent’s learning. We evaluate our system on three axiomatic mathematical domains—propositional logic, natural number arithmetic, and group theory—showing both that agents self-improve successfully in proving theorems in all domains. We also find that they improve at an extrinsic evaluation of theorems (from a classical textbook on logic [ 20 ] , and the Lean Natural Number Game [ 6 ] ), not given in training . In summary, we make the following contributions:

• We introduce a method for conjecturing using LMs that generates valid conjectures by construction in an arbitrary theory, using constrained decoding and type-directed synthesis.

• We define a hindsight relabeling method that simultaneously generates training data for conjecturing and theorem proving .

• We combine these methods in a learning loop where a mathematical agent can self-improve in a given formal domain given only the axioms.

• We evaluate agents trained on axioms for propositional logic, group theory and arithmetic, showing that they improve in both intrinsic and extrinsic evaluations.

## 2 Related Work

Our work is primarily related to prior work on mathematical conjecturing, learning to prove theorems, and on intrinsic motivation in Reinforcement Learning. To the best of our knowledge, our work is the first attempt to unify insights from these areas for training mathematical reasoning agents.

##### Mathematical conjecturing.

The task of discovering mathematical facts was the subject of the influential Automated Mathematician (AM), developed by Lenat in the 1970s [ 23 ] . AM was able to conjecture several known mathematical facts and concepts (such as the definition of prime numbers, and the unique factorization theorem). Unlike our system, AM did not aim at proving the conjectures it formulated — instead, it proposed and judged them based on a set of principles and on empirical evidence collected by AM itself. More recently, other works have revisited the idea of generating conjectures by training language models on human-written theorem statements [ 39 , 41 ] . Unlike our approach, this relies on pre-training data, and does not readily extend to conjecturing in new domains.

##### Learning to prove theorems from human data.

A large body of recent work has used Large Language Models to guide formal theorem proving in a number of proof assistants, such as Lean [ 22 ] , Isabelle [ 22 , 18 ] and Metamath [ 31 , 42 ] . Typically, these systems pre-train an LLM on large-scale Internet corpora and fine-tune on human-written formal mathematical proofs. Work on scaling laws for LLMs has shown that they generally improve when their parameter count and dataset size both increase in similar proportion. But the scarcity of formal proofs for training creates a challenge for this approach for learning formal theorem proving: even the largest datasets to date, such as the ProofPile, which aggregates libraries from 5 proof assistants, form relatively small datasets (e.g., 500MB of formal proofs on the ProofPile, contrasting to terabytes of Python code on Github).

##### Learning to prove theorems from synthetic data.

One recent success in automated mathematical reasoning was AlphaGeometry [ 38 ] , which was highly effective in solving olympiad-level geometry problems. AlphaGeometry, like our method, was trained entirely on synthetic data. Crucial to its approach is a method for generating both problems and solutions using only the axioms of geometry and a domain-specific deductive closure solver. This allows AlphaGeometry to synthesize and train on hundreds of millions of problems: many orders of magnitude more than existing human-created datasets of mathematical problems. Our approach shares the goal of AlphaGeometry of only using data derived from the axioms of the domain, with the difference that our method (a) is agnostic to the underlying axiomatic system and (b) does not rely on a domain-specific solver. Another line of work, including TacticZero [ 43 ] and rlCoP [ 19 ] , has explored learning to prove theorems from reinforcement learning only, in a tabula rasa fashion, but still using a human-written set of problems for training (and manually-engineered features, in the case of rlCoP).

##### Intrinsic motivation

We leverage inspiration from the literature on training reinforcement learning agents with intrinsic motivation objectives, allowing an agent to learn without pre-specified goals [ 26 , 34 , 33 , 13 , 27 , 7 , 3 , 37 ] . Our setup is conceptually close to AMIGO [ 7 ] , where agents attempt to generate challenging but achievable next goals. While AMIGO was demonstrated in a simple grid-world environment with a simple goal structure (any point in the grid gives a valid goal), we operate on a much richer setting, where the space of goals is unbounded — all conjectures in a formal mathematical theory. To sample conjectures, we use Synchromesh’s Constrained Semantic Decoding algorithm [ 29 ] , and guide it with type constraints.

##### Self-improvement of language models

A significant line of recent work has explored the idea that LLMs can “self-improve”: increase performance on a given task by fine-tuning on their own generated reasoning traces, which are selected by some criterion that ensures their quality. STaR [ 45 ] fine-tuned on reasoning traces that reached the correct answer on mathematical and multiple choice questions; LMSI [ 16 ] was able to obtain self-improvement on a question-only dataset, sampling multiple rationales and training on those that agree with the majority answer. More related to our work, but less explored, is the direction of having LLMs also generate their own problems for training: this has been explored for self-improving on solving programming problems [ 14 , 37 ] , where code execution provides signal about correctness. In Minimo , since our problems are formal conjectures and our solutions are formal proofs, we can guarantee correctness in a much stronger form than self-generated test cases.

## 3 Minimo

Most recent work on AI for mathematical reasoning assumes a target set of problems to be solved. We deviate from this paradigm by having the agent itself propose problems for it to try to solve and learn from. Our goal is to target increasingly harder problems in a given mathematical domain, where the domain is specified as a set of axioms given in dependent type theory.

Our agent is represented by a language model, which we will use to encode (a) a proof search policy π θ ​ ( a | s ) \pi_{\theta}(a|s) , (b) a value function V π ​ ( s ) V_{\pi}(s) , and (c) a difficulty-conditioned conjecturer P θ ​ ( c | d ) P_{\theta}(c\ |\ d) , where d d is a discretized measure of difficulty and c c is a mathematical statement (a string). Minimo consists of training both components in a loop that alternates between generating conjectures, trying to target hard but provable ones, and doing proof search, as we depict in Figure 1 . As we describe in this section, proof search generates training data both for the conjecturer and the prover components — training on that data thus yields a self-improvement loop as the agent interacts with the environment. We now describe the first step in this loop: generating conjectures.

### 3.1 Conjecturing

We aim to sample conjectures from a language model, conditioned on a target difficulty. By construction, an autoregressive LM gives a distribution over all strings. But if the LM does not have prior knowledge about the domain, it is unlikely to put non-negligible probability mass on valid mathematical statements. We now address the challenge of sampling valid conjectures.