Earlier quoted context omitted.
> I would think the cost multiplier in those cases is much lower for an LLM as compared to a human that doesn't have an inherit understanding and needs to give it thought. Wouldn't you? No. I don't see why proving would require less relative effort for an LLM. In fact, years ago, long before LLMs, I wrote about why it is relatively easy to write sort-of-correct software yet hard to write provably correct software, an…
Every time you compile a statically-typed programming language you are using formal verification, so we have all kinds of industrial scale examples. The reports suggest that outputting tokens for these languages is as easy for LLMs as Javascript. And actually, I would suggest that the reports indicate that LLMs find it easier to output tokens for those languages than Javascript. LLMs are laughably bad at writing Java…
Yeah, this is not what we're talking about here. We're talking about proving properties with deep alternative quantifiers.
> That isn't just hard. Proving software correct in complete generally is impossible. There are all kinds of practical and fundamental constraints that leave it to be impossible. Verification is only useful when you are acting within the scope of a compressed specification of a system's behaviour.
Nobody said anything about complete generality. We're talking about the practice of applying formal methods. It's not writing in Rust, and it's not a general program verifier, but a practice that's applied in some parts of the industry and not others, as the article says.
Put another way, the question is: for those programs and those properties that humans are able to prove with proof assistants, how expensive is it for LLMs to do that work.