using/training llms to call powerful tactics

Stream: Machine Learning for Theorem Proving

[Jared green]

what would it take to build an ai agent for theorem proving that will actually use tactics more powerful than the 'elementary' ones?

[Jared green]

specifically, synthesizing subgoals and then placing a power tactic that might close them

[Eric Wieser]

Does use H$ D.2.2 (φ _ *(L+1)-1) (L.le_sub_of_add_le (by nlinarith[((b.1* b.2+1).totient_pos).2 Nat.succ_pos']))▸(((Nat.dvd_gcd) ( this).1)) this.right count as a "powerful tactic"?

[Jared green]

no, the short ones like aesop, duper...

[Jared green]

the ones intended to be general

[Jason Rute]

Thor does this in Isabelle by calling Sledgehammer as a tactic more or less. Draft-Sketch-Prove (and successors) is even closer to what you want. It uses an LLM to write a proof sketch and uses SledgeHammer to fill in the holes in the sketch.

[Jason Rute]

But AlphaProof also synthesized fairly advanced subgoals. I think that is more important than whether or not those subgoals can be filled in with a single tactic call.

[GasStationManager]

I believe the solution is to have a library of prompt instructions that covers the Lean features that are not well represented in training data. I have a very primitive version in Leantool, where the system prompt introduced the LLM to features like omega, exact?, aesop, and LeanSearchClient's #moogle. This will require additional prompt engineering efforts to make it work well, e.g. adding examples.
If you have (or can write) a good prompt that teaches a Lean feature, let me know and I'd be happy to add it to LeanTool..

[Jared green]

i have no prompt engineering 'skills', i sort of expected something that would be trained from the start with that in mind. if you get a pretrained model to do it, i think you would just add the new power tactic to a list of mcp templates.

[Leni Aniva]

given how existing agents work you either need to incentivize exploration or execute the tactic when some mechanically checkable condition is met