News for hackers. Stuff that matters.
Re:Prediction: AI will make formal verification go mainstream by throwaway613745 on Tuesday December 16, 2025 @05:07PM (#46295262)
GPT 5.2 can't even tell me how many rs are in garlic.
Re:Prediction: AI will make formal verification go mainstream by bglazer on Tuesday December 16, 2025 @05:13PM (#46295329)
This is a very tiring criticism. Yes, this is true. But, it's an implementation detail (tokenization) that has very little bearing on the practical utility of these tools. How often are you relying on LLM's to count letters in words?
Re:Prediction: AI will make formal verification go mainstream by 1970-01-01 on Tuesday December 16, 2025 @05:53PM (#46295821)
The implementation detail is that we keep finding them! After this, it couldn't locate a seahorse emoji without freaking out. At some point we need to have a test: there are two drinks before you. One is water, the other is whatever the LLM thought you might like to drink after it completed refactoring the codebase. Choose wisely.
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.
Re:Prediction: AI will make formal verification go mainstream by andy99 on Tuesday December 16, 2025 @05:33PM (#46295569)
At this point if I was openAI I wouldn’t bother fixing this to give pedants something to get excited about.
Re:Prediction: AI will make formal verification go mainstream by blazingbanana on Tuesday December 16, 2025 @05:39PM (#46295656)
Unless they fixed this in 25 minutes (possible?) it correctly counts 1 `r`.

https://chatgpt.com/share/6941df90-789c-8005-8783-6e1c76cdfc...

Re:Prediction: AI will make formal verification go mainstream by iAMkenough on Tuesday December 16, 2025 @05:34PM (#46295575)
The criticism would stop if the implementation issue was fixed.

It's an example of a simple task. How often are you relying on LLMs to complete simple tasks?

Re:Prediction: AI will make formal verification go mainstream by desman on Tuesday December 16, 2025 @05:45PM (#46295729)
This is like complaining that your screwdriver is bad at measuring weight.

If you really need an answer and you really need the LLM to give it to you, then ask it to write a (Python?) script to do the calculation you need, execute it, and give you the answer.

Re:Prediction: AI will make formal verification go mainstream by bgwalter on Tuesday December 16, 2025 @05:51PM (#46295803)
⌴⌴⌴
Re:Prediction: AI will make formal verification go mainstream by worldsayshi on Tuesday December 16, 2025 @06:03PM (#46295929)
That's a problem that is at least possible for the LLM to perceive and learn through training, while counting letters is much more like asking a colour blind person to count flowers by colour.
Re:Prediction: AI will make formal verification go mainstream by charcircuit on Tuesday December 16, 2025 @07:46PM (#46296834)
Why is it not possible? Do you think it's impossible to count? Do you think it's imposing to learn the letters in each token? Do you think combining the two is not possible.