AI Program Generation and Verification in Lean

Stream: Machine Learning for Theorem Proving

[Daniel Geisz]

I was super compelled by AlphaProof, and this got me thinking: are people trying similar things for AI program generation and verification in Lean?

I'm specifically compelled by AlphaProof's automatic generation of a bunch of proofs that were subsequently used to continuously train its language model. Does anyone know of specific people or research groups that are attempting something similar in Lean, but with an emphasis on code generation? (Obv function generation is equivalent to theorem proving in lean, but I'm interested in cases where people are generating algorithms to accomplish specific tasks, not just mathematical theorems).

Also, if anyone here happens to be involved in this, I'd love to hear about your efforts!

[Jason Rute]

I don't think there is nearly enough done on this topic. Here are some things I know from the past few months:

• miniCodeProps: a Minimal Benchmark for Proving Code Properties
• DafnyBench: A Benchmark for Formal Software Verification
• FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

[Eric Wieser]

I think the space of humans using Lean to write verified algorithms (if that's what you mean to ask) is itself quite sparse; for instance, I think it's currently quite hard to write any proofs about lean's for loops due to lack of related library theorems.

[Adomas Baliuka]

The space of humans using anything to write verified algorithms or programs is already quite niche... Lean really isn't the go-to tool for that either, as much as I'd like it to be.

[Daniel Geisz]

Yeah, I mean that totally makes sense. Idk though... it might be starry-eyed thinking but it seems like Lean would be a really interesting environment to train language models to iteratively autogenerate and verify algorithmic code, AlphaProof style. Excited to dig into this more :)

@Jason Rute, thanks for pointing out those links!

[Jonathan Julian Huerta y Munive]

@Daniel Geisz consider changing your proof assistant. Verification has been the motivation behind the development of older proof assistants like Coq or Isabelle. I do not know what @Lasse Blaauwbroek and @Jason Rute are planning for the Tactician (for Coq), but "program verification" training data should abound there. I am working in Isabelle in the early steps towards a Tactician-like environment for Isabelle. The objective is to create tools for Isabelle users, which are mostly verification people like me.

[Johan Commelin]

Lean is still young compared to these other proof assistants, but in the past year there has been a very conscious effort to make it more suitable for software verification as well. Of course it can't compare to the ecosystem that the others are offering (yet). All I'm saying with this message is that there is no reason the Lean support for verification right now is indicative of what it will be in the (nearish) future

[Jonathan Julian Huerta y Munive]

I agree. Perhaps the verb "change" that I used might be misinterpreted here. I never intended to say that a project in Lean would be futile. We need projects in many proof assistants. Rather, I wanted to say that, if one widens the scope of the question, one might find more people/research groups doing "machine learning for code-generation/verification", specially since other ITPs have a >30-year old history and the ideas are probably older than that.

[Daniel Geisz]

@Johan Commelin are there particular people or orgs behind the push to make lean better for software verification? Trying to get a feel for the state of things

[Johan Commelin]

It is one of the long term focus points of the FRO, and you can find some aspects of it on the two-year FRO roadmap https://lean-fro.org/about/roadmap/
Concretely, there is active work on integrating with SAT solvers, the omega tactic was developed with software verification as one of the motivations, and the std library is being developed, because before verifying software, you need to write the software...