alt Hacker NewsCool. 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.
Replies
fractorial • today at 3:52 AM
Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!
> 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.