Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Claude Fable produced a counterexample to the Jacobian Conjecture

xcancel.com

Post reply on HN
Print view View original

451–460 of 562 posts

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#451

Post by [deleted] »

mathgeek wrote: post #348
unexpectedtrap wrote: post #335

Using LLMs to generate piles of code and/or proofs of dubious quality is very questionable thing, and I understand these non-stop debates about it. But in this case, as using plain brute force is already quite a common thing in searching for counterexamples, using LLMs as a sort of more advanced brute force seems to be just the right thing to do, so I struggle to understand so much hostility to this approach.

> I struggle to understand so much hostility to this approach. It's going to be really rough for a lot of folks as machines get better and better at domains that the human brain was exclusively useful for. I tend to view the hostility as a mix of both "unless we have proof this could all be hokum" and "we're going to lose a lot of what we consider makes humans amazing". Compassion is going to be very, very important…

[deleted]

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#452

Post by astrange »

YeGoblynQueenne wrote: post #450
igravious wrote: post #333

Earlier quoted context omitted.

"using human-like reasoning (in a brute-force way)" that's self-contradictory -- what brute force means is doing an exhaustive search of a search space (brute forcing it) using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree

LLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#453

Post by astrange »

losvedir wrote: post #359
inigyou wrote: post #271

Earlier quoted context omitted.

Just take it as more confirmation that LLMs are unintelligent pattern-matchers.

You must never have faced a situation where you can't believe your eyes. It takes a certain level of - dare I say it - intelligence and maturity to consider that it's more likely you've made a mistake than that you've made a huge breakthrough. In HN terms - it's never the compiler. Yes, very occasionally it might be the compiler, but you're better off assuming it's a bug in your code.

> In HN terms - it's never the compiler. Yes, very occasionally it might be the compiler, but you're better off assuming it's a bug in your code.

Conversely:

- if your company has an internal compiler team then it's likely the compiler because they broke it.

- if it's not the compiler, you're not pushing it hard enough.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#454

Post by zaptheimpaler »

pred_ wrote: post #332
glimshe wrote: post #264

Earlier quoted context omitted.

The parent's absolutely nonsensical post highlights how polarized AI (as everything else) is today. I can understand someone being opposed to AI on moral, cost-benefit or productivity grounds. But we're seeing a lot of extremist "AI is good for nothing" posts out there nowadays.

I don't think it is nonsensical at all. The author and his collaborator both appear to be bright people, so there's a good chance they had to offer non-trivial insights to guide the LLM, yet it's clearly in the interest of his employer to downplay whatever personal contribution they provided. Edit: Now the OP is flagged/dead for some reason. You could disagree on their take (calling it a marketing stunt is maybe a bi…

Believing that AI played a very small role while we know this problem was open for decades with at least a few people taking serious cracks at it is just not a coherent logical position.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#455

Post by YeGoblynQueenne »

astrange wrote: post #452
YeGoblynQueenne wrote: post #450

Earlier quoted context omitted.

LLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.

What are the search algorithms then? DFS, BFS, A*, etc, can you name them?

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#456

Post by abernard1 »

snarkconjecture wrote: post #435
abernard1 wrote: post #366

Earlier quoted context omitted.

I am not confused. Because herein these forums, I predicted everything that was going to happen years ago. And the "insane inefficiency" of deep learning is fully to be expected from how it works. As well, there are provably no—literally no—emergent properties in these models. The choice of metric was a convenient, sloppy, and embarrassing fault of the field. It should be discredited; the field should be embarrassed;…

Current LLMs can absolutely multiply floats without a tool call. In fact, that's a much more rote symbol-manipulation task than doing original math research.

With what accuracy? And with how many intermediate tokens?

We can replace multiplication with any class of problems which should go from 0->100% solution almost immediately if there was actually a concept learned.

There is not. Because they are plain ol' fits. And there are no "emergent" features that pop out without having a sufficient set, where "sufficient" is absolutely gigantic and equivalent to memorizing enough of the space to compress the problem. LLMs are Rain Man.

