Learning Formal Mathematics From Intrinsic Motivation

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.

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. Similarly, 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. Additionally, 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. 2. 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? 3. 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. Some typos I noticed: 1. Line 169: "Mathematically, $\mathcal{C}$ is a function $f_{\mathcal{C} : \Sigma* \to $..." but $\mathcal{C}$ is a set. 2. Line 245: "levarage" -> leverage 3. Figure 2 caption: I think you meant "evaluated" 4. Line 341: "recevies" -> "receives" 5. Line 345: "training tends to collapse to ? by"

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? 2. 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? 3. 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? 4. 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". If 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? 5. 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? 6. 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.

Rating

6

Confidence

4

Soundness

1

Presentation

2

Contribution

3

Limitations

I believe the authors have adequately addressed the limitations and broader societal impacts of their work.

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.

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. * 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. * 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. * 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. * 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. * 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? Overall, 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. [1] Language Models Can Teach Themselves to Program Better. Haluptzok et. al. ICLR 2023.

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? * Why do we start with a randomly initialized Language Model? How does the choice of Language Model affect the performance of conjecture generation? * 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? * Can the authors provide explanation for if/how to apply the approach to environments like Coq and Lean?

Rating

6

Confidence

3

Soundness

2

Presentation

4

Contribution

3

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

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.

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. 2. How does this method facilitates solving dataset such as miniF2F and mathlib?

Questions

Q1: How to guarantee f_C soundness and completeness? Q2: In Figure 2, propositional logic, the search baseline policy at iteration 0 seems missing. 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? 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? Q5: How many evaluated theorems are in the Natural Number Game dataset?

Rating

6

Confidence

3

Soundness

3

Presentation

3

Contribution

3

Limitations

The authors have adequately addressed the limitations.

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.

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. The 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. The 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. The 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.) The presented experiments are small: only five iterations of conjecturing-proving loop are run. Some 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. It would be interesting to see more metrics tracked across the learning iterations for better insights about the process, for instance: - the average length/syntactic complexity of the generated conjectures, - the average length of a proof per iteration, - the duplication rate between consecutive batches of generated conjectures. Some details of the method are not specified clearly (see my questions below). Minor: - evaluate as -- evaluated as (the caption of Fig. 2)

Questions

How the conjecture generation is conditioned on the difficulty level? How do you tokenize formulas? How exactly do you calculate the average proof log-likelihood (Figure 2): - how do you incorporate the failed proof attempts into the average? - 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? - are the conjectures from hindsight relabeling taken into the average here? Is it correct that the lines in Fig. 2, right, for the policies from iterations 0 and 1 are completely overlapping? 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? Why group theory is missing from the evaluation presented in Fig. 4? 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)? 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.

Rating

7

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

The authors correctly identify the major limitations of their approach.

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.

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. 2. 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. 3. 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. 2. 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. 3. 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.

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? 2. How well does an agent trained in one mathematical domain (e.g., propositional logic) generalize to another (e.g., arithmetic)?

Rating

5

Confidence

3

Soundness

3

Presentation

3

Contribution

2

Limitations

Yes

Thanks for your response

Thanks to the authors for the engaging and detailed response! >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. I think a discussion of this would be of great use to include in the paper. This is probably more appendix material than main text, but readers will definitely want to know what advantages Peano brings in this specific context and how it could feasibly be extended to existing theorem provers. I highly encourage the authors to include an even more thorough version of this discussion in the paper. The additional qualitative results are also useful and I hope the authors include these and a few more in the main text, along with a comprehensive analysis of them (which includes the metrics recorded in the general response.) Conditioned on these points, I am increasing my score. I look forward to the extended discussion that the authors will be adding to the main text.