[pron]

> 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, and I don't see why it's any different for LLMs. Their power lies in inductive "intuition", while deduction requires effort, just as it does for humans: https://pron.github.io/posts/people-dont-write-programs

But there's no need to speculate. Those who think verification-by-LLM is feasible and cost-effective on an industrial scale, are welcome to try it and report what they find. So far I've seen only tiny examples, and even they don't show effortless (i.e. token-light) work by the agent.

[win311fwg]

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 Javascript.

On the other hand we can watch humans struggle to do the same. How often have you heard things like "I won't use Rust because it is too hard to use"? I have never seen an LLM refuse to output Rust because it thought it was too hard. So what in that suggests an equivalent multiplier?

> yet hard to write provably correct software

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.

[pron]

> Every time you compile a statically-typed programming language you are using formal verification

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.