Live data from Hacker News

Human mathematicians are being outcounterexampled

xenaproject.wordpress.com

221–230 of 265 posts

Re: Human mathematicians are being outcounterexampled

#221
post #214

Earlier quoted context omitted.

I didn't give a definition of evil, so "close-minded definition" is just a dishonest way of expressing that you subjectively disagree with me. Likewise with trying to make me judge an objective threshold for pollution. It really should be that any polluter needs to morally justify their actions. I find "mostly illusory productivity improvements in white-collar employment" to be an especially indefensible reason for f…

Thank you for using the phrase "stochastic parrot". I only request that you use it at the beginning of your long comments, rather than the end. It saves time.

"LLMs are stochastic parrots" and "stochastic parroting is a powerful medium for computation" are not contradictory statements. [Lisp is a mindless symbolic list processor.] The inability of certain people to accept this speaks to a decades-old contempt for scientific thinking in AI.

https://news.ycombinator.com/item?id=48981271

Re: Human mathematicians are being outcounterexampled

#222

Earlier quoted context omitted.

>GenAI is great at combining existing things in new ways (interpolation). It's terrible at creating new things from scratch (extrapolation). I think you believe a fallacy about how human cognition works if you think we actually do something different than interpolation

I think this is somehow related to GenAI’s issue of “confident incorrectness”. I’ve been trying to prompt GenAI with some highly challenging prompts recently, especially terse ones: > Which Anjunabeats and Anjunadeep compilations have the most breakbeat tracks? GenAI was able to give me breakbeat tracks that were on the Anjuna labels, but it completely flubbed on whether and which those tracks were on compilations. I…

Out of curiosity which model & interface did you use? I'm starting to think that, for IR tasks like this, the number one differentiator among models and harnesses is the ability for the model to look at its available evidence and conclude that it doesn't know the answer. It depends a lot on how the chain of thought goes. I have seen a lot of newer models try to do this in their thinking traces, and it seems very hit or miss.

