logoalt Hacker News

de_aztectoday at 7:11 PM3 repliesview on HN

So essentially: One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.


Replies

layer8today at 7:38 PM

Trust in formal reasoning is necessarily always conditional. You have to start somewhere. The good thing about verified formal proofs is that the only way they can be in error is if the verifier is faulty. This drastically limits the possible reasons for error.

(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)

fancy_pantsertoday at 7:22 PM

One can only trust a verifier as far as they can trust anything made out of software.

AnimalMuppettoday at 8:10 PM

It has nothing to do with LLMs. One cannot trust the proof of anything if one cannot trust the verifier.