PACT Paper

Stream: Machine Learning for Theorem Proving

[Joe Palermo]

Hi, I'm reviewing the PACT paper and I'd love to clarify a few questions I have. @Jason Rute @Jesse Michael Han

1 - For the diagram in Figure 1, how are the expressions in the boxes generated? Also I understand the tactic proof and I can see how the proof term it generates corresponds to it and proves the theorem, but what exactly are the arrows in the syntax tree pointing at?

2 - Section 3.2 describes a recursion into the structure of each proof term. Are the sub-terms simply exprs within the expr of the whole proof term? i.e. this would imply that it is a recursion into an expr-tree as defined here?

[Jesse Michael Han]

re: 2, it's a recursion through the proofterm expr, but it's not quite expr.mfold --- we skip lambda-abstractions and instead accumulate them in a list of binders for creating synthetic tactic states later on

in the lean-step codebase the core function is expr.mfold_with_binders

[Jason Rute]

re 1: I agree it is a confusing picture. Each edge represents a context + goal and the child tree of that edge is the term which completes that goal. So let's work from the top. Here is the tactic proof:

lemma sub_ne_zero_of_ne (a b : int) (h : a ≠ b) : a - b ≠ 0 :=
begin
  intro hab,
  apply h,
  apply int.eq_of_sub_eq_zero hab,
  tactic.trace_result
end

I add the tactic.trace_result at the end so we can see what the proof being generated is. It is:

id (λ (hab : a - b = 0), h (int.eq_of_sub_eq_zero hab))

Ignore the extra id so we get

λ (hab : a - b = 0), h (int.eq_of_sub_eq_zero hab)

Now, like in any mathematical formalism, this expression is a tree. That is the tree drawn in figure one. Specifically, the constructors are lam for lambda abstraction and app for function application, so we can write this expression as something like

( lam (hab : a - b = 0) ( app h ( app int.eq_of_sub_eq_zero hab ) ) )

Now, for every subexpression (or at least the ones in the body of the lambda and on both sides of the application), we have a context and goal. The context is what variables have occurred in outer lambda binders and the goal is the type of the subexpression. These form the edges of the tree.

[Jason Rute]

Does that make sense?

[Joe Palermo]

@Jesse Michael Han Thanks - I'm going to dig into the code

@Jason Rute Ahh yes that makes sense. Thank you for the clarification.

[Joe Palermo]

@Jesse Michael Han Is it fair to say that the PACT data pipeline as described in Section 3.2 is best described by lean_step_main_core_aux? I've been reading the code and I noticed that mfold_with_binders is used only in gather_used_premises as a step before starting lean_step_main_core.

[Jesse Michael Han]

oops yeah, mfold_with_binders was the first implementation of the idea but lean_step_main_core_aux is the more general version that gathers all the data i needed at once

[Joe Palermo]

The paper mentions the use of the fairseq API:

"The fairseq backend supports querying a locally hosted Transformer via the Fairseq CLI (Ott et al., 2019), returning a list of candidates found by beam search, ranked by cumulative log-probabilities."

I'm assuming you trained some models using the fairseq API as a quick baseline to compare against OpenAI's models. I'm assessing different libraries for training LMs, and I'm getting mixed signals about fairseq. I'm curious if you had problems with it or if you would recommend it. Thanks!

[Jason Rute]

@Yuhuai Tony Wu would know best about FairSeq.

[Jason Rute]

If your question is more generally which LM library to use for generating Lean term proofs, I generally don’t know enough from the practical side to be super helpful, but one concern I think you should consider is whether to start with a pretrained model. I think it is fairly clear now that pretrained models, especially if they contain math, but even if they don’t, are good starting points. This will of course limit the options of models and libraries you can use and limit your ability to do domain specific encoding. Also, if you work with a model trained on the Pile or another dataset containing GitHub, you should double check if any Lean repos are in that dataset.

[Joe Palermo]