They interpolate within a known distribution. Search allows places outside of distribution to be explored.

This paper should be required reading [1]. You can explore the curves yourself. You can see exactly what it's doing. And you also have this nagging thing—which you know and I know—that all these models converge and do not diverge upwards. An "emergent" "hyperintelligence"—a characteristic that could be found if something was actually learned and combined with a new concept—would not have this problem.

Exponentials on exponentials added to compute and data and the problem classes still sit at not great places, and require agents, feedback loops, and trial and error to solve. The models are the problem, but more importantly, the people selling things these models could never do are the problem.

[1] https://hai.stanford.edu/news/ais-ostensible-emergent-abilit...

Edit: It should be mentioned, if there's some scary neural architecture that's super-de-duper and doing something beyond the very obvious next string prediction that LLMs clearly do, it can't do what absolutely ancient ML models could do; a network to multiply two floating point numbers should pop out somewhere without symbolic computation, no?

It does not. There's no magic other than the run-of-the-mill SV fake it til you make it magic. And that magic has failed.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#457

Post by CamperBob2 »

YeGoblynQueenne wrote: post #447
antirez wrote: post #254

Earlier quoted context omitted.

So many mathematicians over the years tried hard and failed, but now Anthropic just for some PR magically did it? And this after LLMs obtaining different math wins? What is your logic here really escapes my understanding.

I mean we have no idea what happened exactly, how Fable was used, how many times it was run, whether earlier models were also tried, what was the prompt, how long it run for, etc etc. All we have to go by is a tweet. Why not be skeptical about that?

What you're asking for is exactly the sort of thing that belongs in, and will appear in, a journal article. There will likely be a preprint on arxiv, so you might keep an eye out for that.

In any case, the fact that it was found by a commercial model means that the unfiltered reasoning trace isn't available even to the original author. So there are aspects of the problem-solving process we'll never see. Even if we did get access to the reasoning trace it wouldn't necessarily be definitive, given how these things work.

Hopefully it'll be possible to get the same solution from an open-weight model like one of the 3T heavyweights that are said to be coming up for release. If so, the chain of thought can be scrutinized in-depth.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#458

Post by ViscountPenguin »

gmadsen wrote: post #370
mathisfun123 wrote: post #77

Earlier quoted context omitted.

Because SAS triangle identity proofs are relatable and I'm trying to make a point...?

And my point is it’s a strawman. Advanced math is obviously creative to those who practice it, and it’s disingenuous to boil it down to grade school triangle proofs That would be like saying Shakespeare isn’t creative , since grade school grammar doesn’t feel creative

I have at least some level of experience with advanced maths, but the thing that always struck me was how amenable to automation that a lot of it seemed. While it might be creative for a human to come up with the Schreier refinement theorem, for example, I don't think it fundamentally requires creativity.

On some level, I think the most straightforwardly creative work in maths comes from building up useful generalizations; I can't see current LLMs inventing even something as straight forward as a manifold from first principles; but I also don't think that's fundamentally required to prove useful things, I think it's more of a shortcut for humans.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#459

Post by tptacek »

YeGoblynQueenne wrote: post #450
igravious wrote: post #333

Earlier quoted context omitted.

"using human-like reasoning (in a brute-force way)" that's self-contradictory -- what brute force means is doing an exhaustive search of a search space (brute forcing it) using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree

LLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.

That's not what happened here. This isn't a proof; it's a counterexample. The model was perfectly capable of verifying its correctness. You could have verified it by hand if you wanted; the verification is trivial. Finding it was the hard part.

Re: Claude Fable produced a counterexample to the Jacobian Conjecture

#460

Post by tptacek »

YeGoblynQueenne wrote: post #455
astrange wrote: post #452

Earlier quoted context omitted.

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.

What are the search algorithms then? DFS, BFS, A*, etc, can you name them?

Why are you asking them which basic computer science graph traversal algorithms a frontier model used?
Post reply on HN