Xavier Généreux and Jannis Limperg: Efficient Forward Reason

Stream: Lean Together 2025

[Riccardo Brasca]

A thread for discussion about this talk.

[Jesse Alama]

What kinds of performance gains would be required to (for lack of a better term) go full auto with Aesop and this improved forward reasoning? Is algorithmic complexity keeping us down (I suspect as much!) but perhaps you see some technical changes (possibly major ones) which, if implmeneted, would make these rules (say) 10x faster?

[Rendya Yuschak]

Hi! Really great talk. I have one question. In the abstract you mentioned that the new implementation is "almost fully backwards compatible." Could you clarify the exceptions or edge cases where compatibility might be an issue?

[Jannis Limperg]

Slides: https://github.com/JLimperg/talk-2025-01-lean-together-aesop-forward (go to Releases to get the PDF)

[Jannis Limperg]

Rendya Yuschak said:

Hi! Really great talk. I have one question. In the abstract you mentioned that the new implementation is "almost fully backwards compatible." Could you clarify the exceptions or edge cases where compatibility might be an issue?

The backward-incompatible changes (which are fairly minor) are discussed here: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Upcoming.20changes.20to.20Aesop.20forward.20rules

[Jannis Limperg]

Jesse Alama said:

What kinds of performance gains would be required to (for lack of a better term) go full auto with Aesop and this improved forward reasoning? Is algorithmic complexity keeping us down (I suspect as much!) but perhaps you see some technical changes (possibly major ones) which, if implmeneted, would make these rules (say) 10x faster?

This is a bigger question, so I'll make a couple of points.

First, I didn't mention this in the talk, but the benchmark results were actually worse than you'd hopefully see in practice. We used a unary representation of natural numbers without the optimisations that Lean applies to the standard natural numbers, to simulate larger terms. If you don't do this, the new forward reasoning needs much less than 1ms per hyp added.

Second, the main cost of forward reasoning comes from Lean's basic operations, e.g. reduction, when the type expressions grow larger. I believe these operations could be sped up considerably using Normalisation by Evaluation-style techniques, but I don't have a full implementation yet.

Third, while forward reasoning could be used as a basic saturation-style automated theorem prover, I don't think it would be very efficient or powerful. Modern ATPs (such as the upcoming lean-auto for Lean) employ much more sophisticated calculi than the one we implement and they are fine-tuned with large numbers of heuristics, better indexing data structures, better term representations, etc. Even then, they remain somewhat weak in practice, though they are certainly much stronger than Aesop when used as "push-button" automation.

Put another way, Aesop has never been designed to provide full automation but rather to be a highly customisable tool that allows you to get automation for your specific problem domain with a tolerable amount of effort.

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/gRANtwNOZQY

[Jannis Limperg]

@Xavier Généreux and I now have a draft paper about this new forward reasoning implementation: https://github.com/JLimperg/paper-aesop-forward/releases/download/submission/paper.pdf