PACT paper

Stream: lean-gptf

[Jesse Michael Han]

We released a preprint which documents our novel training methodology, instrumentation of Lean, and evaluation results on mathlib. The main novelty is PACT, a methodology for extract abundant self-supervised data from proof terms for co-training alongside the tactic prediction objective. PACT boosts theorem proving performance on our test set of theorems from mathlib from 32% to 48% and we retain a success rate of 37% on another evaluation set of theorems from the future, i.e. added to mathlib after we extracted our training data.

One of the co-training objectives was theorem naming; we investigate this further in the appendix (following up on the experiment reported in the automatic lemma naming thread) and show that the models are pretty good at suggesting names, and even when its suggestions don't match syntactically they tend to be close or make sense semantically. PACT also improves the ability of our models to successfully predict multiple tactic steps at once using the semicolon combinator, which is remarkable because semicolons are specific to the tactic step data and not part of PACT at all.

The new model is now available by default. Please do keep probing its reasoning capabilities---we'd love more feedback on how to make this tool better for Lean users.