Even Opus 4.8, GPT 5.5, and Gemini 3.1 Pro (haven't tried 5.6 yet) confidently make up BS sometimes and needed to be reminded to verify thnings instead of inferring or relying on "memory" from training data.

IMO harnesses need some kind of built in "are you sure about that?" loop checkpoint that pauses the main interaction and asks the LLM to evaluate the strength of evidence for a claim it's about to make. It seems almost unreasonable to expect an LLM to next-token-predict its way to such a conclusion, reliably, without prodding. That or we just need another year of RLHF and another 250 billion parameters, IDK.

I feel like that should work becaus when you're using an LLM for a batch inference or classification type of task, it's not that hard to prompt them to emit an "unknown" flag. They just won't do it on their own, and in a coding harness there is so much else going on that a prompted reminder gets lost.

Re: Human mathematicians are being outcounterexampled

#223

Earlier quoted context omitted.

They're trained on human data. I would expect them to emulate human biases as closely as possible.

No, they are not. Specifically, this was a method based specifically on learning from scratch, like most modern AI models. Why do you think it's called Alpha ZERO?

I think you're in the wrong thread. This one is about Claude producing counterexamples. The Go thread is next door.

Re: Human mathematicians are being outcounterexampled

#224

Earlier quoted context omitted.

I think this is somehow related to GenAI’s issue of “confident incorrectness”. I’ve been trying to prompt GenAI with some highly challenging prompts recently, especially terse ones: > Which Anjunabeats and Anjunadeep compilations have the most breakbeat tracks? GenAI was able to give me breakbeat tracks that were on the Anjuna labels, but it completely flubbed on whether and which those tracks were on compilations. I…

Out of curiosity which model & interface did you use? I'm starting to think that, for IR tasks like this, the number one differentiator among models and harnesses is the ability for the model to look at its available evidence and conclude that it doesn't know the answer. It depends a lot on how the chain of thought goes. I have seen a lot of newer models try to do this in their thinking traces, and it seems very hit…

GPT 5.5

> IMO harnesses need some kind of built in "are you sure about that?" loop checkpoint that pauses the main interaction and asks the LLM to evaluate the strength of evidence for a claim it's about to make.

As a practitioner of ML for the past decade, this is the part of LLMs that has always been least satisfying for me. The shared intuition amongst myself and my colleagues has always been that the strongest models are the ones that produce actionable insights directly. Doing all sorts of data preprocessing gymnastics and then following up inference with a 1000-line wall of if-else business logic has always indicated to me that the model is somehow deficient, and not truly capturing the kernel of “truth” within the data, either because the model choice is wrong (e.g. linear regressor for nonlinear problem), or, more likely in practice, the collected data does not effectively capture the underlying “truth” of the measured phenomena with a sufficient signal-to-noise ratio.

LLMs are powerful and have essentially limitless utility, but there’s something missing at a fundamental architectural level for which harnesses are simply a bandaid. Of course, solving that fundamental architectural issue is probably the key to AGI, so…

Re: Human mathematicians are being outcounterexampled

#225
post #217

Earlier quoted context omitted.

In a constructive system, it’s often possible to refute a universal proposition without exhibiting a counterexample, by proving that the proposition implies falsehood. The constructivist will still object that you can’t, from that, conclude that “…therefore a counterexample must exist,” without actually providing a counterexample. But the general principle I was describing still applies - a proof often gives you insi…

To roughly repeat myself from a sibling comment: I may have been unclear. I didn't claim that the only way to disprove something in a constructive system is to produce a counterexample. The part that I was referring to was the last statement from the OP: that "a proof of existence of a counterexample necessarily provides more insight than a counterexample". I can't imagine a constructivist would agree with that in ge…

I'm the OP. In the cases where a proposition can be refuted by a proof that doesn't involve counterexamples, by its nature that proof will tell you something about the reason that the proposition is false.

Whereas a counterexample, on its own, proves the proposition false but doesn't necessarily tell you anything else.

The real difference in the constructive case is that there are fewer classes of proposition for which a proof without witnesses is possible.

(Edit: side note, I didn't explicitly say "necessarily" in my original comment. I suppose there could be exceptions, although I'm struggling to think of an example. Constructively speaking, the ball is in your court!)

Re: Human mathematicians are being outcounterexampled

#226
When I was still much more skeptical of AI, I asked ChatGPT to write me a proof of the Goldbach Conjecture. Of course it didn't, but it gave me a several-screens-long research program for how one might get there, with a few alternate paths and what pieces are still missing from each one. Maybe it cribbed that all from some grad student's blog, but it was still pretty impressive.

A week or two ago I asked Claude Code to write a comprehensive testing plan for a new Postgres feature I wrote, UPDATE/DELETE FOR PORTION OF. I was a bit anxious about how many bugs were discovered as soon as it was merged this spring. Claude found some untested areas, then it wrote more tests for them. I'm not talking about LOC covered, but feature combinations. (I've been meaning to submit this as a followup patch. . . .) Fortunately it didn't find any more bugs.

I sense that testing plan has affinity with the findings in the OP, even though it is far more humble than research mathematics. Even better would be if we knew good ways to express invariants about Postgres's behavior, and then we could ask LLMs to violate them. I'm sure there are good ways already, and the "we" who is not knowing is not "all humans" but "the Postgres team" or just "me".

As a counterexample to the article (heh): even though Claude didn't uncover any new bugs, a human did, just a few days ago. Alas!

Re: Human mathematicians are being outcounterexampled

#227

Earlier quoted context omitted.

Out of curiosity which model & interface did you use? I'm starting to think that, for IR tasks like this, the number one differentiator among models and harnesses is the ability for the model to look at its available evidence and conclude that it doesn't know the answer. It depends a lot on how the chain of thought goes. I have seen a lot of newer models try to do this in their thinking traces, and it seems very hit…

