[pron]

Whatever the cost multiplier is, I see no reason why that same multiplier won't remain with AI.

Personally, I don't think that picture is quite accurate. Yes, there is a high cost multiplier for small programs, albeit perhaps not so prohibitive. But for large programs, that multiplier is, for most intents and purposes infinite, unless, perhaps, you have experts who know what's worth proving and what is not.

Anyway, I'd like to see that put to the test. Have an LLM write a 50-100KLOC program and prove all correctness properties - with the properties themselves approved by an expert human - and tell us what it cost. A colleague of mine stopped his AI proof experiment when he got an email from some functionary at the company to stop doing what he was doing with the model, because it was costing too much money.

[win311fwg]

> Have an LLM write a 50-100KLOC program and prove all correctness properties [...] and tell us what it cost.

Assuming the 50-100KLOC program is of real-world use and not something contrived for the sake of offering something to prove, it is unlikely that proving all correctness properties will be possible, fundamentally. So costs will be nothing — or infinite if you foolishly remain determined to try the impossible.

In the real world we restrict what properties we care about and what models we reason in. Some of those models are woven into the fabric of an LLM. 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?

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