News for hackers. Stuff that matters.
Re:Prediction: AI will make formal verification go mainstream by 101008 on Tuesday December 16, 2025 @05:14PM (#46295353)
It's an example that shows that if these models aren't trained in a specific problem, they may have a hard time solving it for you.
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.

Re:Prediction: AI will make formal verification go mainstream by Uehreka on Tuesday December 16, 2025 @05:32PM (#46295543)
No, it’s an example that shows that LLMs still use a tokenizer, which is not an impediment for almost any task (even many where you would expect it to be, like searching a codebase for variants of a variable name in different cases).
Re:Prediction: AI will make formal verification go mainstream by 8note on Tuesday December 16, 2025 @05:55PM (#46295840)
the question remains: is the tokenizer going to be a fundamental limit to my task? how do i know ahead of time?
Re:Prediction: AI will make formal verification go mainstream by worldsayshi on Tuesday December 16, 2025 @06:09PM (#46295996)
Would it limit a person getting your instructions in Chinese? Tokenisation pretty much means that the LLM is reading symbols instead of phonemes.

This makes me wonder if LLMs works better in Chinese.

Re:Prediction: AI will make formal verification go mainstream by victorbjorklund on Tuesday December 16, 2025 @05:55PM (#46295841)
No, it is the issue with the tokenizer.