Learning Formal Mathematics From Intrinsic Motivation — part 3/5
Cleaned-text code points [31597, 47517). Bibliography omitted here; source.md includes it.
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 to 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 1 has higher log-likelihood for the proofs to the new conjectures found at iteration 1, when compared to the initial policy from iteration 0. 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—successful 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 3 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 conjectures fail to remain challenging—all provable conjectures end up with high log-likelihood as training progresses, and the conjecturer is unable to leave that regime. We attribute this to 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, a 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 textbook “Introduction to Metamathematics” [ 20 ] . Precisely, in Theorem 41, Kleene states (and proves a subset of) 35 useful statements of Propositional Logic (such as contraposition rules, commutativity and transitivity laws of logical connectives, and properties of double negation). For arithmetic, we use the Natural Number Game [ 6 ] , a popular game used to introduce formal mathematics in the Lean theorem prover. We take levels of the game that are (a) theorems about natural numbers, and (b) do not refer to 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 our agents on their success rate on those problems within 2000 MCTS expansions.
Figure 4 shows the results. We find that, as our agents train on their self-generated problems, they steadily become more successful at proving theorems from both Kleene’s book and the Natural Number Game. This happens even though these theorems are not targeted during training, since our agent only uses its own conjectures. Four theorems in Propositional Logic are only proved after the last iteration of training: commutativity and transitivity of the “if and only if” logical connector, a law connecting double negation and implication ( ¬ ¬ ( A ⇒ B ) , ¬ ¬ A ⊢ ¬ ¬ B \neg\neg(A\Rightarrow B),\neg\neg A\vdash\neg\neg B ), and the “currying law” of the conjunction — ( A ∧ B ) ⇒ C ⊢ A ⇒ ( B ⇒ C ) (A\wedge B)\Rightarrow C\vdash A\Rightarrow(B\Rightarrow C) . In the Natural Number game, only the final agent proves ∀ n , ∀ m , s u c c ( n ) + m = s u c c ( n + m ) \forall n,\forall m,succ(n)+m=succ(n+m) , a theorem requiring induction on the correct variable (m) and a non-trivial sequence of rewrites in the inductive case (we include the full proof in the Appendix). While admitedly small scale, these results suggest a 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.
## 5 Limitations and Conclusion
We present Minimo : an approach to training agents for formal mathematical reasoning starting from only the axioms of a given domain. The agent jointly 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 on generated conjectures (i.e., not found by hindsight) increased from 2.67 steps in the first iteration, when the model is randomly initialized, to 5 steps by iteration 4, with proofs for ‘hard’ conjectures growing from 3.67 to 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 5 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 it from (a) discovering deep mathematical theories, and (b) scaling up to large theories. First, even if the agent’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 e=e ; by the last iteration, the conjecture requiring the longest proof reads as ∀ g ∈ G , if e = ( g − 1 ) 2 then e 2 = e ( e ( e ( ( g − 1 ) 2 ) ) ) \forall g\in G,\text{if }e=(g^{-1})^{2}\text{ then }e^{2}=e(e(e((g^{-1})^{2}))) (proved in 9 steps). In contrast, human mathematicians develop deep theories by accumulating results and definitions along the way, in such a 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 , 11 ] ) will be a key direction for future work.
Another bottleneck in our current setup is that a large library can cause the current action enumeration algorithm in Peano to become prohibitively slow (a 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 human-written 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 library.
Together, lifting these limitations from our method might lead to 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 Teodorescu for insightful discussions on preliminary ideas related to this work; Jeremy Avigad, Patrick Massot and other members of the Hoskinson Center for Formal Mathematics for useful feedback on an early presentation of this work, as well as the anonymous reviewers for discussions and comments that improved our manuscript. 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.
## Appendix A Training details
We represent our agents with GPT-2-style 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, we train the LM for a fixed number of 2000 steps of the AdamW optimizer (learning rate of 1 e − 4 1e-4 ) with a dynamic batch size of most 10000 characters (random examples are added until their padded sequence lengths add up to 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 to convergence in training loss.
Our training runs (5 iterations of generating and proving 200 conjectures in each) were done on 2 machines with 5 NVIDIA A40 40GB GPUs each. Each run took from 8 to 16h on a single GPU, totalling 288 GPU hours for the runs underlying our main results.
## Appendix B Proof log-likelihood and MCTS Expansions
Throughout the paper, we used the likelihood of the proof under the policy as a measure of difficulty. Figure 5 shows that this quantity is linked to the number of iterations that MCTS takes to find the proof. This allows us to estimate difficulty easily without running search for theorems that we have proofs for (such as those we find by hindsight relabeling).
## Appendix C Fraction of provable conjectures across iterations
Our conjecturing procedure steers to LM to 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 is 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 to 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 is unclear — it is still perhaps positive to generate false conjectures, as long as the process of proving them leads to learning progress (as seems to be the case in Arithmetic).
## Appendix 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. z : nat. s : [nat -> nat]. + : [nat -> nat -> nat]. * : [nat -> nat -> nat]. +_z : [(’n : nat) -> (= (+ ’n z) ’n)]. +_s : [(’n : nat) -> (’m : nat) -> (= (+ ’n (s ’m)) (s (+ ’n ’m)))]. *_z : [(’n : nat) -> (= (* ’n z) z)]. *_s : [(’n : nat) -> (’m : nat) -> (= (* ’n (s ’m)) (+ ’n (* ’n ’m)))]. nat_ind : [(’p : [nat -> prop]) -> (’p z) -> [(’n : nat) -> (’p ’n) -> (’p (s ’n))] -> [(’n : nat) -> (’p ’n)]]. #backward nat_ind. #forward +_z ((+ ’n z) : nat). #forward +_s ((+ ’n (s ’m)) : nat). #forward *_z ((* ’n z) : nat). #forward *_s ((* ’n (s ’m)) : nat).
### D.2 Propositional Logic
prop : type. false : prop. /* Connectives */ not : [prop -> prop]. and : [prop -> prop -> prop]. or : [prop -> prop -> prop]. iff : [prop -> prop -> prop]. /* Introduction rule for conjunction */ #backward and_i. and_i : [(’P : prop) -> (’Q : prop) -> ’P -> ’Q -> (and ’P ’Q)]. /* Elimination rules for conjunction */ #forward and_el (’_ : (and ’P ’Q)). and_el : [(’P : prop) -> (’Q : prop) -> (and ’P ’Q) -> ’P]. #forward and_er (’_ : (and ’P ’Q)). and_er : [(’P : prop) -> (’Q : prop) -> (and ’P ’Q) -> ’Q]. /* Introduction rules for disjunction */ #backward or_il. or_il : [(’P : prop) -> (’Q : prop) -> ’P -> (or ’P ’Q)]. #backward or_ir. or_ir : [(’P : prop) -> (’Q : prop) -> ’Q -> (or ’P ’Q)]. /* Elimination rule for disjunction */ #backward or_e infer infer infer infer subgoal subgoal. or_e : [(’P : prop) -> (’Q : prop) -> (’R : prop) -> (or ’P ’Q) -> [’P -> ’R] -> [’Q -> ’R] -> ’R]. /* Introduction rule for negation */ #backward not_i. not_i : [(’P : prop) -> [’P -> false] -> (not ’P)]. /* Elimination rule for negation */ not_e : [(’P : prop) -> (not ’P) -> ’P -> false]. #backward exfalso. exfalso : [false -> (’P : prop) -> ’P]. /* Introduction rules for equivalence */ #backward iff_i. iff_i : [(’P : prop) -> (’Q : prop) -> [’P -> ’Q] -> [’Q -> ’P] -> (iff ’P ’Q)]. /* Elimination rules for equivalence */ #forward iff_el (’_ : (iff ’P ’Q)). iff_el : [(’P : prop) -> (’Q : prop) -> (iff ’P ’Q) -> [’P -> ’Q]]. #forward iff_er (’_ : (iff ’P ’Q)). iff_er : [(’P : prop) -> (’Q : prop) -> (iff ’P ’Q) -> [’Q -> ’P]]. /* Excluded middle */ #forward em. em : [(’P : prop) -> (or ’P (not ’P))].
### D.3 Groups
= : [(’t : type) -> ’t -> ’t -> prop]. G : type. op : [G -> G -> G]. id : G. /* Associativity */ #forward op_assoc ((op (op ’a ’b) ’c) : G). op_assoc : [(’a : G) -> (’b : G) -> (’c : G) -> (= (op (op ’a ’b) ’c) (op ’a (op ’b ’c)))]. /* Commutativity */ #forward op_comm ((op ’a ’b) : G). op_comm : [(’a : G) -> (’b : G) -> (= (op ’a ’b) (op ’b ’a))]. /* Identity */ #forward id_l. id_l : [(’a : G) -> (= (op id ’a) ’a)]. /* Inverse */ inv : [G -> G]. #forward inv_l. inv_l : [(’a : G) -> (= (op (inv ’a) ’a) id)].
## Appendix E Extrinsic evaluation problems
Here we list all problems used in the extrinsic evaluation in Arithmetic and Propositional Logic.
### E.1 Arithmetic
The following are the 10 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 is essentially about propositional logic). The prefix in these problems tell which “world” of the game it came from: t stands for the Tutorial World, a is for the Addition World, and finally m is for the Multiplication World.