Thanks, definitely planning to use a pre-trained model. Was planning to pre-train on LIME (https://arxiv.org/abs/2101.06223) also.

[Brando Miranda]

hi @Jason Rute @Jesse Michael Han! I was also reading the paper and saw one term that was used that had no reference I could use to figure out what it meant. In particular, it said:

...it is possible to augment a seed dataset of human proofs with new successful trajectories using rein-forcement learning or expert iteration.
What is expert iteration? Is there a paper or reference to learn about it? Thanks for time in advance

[Jesse Michael Han]

expert iteration is described in this paper: https://arxiv.org/abs/1705.08439

[Brando Miranda]

I'm curious, is expert iteration not very popular? (or does not work very well) I've never heard of it before and have not seen it before mentioned by name before PACT. Does someone know? (Thanks for the reference!)

[Yuhuai Tony Wu]

Expert iteration can be understood as a very general concept, also known as iterated amplification and distillation. Essentially the idea is that you start with a weak agent, and apply some amplifier (usually some search method) to obtain better data ("expert trajectories"), and then you distill the data back to the agent by supervised learning. AlphaGo/AlphaZero also relies on the same idea .

[Brando Miranda]

Hi PACT authors! I was curious about the details of the optimizer you used. What type of optimizer did you use (+ scheduler) and what hyperparameter search did you do to find them (if any)?

[Aidan Swope]

The optimization strategy is described on page 6 of the PACT paper
(I am not an author of the work)

[Jason Rute]

If you still have questions after looking at the paper, I think @Stanislas Polu would know best.

[Yichen Xu]

Hi @Jason Rute @Jesse Michael Han! I was curious about the details of co-training when reading the paper. When training the model on the tactic and mix1 mix2 datasets, will the language modeling loss of the prompt part (for instace, the lm losses computed from GOAL <TacticState> PROOFSTEP part in proof step samples) get masked? Or would the model be optimized from the loss calculated on the whole sample?

[Jason Rute]

(deleted)

[Stanislas Polu]

We used the whole sample, no masking at training :+1:

[Jason Rute]

Is it also the same for the validation loss we report in the charts? Whole string, no masking? @Stanislas Polu

[Stanislas Polu]

Validation loss is masked :+1:

[Yichen Xu]

A lot of thanks!

[Yichen Xu]

Hi @Stanislas Polu @Jason Rute! Thanks again for the clarification. I have another small question about the tactic dataset: I followed the instructions from lean_proof_recording and run the full pipeline to extract the dataset. While the B.2 section of the paper said that the dataset has around 128K examples, I got over 200K examples finally. I am wondering is the difference of runtime environment causing this? Or would PACT clean/filter the generated samples before training the model on them?

[Arthur Paulino]

mathlib has grown since then. That's probably why

[Yichen Xu]

And it seems that the local context classification task is missing from the lean-step-public repo. Is it because the released extraction script for mix1 and mix2 is not that up-to-date? :D

EDIT: I realised that the Proof step classification task is actually the local context classifcation task. Sorry for the noise!

[Yichen Xu]

Arthur Paulino said:

mathlib has grown since then. That's probably why

Ah yes! That looks reasonable.

[Yichen Xu]

So the dataset size nearly doubled after one year, which may result in better model performance even without the changes in algorithms! It is exciting to see that the machine learning models somewhat grow together with humans. :D

[Yichen Xu]

Hey @Stanislas Polu! Recently I have been trying to reproduce the results of PACT on a GPT model trained by our lab. I am curious about the technical details about decoding strategy: is PACT using nuclear sampling? and how would temperature affect the performance?

[Yichen Xu]

And we found that our model is really vulnerable to overfitting on mix1 and mix2. Did this also happen in your settings?

[Stanislas Polu]

@Yichen Xu we generally simply sample at T=1.0; which is rather high but the diversity of samples overall helps performance we found.

[Yichen Xu]

Tons of thanks! :^)

[venom Yu]

@Jason Rute Hi, I am trying to reproduce some Automated Theorem Proving work and I noticed that they were all pretrained on WebMath dataset. I wonder whether this dataset has been released?

[Jason Rute]

@venom Yu No. The closest public dataset I know is the Pile, especially the arXiv, GitHub, and stack exchange parts of the Pile.

[Yuhuai Tony Wu]

https://huggingface.co/datasets/hoskinson-center/proof-pile from @Zhangir Azerbayev also quite valuable asset

[Zhangir Azerbayev]

Yuhuai Tony Wu said:

https://huggingface.co/datasets/hoskinson-center/proof-pile from Zhangir Azerbayev also quite valuable asset

Thanks for the mention Tony. I've also trained 1.3B and 6.7B parameter models on this datase. Here are the huggingface links: 1.3B, 6.7B

[Jason Rute]

Nice!

[venom Yu]

Thanks a lot!