GPT 5.5 > IMO harnesses need some kind of built in "are you sure about that?" loop checkpoint that pauses the main interaction and asks the LLM to evaluate the strength of evidence for a claim it's about to make. As a practitioner of ML for the past decade, this is the part of LLMs that has always been least satisfying for me. The shared intuition amongst myself and my colleagues has always been that the strongest mo…

I find this perspective surprising coming from someone who's done ML for a decade.

How much of a good machine learning system in production is really "the model"? How many lines of code are dedicated to constructing features and preprocessing them? How many lines are needed to process the decision emitted by the model in context of whatever else is going on? How often does the customer interact directly with the inference/prediction from a machine learning model?

My experience has been that model-fitting and model inference very often ends up being part of a bigger system anyway. And even if you do end up with some kind of super-duper all-purpose predictor model, it's rarely the thing you start with, instead you work up to it over weeks or months of iteration. So why should we put so much privilege and esteem on the matrix transformatinos or the decision tree, when they are really just part of a bigger system that receives some input from somewhere and produces useful output for someone?

The same holds for AI in my opinion. An AI system is a system that accepts inputs and produces useful outputs. LLMs are borderline miraculous in that an AI system built around an LLM can do so much more than anything that came before, and you can push a lot of amazing things right down into the tensors inside the LLM. But how far can that go? I don't think we even have an answer yet, because it's all so new and every time it looks like it's going to plateau, the big labs come out with another big step forward.

But there are other questions too, which should look familiar to anyone in industry. Do we need to do it that way? Should we do it that way? If our goal is to build a useful AI system that balances power and cost, then maybe we shouldn't. What if we can make models 10x bigger and spend 10x on RLHF and achieve the behavior we're talking about entirely in tensors. OK, so what if we can? We can also run a collection of little models in a carefully designed harness and achieve that behavior right now, today, at a much lower cost both in terms of up-front investment and marginal cost per unit of work completed.

I get it from an elegance perspective, but I guess I have completely the opposite mindset. Industry has bled me dry of any desire for elegance. The stuff I build now is stupid and crude but it makes our customers happy and costs peanuts to run and that's exactly what my job wants from me. So I say let's commoditize LLMs and start being clever about how we use them. It's not that we shouldn't also push the frontier in size and power, but unless things change w.r.t. the actual costs involved, it doesn't really seem like the best way forward in the short term for achieving smarter AI systems without also making costs go up and up forever.

The bitter lesson still holds of course. But eventually you have to pay for all that power. And you might not want to shell out $20/1M just so you can be sure your LLM can detect uncertainty in its own context and be more honest about when it doesn't know anything about some obscure record label.

Re: Human mathematicians are being outcounterexampled

#228
post #24

Earlier quoted context omitted.

I was once in a presentation for a math PhD thesis. During the thesis, the evaluator of the thesis noticed a flaw in their proof. The student understood and then asked “What now?” The evaluator prof simply shrugged.

A recording of a car crash: discovering on live radio/podcast that the central tenet of your book is wrong, and amateurishly so. Naomi Wolf 'death recorded' on BBC[1], skip to 5:51. After this the book was pulped and she had some sort of psychotic break during COVID and allied with ultra-right and COVID denialist loonies. [1] https://www.bbc.com/news/av/world-us-canada-48639663

It doesn't seem too egregious an error to assume "death recorded" means they were executed, rather than the opposite where death was recorded as the verdict but not actually executed.

Not checking newspaper reports of the period is lazy though and exactly the kind of thing I'd expect a journalist to do and therefore be the one to discover the flaw.

Re: Human mathematicians are being outcounterexampled

#230
> A member of the faculty (who I won’t name) said to me that the fact that the counterexample was so easy to find just indicated that humans had not spent enough time thinking about the problem, implying that a 60-year-old question of Grothendieck was not actually that interesting to work on. I didn’t tell him that at some point earlier in my career I had spent a week working hard on the problem. In my mind my colleague is just going through the five stages of grief; right now they seem to be in the denial phase.

It seems to me also that the very vocal anti-LLM crowd are in the denial phase of grief.

Post reply on HN