Learning Formal Mathematics From Intrinsic Motivation
Authors: Gabriel Poesia
David Broman
Nick Haber
Noah Goodman
Venue: NeurIPS 2024 oral (2024)
Keywords: reasoning
reinforcement learning
formal mathematics
logic
Primary area: machine_learning_for_other_sciences_and_fields
TL;DR: We jointly learn to prove formal mathematical theorems and to propose harder provable conjectures in a self-improving loop

Abstract: How did humanity coax mathematics from the aether? We explore the Platonic view that mathematics can be discovered from its axioms---a game of conjecture and proof. We describe 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.

Learning Formal Mathematics From Intrinsic Motivation
Gabriel Poesia'
David Broman* Nick Haber
Noah D. Goodman
(poesia, nhaber ngoodman] Ostanforstoooooooo edu Departments of Computer Science', Psychology² and Education", Stanford University, USA EECS and Digital Futures KTH Royal Institute of Technology. Sweden
dbro@kth. se
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 dependent type theory, we first combine methods for constrained decoding and type-directeds synthesis to sample valid conjectures from language model. Our method guarantees well-formed conjectures by construction, randomly initialized model. We use the same model to represent policy and value function for guiding proof search. Our agent targets generating hard but provable conjectures-4 moving target, since its own theorem proving ability also improves it trains. We propose novel methods for hindsight relabeling 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 finding proofs.
start with
Introduction
Mathematical reasoning stands as 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 Al community (22
46
30 42). it still remains far from the breakthroughs that areas such as generation or protein folding (35) have witnessed.
general game playing 36 image
32
Prior work has reflected two main visions of how AI might achieve general mathematical reason- ing abilities. One such strategy is leverage all of the available human
human- produced mathematical knowledge as a starting point (31. This knowledge encoded in source as varied as textbooks, online forums, academic papers, 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 unified manner, and provide foundation for tasks in both formal and informal mathematics. Benchmarks of mathematical problem solving in natural language, such as GSM8K [0] and MATH [15), have measured rapid progress over the years, but they remain limited problems where the final answer is number, due to the challenge of assessing the correctness of mathematical arguments written in natural language. This difficulty 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
a challenge in formal theorem proving.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

Conjecturing
Theorem Proving
Proof Search (MCTS)
Axioms
Conjecture 1: (1+1+ + 0) 01
Conjecture EASY
Conjecture 2
Conjecture FAIL
Conjecture 2: V(n: out), (0
Constrained Decoding
Conjecture Vin, nat), -
EGix Language Model
New training data for Policy Value Conjecturing
Figure 1: We train mathematical reasoning agents starting only from the axioms of a given formal domain, where they jointly learn pose challenging but provable conjectures and to find their proofs.
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 Al 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 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 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 mathematics, 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 a crucial and often neglected difference between mathematics and traditional board games where game- paaniengaiing AI has succeeded: mathematics is game with intrinsic rewards (8). Board games, such as Go Chess, have a fixed starting configuration, and their rules determine the outcome of the game unequivocally. Mastering the game then amounts to learning policy that optimizes for the extrinsic signal of winning. In theorem proving, starting configuration is given by a theorem statement, and the correctness of proof can be assessed objectively in formal system. But the choice work on a particular statement not given a priori by the rules of the game of mathematics. Instead, these goals come from the intrinsically motivated agents 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 IO 15), all measure performance on an extrinsically defined set of problems, without space for further discovery.
conjecture, before is proved is
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 [2]. We borrow inspiration from the literature of intrinsic motivation in Reinforcement Learning (RL) 7 33 26 . where agents can learn from interacting with 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 [.. 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 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 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 dependent type theory, guiding search using the LM as a policy and value function. When a proof found, proof search generates training data for improving the policy and values; 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 [ 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 's learning. We evaluate our system on three axiomatic mathematical domains propositional logic, natural number arithmetic, and group theory- theory-showing both that agents self-improve successfully in proving theorems in all domains. We also find that they improve at extrinsic evaluation of theorems (from classical textbook on logic [20), and the Lean Natural Number Game [6], nol given in training. In summary, make the following contributions:
We introduce 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 learning loop where a mathematical agent can self- 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 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 written theorem statements 39 41 Unlike our approach, this relies on pre-training data, and does not readily extend to conjecturing 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 number of proof assistants, such as Lean [22], Isabelle [22 [8] and Metamath [3] 42). Typically, these systems pre-train an LLM on large-scale Internet corpora and fine-tune on numan--ritten 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 searcity 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 method for generating both problems and solutions using only the axioms of geometry and Nomain--secifff 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 a Nomain-speciftt solver. Another line
3

---

of work, including TacticZero 43 and riCoP 19, has explored learning to prove theorems from reinforcement learning only, in tabula rasa fashion. but still using human-written set of problems for training (and mannally-engineereed features, in the case of rICoP).
Intrinsic motivation We leverage inspiration from the literature training reinforcement learning agents with intrinsic motivation objectives, allowing an agent to learn without pre-specified goals 126 34 33 13 27 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 simple goal structure (any point in the grid gives valid goal), 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 '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 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- seff-improvement on 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 a much stronger form than self-gen geffeeeeerted 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 try to solve and learn from. Our goal is to target increasingly harder problems in given mathematical domain, where the domain is specified as a set of axioms given dependent type theory.
Our agent is represented by a language model, which we will use to encode (a) proof search policy To(als). (b) value function Va (s). and (c) difficulty-conditioneed conjecturer Po(e d), where d is a discretized measure of difficulty and e 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 I 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.
As we describe in this
3.1 Conjecturing
We aim to sample conjectures from a language model, conditioned on a target difficulty. By con- struction, autoregressive LM gives 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.
To that end, our main insight is to leverage constrained decoding to obtain valid conjectures by construction. Our method will turn any language model including a randomly initialized one, which is what we start with - into a probability distribution over strings that represent forl-formed conjectures in dependent type theory over given set of axioms. Ultimately, we will also train the LM to generate conjectures given a target difficulty. We use this ability to attempt to generate increasingly difficult problems for training, according to the agent's 's current ability to prove theorems.
To reason about constraining the LM's outputs, we leverage the abstraction of a completion engine, first introduced in the context of code generation with language models [29]. Assuming C is the set of all valid conjectures, a completion engine will allow us to use any LM to sample strings from in an autoregressive fashion. Mathematically, C is function fc - P(E*), ), taking string e Σ" and

---

returning set of strings fc(s) D Intuitively, we will sample conjectures from our LM by constraining it to strings that can be generated with iterated calls to fc. Concretely, we will start with s "", and query fc(s) to obtain the set of valid ways to begin to state a conjecture. After we choose one of those 81 E fs(),, we can then query fc(s1) to obtain the valid ways to proceed, and repeat until we have a complete conjecture. Our main challenge here is to construct suitable fc that it is sound (all conjectures obtained by this procedure are valid) and complete (all valid conjectures can be obtained by this procedure). After we define fc. we can sample from any LM while guaranteeing that the output will belong to C' by using the Constrained Semantic Decoding (CSD) algorithm [29]
To construct fe. we analyze the minimal formulation of dependent type theory backing Peano 28 essentially the classical Calculus of Constructions (CoC) [12]. In the CoC, mathematical propositions are constructions of type prop. Since generating a proposition might involve generating objects of arbitrary other types, depending on the axioms of the given domain, we will define a more general family of completion engines, ft. which will constrain the LM to sample an object of an arbitrary type/ t. At the end, we obtain fc fprop-
To sample an object of type t, we leverage the simple grammar of terms in Peano 28 to guide a recursive type-directed synthesis algorithm. Syntactically, terms in Peano are defined by the grammar e ::= type prop x (e (lambda x : e, e,e) [(2r e) + e]. The first two production rules give the names of two built-in base types, type and prop. We then have variables, function application. lambda functions, and function types (denoted in square brackets). As conventional in type theory, let I be our ryping context: a sequence of pairs of names and their types. For example, we might have T= [not: type, nat, succ: : [nat - nat]], context with three objects: type nat, an object having that type, and function succ from nat to nat. Given a context, to obtain an object of type f, it suffices to consider the formation rules in CoC to guide generation:
If our target type is f = type, we can generate either one of the names in I having type = type (e.g., nat, for the example context above), or a function type.
If our target type is f prop, we can generate either one of the objects in I' having type prop, or function type where the output type has type prop.
If our target type is function type, we must start by generating square bracket; then, we (recursively) iteratively generate a type for the next parameter, or, if we already have at least one parameter, we also generate the final output type.
An object of any type can be formed by function application of function f chosen from T, provided that the output type of f can be unified with f.
These rules allow to determine the possible valid tokens any point during generation. Besides the base types type and prop, objects of all other types are either in I or the result of a function application. We use recursive descent parser parse the (incomplete) term we have far (as originally done in (29)), and compute the target type at the current point in generation. Then, we enumerate the possible next tokens for the LM by using the rules above, return the union of the sets of choices allowed by each rules as the output of ft-
Note that this is a general procedure for searching for objects of any given type (i.c., inhabitants of that type). This is undecidable in general (theorem proving is a special case of type inhabitation). so this procedure might not terminate. Therefore. we set maximum number of tokens K (150, in our experiments), and ignore samples where the LM fails to generate a conjecture after K tokens. In practice, we find the rejection rate for generating propositions to be low, 10% of the generations.
The above procedure forces the LM to generate a valid conjecture, but the LM still assigns a distribution over those. During training, we also aim to generate conjectures that are provable, but hard to prove. The signal on both success and difficulty is generated by running proof search (as we describe next) and, in cases where proof is found, measuring it's log-likelihood under the current policy, which correlates with how many iterations MCTS takes to find the proof (see Appendix).
'This set can be implicitly defined by a regular expression, so it might be infinite. This allows a completion engine to represent constraints such as "what follows can be any valid identifier".
5

---

3.2 Proof Search
Having a conjecture represented by a target type I, we then perform proof search using Monte Carlo Tree Search (MCTS: [21]. 42)), guided by learned policy Te and value function Vo. We represent both Th and Ve using the same underlying language model that we use for conjecturing. We use Peano [2 as the environment for proof search. Peano exposes a finite action space, so we don't need to generate actions using To - it suffices to be able to evaluate them. More precisely, at a given state where have actions a!") available, we compute the distribution no(a;") (s) by evaluating
the likelihood of each ai as the completion to string of the form "STATE: 
; POLICY:" :. We read out the value of state in a similar way- - by considering the likelihood of or as being the next token following "STATE: 
; VALUE: ". In both cases, the probability of the next token is normalized over only the choices that can lead to a valid completion.
States and actions in Peano are similar to several other interactive theorem provers, such as Lean and Coq. The state consists of a of typed objects, along with set of open proof goals (which are types). Objects in the state whose type is a proposition type are interpreted as evidence for that proposition (either a proof or an assumption). Actions might add new objects to the state (e.g., take the successor of one existing natural number, or use an equality to rewrite an existing proposition into a new one), change the goal (by backward chaining), or both (e.g.. if the goal is to prove A + B, which is used to represent both logical implication and universal quantification, the intro action will add object of type A to the state and change the goal to B).
When proof search succeeds, we can extract examples to train both the policy and the value function. For the policy, we simply extract the actions that lead to the proof as language modeling examples, using the same format we use to query Tg. For the value function, we take the states in the subtree that complete the proof examples with value 1, and a random set of other states examples with value 0 for training. When proof search fails, however, this naïve procedure does not extract any training examples. This happens often the beginning, since our model initially generates large number of conjectures it cannot prove (either because they are false, or because naïve proof search times out). But forward actions in the proof search tree often construct proof' for other propositions. even if they are irrelevant for proving the original goal. We levarage this fact for generating training data by hindsight relabeling, as we describe next.
3.3 Hindsight Relabeling
Even conjecture that fails to be proven can be highly informative about the domain. During proof search, forward actions that apply functions whose result type is a proposition type (e.g., concluding A from (and A B)) produce proofs, even when those proofs might not be useful for proving the original conjecture. In Reinforcement Learning, the well-known method of Hindsight Experience Replay [ extracts training data for the policy from such failed trajectories by relabeling the trajectories with goals that were in fact achieved, as opposed to the original goal. For those alternative goals, the trajectory then represents successful sequence of actions. We apply this idea to extract training examples for both the policy and value functions from proof search trees, by picking nodes after forward actions that produced a proof, and walking upwards in the tree until we find a backward action (since those change the goal). That path then becomes a successful trajectory after we relabel the goal. Two important steps to improve data quality are (1) we clean up the solutions by eliminating steps irrelevant for the proof of the new goal, and (2) we only add proofs of goals never seen before, to avoid oversampling trivial facts that are rediscovered extremely often (such as 0 = 0).
We go one step further and observe that hindsight relabeling can also be useful for training the conjecturer. Concretely, the procedure we described above produces a set of proofs p. for relabeled statements gt- All of these statements are therefore true in the mathematical domain, and we use them as examples of true conjectures. As a concrete example, in arithmetic, the agent will often conjecture simple expressions such as 2 + 1 = O. Most equalities generated at random will be false. However, by applying the Peano Axioms and facts about equality in succession, the agent eventually finds proof of 2 + 1 = 3. Evaluating the likelihood of the proof under πe gives measure of the difficulty of this alternative statement for the current policy. This insight allows our agent to learn about hundreds of new unique, true statements in each proof search. As our experiments show, we find hindsgght relabeling to be crucial for enabling the agent to steadily conjecture harder statements that it is able to prove.

---

Problem difficulty across iterations
Arithmetic
Groups
Propositional Logic
Mean proof log- segliiklihoodd
0-
-2-
-4
-6
-8-
-10-
Policy's Iteration
-12
2
3 Conjecture Iteration
1
3
Conjecture Iteration
Conjecture Iteration
Figure 2: Difficulty of proved conjectures found in each iteration of MINIMO, evaluate as the log- probability of the proof under the policy checkpoints after each iteration of the training loop (with standard error bands for runs with 3 random seeds).
3.4 Training loop
Finally, we tie all components together by alternating between (a) generating a batch of conjectures, (b) running proof search on them, (c) extracting training examples from the search trees, and finally (d) training the underlying LM using the standard cross-entropy objective. When a proof is found, either directly by hindsight relabeling, we first compute a continuous difficulty metric of the statement by taking the log- likelihhood of the proof under the current policy. To discretize difficulties, we then consider difficulty percentiles of the last batch of conjectures: we take the 10% least likely proofs to be associated with "hard" conjectures, the 50% most likely to be considered "trivial", and the remaining are taken as "easy". When put together, these components form self-improving loop that starts only from the axioms of the given mathematical domain, as our experiments show.
4 Experiments
We now evaluate MINIMO on three mathematical domains. We experiment with axiomatic systems for (a) propositional logic, (b) arithmetic, and (c) abstract groups. All the axioms are given in the Appendix. We then train agents over 5 iterations of conjecturing and theorem proving, generating 200 conjectures in each batch, running MCTS for proof search with 1000 expansions, and evaluate our agents guided by the following research questions:
RQ1: Can our conjecturing method generate increasingly harder conjectures as training progresses?
RQ2: Do agents improve at theorem proving as they train on their own generated problems?
RQ3:
Is hindsight relabeling effective at improving conjecturing and theorem proving?
RQ4: Do our agents improve at proving an externally given set of human-selected theorems, even if these are not given during training?
The first three questions require intrinsic evaluations they ask whether the learning dynamics of agents trained with MINIMO matches the desiderata of self-improving at both conjecturing and theorem proving while given only the axioms. The last question is an extrinsic assessment of what our agents learn - we evaluate whether the learning progresses way that aligns with an external criteria- namely, the proficiency of the agent at proving theorems from human sources (a textbook and Lean game).
4.1 Learning dynamics
We first investigate RQI and RQ2. Figure 2 shows the progression difficulty across iterations of the MINIMO learning loop (first conjecturing, then running proof search, and training on collected
Our code is available at htttttss///tthubb.... /mmia
7

---

examples). Here, we evaluate the average log-likelihood (y-axis) of conjectures proven at each conjecturing iteration (x-axis) under the policy after each iteration (line color). Policy 0 is the initial (randomly initialized) policy, while subsequent policies were trained on the examples obtained during proof search, with hindsight relabeling, up to the previous iteration. Lower log- ogllikelihood generally means harder conjectures (i.e., they tend to take more search iterations, see Appendix).
Difficulty increases as training progresses (RQI). Fixing an early policy, the oog-likelihood of proofs under that policy steadily decreases across training iterations. This is reflected in the negative slope of difficulty across iterations when the policy is fixed. In particular, the policy at iteration O serves naive search baseline, since it is essentially uniform. We observe that, training progresses, this policy struggles increasingly more with each new batch of conjectures. The same pattern repeats for subsequent policies when consider conjectures generated in future iterations, giving a generally downward trend in oggliiklihood of the solutions for any given policy, showing that conjectures get increasingly more challenging. This provides positive evidence for answering RQI: in all 3 domains, the conjecturer is able to increasingly propose harder provable conjectures as training progresses.
Proof policy improves as training progresses (RQ2). At each iteration, we sample a new set of unseen conjectures for training. From Figure 2 we see that later policies generally perform better than earlier ones, at a fixed conjecture iteration. This reflects the fact that each new policy assigns higher likelihood the proofs, even for unseen conjectures at each iteration. For example, after training on the data generated from the first iteration, the policy on iteration I has higher log-likelihood for the proofs to the new conjectures found at iteration 1, when compared to the initial policy from iteration O. This pattern repeats at each iteration, showing that the prover is also progressing and generalizing to unseen problems, though with diminishing gains in the final iterations. This suggests a positive answer to our second research question: our agents effectively self-improve in their ability to prove new statements.
Hindsight relabeling is necessary for joint self-improvement (RQ3). The results so far all used hindsight relabeling on all proof searches-succeseee or not-to extract training data for the policy and value function, as well as conjecturing. To evaluate whether our agents would still show the same continuous self-improvement regardless of the data efficiency gains from hindsight relabeling, Figure 3 compares agents trained with and without hindsight relabeling across 5 iterations over the same axiomatic domains. Here, we look at the ability of the agent to achieve the goal of constantly proposing provable but challenging conjectures for itself. Ideally, the difficulty of conjectures should not fluctuate significantly during the course of training: we would like the agent to always find new challenging conjectures that it nevertheless still proves. We find that, in all 3 domains, the agent fails to achieve this goal when not trained with hindsight relabeling. Instead, as it trains on its own proofs, the agent's is conjectures fail remain challenging-a0 provable conjectures end up with high log-likelihood as training progresses, and the conjecturer is unable to leave that regime. We attribute this the volume of signal that the conjecturer receives: at each initial batch, only around 10-20% of the conjectures are proven. When not using hindsight relabeling, the only feedback that the conjecturer recevies is that proof search timed out on these statements. On the other hand, with hindsight relabeling, even these failures lead the conjecturer to observe hundreds of actual true statements in each domain (along with their proofs), leading to better learning dynamics. This provides positive evidence for RQ3: hindsight relabeling significantly helps the agent to jointly improve in conjecturing and theorem proving without it, training tends to collapse to by proposing only easy conjectures.
4.2 Proving human-written theorems (RQ4)
Finally, we evaluate whether our agent, trained only on problems that it proposes to itself, also improves in solving problems that are of interest to humans. Since our agent does not grow its library of theorems over time, starting every new proof from the axioms, meaningful evaluation requires theorems that can be reasonably proven straight from the axioms, without lemmas. We thus use two human- written sources of theorems meeting this criterion, for the domains of propositional logic and arithmetic. For logic, we take the set of 35 theorems of propositional logic from Stephen Kleene's 's textbook "Introduction to Metamathematics" (20). Precisely, in Theorem 41, Kleene states (and proves subset of) 35 useful statements of Propositional Logic (such contraposition
8

---

Arithmetic
Groups
Propositional Logic
Proof aggliikllhood
-1
-2
-3
-4
Hindsight?
5
With Hindsight
Without Hindsight
0
1 2
3
4
1
2
3
2
3
Iteration
Iteration
Iteration
Figure 3: Difficulty of proved conjectures proposed in each iteration under the current policy that same iteration, comparing when using and not using hindsight relabeling to generate new proofs and conjectures, with standard error bands for runs with 3 random seeds. Ideal behavior would be flat line, representing constant relative difficulty. Hindsight significantly helps the agent conjecture propose harder problems.
rules, commutativity and transitivity laws of logical connectives, and properties double negation). For arithmetic, we use the Natural Number Game [6). popular game used to introduce formal mathematics in Lean theorem prover. We take levels of the game that are (a) theorems about natural numbers, and (b) do not refer previous lemmas, only the axioms; this results in 10 levels spanning the Tutorial, Addition, and Multiplication worlds. We translate the statements into Peano, and evaluate agents on their success rate those problems within 2000 MCTS expansions.
Figure 4 shows the results. We find that, as our agents train on their self- generaedd problems, they steadily become more successful at proving the- orems from both Kleene's book and the Natural
Success rate on human-written theorems
Proof Search Success Rate
0.7
Theory
Number Game This happens even though these theorems are not turgeted during training, since our agent only uses its own conjectures. Four only proved
Arithmetic
Propositional Logic
0.6
theorems in Propositional Logic after the last itcration of training: commutativ- ity and transitivity of the "if and only if" logi- cal connector, a law connecting double negation and implication (--(A and the "currying law" of the conjunction (A B) C A + (B = C). In the Nat- ural Number game, only the final agent proves Vn, Vm, succ(n) + + suce(n + m), a theorem requiring induction on the correct variable (m) and non-trivial sequence of rewrites in the inductive case (we include the full proof in the Appendix). While admitedly small scale, these results suggest positive answer to our last research question: agents trained on their own conjectures can also improve at solving human written problems, which are not given during training.
0.5
0.4
0.3
B), - + B-B),
2 3
Checkpoint Iteration
Figure 4: Success rate our agents at proving theorems from the "Introduction to Metamathe- matics" textbook and the Natural Number Game. As agents train their own conjectures, they also improve at solving problems from these two Human--ritten sources.
5 Limitations and Conclusion
We present MINIMO: an approach to training agents for formal mathematical reasoning starting from only the axioms of given domain. The agent jointl learns to propose challenging conjectures and to prove them. Our experiments show evidence of MINIMO improving its performance across training iterations. In the Groups domain, the average proof length it finds generated conjectures (i.c.,

---

not found by hindsight) increased from 2.67 steps in the first iteration, when the model is randomly initialized, steps by iteration 4, with proofs for 'hard' conjectures growing from 3.67 6.10 steps. The longest proofs found grew from 4 steps to 9 steps from the first to last iteration. Similar trends appear in Propositional Logic (average length from 2.75 to 4.21 steps, longest proofs from to 11 steps) and Arithmetic (average from 2.36 to 3.35 steps, longest from 4 to 7 steps).
However, MINIMO currently has two crucial limitations that prevent from (a) discovering deep mathematical theories, and (b) scaling up to large theories. First, even if the agent's 's policy improves, its library remains fixed to the definitions and axioms that it starts with. Proofs that do not use lemmas (cut-free proofs in logic) can be exponentially longer than equivalent ones that do, and thus quickly grow beyond the reach of search. With this constraint, our agent most often finds harder conjectures by making the statements longer and more complicated. For example, in Groups, early conjectures include trivial statements like e = e; by the last iteration, the conjecture requiring the longest proof ((<(<(((=-))))) (proved in 9 steps). In contrast, human mathematicians develop deep theories by accumulating results and definitions along the way, in such way that even very high-level results can be described succinctly at the right level of abstraction. Understanding how to bootstrap such cumulative learning in an agent (e.g., exploring notions of usefulness or interestingness, several of which have been posited 4 will be key direction for future work.
reads as Vg E G, if e (g= then e²
Another bottleneck in our current setup is that large library can cause the current action enumeration algorithm in Peano to become prohibitively slow finite action space can still become intractable). A method that scales unboundedly should incorporate some form of premise selection [17] In past work, premise selection has either been based on symbolic heuristics or in learning useful premises from Homan--rittee proofs. We believe that developing a premise selection method that bootstraps together with the other learned components will be as important as understanding how to grow the agent's s library.
Together, lifting these limitations from our method might lead a completely compute-bound self-improving agent for formal mathematics capable of discovering deep mathematical theories starting only from basic axioms- the rules of the game of mathematics.
Acknowledgments
We thank Daniel Selsam and Laetitia Teodoreseu for insightful discussions on preliminary ideas related this work, well the anonymous reviewers for their helpful feedback. This work was supported by the NSF Expeditions Grant with Award Number (FAIN) 1918771, and by NSF grant #2302701. GP was also supported by the Stanford Interdisciplinary Graduate Fellowship (SIGF). This work was also partially supported by the Wallenberg Al, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
References
[1] Marcin Andrychowicz. Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, OpenAI Pieter Abbeel, and Wojeiech Zaremba. Hindsight experience replay. Advances in neural information processing systems, 30, 2017.
[2] Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023.
[3] Mare Bellemare, Sriram Srinivasan, Georg Ostrovski, Tom Schaul, David Saxton, and Remi Munos. Unifying count-based exploration and intrinsic motivation. Advances in neural information processing systems, 29, 2016.
[4] Yoshua Bengio and Nikolay Malkin. Machine learning and information theory concepts towards an ai mathematician. arXiv preprint arXiv:2403.04577 2024.
[5] Yuri Burda, Harrison Edwards, Amos Storkey, and Oleg Klimov. Exploration by random network distillation. arXiv preprint arXiv: 2018.
[6] Kevin Buzzard. Natural number game. https: h http://wwww.m. ma. imtemialpeaa.....m ac. uk//buzzard/
Cena/natural. wwttaaarralnuubbrraetet _game/ 2019.
10

---

[7] Andres Campero, Roberta Raileanu, Heinrich Küttler, Joshua B Tenenbaum, Tim Rocktäschel, and Edward Grefenstette. Learning with amigo: Adversarially motivated intrinsic goals. arXiv preprini arXiv:2006. 12/22, 2020.
[8] Nuttapong Chentanez, Andrew Barto, and Satinder Singh. Intrinsically motivated reinforcement learning. Advances in neural information processing systems, 17, 2004.
[9] Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: proof- producing superposition theorem prover for dependent type theory. In International Conference on Interactive Theorem Proving, 2024.
[10] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110. 14168, 2021.
[11] Simon Colton, Alan Bundy, and Toby Walsh. On the notion of interestingness in automated mathematical discovery. International Journal of Human-Compuee Stulies, 53(3):351-375, 2000.
[12] Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986.
[13] Nick Haber, Damian Mrowca, Stephanie Wang, Li F Fei-Fei, and Daniel L Yamins. Learning to play with mottivvtee, sclf- agents. Advances in neural information processing systems, 31, 2018.
[14] Patrick Haluptzok, Matthew Bowers, and Adam Tauman Kalai. Language models can teach themselves to program better. The Eleventh International Conference on Learning Represen- tations, 2023.
[15] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. In Thirty-fifth Conference Neural Information Processing Systems Datasels and Benchmarks Truck (Round 2), 2021.
[16] Jiaxin Huang, Shixiang Gu, Le Hou, Yuexin Wu, Xuezhi Wang, Hongkun Yu, and Jiawei Han. Large language models can self-improve. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 1051-1068, Singapore, December 2023, Association for Computational Linguistics.
[17] Geoffrey Irving, Christian Szegedy, Alexander Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016.
[18] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210. /2283, 2022.
[19] Cezary Kaliszyk, Josef Urban, Henryk Michalewski. and Miroslav Olšák. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018.
[20] Stephen Cole Kleene. Introduction to metamathematies. Van Nostrand, 1952.
[21] Levente Kocsis and Csaba Szepesvári. Bandit hased monte-carlo planning. In European conference on machine learning, pages 282-293. Springer, 2006.
[22] Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving, Advances in neural information processing systems, 35:26337-26349, 2022.
[23] Douglas Bruce Lenat. AM: an artificial intelligence approach to discovery in mathematics as heuristic search. Stanford University, 1976.
[24] David McAllester. Mathzero, the classification problem, and set-theoretic type theory. arXiv preprint 2rXiv:2005.05552, 2020.
11

---

[25] Allen Newell and Herbert Simon. The logic theory machine a complex information processing system. IRE Transactions on information theory, 2(3):61-79, 1956.
[26] Pierre-Ye Yves Oudeyer, Frdric Kaplan, and Verena Hafner. Intrinsic motivation systems for autonomous mental development. IEEE transactions evolutionary computation, 11(2):265- 286, 2007.
[27] Deepak Pathak, Pulkit Agrawal, Alexei A Efros, and Trevor Darrell. Curiosity exploration by self-supervised prediction. In International conference machine learning, pages 2778- 2787. PMLR, 2017.
[28] Gabriel Poesia and Noah D Goodman. Peano: learning formal mathematical reasoning, Philo- sophical Transactions of the Royal Society A, 381 381(2211:20220044, 2023.
[29] Gabriel Poesia, Alex Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. Synchromesh: Reliable code generation from pre-trained language models. In International Conference on Learning Representations, 2021.
[30] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and llya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01334, 2022.
[31] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint 3xXiv:2009003993 2020.
[32] Aditya Ramesh, Mikhail Pavlov, Gabriel Goh, Scott Gray, Chelsea Voss, Alec Radford, Mark Chen, and Ilya Sutskever. Zero-shot text-to-image generation. In International conference on machine learning. pages 0821-8831. Pmlr, 2021.
[33] Jürgen Schmidhuber. Formal theory of creativity, fun, and intrinsic motivation (1990-2010). IEEE transactions on autonomous mental development, 2(3):230-22) 247, 2010.
[34] Jürgen Schmidhuber. Powerplay: Training an increasingly general problem solver by continually searching for the simplest still unsolvable problem. Frontiers in psychology, 4:46492, 2013.
[35] Andrew W Senior, Richard Evans, John Jumper, James Kirkpatrick, Laurent Sifre, Tim Green, Chongli Qin, Augustin Židck. Alexander WR Nelson, Alex Bridgland, et al. Improved protein structure prediction using potentials from deep learning. Nature, 577(7792):706-710, 2020.
[36] David Silver, Thomas Hubert, Julian Schritwieser, loannis Antonoglou, Matthe Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science, 140-6419) 2018
[37] Lactitia Teodorescu, Cédric Colas, Matthew Bowers, Thomas Carta, and Pierre- Yves Oudeyer. Codeplay: Autotelic learning through collaborative self-play in programming environments. In IMOL 2023-Intrinsicall Motivated Open-ended Learning workshop at NeurIPS 2023, 2023.
[38] Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 42567995):446-482, 2024.
[39] Josef Urban and Jan Jakubūy. First neural conjecturing datasets and experiments. In Intelligent Computer Mathematies: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings 13, pages 315-323. Springer, 2020.
[40] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention all you need. Advances in neural information processing systems, 30, 2017.
[41] Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. Advances Neural Information Processing Systems, 33:18 1811188411117,, 2020.
[42] Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv: 02644, 2016.
12

---

[43] Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34:9330-9344 2021.
[44] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- auggeetee language models. Advances in Neural Information Processing Systems, 36, 2023.
[45] Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. Star: Bootstrapping reasoning with reasoning. Advances in Neural Information Processing Systems, 35:15476-15488 2022.
[46] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-leve mathematics. arXiv preprint arXiv:2109.00/ 2021.
13

---

A
Training details
We represent our agents with GPy----tyle character-level Transformer models totalling approximately 8.45M parameters each (8 layers, 8 attention heads, hidden size 512, feed-forward size 2048, vocabulary size 128, absolute positional embeddings, with maximum context size of 1024). After each training iteration, (learning rate of le - 4) with dynamic batch size of most 10000 characters (random examples are added until their padded sequence lengths add up more than 10000). We found these parameters to generally lead to stable training across all runs, without divergence, and 2000 steps was enough to bring each iteration convergence in training loss.
train the LM for a fixed number of 2000 steps of the A optimizer
Our training runs (5 iterations of generating and proving 200 conjectures in each) were done on machines with 5 NVIDIA A40 40GB GPUs each. Each took from 8 to 16h single GPU, totalling 288 GPU hours for the runs underlying our main results.
B Proof log-likelihood and MCTS Expansions
Throughout the paper, used the likelihood of the proof under the policy measure of difficulty. F shows that this quantity is linked to the number of iterations that MCTS takes to find the proof. This allows to estimate difficulty easily without running search for theorems that we have proofs for (such as those we find by hindsight relabeling).
2,000
1,800
1,600
MCTS Iterations
1,400
1,200
1,000
800
600
400
200
-20
-13
-9
-5
Proof likelioeld
Figure 5: Relation between MCTS iterations until the proof is found, vs log- likeelhooooo of the proof that is found. The higher the likelihood, the faster MCTS is in finding the proof.
C Fraction of provable conjectures across iterations
Our conjecturing procedure steers to LM generate "hard", where that means they can still be proven by the current agent. Figure 6 shows how the ratio of proven conjectures evolves across training. In Groups and Propositional Logic, this ratio steadily increases both when and when not using hindsight. In Arithmetic, we observe that the ratio remains consistent up to iteration 3, but then decreases, whereas it increases sharply without hindsight. We note that this sharp increase due to the conjecturer generating mostly trivial conjectures, by adding new combinations of assumptions that are not necessary for the proof (e.g.. the most common conclusion for the conjecturer generate without hindsight is often 0 = 0). Even though the hard conjectures with hindisight often fail to be proven, they still seem to generate useful training data for the prover, as we see in our extrinsic evaluation with problems from the Natural Number Game. Thus, this analysis points out that ideal behavior for the conjecturer unclear - is still perhaps positive to generate false conjectures, as long as the process of proving them leads to learning progress (as seems be the case in Arithmetic).
14

---

Fraction of proven conjectures by iteration
Arithmetic
Groups
Propositional Logic
1.00
Ratio Proven Conjectures
0.90
Hindsight?
Hindsight Without Hindsiight
0.80
0.70
0.60
0.40
0.30
0.20
0.10
0.00
Iteration
Iteration
Iteration
Figure 6: Ratio of proven conjectures each batch 200, at each iteration of training.
D
Axioms
We here provide the full Peano axiomatization of each domain.
D.1 Arithmetic
Our axiomatization of arithmetic includes the classical unary definition of the natural numbers (zero and successor function), axioms about addition, multiplication, and the principle of induction.
[('t type) -> 't -> 't -> prop].
nat type.
nat.
s [nat -> nat].
+ [nat -> nat -> nat]
[nat -> nat nat].
+_z [('n nat) -> (=
2) 'n)l.
+_s [('n nat) -> ('m : nat) -> (= (+ 'n (s 'm) (s (+ pn ?m)))].
*_z [('n nat) -> (= (* 'n z) z)].
*_s [('n nat) ('m nat) -> (= (* (s 2m) (t 'n (* 'n mm)))]
nat_ind [('p [nat -> prop)) -> ('p 2) -> [('n nat)
('p 'n) -> ('p (s 'n))] -> [('n nat) -> ('p 'n)]].
#backward nat_ind ind.
#forward +_2 ((+ 'n 2) nat).
#forward +_s ((+ Pn (s mm)) nat).
#forward +_ ((* Pn 2) nat).
#forward ((* 'n (s m)) nat).
D.2 Propositional Logic
prop type. false prop.
/* Connectives */ not [prop -> prop].
15

---

and [prop -> prop -> prop].
or [prop prop propl.
iff [prop -> prop -> propl.
** Introduction rule for conjunction */ #backward and_i.
and_i [('P prop) -> ('Q prop) -> PP -> ²Q -> (and p pQ)].
/* Elimination rules for conjunction */
#forward and_el ('_ (and d Qq)).
and_el : [(PP : prop) -> ('q prop) (and P QQ) -> 'P]
#forward and_er ('_: (and o QQ)).
erd_er : [(PP : prop) -> ('q prop) -> (and p 2Q) -> QQ]
/* Introduction rules for disjunction */ #backward or or_il.
or_il: [(' prop) -> ('Q prop) -> P -> (or pp .Q)].
#backward or_ir.
or_ir [(P : prop) -> ('Q prop) -> ' -> (or p 2Q)]
/* Elimination rule for disjunction */
#backward or_e infer infer infer infer subgoal subgoal.
or_e [('P prop) -> ('Q prop) ('R prop)
(or pp PQ) -> ['P -> 'R] -> ['Q -> RR] -> 'R].
** Introduction rule for negation +/ #backward not_i.
not_i: [('P prop) -> ('P -> false] -> (not pP)] /* Elimination rule for negation */
not_e [(PP prop) -> (not 'P) -> pp -> false]. #backward exfalso.
exfalso [false -> ("P prop) -> PP]
/* Introduction rules for equivalence +/ #backward iff_i.
iff_i: [('P prop) -> ('Q prop) -> [P -> 'Q] -> ['Q -> PP] -> (iff d 'Q)
/* Elimination rules for equivalence */
#forward iff_el ('_: : (iff p 'Q)).
iff_el [(PP : prop) -> ('Q prop) -> (iff p 2Q) -> ['P -> []]
#forward iff_er (²_: : (iff d 'Q)).
iff_er : [(P : prop) -> ('q prop) -> (iff p QQ) -> [QQ -> PP]]
/* Excluded middle */ #forward em.
em [(P prop) -> (or d (not }P))]
D.3 Groups
= [(t type) -> 2t -> it -> prop].
G type.
op [G - G -> G)
id G.
/* Associativity */
#forward op_assoc ((op (op aa bb) cc) G))
as_assoc [('a G) ('b c) - ( : G) -> (= Cop (op 'a ²b) 'c) (op Cop bb )c))).
/* Commutativity */
#forward op_ comm (op a bb) G).
16

---

comm
[('a G) -> ('b G) -> (= Cop 'a (b) Cop "b Pa))].
/* Identity */
#forward id_1. id_1: [('a G) -> (= (op id 'a) *a)].
/* Inverse */
inv : -> G]. #forward inv_l.
inv_l [('a G) (= (op (inv aa) aa) id)].
E
Extrinsic evaluation problems
Here list all problems used in the extrinsic evaluation in Arithmetic and Propositional Logic.
E.1
Arithmetic
The following are the problems we extracted from from the Natural Number Game that (a) don't use previous lemmas, being reasonably provable straight from the axioms, (b) are about natural numbers (so, for example, this excludes the Proposition World, which essentially about propositional logic). The prefix in these problems tell which "world" of the game it came from: stands for the Tutorial World, a for the Addition World, and finally m is for the Multiplication World.
t_ example1. [('x : nat) -> (2y nat) -> ('z nat) -> (= (+ (* x y) 2) (+ (*x y) z))]
t_ example2. [('x : nat) ('y nat) (= 'y (+ 'x n7)) >> (= n2 'y) (* n2 n7)))
t_ example3. [('a : nat)
-> (?b nat) -> (= (s 'a) bb) -> (= (s (s 2a)) (s bb))]
add_dd_suee add__scc__zeee [('a nat) -> (=
(s 2)) (s 'a))]
a_ zerzzerrdee add. [('n : nat)
-> (=
'n)
'n)]
a add_assoc. [('a nat)
('b nat)
('c : nat) -> (= (+ (t a bb c) (+ 'a (+ "b .c)))
a succ_addd. [('a : nat) >> (*b nat)
>> (= (+ (s 'a) 1b) (s (+ aa bb)))
a
__succ_eq_add_ook
[('n : nat)
(= (s 'n) (+ 'n (s z)))]
n_zero_miu [('m nat) -> (= (* mm) z)]
m_ n_mul_one. [('m nat) -> (= (*
z)) m
Notably, we give below the full proof best agent for Arithmetic finds for _suuc__add
theorem a_succ_ade intro x nat.
[('a0 nat) -> ('al nat) -> (= (+ (s aa aa) (s (+ 2a aa1)))] {
apply nat_ind.
goal (= (+ (s x) 2) (s (t x 2))) {
show (= (+ (s x) 2) (s x)) by +_z.
show (= (+ x 2) x) by +_z.
show (= (+ 2)) by eq_symm
show (= (+ (s x) 2) (s (+ x 2))) by rewrite.
}
goal [('n : nat) -> (= (+ (s x) 'n) (s (+ x nn)) >>
(= (+ (s x) (s 'n)) (s (+ x (s 'n)))) {
intro x0 : nat.
intro x1 :
x) x0)
x0))).
show (= (s (+ x x (+ (8 x) x0)) by eq_symm.
show
(= (+ x0)
x0) (+) (+
(8 x0)) by rewrite.
show
(= (s (+xxxx))
(xxxxxx)))
by rewrite.
show
(= (+
x0))
(s x+xx by +_s.
show
(= (+ (s x0))
(+ (s x) x0)) by rewrite.
show
(= (s x0)
(+ (s x0))) by eq_symm.
show
(= (+ (s x) x0)
(+ (s x0))) by rewrite.
show
(+ x (s x0))
(+ x (s x0))) by rewrite.
show
(= (+ (s x) (s x0)) (s (+ (s x) x0))) by +_s.
17

---

show (= (+ (s x) (s x0)) (s (+ x (s x0)))) by rewrite.
}
This proof is not minimal - our human-writter Peano proof for this level of the game has 7 steps in the inductive case, compared to 12 in the proof the agent finds. Nevertheless, this is non-trivial theorem to prove by hand in this low-level axiomatic system, and our agent was not explicitly trained target this theorem. Thus, this shows that it does learn general patterns that are useful in proof search.
E.2 Propositional Logic
We here list all the statements in Theorem 41 of Kleene's book 220 "Introduction to Metamathemat- ics". represented in Peano:
1. [('A prop) ['A AA]]
2. [('A prop) -> ('B prop) -> ('C
prop) -> ['A -> 'B] >> [B CC] -> ['A -> C]]
3. [('A prop) ('B prop) ('C
prop) -> ['A -> [BB 'C]] -> ['B -> ['A 'G]1l
4. [('A prop) -> ('B prop)
- ('C prop) -> ['A -> [>B -> [(and ' 'B) -> 'C]]
5. [('A prop) ('B prop)
('C
prop) -> [(and 'B) 'C]
['A
['B
'[]]]
6. [('A prop) -> ('B prop)
-> ('C
prop) -> ['A -> 'B] -> [['B -> 'C] -> ['A -> *[]]]
7. [('A prop) -> ('B : prop) -> ('C
prop) -> ['A -> 'B] >> [['C -> 'A] -> ['C -> 'B]]]
8a. [('A prop) -> ('B prop) -> (
prop) -> [*A -> 'B] -> [(and 'A ²C) -> (and BB 2C)]]
8b. [('A prop) -> ('B prop) -> ('C prop) -> ['A -> 'B]
-> [(and 'C 'A) -> (and O 'B)]]
9a. [('A prop) -> ('B prop) -> (*C prop) -> ['A -> 'B]
-> [(or 'A *C) -> (or BB CC)]]
9b. [('A prop) -> ('B prop) -> ('C prop) -> ['A -> 'B]
-> [(or 'A CC) -> (or BB CC)]]
10a. I('A prop)
('B prop) -> [(not 'A) -> ['A -> 'B]]]
10b. I('A prop) -> ('B prop) -> ['A - [(not 'A) -> 'B]]]
11. [('A prop) -> ('B prop) -> ['B -> ['A -> 'B]]]
12. [('A prop) -> ('B prop) -> ['A -> 'B] -> [(not 'B) -> (not 'A)]]
13. [('A prop) (BB prop) -> ['A -> (not 'B)] -> ['B -> (not *A]]]
14. [('A prop) -> ('B prop) -> [(not 'A) -> 'B] -> [(not 'B) -> *A]]
15. [('A prop) -> ('B prop) -> [(not 'A) -> (not 'B)] -> [ -> *A]]
16. [('A prop) -> ('B prop) -> ['A -> 'B] -> ['B -> 'A] -> (iff 2A 'B)]
17a. [('A prop) ('B prop) -> (iff 'B) ['A -> 'B]]
17b. [('A prop) -> ('B prop) -> (iff
'A
1B) >> ['B -> 'A]]
18a. I('A prop) (BB prop) -> (iff 1B)
'B]
18b. [('A prop) -> ('B prop) -> (iff 'A (B)
>> PB >> 'A]
[('A prop) -> (iff 'A)]
20. [('A prop) -> ('B prop) -> (iff 'A 'B) >> (iff 'B 'A)]
21. [('A prop) -> ('B prop) -> (2C prop)
(iff 'A 'B) -> (iff CC)
(iff 'A CC)
22. [('A prop) -> (BB prop) -> ('C prop) -> [2A -> ['B -> c]]] ->
[(not (not 1A)) [(not (not BB)) -> (not (not 'C))]]]
23. [('A prop) -> ('B prop) -> [(not (not ['A -> B])]]
[(not (not 'A)) -> (not (not BB)]]]
24. [('A prop) -> ('B : prop) -> ('C prop) -> [(not (not [' -> BB))) ->
[(not (not ['B -> *[]))] -> [(not (not ['A -> 'c]))]]
25. [('A prop) >> ('B prop) ->
(iff (not (not (and 'A BB)) (and (not (not *A) (not (not BB))))}
We use the numbering from the book here there are 30 statements, even if the last one is labeled 25.
F Discussion: extension to other proof assistants
While our approach implemented in Peano, can principle extended to mainstream theorem provers like Lean and Coq. Peano's 's typing rules (a version of the Calculus of Constructions, without native inductive types) are essentially a subset of these systems' more expressive calculi, and its minimalism makes it particularly suitable for automated proof search. The most practical path to
18

---

integration would be similar to recent tools like Duper 19: embedding problems from the target system (e.g.. Lean) into a Peano representation. running the prover, and then reconstructing the discovered proofs in the original system. While developing Peano-to-I Lennen proof object translator would relatively straightforward given the simplicity of Peano's type system, translating arbitrary Lean problems to Peano would require significant more engineering effort (e.g.. we would need to generate explicit axioms for inductive types and quotients, which are not part of Peano). However, we believe simplified environment is valuable for investigating how self-improving agents can build towards deeper theorems, eventually being able to invent new definitions and accumulate a growing library (which MINIMO does not, yet). Once these capabilities demonstrated convincingly, the engineering investment in proof translation will become more compelling.
19

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We claim approach to training self-improving mathematical reasoning agent starting just from axioms. This demonstrated in axiomatic domains Section
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: Our key limitations are explicitly discussed in Section
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
20

---

Justification:
No theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: We list all of the axioms in Peano we use in the Appendix. For conjecturing, we use a public implementation of Synchromesh, together with the completion engine algorithm we describe in Section 3.1 The MCTS proof search procedure we use is standard, and present in previous papers with open-source implementations acknowledge that the paper required significant implementation, and thus reproducibility will be much easier with our code release, which will do after the submission.
42 Nevertheless,
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (c.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (c.g., to registered users), but it should be possible for other researchers to have some path to reproducing verifying the results.
21

---

5. Open access to data and code
Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Question:
Answer: [Yes]
Justification: We provide a zip file containing all of our implementation in our supplementary material, and the configuration files and commands used to the main experiments. This was also released on Github (httts: /ttp/ggtttbbb///// com/ appoesia/minima
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips... cc/
for more details.
While we encourage the release of code and data, we understand that this might be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to rum to reproduce the results. See the NeurlPS code and data submission guidelines (https
//nips.co ttt.cc//pbbb. waccc/pullc//eee www.///gg//eeeeeeeeeeeeeee httpg//ddd//oeeeubmimii Sww./Sooieisiiiiaaooaa wommiissiooiiicy for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: These are provided in the Appendix, and in the code release.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer:
[Yes]
Justification: Figures and contain standard error bands, together with a description of those in the captions.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emoo bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
22

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
If error bars reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We provided these details in the Appendix.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethics
Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics
Question:
Answer: [Yes]
Justification: our paper only uses synthetic data of formal mathematics, and thus not incurr in any of the issues listed in the Ethics guideline.
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. there a special consid- eration due to laws regulations in their jurisdiction)
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: We don't it foresee any social impact of work in its current form, since only train agents on synthetic data, collected from formal mathematical environments, and evaluate their behavior there.
Guidelines:
23

---

The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negatíve societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g.. gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our models have no such potential for misuse.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset used and, possible, include a URL
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
24

---

If assets are released, the license, copyright information, and terms of use in the thcode. has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, paperswi
batasets.papersstt
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is available online, the authors encouraged to reach out the asset's s creators.
13. New Assets
Question: Are assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: We provide README in code release, which plan to gradually improve in our open-source repository.
Guidelines:
The answer NA means that the paper does not release assets.
Researchers should communicate the details of the dataset/code/model part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: N/A
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: N/A
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
25

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
26


Reviews:
[{"review_id": "qV0pciEZAA", "reviewer": "Reviewer_8wJE", "summary": "This paper presents a new method for training LLM agents in mathematical reasoning, starting only from basic axioms. The main idea is to make the agent learn two skills together: coming up with hard math problems (conjecturing) and solving them (theorem proving). The authors use a language model to do both tasks, and they introduce clever ways to generate valid math statements and learn from failed attempts at proofs. They test their method on three areas of math: logic, arithmetic, and group theory. The results show that the agents get better at both making harder problems and solving them over time. Importantly, the agents can also solve some human-written math problems they weren't directly trained on.", "questions": "1. Did the authors consider evaluating the system on widely-used benchmarks like mathlib or mini-f2f? If not, what are the main challenges in adapting the approach to these benchmarks?\n2. How well does an agent trained in one mathematical domain (e.g., propositional logic) generalize to another (e.g., arithmetic)?", "limitations": "Yes", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1. The paper introduces a new way to train LLMs for math, starting only from basic rules (axioms). It makes the LLM learn to create hard math problems and solve them at the same time, which is different from other methods that use lots of human-made math examples.\n2. The authors use smart techniques to make their method work well, like special ways to generate valid math statements and learn from failed attempts. They test their method on three different areas of math, showing it works in various situations. The paper explains these ideas clearly, though some parts might be hard for people who don't know much about certain math topics.\n3. This work could lead to AI systems that can do math research on their own, without needing human-made examples. This might help discover new math ideas in areas people haven't explored much. It's also important for making LLM that can think and create on its own, not just follow human instructions.", "weaknesses": "1. The current approach does not accumulate a growing library of proven theorems, which limits its ability to tackle more complex mathematical problems efficiently. This restriction to essentially \"cut-free\" proofs could become a significant bottleneck as the complexity of the target domain increases.\n2. The paper doesn't show how this new way compares to other neural ATP methods. This makes it hard to know how good it really is.\n3. The authors didn't try their model on standard math problem sets like mathlib or mini-f2f, which many other neural ATP methods use. This makes it hard to compare their results to other research.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the through review and encouraging comments about our work, especially about not relying on human-made examples. We answer the questions below, but are happy to engage further.\n\n> The current approach does not accumulate a growing library of proven theorems, which limits its ability to tackle more complex mathematical problems efficiently. This restriction to essentially \"cut-free\" proofs could become a significant bottleneck as the complexity of the target domain increases.\n\nThat's correct, we acknowledge this current limitation in the paper. We note that accumulating a library by itself is not technically challenging – the main open research problem here is to determine what theorems are worth adding to the library. This might require some metric for the interestingness, or usefulness, of a theorem. These are important but still understudied topics in mathematical discovery, as most current work on AI for mathematics only focuses on solving a target set of problems, not discovering new theorems autonomously. Our work sets up an experimental foundation for future work to explore these metrics and empirically observe what libraries they end up discovering.  \n\n> The paper doesn't show how this new way compares to other neural ATP methods. This makes it hard to know how good it really is.\n\nOur work contributes both a new problem setting where an agent bootstraps itself from only the axioms of a domain, and a pipeline for learning in this setting. One of the components of this pipeline is the prover (ATP) agent, but the pipeline is agnostic to the specific neural ATP method that the prover employs. Our specific ATP is most similar to Holophrasm [1], using MCTS with learned value and policies, as has become standard since then. But any other proof search method from prior work, like HTPS, could also work with our pipeline, complementing the other components (conjecturing, and the outer learning loop). Thus, our pipeline is not a direct competitor to other neural ATP methods, but rather a novel method for bootstrapping one using no pre-existing training data. To the best of our knowledge, our system is the first to learn entirely from self-generated conjectures, without requiring human training data. This is our main contribution.\n\n> Did the authors consider evaluating the system on widely-used benchmarks like mathlib or mini-f2f? If not, what are the main challenges in adapting the approach to these benchmarks?\n\nWe emphasize that the focus of our contribution was mathematical discovery and self-improvement, jointly learning to conjecture and prove theorems starting only from axioms, but crucially no pre-training data. This is fundamentally different from approaches that rely on massive pre-training on existing problems, which is common to the methods typically evaluated on mathlib or minif2f. \nWhile we hope that agents trained in a setup like ours will eventually be able to rediscover much of mathlib and solve problems from minif2f, there are still scalability challenges that require further research (such as in accumulating a library, discussed above) before benchmarks like minif2f become within reach. However, if we can overcome those challenges, our approach in principle can work in new mathematical domains, whereas it's still not clear how methods that require massive pre-training to do well will be capable of that generalization.\n\n> How well does an agent trained in one mathematical domain (e.g., propositional logic) generalize to another (e.g., arithmetic)?\n\nWe attempted to initialize an agent for one domain using the last checkpoint of another to evaluate transfer, but did not observe any improvements. We will note this in the appendix. We believe that this is just due to overfitting, since the three domains we tested are very different from each other (for instance, axiom names, types, etc, are all different, thus completely unseen when the agent starts in the new domain). We believe that bootstrapping on a significantly wider spanning set of domains, coupled with library learning, might be enough to observe transfer.\n\nWe also note that we provided more examples of conjectures and proofs in the global response.\n\nThanks again for the review! We'd be happy to answer further questions.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "SlcflkBvli", "reviewer": "Reviewer_viHR", "summary": "The authors investigate a novel setting for ML-based formal theorem proving, where the proving agent in addition to learning to prove theorems at the same time learns to propose conjectures. The process is composed into a self-improving feedback loop that starts just from axioms and continues to prove increasingly difficult self-generated conjectures. The hindsight relabeling method is introduced that extracts training data points even from the failed proof searches, which improves the learning process.", "questions": "How the conjecture generation is conditioned on the difficulty level?\n\nHow do you tokenize formulas?\n\nHow exactly do you calculate the average proof log-likelihood (Figure 2):\n- how do you incorporate the failed proof attempts into the average?\n- what is the set of conjectures you compute the average for: is it across a new batch of 200 conjectures, or the old ones (which were used for training the prover) are also used?\n- are the conjectures from hindsight relabeling taken into the average here?\n\nIs it correct that the lines in Fig. 2, right, for the policies from iterations 0 and 1 are completely overlapping?\n\nWhy do you display the proof log-likelihood instead of perhaps more interpretable metrics like the proving success rate for a batch of new conjectures or the average length of a proof search / a proof size?\n\nWhy group theory is missing from the evaluation presented in Fig. 4?\n\nIs the success rate in Fig. 4 computed independently per each iteration, or rather cumulatively (taking union of theorems proved in all the past iterations)?\n\nCould you provide a list of requirements to create a Python environment for running the supplemented code? I would like to test it, but there is no detailed installation instructions.", "limitations": "The authors correctly identify the major limitations of their approach.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "Formal theorem proving is a great challenge for testing and developing AI approaches. In contrast to natural language mathematical settings, the formal environment provides grounding not allowing for any mistakes by the ML agent.\n\nThe topic of conjecturing is an interesting one and at the same time very much under-explored. Moreover, combining proving and conjecturing is novel and, as far as I know, was not researched before.\n\nThe proposed setting is arguably quite simple, but as this is one of the first studies of this kind it is justifiable and actually beneficial -- it allows to more precisely control and understand the whole learning process, which may inform some follow-up studies.\n\nThe authors provide code for the Peano environment and for reproducing the learning experiments.", "weaknesses": "As the presented setting is limited (simple conjectures generated, no mechanism for abstracting reusable lemmas), it is not clear to what extent the proposed methodology will transfer to fully-fledged formal proving environments like Lean, Coq, or other ITPs. (The authors are aware of this limitation and they mention it in Section 5.)\n\nThe presented experiments are small: only five iterations of conjecturing-proving loop are run.\n\nSome hyper-parameters of the experimental setup are fixed in an ad hoc manner without performing any grid searches (n. of conjectures generated per iteration, n. of expansions in the MCTS). It would perhaps be good to measure the effect of some of these parameters.\n\nIt would be interesting to see more metrics tracked across the learning iterations for better insights about the process, for instance:\n- the average length/syntactic complexity of the generated conjectures,\n- the average length of a proof per iteration,\n- the duplication rate between consecutive batches of generated conjectures.\n\nSome details of the method are not specified clearly (see my questions below).\n\nMinor:\n- evaluate as -- evaluated as (the caption of Fig. 2)", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the through and encouraging assessment of our work! We provide clarifications below, and would be happy to answer any questions that remain.\n\n> How the conjecture generation is conditioned on the difficulty level?\n\nOnce we attempt to prove a conjecture, we obtain a difficulty evaluation (failed, easy or hard, where easy and hard are relative to the batch of conjectures that were attempted). Using this feedback, we then generate training examples (strings) where the difficulty comes first, followed by the statement of the conjecture. For example (examples generated from the first conjecturing iteration of a run on propositional logic, after running proof search on this batch):\n\n```\n\"Conj:(fail) false\"\n\"Conj:(triv) (iff (not (not (not false))) false)\"\n\"Conj:(hard) [('a0 : (or false false)) -> false]\"\n```\n\nAll these conjectures were first sampled by conditioning on \"Conj:(hard) \" (the conjecturer starts untrained, so initially that doesn't mean anything to it). Then, after training on the strings above, in addition to the examples from proof search, we sample again the next batch of conjectures.\n\n> How do you tokenize formulas?\n\nWe used character-level tokenization. Since we assumed no initial data to train a BPE tokenizer, we found this to be the simplest, more general choice.\n\n> How exactly do you calculate the average proof log-likelihood (Figure 2):\n\nA proof p corresponds to a sequence a_1, …, a_n of actions in the search tree. For the proof log-likelihood, we average the log-likelihood of each action being taken at the corresponding state. So if the starting state is s_0, that is the average of log p(a_1 | s_0), log p(a_2 | s_1), and so on. Each s_k is obtained by taking the action in the proof from the previous state. Each of these probabilities is a readout from the policy LM. The closer this probability is to 1, the more likely is this proof for the LM; correspondingly, the faster MCTS will explore these paths and find this proof during proof search.\n\n> how do you incorporate the failed proof attempts into the average?\n\nIn Figure 2 we only analyze conjectures that were proved (4.1, L302). We cannot compute the likelihood above if we indeed find a proof (since p appears in the formula). However, given one proof, we can evaluate its likelihood under any policy, even if previous policies assign much lower likelihood to it (and thus would take longer search, or time out, in finding it). We show and discuss the fraction of proved conjectures at each iteration in Appendix C.\n\n> what is the set of conjectures you compute the average for: is it across a new batch of 200 conjectures, or the old ones (which were used for training the prover) are also used?\n\nOnly new conjectures that were proposed at each iteration. They are guaranteed to be (at least syntactically) different from previous ones, since we reject samples that have been seen in the past.\n\n> are the conjectures from hindsight relabeling taken into the average here?\n\nNo, only the conjectures in the batch are.\n\n> Is it correct that the lines in Fig. 2, right, for the policies from iterations 0 and 1 are completely overlapping?\n\nThat's right, they were nearly indistinguishable. \n\n> Why do you display the proof log-likelihood instead of perhaps more interpretable metrics like the proving success rate for a batch of new conjectures or the average length of a proof search / a proof size?\n\nThere are two main reasons for using the likelihood compared to success rate:\n- It can be seen as a sort of continuous version of the success rate. We found that the more likely the proof is under a policy, the faster MCTS reaches it. Thus, whether MCTS finds it within the budget depends on the search cut-off, whereas the likelihood doesn't (even two policies that both fail, or both succeed, on the same problem can still be differentiated by the likelihood).\n- Although closely related, it is much faster to compute. While proof search can take 1-4 minutes depending on the problem and with the search budget we used, the likelihood can be computed in a second. This makes larger scale analyses feasible, such as the one in Figure 3 (> 50k proof-policy evaluations).\n\n> Compared to proof size, the main advantage is that the likelihood takes into account the branching factor. There are long proofs that are nonetheless easy because there aren't many options at each step (e.g., most are 'intro').\nIs the success rate in Fig. 4 computed independently per each iteration, or rather cumulatively (taking union of theorems proved in all the past iterations)?\n\nIndependently.\n\n> Could you provide a list of requirements to create a Python environment for running the supplemented code? I would like to test it, but there is no detailed installation instructions.\n\nWe apologize, our release script ignored .txt files, but that included requirements.txt. Here is the content of this file (in `learning`):\n\n```\naltair\nbottle\ncoloraide\nhydra-core\nmaturin\nnumpy\nomegaconf\nredis\nrq\nsympy\ntorch\ntqdm\ntransformers\nwandb\ncelery\n```\n\nmaturin installs an executable (called maturin) that allows you to compile and install the Peano Python package easily. You can go to environment/ and run maturin develop –release to both build and automatically \"pip install\" the package in your local environment (after that, `import peano` should work from Python). We will expand broadly on our tutorial in the public code release.\n\nFor an additional analysis of the generated conjectures across iterations, please refer to our global response.\n\nWe will update the paper to incorporate these descriptions that were missing or confusing. We again thank the reviewer, and would be happy to discuss or clarify further!", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ebDLnYcrq6", "reviewer": "Reviewer_6DqB", "summary": "This paper proposes to create mathematical agents by jointly learning to posing challenging problems (conjecturing) and solving the problems (theorem proving). Specifically, they use a randomly initialized Transformer to perform both conjecturing and proof search in a loop.", "questions": "Q1: How to guarantee f_C soundness and completeness?\nQ2: In Figure 2, propositional logic, the search baseline policy at iteration 0 seems missing. \nQ3: According to Appendix B and Figure 5, the authors use the likelihood of the proof under the policy as a measure of difficulty. To what extent is the distinction of the difficulty between the log-likelihood of -13 and -1? Could you please provide some cases for each? \nQ4: Figure 2 shows diminishing gains in conjecture and policy iteration 4. Does it mean approaching the saturated performance? How to decide the number of iterations? \nQ5: How many evaluated theorems are in the Natural Number Game dataset?", "limitations": "The authors have adequately addressed the limitations.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The proposed method is demonstrated generating more difficult conjectures and obtaining better theorem proving policy over several iterations. Experiments are also conducted on proving human-written theorems.", "weaknesses": "1. Further justification of using log-likelihood as the main evaluation in this paper. \n2. How does this method facilitates solving dataset such as miniF2F and mathlib?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the encouraging review of our work! We provide clarifications below, and would be happy to answer any questions that remain.\n\n> Further justification of using log-likelihood as the main evaluation in this paper.\n\n- It can be seen as a sort of continuous version of the success rate. We found that the more likely the proof is under a policy, the faster MCTS reaches it. Thus, whether MCTS finds it within the budget depends on the search cut-off, whereas the likelihood doesn't (even two policies that both fail, or both succeed, on the same problem can still be differentiated by the likelihood).\n- Although closely related, it is much faster to compute. While proof search can take 1-4 minutes depending on the problem and with the search budget we used, the likelihood can be computed in a second. This makes larger scale analyses feasible, such as the one in Figure 3 (> 50k proof-policy evaluations).\n\n> How does this method facilitates solving dataset such as miniF2F and mathlib?\n\nWe emphasize that the focus of our contribution was mathematical discovery and self-improvement, starting only from axioms, but crucially no pre-training data. This is fundamentally different from approaches that rely on massive pre-training on existing problems, which is common to the methods typically evaluated on mathlib or minif2f. While we hope that agents trained in a setup like ours will eventually be able to rediscover much of mathlib and solve problems from minif2f, there are still scalability challenges that require further research (such as in accumulating a library, discussed above). If those are overcame, then this would be one path to impacting those benchmarks. Another path would be to investigate a setup similar to what we propose, but starting with a pre-trained LLM. Conjecturing can help expand the existing training data, and potentially improve performance on the benchmarks. However, it's still unclear whether this would generalize to domains beyond those seen in pre-training, such as those already on mathlib. Our goal was to not have this dependency.\n\n> Q1: How to guarantee f_C soundness and completeness?\n\nCompleteness is given by the fact that the completion engine expansion rules (L193-201) consider all of the typing rules in Peano (which are few). Thus, given any valid conjecture c, the choices that have to be made to generate c have to fall in one of these cases. Soundness relies on the soundness of unification in Peano, but is basically the fact that at each step we either directly give out an object from the context from the desired type (which is sound), or give the result of a function that Peano believes can produce the desired type (by unifying the type with the result type of the function). \n\n> Q2: In Figure 2, propositional logic, the search baseline policy at iteration 0 seems missing.\n\nIt is there, but almost coincides with iteration 1. We generally found little improvement in the policy in propositional logic after a single iteration, but it starts to pick up later.\n\n> Q3: According to Appendix B and Figure 5, the authors use the likelihood of the proof under the policy as a measure of difficulty. To what extent is the distinction of the difficulty between the log-likelihood of -13 and -1? Could you please provide some cases for each? \n\nPlease refer to the global response for additional examples in each domain with their likelihoods. We will include these in the appendix.\n\n> Q4: Figure 2 shows diminishing gains in conjecture and policy iteration 4. Does it mean approaching the saturated performance? How to decide the number of iterations?\n\nYes, the policies start to converge at that point. We believe that this is due to the main limitation we highlighted in Section 5: our agent still can't come up with new definitions, or reuse past theorems. As a result, the way the agent finds to produce harder conjectures is to make the statements more convoluted. But in human mathematics, even deep, interesting theorems tend to have short statements (posed in terms of the right high-level definitions). Our main contribution is to set up a self-improvement pipeline where future work can tackle the open problem of understanding how to build towards \"interesting\" deeper theorems. If this is achieved, then in principle there would be no limit to how many iterations one could run for, as the agent would be able to keep raising the level of abstraction of the theorems it discovers (which our current agent does not yet do).\n\n> Q5: How many evaluated theorems are in the Natural Number Game dataset?\n\nThe whole game (in the website) contains 83 unique theorems. Since in its current form our method doesn't yet accumulate a library with its previously proved theorems, it can only plausibly prove the levels that only refer to the axioms (rather than previous lemmas), which leaves 10 theorems spread across the first 3 \"worlds\" in the game (Tutorial, Addition, Multiplication). We included all these problems in Appendix E.\n\nThank you again for the comments and questions! We'd be happy to answer any further questions, or discuss these in more depth.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "xO6FfVacPa", "reviewer": "Reviewer_XdUe", "summary": "The authors propose a novel approach to formal theorem proving (FTP) that leverages a language model's self-improvement capabilities by framing mathematical theorem proving as a sequential game involving generating a conjecture to be proven, and then proving it, and so forth. The approach consists of two primary steps: first, the authors use a constrained decoding approach to generate mathematically valid conjectures of a target difficulty, treating an arbitrary language model (LM) as a probability distribution over conjectures in a given domain. Then, the generated conjectures are solved using an MCTS-guided policy, which allows for backtracking-based relabeling for improved reward shaping signal during policy learning. Experimental results conducted in the Peano language on three different domains of theorems show that the proposed approach can find increasingly challenging conjectures and train a policy that solves them, and that this learned policy can also solve human-written conjectures of interest.", "questions": "* Later iterations of the policy seem to be a bit worse on (or consider a bit harder) \"easy\" conjectures, and seem to do better on (or consider to be easier) \"harder\" conjectures (as evidenced by Fig. 2.)  Why do these further trained policies have more trouble discerning what is \"easy\" and what is \"hard\"? Is it just generally 'good' at solving all conjectures? Or would it be useful to have a curriculum-style approach that occasionally asks \"easy\" conjectures even later in training?\n* Why do we start with a randomly initialized Language Model? How does the choice of Language Model affect the performance of conjecture generation?\n* I didn't seem to fully understand how the approach chooses a specific difficulty of conjecture generator. I understand where difficulty 'scores' come from, but how do we choose a conjecture based on its difficulty?\n* Can the authors provide explanation for if/how to apply the approach to environments like Coq and Lean?", "limitations": "Limitations are discussed in the paper but there are some questions about the limitations of the approach and its applicability to other environments (that I have detailed above.)", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 4, "contribution": 3, "strengths": "* Self-guided improvement of LLMs is a powerful paradigm that has shown novel improvements in a number of challenging areas, such as code generation and prose writing. Approaching the important problem of automated theorem proving from a lens of self-improvement is novel and valuable and I believe can provide a foundation for a new class of approaches to LLM-guided FTP.\n* The game-theoretic framing of the problem is intuitive and MCTS, under the structure that the Peano environment provides, is a smart way to frame policy learning that makes hindsight relabeling efficient. The usage of hindsight relabeling to further guide conjecture generation and policy training is valuable.\n* The paper is very well written and generally easy to follow.", "weaknesses": "* There is a substantial body of work on the self-improvement of LLMs that I felt was not adequately addressed by the authors. Although I am not familiar with an existing self-improvement approach in the space of FTP specifically, there are numerous works like [1] that allow LLM-generated content to improve themselves. The paradigm proposed in this paper is not exactly the same, but a comparison to and acknowledgement of this related work should be included. The 'mathematical conjecturing' section of the related work could be condensed (or moved to the appendix) in favor of covering this topic that appears to have more recent and relevant literature.\n* The MCTS policy and learning approach was a bit light on detail. What exactly is the state for the MCTS policy? What are the details of each operator in the MCTS approach? This information will help the reader understand just how general the approach proposed is for general FTP and not just Peano-based domains. This could be included even in the appendix.\n* To the previous point - it would be nice to see the authors include a more thorough discussion regarding if and how their approach could extend to popular theorem proving environments like Coq and Lean. Is it applicable? Why or why not? The strongest addition would be to actually show the approach in one of these environments. I don't think it's necessarily a knock on the approach to be instantiated only in Peano, but the community would greatly benefit from an instantiation of this approach in Coq or Lean, or at least a discussion of how and why this can be done.\n* The idea of using the (fixed) learned policy itself to evaluate 'difficulty' of conjectures does not totally inspire confidence in the claims made in the paper. Is there a qualitative analysis for RQ1 that can be done on these conjectures to show that they indeed become harder over time? \n\nOverall, I think the contribution is novel and of great interest to the community, but I am left unsure about a lot of details regarding the approach and its design decisions. I am happy to increase my score based on the authors' response. \n\n[1] Language Models Can Teach Themselves to Program Better. Haluptzok et. al. ICLR 2023.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the through review and encouraging comments! We agree that several of the clarifications you requested should be addressed in the paper, and will do so (including the additional examples in the global response).\n\n> There is a substantial body of work on the self-improvement of LLMs that I felt was not adequately addressed by the authors.\n\nWe agree. Some prior work has also focused on self-improvement on informal math (eg GSM8k), which is also relevant, though none that we know of do it for FTP or without pre-training data. We will acknowledge this literature and add references accordingly.\n\n> MCTS was a bit light on detail. What exactly is the state for the MCTS policy? [...]\n\nThis makes sense, we will include concrete examples of states and MCTS expansions in the Appendix. The state in Peano has the same form as the proof state in the interactive modes of Coq and Lean – a set of objects with their types, and a goal type. We just represent it as a string to feed to the Transformer model, so nothing Peano-specific in what the LLM does. One random example:\n\n\"State: { x : G, x0 : G }\\nGoal: [('a2 : G) -> (= (op id 'a2) 'a2)]\"\n(the state has two elements of the group G and still has a 'forall a2 : G, id * a2 = a2' in the goal)\n\nThe proof search method we use is broadly similar to the instantiations of MCTS is used in recent prior work like in gpt-f or Holophrasm. The main difference is that, since Peano has a finite action space, we don't sample the action as a sequence of tokens from the policy, but rather just score the enumerated actions using the LM. Other search algorithms, like HTPS, can well be used in our setup as well instead.\n\n> To the previous point - [...] discussion regarding if and how their approach could extend to popular theorem proving environments like Coq and Lean\n\nYes, good question! Peano's typing rules are essentially a subset of Lean's and Coq's (CoC vs CIC, with variations), and its simplicity makes it more appropriate to do proof search in it. It would be relatively simple to develop a Peano -> Lean proof object translator, that takes proof objects found in Peano and generates the equivalent Lean proof object. The opposite direction would take more engineering work, but is also possible (the additional complexity of the Lean type system makes it much more convenient for users, but is not fundamentally required to represent mathematics). Thus, to make our approach available in Lean (for instance), the shortest path is likely to be something like the recent Duper (https://github.com/leanprover-community/duper), which takes the problem in Lean, translates it to the external prover, calls the prover, and then attempts to reconstruct the proof in Lean. We think Peano's more minimal type system makes it suitable to investigate how to get the self-improving agent to eventually build towards much deeper theorems (making new definitions and a library on the way), and at the point where that works it will pay off to spend the engineering effort to build proof object translators.\n\n> Is there a qualitative analysis for RQ1 that can be done on these conjectures to show that they indeed become harder over time?\n\nPlease refer to the global response for examples of conjectures that show up during training. We will include those (for all 3 domains) in the Appendix. Overall, we see both the longest proofs that the agent is capable of finding getting longer, as well as the hardest conjectures being more complex. Since the agent still doesn't make new definitions or reuse past lemmas, the conjectures however don't yet evolve in complexity in a human-like way, which we believe to be an extremely interesting direction for future work that our setup can be used to explore.\n\n> Later iterations of the policy seem to be a bit worse on (or consider a bit harder) \"easy\" conjectures\n\nThat's true, we do seem to observe a distribution drift over time in terms of conjectures. As the conjecturer starts to focus on hard ones (which in this case, since the agent doesn't make up new definitions to shorten higher-level statements, tends to mean longer conjectures), the policy seems to be slightly more uncertain in easier problems than the policy at iterations 1-2 (which have been trained more recently on easier conjectures). Yes, we believe a curriculum-style approach could be useful to mitigate this behavior. However, in terms of proof search, this uncertainty tends to not be that much of a problem in easier conjectures because they have either shorter proofs or lower branching factor (thus, MCTS still finds the proof even if the agent prioritizes other branches at first).\n\n> Why do we start with a randomly initialized LM? How does the choice of LM affect performance?\n\nOur main goal is to build towards a self-improving pipeline that does not require pre-training data, much like AlphaZero did for board games. If this is achieved, then our agent will be able to produce mathematics in both existing domains for which we have plentiful training data, and for novel domains for which we do not. For the LM, we chose a standard GPT-2-based Transformer architecture, but we don't believe this is crucial to the idea, as work in LLMs generally show that scale and data matter more than architecture details (sticking to Transformers specifically).\n\n> [...] how the approach chooses a specific difficulty of conjecture generator.\n\nWe always try to generate hard conjectures. Here, \"try\" means that we condition the Transformer on the 'hard' difficulty. After proof search on a batch of samples, we get the actual observed difficulty by whether the prover succeeded and, if so, the log-probability of the proof under the current LM. That feedback signal is then used to further train the conjecturer (by generating LM training examples where the conjecture's statement is paired with the observed difficulty, rather than always 'hard').\n\nThanks again for the review. We're happy to engage or clarify further!", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "bMOqZ7cCv2", "reviewer": "Reviewer_awrR", "summary": "This work targets the problem of formal theorem-proving, in the particular setting where a learning agent starts only from axioms (contrary to most other works which use models trained on a plethora of mathematics data already) similar to an AlphaZero style setup. They use a single neural model (transformer) to learn to (1) produce conjectures (2) a distribution over proof steps (3) a value function for proof search. In an alternating process, conjectures are sampled from the model using constrained decoding, on which proof search is then attempted, yielding data for further training, with the goal of producing a model capable of generating harder conjectures as its proof-writing ability increases. They also incorporate hindsight relabeling in this setting. The results indicate that the model does learn to generate harder conjectures and become better at proving them. On a set of known theorems from arithmetic and propositional logic, the model is capable of improving as it learns to prove more of the conjectures it generates.", "questions": "1. Given the simple evaluation domains, the lengths of proofs for conjectures (measured in # of tactics) at the end of each iteration could be a useful indicator for how the both how the proof search improves over time, and how difficult the conjectures become. Can you report numbers measuring problem difficulty as length of proofs? Can you include examples of proofs found over iterations?\n\n2. How often does the conjecturer produce \"trivial\" conjectures? Do you have any measure as to how sound the completion engine is as iterations proceed? I imagine that the first round of conjectures is entirely random given the model is untrained. Can you include examples of conjectures produced over the iterations?\n\n3. It seems unclear whether this sort of learning in multiple phases is better than just performing one single phase. In AlphaGeometry (https://www.nature.com/articles/s41586-023-06747-5), though geometry is a particularly pointed domain, all data is generated upfront and then a model is trained. In this paper, the extra training data produced from hindsight relabeling is crucial, they indicate on line 336 that the approach does not reach its intended goal without it. Perhaps upfront training may be better? It could be the case that by placing a somewhat more complex distribution on the constrained decoding, one can generate many harder yet valid conjectures without learning a transformer first. Can the authors comment on this?\n\n4. On page 22, Is the supplied full proof for a_succ_add exactly that found by the proof search? For example, is the step \"show (= x (+ x z)) by eq_symm\" predicted by the model, or just \"eq_symm\"? Similarly does the model produce \"intro x1 : (= (+ (s x) x0) (s (+ x x0)))\" or just \"intro x1\".\nIf the case of the former, does the Peano language automatically enumerate all relevant types and reachable hypotheses? Otherwise generating a type like \"(= (+ (s x) x0) (s (+ x x0))\" might make the action space infinite?\n\n5. The performance of the last checkpoint compared to the initial checkpoint on the propositional logic extrinsic set is not very different, can you comment on why this might be the case? That extrinsic set, as specified on page 23, does not seem to be particularly challenging?\n\n6. Sampling conjectures from a small model should be fairly quick. Can the authors comment on how much time is spent generating conjectures and proving conjectures separately? Only the aggregated number is reported in the appendix section A.", "limitations": "I believe the authors have adequately addressed the limitations and broader societal impacts of their work.", "rating": 6, "confidence": 4, "soundness": 1, "presentation": 2, "contribution": 3, "strengths": "The paper discusses a question of great significant in the field of AI-for-mathematics: How can we produce systems which can learn from scratch (from axioms)? The topics of conjecturing and proving have, as far as I know, not been heavily investigated $\\emph{together}$ and this work serves as a nice exploratory piece on this area, which I suspect will become more popular. While there are prior works on RL for theorem proving, the use of intrinsic motivation from RL in this field is a first, to the best of my knowledge.", "weaknesses": "1. Lack of evidence: While conjecturing is a main component of the approach, examples of conjectures provided by the model (at any stage) are not provided neither in the main content nor in the appendix. It is hard to judge the quality of such conjectures or to empirically see an improvement in conjecture difficulty over phases when none are provided.\n\nSimilarly, only a single proof is included in the entire submission, in the appendix. It is useful for the reader to get a sense of what kinds of proofs the model is finding, especially amongst each of the three domains, on both extrinsically defined goals and those the conjecturer comes up with.\n\nAdditionally, only the propositional logic and arithmetic tasks have an extrinsically defined set of theorems for testing. Why is a similar set not included for the abelian group task? Judging from Figures 2 and 3, the learning dynamics for the group theory task are different than the other two tasks.\n\n2. Conjecturing & intrinsic motivation: It is unclear how much the agent itself is producing conjectures that it is intrinsically motivated to solve. As I understand it, the conjectures are generated via a constrained decoding on the language model, but I'm not sure how much the LM would actually generate conjectures without the constraint after being trained for a while. How much is the conjecturing really improving, given that at the end of each proof search round, only 10% of conjectures are considered hard, 40% easy, and the rest trivial. Perhaps it is better to discretize difficulty based on proof length? \n\n3. Poor scalability: Even with the modest compute resources as described in the appendix, the tasks are quite simple, as are the extrinsically defined goals, which the model shows improvement on mostly on the arithmetic task sourced from NNG. On the propositional logic task, the model at the end of the fifth policy can only solve 4(?) more of 30 problems as compared to the randomly initialized model from the 0th iteration on the policy.\n\nSome typos I noticed:\n1. Line 169: \"Mathematically, $\\mathcal{C}$ is a function $f_{\\mathcal{C} : \\Sigma* \\to $...\" but $\\mathcal{C}$ is a set.\n2. Line 245: \"levarage\" -> leverage\n3. Figure 2 caption: I think you meant \"evaluated\"\n4. Line 341: \"recevies\" -> \"receives\"\n5. Line 345: \"training tends to collapse to ? by\"", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the through assessment of our work, and the comment on the significance of our research question! We provide responses below, and additional examples in the global response.\n\n> Can you report numbers measuring problem difficulty as length of proofs? Can you include examples of proofs found over iterations?\n\nPlease refer to the global response for numbers on the proof length per iteration. We also included a few examples of proofs with the lowest log-probs found during training (proofs found on average get longer).\n\n> How often does the conjecturer produce \"trivial\" conjectures? Do you have any measure as to how sound the completion engine is as iterations proceed? I imagine that the first round of conjectures is entirely random given the model is untrained. Can you include examples of conjectures produced over the iterations?\n\nAt first, most of the conjectures that are successfully proved are trivial (we analyzed provability in Appendix C), and many are trivially false (e.g. '!!false' in propositional logic). Hindsight replay allows the agent to uncover non-trivial conjectures and learn. We refer to the global response for concrete examples of conjectures.\n\n> It seems unclear whether this sort of learning in multiple phases is better than just performing one single phase, like in AlphaGeometry. [...] Perhaps upfront training may be better? Can the authors comment on this?\n\nGood question! Earlier in the project, we did consider trying something like the AlphaGeometry approach. There are two main challenges for this. One is that, in AlphaGeometry, problems and solutions are simultaneously generated in the forward direction only, both simultaneously, by creating new hypotheses and applying forward deduction. While that works for the Euclidean geometry axioms, it does not generalize easily to a general formal system like dependent type theory. As an example of where it becomes hard, in arithmetic, our conjecturer generates several statements that are then proved by induction (as it is likely to generate something equivalent to forall ('n : nat), …). For these conjectures to be produced in the forward direction, like in AlphaGeometry, we would need to independently stumble upon proofs of matching base and inductive cases without actually planning to do so. It's also not entirely clear how the proof of the inductive case would be generated in the forward direction, without having a goal. The other challenge is that AlphaGeometry also relied on an existing, complete, domain-specific deductive closure solver for Geometry to generate data, which our approach for data generation doesn't require (and which doesn't exist for dependent type theory, given that the deductive closure can be infinite).\n\n> On page 22, Is the supplied full proof for a_succ_add exactly that found by the proof search? [...] does the Peano language automatically enumerate all relevant types and reachable hypotheses?\n\nWe reconstruct the proof in Peano concrete syntax from the proof search tree as it is found (to get the equivalent proof as if human-written), though at each step the model gets the proof state, current goal, and only chooses the next step. But you are correct, Peano enumerates the relevant types and reachable hypotheses. So for 'intro', which takes the next universally quantified variable from the goal into the state, it suffices for the model to choose 'intro' as an action, as the rest is forced (both the name - we just generate a numbered identifier, and its type is taken from the goal by Peano). For 'eq_symm', eq_symm can be applied to any equality currently in the state, so Peano will enumerate those (not with a particular algorithm for eq_symm, just looking at the type signature of eq_symm). So in this case the policy first chooses 'eq_symm', then chooses one of the valid results to get from it in the current state.\n\n> The performance of the last checkpoint compared to the initial checkpoint on the propositional logic extrinsic set is not very different, can you comment on why this might be the case?\n\nGiven that our agent is only trained on its own self-generated problems, there is no a priori guarantee that it gets better at solving human-written problems, which are only a very small subset of what is formally true (one open problem is how to characterize this subset that we find interesting, to focus discovery on it). Looking at the conjectures generated and proved by our agent, it is clear that they do not generally resemble human theorems. (see examples in the global response)\n\nThus, our extrinsic set served just to give a signal of whether there is some intersection between where the improvements take place and the set of problems that are interesting to humans. We observe some improvement, although it is still small in absolute terms, as you point out. We think a really interesting and important problem that this suggests is exactly how to structure the learning process so that the conjectures evolve in better alignment with theorems that are interesting for humans. Our setup can serve as a starting point for this investigation.\n\n> Sampling conjectures from a small model should be fairly quick. Can the authors comment on how much time is spent generating conjectures and proving conjectures separately? Only the aggregated number is reported in the appendix section A.\n\nYou are correct, conjecture generation in each iteration is fairly quick. Sampling 200 new, unique conjectures takes 1-3 minutes in each iteration, whereas proof search on 200 conjectures takes 2-4 hours of compute (which our implementation distributes across several prover processes, since proof attempts in each batch are independent). Sampling is mostly GPU-bound, while proof search also spends measurable time on Peano enumerating actions during MCTS, especially in deep states where the state can get large.\n\nThank you again for the detailed review. We're happy to engage further if any other questions remain!", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
We thank all reviewers for the detailed evaluations of our submission. We appreciate the general comments on the novelty of our conjecturing and proving loop. One common request was to show more examples of conjectures and proofs as they evolve during training. We provide examples here (all *sampled* conjectures, not from hindsight). Due to space, we show iterations 0, 2 and 4 for groups, with some complete proofs, and summaries for other domains.

# Groups

## Iteration 0

**Avg. proof length**: 2.67 steps

**Avg. proof length on 'hard' conjectures**: 3.67 steps

### Hardest 3 problems:

Conjecture: `[('a0 : (= id (op id (op id (op (op (op id id) (inv id)) (inv (op id id))))))) -> (= (op id (inv id)) id)]`  (Proof Logprob: -8.51928925095947, 4 steps)

Proof:
```
  show (= (op (inv id) id) id) by inv_l.
  show (= (op (inv id) id) (op id (inv id))) by op_comm.
  show (= (op id (inv id)) id) by rewrite.
  intro _ : [('a0 : (= id (op id (op id (op (op (op id id) (inv id)) (inv (op id id))))))).                                                                      
```

Conjecture: `(= id (op (inv id) id))`  (Proof Logprob: -7.6116456751792665, 3 steps)                                                                                                            

Proof:
```
 show (= (op id id) id) by id_l.               
 show (= (op (inv id) id) id) by inv_l.                                                                                                                                                      
 show (= id (op (inv id) id)) by eq_symm.
```
Conjecture: `[('a0 : G) -> ('a1 : G) -> (= 'a0 (op id 'a0))]`  (Proof Logprob: -7.2510264460057865, 4 steps)
                                                                                                                                                                                             
### Easiest 3 problems:

Conjecture: `[('a0 : (= id id)) -> ('a1 : (= (op (op id id) id) id)) -> (= id id)]`  (Proof Logprob: -2.347079877108669, 2 steps)                 

Conjecture: `[('a0 : (= id id)) -> (= id id)]`  (Proof Logprob: -1.5468491897693764, 1 steps)                                                                                                   

Conjecture: `(= id id)`  (Proof Logprob: -1.2030829999623922, 1 steps)

## Iteration 2

**Avg. proof length**: 4.10 steps

**Avg. proof length on 'hard' conjectures**: 6.88 steps

### Hardest 3 problems:

`[('a0 : G) -> ('a1 : (= id (inv (op id id)))) -> (= (inv (op id id)) (inv (op (inv (op id (inv (op id id)))) id)))]`  (Proof Logprob: -6.0811389550124035, 5 steps)

`(= (op (op id id) (op id id)) (op id (op id id)))`  (Proof Logprob: -5.707431809481172, 3 steps)

`[('a0 : (= (inv id) id)) -> ('a1 : G) -> ('a2 : G) -> ('a3 : G) -> ('a4 : G) -> ('a5 : (= 'a4 (inv id))) -> (= 'a4 (inv (inv (inv id))))]`  (Proof Logprob: -5.4084035606314, 9 steps)

### Easiest 3 problems:
`[('a0 : (= id (op id (op (inv id) (op id id))))) -> ('a1 : G) -> ('a2 : (= id 'a1)) -> (= id 'a1)]`  (Proof Logprob: -0.2945812885670408, 3 steps)

`[('a0 : (= (op (inv id) (op id id)) (inv id))) -> ('a1 : G) -> ('a2 : (= 'a1 'a1)) -> (= 'a1 'a1)]`  (Proof Logprob: -0.20977646226311422, 3 steps)

`[('a0 : G) -> ('a1 : G) -> ('a2 : G) -> ('a3 : G) -> ('a4 : G) -> ('a5 : (= 'a4 'a4)) -> ('a6 : G) -> ('a7 : (= 'a2 (op 'a0 (op (inv 'a4) 'a4)))) -> (= 'a4 'a4)]`  (Proof Logprob
: -0.17343407015213588, 8 steps)


## Iteration 4

**Avg. proof length**: 5.00 steps

**Avg. proof length on 'hard' conjectures**: 6.10 steps

### Hardest 3 problems:

`[('a0 : G) -> ('a1 : (= id (op (inv 'a0) (inv 'a0)))) -> (= (op id id) (op id (op id (op id (op (inv 'a0) (inv 'a0))))))]`  (Proof Logprob: -9.726059012187891, 9 steps)

Proof:
```
 intro x : G.
 intro x0 : (= id (op (inv x) (inv x))).
 show (= (op id (op id (op (inv x) (inv x)))) (op id (op (inv x) (inv x)))) by id_l.
 show (= (op id (op (inv x) (inv x))) (op id (op (inv x) (inv x)))) by rewrite.
 show (= (op (inv x) (inv x)) (op (inv x) (inv x))) by rewrite.
 show (= (op id (op (inv x) (inv x))) (op id (op id (op (inv x) (inv x))))) by eq_symm.                                                                                                      
 show (= (op (inv x) (inv x)) id) by eq_symm.
 show (= (op id id) (op id (op id (op (inv x) (inv x))))) by rewrite.                                                                                                                        
 show (= (op id id) (op id (op id (op id (op (inv x) (inv x)))))) by rewrite.
```

`[('a0 : G) -> (= (op id (op (inv 'a0) (op 'a0 'a0))) (op id (op (op 'a0 'a0) (inv 'a0))))]`  (Proof Logprob: -7.7850161602701835, 6 steps)

`[('a0 : (= (inv id) (inv (op id (inv id))))) -> (= (inv id) (op id (inv (op id (inv (op id (inv id)))))))]`  (Proof Logprob: -7.032775252968119, 5 steps)

### Easiest 3 problems:

`[('a0 : G) -> ('a1 : G) -> (= (op id (op id (op 'a1 (inv id)))) (op id (op 'a1 (inv id))))]`  (Proof Logprob: -1.017160122076225, 3 steps)

`[('a0 : G) -> (= (op id (op 'a0 (op id (op id 'a0)))) (op 'a0 (op id (op id 'a0))))]`  (Proof Logprob: -0.8543304965071575, 2 steps)

`[('a0 : G) -> ('a1 : (= 'a0 (op (op 'a0 (inv 'a0)) 'a0))) -> (= 'a0 (op (op 'a0 (inv 'a0)) 'a0))]`  (Proof Logprob: -0.08850505636260465, 2 steps)

# Prop. Logic

**Avg. proof length**: 2.75 -> 4.14 -> 4.21 steps

**Average proof length on 'hard' conjectures**: 5.75 -> 7.67 -> 7.78 steps

**Top hard conjecture in iteration 0 vs 4**: `[('a0 : false) -> false]` (1 step) vs ` (or (not (and (not false) (not (or (not false) (or false false))))) (or (not (not (or (or false false) (not (or false false))))) false))` (11 steps)

# Arithmetic

**Avg. proof length**: 2.36 -> 2.50 -> 3.35 steps

**Average proof length on 'hard' conjectures**: 4.00 -> 4.62 -> 5.50 steps

**Top hard conjecture in iteration 0 vs 4**:
`(= (* z z) (* (* (* z z) (* (s (* z z)) (s z))) z))` (4 steps) vs `[('a0 : (= (s (+ z (+ z z))) z)) -> (= z (s (+ z (+ z (s (+ z z))))))]`  (7 steps)

Meta-review: The paper provides a novel scheme for generating mathematical conjectures and proving them when the input is the theory axioms only.
All reviewers acknowledged that this is a challenging and highly interesting task and that the approach is quite pioneering.  The critic by reviewers is centered on the small scale of experiments, and issues of non-scalability. The authors provided detailed rebuttals that was well received by the reviewers (and one raised its score). Overall,  all reviewers were quite positive.
Decision: Accept (oral)