gptf generating theorems

Stream: Machine Learning for Theorem Proving

[Kevin Buzzard]

I was showing one of my sons gptf (in the lean-liquid repo) and he suggested that instead of training GPT to generate proofs, could one use it to generate theorem statements? I am not a computer scientist but this sounded like a reasonable enough question to me!

[Jesse Michael Han]

yeah this would be a fun experiment! this has been studied elsewhere: the N2Formal team had some experiments with unconditional generation in HOL Light

currently the model is trained on theorem naming: lean statement -> theorem_name_in_mathlib, one could reverse the role of the names and statements and then try seeing what happens when you supply a reasonable-looking theorem name it's never seen during training

one way you can try playing with (goal-conditioned) conjecturing now is to use gptf {prefix := "have :"} to force it to synthesize a have-statement

[Alex J. Best]

If you visit https://beta.openai.com/playground?model=formal-lean-wm-to-tt-m1-m2-v4-c4 and sign in (assuming you signed up for the beta they announced some time back) you can play around with just clicking submit and having the model generate statements and then try and prove them. Basically given any prefix gptf will try and complete it, so you can start with something like

<|endoftext|>LN] GOAL α : Type u_1, _inst_1 : group α,  g h : G ⊢ g * h

and click submit to see what gptf thinks this term should be, I just tried this a couple of times and got g * h = g * h by rfl, but more interestingly also the theorem

g * h * h⁻¹ = g PROOFSTEP rw [mul_assoc, ← gpow_add, add_right_cancel_iff, one_mul]

not sure that the proof works in this case :grinning:

[Jesse Michael Han]

neat, thanks Alex! yeah the playground at beta.openai.com might be your best bet for playing with the model while avoiding all the gptf theorem proving machinery

[Jason Rute]

And if you want top level theorems with no assumptions, use the prefix GOAL ⊢ or TYPE (and whatever boilerplate you need at the beginning). The TYPE keyword might be better even since that was just trained on Lean top level theorems (and definitions, maybe).

[Jason Rute]

See Figure 4 in https://arxiv.org/pdf/2102.06203.pdf for all the available keywords.