Add New Rule Builder: Tactic Generator

[yangky11]

This PR adds a new rule builder, allowing the user to tag an MVarID -> MetaM (Array (String × Float)) as a "tactic generator". For example,

@[aesop unsafe 80% tactic]
def x : MVarId → MetaM (Array (String × Float)) := fun _ => do
  return #[("rw [Nat.add_comm b]", 0.5), ("rw [Nat.add_assoc]", 0.9), ("rw [Nat.add_comm]", 0.8)]

Here the scores (0.5, 0.9, 0.8) are "probability modifiers". They are multiplied to the success probabilities during proof search.

Please see the new AesopTest/TacGen.lean file for a complete use case.

The user is free to make the tactic generator arbitrarily complex (e.g., using LLMs).

[JLimperg]

Hey Kaiyu! Thanks for the nice PR. I've made various changes (hopefully improvements), but didn't want to clobber your master branch, so I've pushed them here:

https://github.com/JLimperg/aesop/tree/aesop-llm

Could you look at these to check whether anything seems wrong to you?

[yangky11]

Hi @JLimperg, thank you for the changes; they look great to me. I'll try to integrate it with LLMs and do more testing. I'll post an update later.

[yangky11]

Hi Jannis, I see you're also working on the script builder (not in this PR). How far are we from always being able to produce a proof script whenever the aesop tactic succeeds? The script builder is important for LLM-aesop to become useful, because LLMs may not generate the same set of tactic suggestions every time. It's important for the user to be able to replace the aesop tactic with the actual tactics found during proof search.

[yangky11]

I have tested https://github.com/JLimperg/aesop/tree/aesop-llm in the dev branch of LeanInfer: https://github.com/lean-dojo/LeanInfer/blob/dev/LeanInferTests/Aesop.lean. It works great!

I plan to integrate this feature into the next release of LeanInfer, which will probably come out later this month (together with ongoing improvements in the speed and quality of tactic generation).

A minor question: The 100% here doesn't really play any role (since the probabilities are produced by the model)? If so, can we get rid of it?

[JLimperg]

How far are we from always being able to produce a proof script whenever the aesop tactic succeeds?

Producing a functioning script is not so difficult and should already work, apart from small bugs. E.g. in AesopTest.List, there's only one Aesop call that doesn't produce a functioning script. If you do set_option aesop.check.script true, Aesop will check whether the generated script would solve the goal.

What I'm currently working on is making these scripts more idiomatic (no weird tactics, proper structure, etc.). This is, as it turns out, quite annoying.

I have tested https://github.com/JLimperg/aesop/tree/aesop-llm in the dev branch of LeanInfer: https://github.com/lean-dojo/LeanInfer/blob/dev/LeanInferTests/Aesop.lean. It works great!

Nice, happy to hear! I'll merge this into Aesop master then.

A minor question: The 100% here doesn't really play any role (since the probabilities are produced by the model)? If so, can we get rid of it?

I could maybe special-case TacGen rules. Will see.

[JLimperg]

Closing this PR since the aesop-llm changes are now in master.