Comment by davemp
15 hours 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.
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.
> 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.
> 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.
> 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 for the case of provably-efficient parallelism and garbage collectors
> Really unnecessary levels of snark here. [..] Have you ever heard of prolog?
Why do you look at the speck of sawdust in your brother's eye and pay no attention to the plank in your own?
> I’m sure a prolog program can express whatever property you’re attempting to write just as tersely
No, you won't be able to express the most basic properties in Prolog at all, let alone as tersely as in a proper specification language.
E.g. if you have a language interpreter and a bytecode interpreter, pretty much every specification language will let you express the correctness of a compiler `compile(x)` as
``` for all scripts x and inputs i,
bytecodeInterpreter(compile(x),i) == languageInterpreter(x,i) ```
Good luck expressing this in Prolog, let alone equally tersely.
Huh, I wasn't actually going for snark. I was trying to preemptively be over-specific about what I meant. As in, you said "... writing the correct program..." and I meant that I'm talking in terms where functions are equal or distinct only based on extensional equality and with some flexibility on computational interpretation and axioms of the logic.
Like, if you meant "the correct program" in a sense where two pure total functions can be different despite both having the same outputs on the same inputs, then that's not what I'm responding to.
And yeah I know prolog, but proof assistants and logic programming are totally different beasts. Definitely not copy/pastable to/from lean, at least as I've seen and used each.
> 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).
I think you're totally misunderstanding. What I'm saying is that in something like Lean (just because I know it best) I can say, "this function takes inputs satisfying Prop1 and returns outputs satisfying Prop2," in ways where I write some brute-force equivalent formalization of Prop1 and Prop2 in the most straightforward way, and then go on to prove that they are true of my program that is not the brute force implementation. Like the wacky famous magical inverse square root implementation from Quake III. You could write a spec that "output = 1/sqrt(input) up to float properties" and the implementation in the famous brainfuckery way. To your comment about how the spec is as hard as the implementation, "output = 1/sqrt(input)" is way easier than the weird efficient implementation, and that class of distinction is super common.
And as you said, the annoying part is showing that the efficient implementation satisfies the spec, but what's magic today is that we have great tools and LLMs can and do fill in the blanks. In practice, I write the spec by hand for the stuff I care about and then prompt the rest and know that my spec is what the LLM implemented.
> > 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.
I tried rocq back when it was coq too, and now do most of my work in lean and rust and python with totally normal folks and I'm convinced that the tooling and languages are finally just about Good Enough. If you have any interest in the field, which it sounds like you do, and if you haven't checked out the ecosystem in the last couple years, I'd recommend you check it out again.
Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!