Summary
This paper proposes POETRY, a method for formal theorem proving using language models by training the model to iteratively decompose the problem into sketches, recursively. The authors focus on Isabelle. At each step, POETRY takes a proof state and goal and predicts either a formal sketch (a proof using sorry at each step), or a ground proof step (e.g. 'by ...') that requires no recursion. These intermediate states are visited within best-first search, where the score of a node is given by the log-probability of all predictions made so far to get to that node. Intuitively, POETRY works by recursively generating lower level steps / sketches, until finding a complete proof, getting feedback from the formal environment at each step. To train the LM, the authors introduce a simple method to decompose existing Isabelle proofs from the AFP as if they had been generated by this recursive proof generation process. Experiments on minif2f show improvements on top of GPT-f and a version of Thor without Sledgehammer.
Strengths
The paper is well motivated and tackles a timely topic, using a standard, hard benchmark (minif2f) for methods in this space. The writing is mostly clear (though see some notes below).
POETRY is a simple, sound and novel method to structure the proof generation process. It should be adaptable to other interactive theorem provers with some work. POETRY allows the prover model to get more intermediate feedback from the environment compared to methods that try to produce the whole proof at once. It also uses this feedback in a way that is complementary to proof repair methods (generally what the standard when we consider using intermediate feedback).
Weaknesses
The choice of baselines (for Table 1) seems a bit convoluted. In particular, I don't really understand why use Thor without sledgehammer. The main point of Thor is to learn when to use hammers in proofs. Removing this makes the model much more similar to the GPT-f baseline.
As for the choice of pass@1, even though POETRY only makes a single prediction at the end, it gets feedback from Isabelle at each node in its tree. So that doesn't seem like a fair comparison either, if POETRY makes many intermediate predictions and calls Isabelle during its search, whereas GPT-f and Thor w/o sledgehammer seem to only produce and test a single prediction. It might be more fair to match the methods based on some other metric, like number of tokens generated, or number of calls to Isabelle (whichever seems to be the most significant bottleneck).
The question of "Can POETRY find longer proof?" is a bit ill posed as is. It would be possible for a method to find very long proofs that do not *need* to be long, and do better on this analysis without really being able to prove more complex theorems. What I think the authors are trying to show here is that POETRY can solve harder problems, estimating hardness by looking at proof length. For this, you might want to compare success rate based on the length of the ground truth proof: perhaps the baselines perform very poorly on theorems where the human proof is longer, whereas POETRY might have a better success rate. Another option is to show that either POETRY generates proofs of similar length to the ground truth proof (so, when POETRY generates long proofs, you'd estimate that the ground truth proof would also be long), or that it generates proofs of similar length to the baselines in cases where they all manage to prove a theorem. Any of these would help show that this result is not trivial.
Questions
* Is an intermediate sketch valid (accepted by Isabelle) as long as it's syntactically correct and the last step shows the thesis? Or do you manage to get richer feedback besides that the last step declares to show the thesis?
* For problems that both POETRY and the GPT-f baseline solve, does POETRY tend to generate longer proofs?
* As for the relationship with LEGO-Prover, you mention that in some cases it is impossible to decompose a proof into lemmas, but still possible to decompose it into sketches recursively. Do you have an example?
* What exactly is the search algorithm used in the Thor w/o sledgehammer and GPT-f baselines? It is a one-shot prediction? Or do you use the (also best-first) search method described in the original GPT-f paper?
* What is Thor without sledgehammer? It sounds like a different thing other than Thor.
* I'm confused by what Figure 5 is trying to show. Fundamentally, reorganizing a proof into sketches shouldn't change its inherent complexity (e.g., the atomic proof steps). Is this just comparing the full proof length against the number of steps in the top-level sketch (without considering the deeper sketches recursively)? If you were to consider the steps in the deeper sketches recursively, I'm assuming you would not expect to see a reduction (if you do, where would that come from? do you have an example?)
Limitations
Yes, adequately addressed.