3 ms·
Hallucinations are more or less a solved problem for me ever since I made a simple harness to have Codex/Claude check its work by using static typechecking.
by johnfn 9mo ago
Hallucinations are more or less a solved problem for me ever since I made a simple harness to have Codex/Claude check its work by using static typechecking.
- emp17344 9mo agoBut there aren’t very many domains where this type of verification is even possible.
- nextaccountic 9mo agoThen you apply LLMs in domains where things can be checked Indeed I expect to see a huge push into formally verified software just because sound mathematical proofs provide an excellent verifier to put into a LLM hardness. Just see how Aristotle has been successful at math, and it could be applied to coding too Maybe Lean will become the new Python https://harmonic.fun/news#blog-post-verina-bench-sota https://harmonic.fun/news#blog-post-verina-bench-sota
- filoeleven 9mo ago"LLMs reliably fail at abstraction." "This limitation will go away soon." "Hallucinations haven't." "I found a workaround for that." "That doesn't work for most things." "Then don't use LLMs for most things."
- baq 9mo agoUm, yes? Except ‘most things’ are not much at all by volume.
- johnfn 9mo ago"Autocomplete is great!" "It doesn't work in bash" "Then don't use it in bash." I don't see what's wrong with this argument, and I certainly don't see it as a proof that the particular technology is actually useless, as you seem to be suggesting.