6 ms·

Cool. Now we can write bugs in our theorem descriptions instead of source code. Seriously, please review Curry Howard Isomorphism if you’re getting pulled down

by davemp 2mo ago

Cool. Now we can write bugs in our theorem descriptions instead of source code. Seriously, please review Curry Howard Isomorphism if you’re getting pulled down this rabbit hole. Programs are proofs. Proofs are programs. So if you can formally describe the correct output for every input, you can have an LLM loop automatically fill in the gaps of how to get there. Congrats, that sounds at least as hard as writing the correct program in most cases. Don’t get me wrong, I do think there are useful tools combining formal methods and llms. Let’s just not get carried away.

fractorial 2mo ago
Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!
6gvONxR4sf7o 2mo ago
> Congrats, that sounds at least as hard as writing the correct program in most cases. That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted. The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness. [0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.
- deleted 2mo ago
  [deleted]
- davemp 2mo ago
  > That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. Really unnecessary levels of snark here. > often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted Have you ever heard of prolog? I’m sure a prolog program can express whatever property you’re attempting to write just as tersely (if that’s your metric for hard). Almost copy/pastable to and from a theorem proofer. Or are you saying that the program has to be the efficient implementation? Because that’s a different ball game. I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. (At that point we’ll have finally created the fabled “sufficiently smart compiler” and probably solved p=np). A huge majority of software is simple business rules + CRUD that is trivially verifiable. The entire problem is showing that an efficient/reliable program actually implements those rules. > The magic is that you can write a spec that's clear Maybe you can. But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation.
  - gr_norm 2mo ago
    > I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. > The entire problem is showing that an efficient/reliable program actually implements those rules. Reliability is a standard matter of correctness and captured (partly) by specifications. Efficiency tends to be easy to empirically test, but it is also possible to capture at the specification level [1]. Mind that specifications need not be all-consuming. > But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation. Agree! But this stuff just got massively more accessible, and the tooling around it is growing quickly. I think we'll end up growing specification systems specific to various domains which will be palatable to those "systems engineers", but I err on the side of optimism here. There's definitely a lot left to do for practicality. [1] See the work of https://cs.nyu.edu/~shw8119 https://cs.nyu.edu/~shw8119 for the case of provably-efficient parallelism and garbage collectors
  - 2mo ago
gr_norm 2mo ago
It is true that finding the correct specification is a formidable task; knowing what correctness even means is arguably most of the difficulty of programming. However! "Moving bugs up from programs to types" isn't how this shakes out in practice, at all. Another commenter already noted that it's often much easier to communicate your intent through specifications, because you can essentially always say what a computation should do much more simply than you can say exactly how to do it. I think it's also important not to miss the forest for the trees: even relatively simple specifications like "the compress and decompress functions must be inverses for all inputs" rules out vast classes of bugs in a compression library. This is not a complete specification; for instance, it does not speak about how the decompressor behaves on malicious input. But in my experience, even partial specifications carry the promise of hitting warp speed with LLMs in a way that I haven't seen anywhere else. After a certain level of specification, you have decent guarantees of being able to whole-heartedly forget about the implementation details of the synthesized program. And you get a better-built, more robust program out of it at the end! The comment at the end of the article about having LLMs directly generate assembly against specifications and letting them rip with finding custom optimizations is the sort of crazy stuff this enables. I really think we're only seeing the tip of the iceberg here. People keep asking what we can do with LLMs that we couldn't before; this is the answer.

by davemp 2mo ago

fractorial 2mo ago

Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!

6gvONxR4sf7o 2mo ago

> Congrats, that sounds at least as hard as writing the correct program in most cases. That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted. The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness. [0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.

deleted 2mo ago
[deleted]
davemp 2mo ago
> That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. Really unnecessary levels of snark here. > often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted Have you ever heard of prolog? I’m sure a prolog program can express whatever property you’re attempting to write just as tersely (if that’s your metric for hard). Almost copy/pastable to and from a theorem proofer. Or are you saying that the program has to be the efficient implementation? Because that’s a different ball game. I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. (At that point we’ll have finally created the fabled “sufficiently smart compiler” and probably solved p=np). A huge majority of software is simple business rules + CRUD that is trivially verifiable. The entire problem is showing that an efficient/reliable program actually implements those rules. > The magic is that you can write a spec that's clear Maybe you can. But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation.
- gr_norm 2mo ago
  > I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. > The entire problem is showing that an efficient/reliable program actually implements those rules. Reliability is a standard matter of correctness and captured (partly) by specifications. Efficiency tends to be easy to empirically test, but it is also possible to capture at the specification level [1]. Mind that specifications need not be all-consuming. > But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation. Agree! But this stuff just got massively more accessible, and the tooling around it is growing quickly. I think we'll end up growing specification systems specific to various domains which will be palatable to those "systems engineers", but I err on the side of optimism here. There's definitely a lot left to do for practicality. [1] See the work of https://cs.nyu.edu/~shw8119 https://cs.nyu.edu/~shw8119 for the case of provably-efficient parallelism and garbage collectors
- 2mo ago

gr_norm 2mo ago

It is true that finding the correct specification is a formidable task; knowing what correctness even means is arguably most of the difficulty of programming. However! "Moving bugs up from programs to types" isn't how this shakes out in practice, at all. Another commenter already noted that it's often much easier to communicate your intent through specifications, because you can essentially always say what a computation should do much more simply than you can say exactly how to do it. I think it's also important not to miss the forest for the trees: even relatively simple specifications like "the compress and decompress functions must be inverses for all inputs" rules out vast classes of bugs in a compression library. This is not a complete specification; for instance, it does not speak about how the decompressor behaves on malicious input. But in my experience, even partial specifications carry the promise of hitting warp speed with LLMs in a way that I haven't seen anywhere else. After a certain level of specification, you have decent guarantees of being able to whole-heartedly forget about the implementation details of the synthesized program. And you get a better-built, more robust program out of it at the end! The comment at the end of the article about having LLMs directly generate assembly against specifications and letting them rip with finding custom optimizations is the sort of crazy stuff this enables. I really think we're only seeing the tip of the iceberg here. People keep asking what we can do with LLMs that we couldn't before; this is the answer.