simplicity

Stream: lean-gptf

[Julian Berman]

Hi -- naive question perhaps, but how does/did gpt-f learn what constitutes a simpler proof than another? Or more specifically, what made it produce this: https://github.com/leanprover-community/mathlib/pull/5903/files -- is it explicitly trained that rw is a simpler tactic than simp even though in terms of number of characters that's longer?

[Mario Carneiro]

The comments on the last few gpt-f PR's suggest that it's using the length of pp.all output

[Julian Berman]

A ha.

[Jesse Michael Han]

Mario Carneiro said:

The comments on the last few gpt-f PR's suggest that it's using the length of pp.all output

it is just the length of format.to_string <$> format.flatten <$> tactic.pp $PROOF_TERM with default pretty-printing settings --- they get an order of magnitude larger with pp.all enabled

[Alex J. Best]

But it's not trained to output short proofs , is that right? It just happens to find shorter ones sometimes?

[Jesse Michael Han]

correct, it's not explicitly trained to produce short proofs, nor do we optimize the data collection process in any way for this --- it just tries to predict what it thinks is the most likely tactic for a given tactic state, based on the training data (tactic steps in mathlib)

[Jesse Michael Han]

we determined which proofs were shorter with another script which replays the proofs found by gptf and compares the proof term to the one already in the environment.

[Julian Berman]

Makes sense, thanks! Nonetheless I suppose, during training did it get to see multiple proofs of the same thing at all?

[Jesse Michael Han]

probably --- remember, its training data is precisely what you see when you step through a tactic proof in mathlib, so for example, it's probably seen false proven from Q and not Q (and other extraneous hypotheses in the context) using contradiction, exact absurd h1 h2, tauto, finish...

we can check this rigorously, but later---our attention is occupied with some other experiments at the moment.