4 ms·

Check out this paper: https://leandojo.org/ https://leandojo.org/ People have already trained models to assist suggestion tactics. They then linked it up to C

by steego 3y ago

Check out this paper: https://leandojo.org/ https://leandojo.org/ People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs. In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step. FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago. Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up. As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization. If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.

staunton 3y ago
> it has been designed for verification from the ground up. It has a lot of places where you assume things work in a certain way and a lot of ways to assume it (and you can prove `false` if any of those assumptions aren't correct). I'd say it's a lot more geared towards formalizing math than verification. There's some more things, e.g., the `Expression -> C-code` "compiler" isn't verified and neither is the C-compiler. Those could be fixed with some work (that nobody is working on currently, as far as I can tell). But the first issue seems pervasive. I don't think Lean will become a standard tool for software verification or significantly advance the discipline. Of course, I'd love to be wrong.
- zozbot234 3y ago
  If the foundations are workable (and they seems to be, though IIRC there is a quotienting construct that's quite ad hoc and that people have complained about), the fact that you can additionally "assume" other things is fairly irrelevant, these are no different than extra axioms.
  - staunton 3y ago
    It's not useful to prove that "your program does what you want, provided the following 10000 functions implemented in C do what we assumed they do". Almost certainly at least one of them doesn't. There isn't even a straightforward (let alone verified) way to list all assumptions of this type for some proof (you can print the axioms that a definition depends on, but that's not the same thing). It's possible to prove `false` in Lean using functions you'd normally use to make pretty much any useful program.
- steego 3y ago
  You’re right and thank you for correcting this. I was playing fast and loose with the term verification and was thinking about it in a broader context.

by steego 3y ago

staunton 3y ago

> it has been designed for verification from the ground up. It has a lot of places where you assume things work in a certain way and a lot of ways to assume it (and you can prove `false` if any of those assumptions aren't correct). I'd say it's a lot more geared towards formalizing math than verification. There's some more things, e.g., the `Expression -> C-code` "compiler" isn't verified and neither is the C-compiler. Those could be fixed with some work (that nobody is working on currently, as far as I can tell). But the first issue seems pervasive. I don't think Lean will become a standard tool for software verification or significantly advance the discipline. Of course, I'd love to be wrong.

zozbot234 3y ago
If the foundations are workable (and they seems to be, though IIRC there is a quotienting construct that's quite ad hoc and that people have complained about), the fact that you can additionally "assume" other things is fairly irrelevant, these are no different than extra axioms.
- staunton 3y ago
  It's not useful to prove that "your program does what you want, provided the following 10000 functions implemented in C do what we assumed they do". Almost certainly at least one of them doesn't. There isn't even a straightforward (let alone verified) way to list all assumptions of this type for some proof (you can print the axioms that a definition depends on, but that's not the same thing). It's possible to prove `false` in Lean using functions you'd normally use to make pretty much any useful program.
steego 3y ago
You’re right and thank you for correcting this. I was playing fast and loose with the term verification and was thinking about it in a broader context.