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.

Can you report numbers measuring problem difficulty as length of proofs? Can you include examples of proofs found over iterations?

Please 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).

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?

At 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.

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?

Good 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).

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?

We 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.

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?

Given 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)

Thus, 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.

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.

You 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.

Thank you again for the detailed review. We're happy to engage further if any other questions remain!

I thank the authors for the interesting remarks regarding my question, and the comments about compute requirements. I feel that works like GPT-f and HTPS are on the extreme end of the compute scale, and there are many reasonable works exist that show "good results" with a fairer compute budget.

The primary concern I have is how to judge an adequate attempt at a highly interesting problem. The results are not particularly convincing, especially when referring to performance on the extrinsic set of problems, and the conjectures generated are closer to "alien math" (which is fine) but also seem to not convey any particularly interesting results, even on a simple level. However, this paper is the first to attempt this conjecturing-proving setup as far as I know. I think the particularly interesting research ideas would be those which show real improvements on this task. Further consideration of this is better done by the metareviewer.

Because the authors have nicely addressed my questions and clarified their work, I have increased my score.

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).

There is a substantial body of work on the self-improvement of LLMs that I felt was not adequately addressed by the authors.

We 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.

MCTS was a bit light on detail. What exactly is the state for the MCTS policy? [...]

This 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:

"State: { x : G, x0 : G }\nGoal: [('a2 : G) -> (= (op id 'a2) 'a2)]" (the state has two elements of the group G and still has a 'forall a2 : G, id * a2 = a2' in the goal)

The 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.

To the previous point - [...] discussion regarding if and how their approach could extend to popular theorem proving environments like Coq and Lean

Yes, 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.

Is there a qualitative analysis for RQ1 that can be done on these conjectures to show that they indeed become harder over time?

Please 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.

Later iterations of the policy seem to be a bit worse on (or consider a bit harder) "easy" conjectures

That'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).

Why do we start with a randomly initialized LM? How does the choice of LM affect performance?

Our 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).

[...] how the approach chooses a specific difficulty of conjecture generator.

We 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').

Thanks again for the review. We're happy to engage or clarify further!

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.

Further justification of using log-likelihood as the main evaluation in this paper.

• 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).
• 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).

How does this method facilitates solving dataset such as miniF2F and mathlib?

We 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.

Q1: How to guarantee f_C soundness and completeness?

Completeness 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).

Q2: In Figure 2, propositional logic, the search baseline policy at iteration 0 seems missing.

It 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.

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?

Please refer to the global response for additional examples in each domain with their likelihoods. We will include these in the appendix.

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?

Yes, 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).

Q5: How many evaluated theorems are in the Natural Number Game dataset?

The 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.

Thank you again for the comments and questions! We'd be happy to answer any further questions, or discuss these in more depth.

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.

How the conjecture generation is conditioned on the difficulty level?

Once 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):

"Conj:(fail) false"
"Conj:(triv) (iff (not (not (not false))) false)"
"Conj:(hard) [('a0 : (or false false)) -> false]"

All 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.

How do you tokenize formulas?

We 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.

How exactly do you calculate the average proof log-likelihood (Figure 2):

A 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.

how do you incorporate the failed proof attempts into the average?

In 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.

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?

Only 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.

are the conjectures from hindsight relabeling taken into the average here?

No, only the conjectures in the batch are.

Is it correct that the lines in Fig. 2, right, for the policies from iterations 0 and 1 are completely overlapping?

That's right, they were nearly indistinguishable.

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?

There are two main reasons for using the likelihood compared to success rate:

• 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).
• 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).

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'). Is the success rate in Fig. 4 computed independently per each iteration, or rather cumulatively (taking union of theorems proved in all the past iterations)?

Independently.

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.

We apologize, our release script ignored .txt files, but that included requirements.txt. Here is the content of this file (in learning):

altair
bottle
coloraide
hydra-core
maturin
numpy
omegaconf
redis
rq
sympy
torch
tqdm
transformers
wandb
celery

maturin 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.

For an additional analysis of the generated conjectures across iterations, please refer to our global response.

We 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!

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.

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.

That'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.

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.

Our 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.

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?

We 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. 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) 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.

How well does an agent trained in one mathematical domain (e.g., propositional logic) generalize to another (e.g., arithmetic)?

We 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.

We also note that we provided more examples of conjectures and proofs in the global response.

Thanks again for the review! We'd be happy to answer further questions.