Verified Code Transpilation with LLMs

[flagged]

Yes I was being satirical. I've argued for a while now that if we run an llm through a proof engine, we can get rid of hallucinations. In the worst case we'll fail to find a proof. In effect that is gives us an LM that can honestly tell us when it "doesn't know" an answer - at least in this very strictly defined formal context.

But there is a whole cadre of Yann-pilled LLM truthers who cite Yann LeCunn's handwaved proof that LLMs must hallucinate. And they do it incessantly.

Some that I've talked to have gone so far as to assert, with no proof, that an LLM system will hallucinate no matter how many bells and whistles you add to an llm or its architecture. I'm afraid I was taking out my frustration.

But I hope it also challenges some truthers!

This paper is a clear counterexample of a system that will either output nothing (failing after that maximum number of tries) or output a correct proof.

(Ps. I think that it won't matter to most truthers. First if you're an llm truther, you probably don't know or care about proof engines, and might even dispute that proofs represent truth. Second, truthers seem motivated at all costs to deny any possible encroachment of AI on two human mind territory. So even if llms stop hallucinating, they'll move the goal post and find another rallying call.)

[flagged]