News for hackers. Stuff that matters.
Re:Prediction: AI will make formal verification go mainstream by altruios on Tuesday December 16, 2025 @06:15PM (#46296059)
An analogy is asking someone who is colorblind how many colors are on a sheet of paper. What you are probing isn't reasoning, it's perception. If you can't see the input, you can't reason about the input.
Re:Prediction: AI will make formal verification go mainstream by 9rx on Tuesday December 16, 2025 @11:30PM (#46298271)
> What you are probing isn't reasoning, it's perception.

Its both. A colorblind person will admit their shortcomings and, if compelled to be helpful like an LLM is, will reason their way to finding a solution that works around their limitations.

But as LLMs lack a way to reason, you get nonsense instead.

Re:Prediction: AI will make formal verification go mainstream by Nevermark on Wednesday December 17, 2025 @12:16AM (#46298526)
> But as LLMs lack a way to reason, you get nonsense instead.

I suppose we should conclude humans don't reason either, since they do this all the time. Reason over blindspots without realizing it, is endemic in humans.

LLMs reason differently because their architecture is different, the way they learn is different, and their mode of inference is different. They will be bad at some things we are good at.

And yet their reasoning is far wider than ours (able to weave together virtually any disparate topics sensibly), and almost always better than humans at moderate depth one-shot responses.

Human's are truly awful at one-shot reasoning.

Re:Prediction: AI will make formal verification go mainstream by altruios on Friday December 19, 2025 @01:15PM (#46328988)
What tools does the LLM have access to that would reveal sub-token characters to it?

This assumes the colorblind person both believes it is true that they are colorblind, in a world where that can be verified, and possesses tools to overcome these limitations.

You have to be much more clever to 'see' an atom before the invention of a microscope, if the tool doesn't exist: most of the time you are SOL.