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

What sort of maths are LLMs good at?

gowers.wordpress.com

Post reply on HN
Print view View original

171–180 of 189 posts

Re: What sort of maths are LLMs good at?

#171

Post by xnorswap »

aphid_yc wrote: post #166
xnorswap wrote: post #28

Earlier quoted context omitted.

What proportion of the human population could answer the example from that paper? Question: Strangers A, B, C, D, and E line up from youngest on the left to oldest on the right. Their clothing colors and shoe colors all differ, and they come from five different regions. Known facts: 1. A is from Morocco. 2. D is five years older than B. 3. E is older than A. 4. C stands next to D. 5. A stands next to B. 6. The person…

This is a neat puzzle but you really don't need prolog. Spend a couple minutes thinking about it and you can solve this just fine. Your question: It just means they have both green shoes and clothes, probably. It's aimed to confuse a model with a bunch of information you-just-don't-really-need. The trick is to fish out which hints are more important than others. The order in which you apply them matters to make the p…

> The answer to the question is 17

Except, according to the linked paper, the answer to the question is 420.

I got to 420 too, but only by ignoring almost all clues: https://news.ycombinator.com/item?id=49271594

A puzzle where nearly all clues are badly defined or irrelevant is not really a puzzle.

Re: What sort of maths are LLMs good at?

#172

Post by aphid_yc »

parhamn wrote: post #78

> If they were, then their big speed advantage over us would mean that there would be much more of a flood of results. Is this true right now? Just recently Jarred Sumner tweeted [1] that he managed to make some progress on the Riemann hypothesis while on a jog. Managed to get somewhere by encouraging the llm to “keep going” and “believe in yourself”. This raised a few questions for me. Had no one at Anthropic though…

A real-world high-value breakthrough in physics would be to find some substantially cheaper (than the giant tokamak approach) arrangement of matter that can create sustained nuclear fusion with energy out to energy in factors over 10, which can also feasibly be built within a decade or two.

Advances in astrophysics or fundamental models are all very cool but won't be of much real-world applicability, at least in the short or medium term.

Re: What sort of maths are LLMs good at?

#174

Post by wyager »

TuringTest wrote: post #134
wyager wrote: post #124

Earlier quoted context omitted.

> But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time Having models write Lean proofs of mathematical claims is standard op…

Yeah but the LLM can only handle proofs that hold inside its context window. Proofs for novel theories requiring thousands of pages with dozen millions of steps will need support from external tools to organize the full structure of the formal document; it cannot be done by the LLM inference process alone, which was my point. It would be like asking a mathematician to proof theorems without pen and paper; external to…

Every LLM harness released in the last year has handled this gracefully via delegation, structured memory systems, etc.

Re: What sort of maths are LLMs good at?

#175

Post by zahlman »

black_knight wrote: post #144
TuringTest wrote: post #134

Earlier quoted context omitted.

Yeah but the LLM can only handle proofs that hold inside its context window. Proofs for novel theories requiring thousands of pages with dozen millions of steps will need support from external tools to organize the full structure of the formal document; it cannot be done by the LLM inference process alone, which was my point. It would be like asking a mathematician to proof theorems without pen and paper; external to…

Not sure how true this restrictions is once you have the agents hammering on at a big code base of formalised proofs. Proofs stretching thousands of pages are split into lemmas, grouped into sub theories. What I haven’t seen agents do yet is to develop new ideas for entire such theories. I have usually seen them bite into some existing idea and grinding out related results. But I am less sure than ever that they won’…

The thread title is "What sort of maths are LLMs good at?"

The codebase you describe would be an external tool in GP's conception.

Re: What sort of maths are LLMs good at?

#176

Post by zahlman »

redox99 wrote: post #143
CamperBob2 wrote: post #132

Earlier quoted context omitted.

"ChatGPT" could mean anything from Instant to Pro. What was the prompt, and which model(s) did you try?

Almost surely the free model on the web ui. So a dumb model, no harness, and probably a bad prompt.

My point was that the kind of error it made was nothing like the kind of error a contestant would make.

Re: What sort of maths are LLMs good at?

#177

Post by CamperBob2 »

zahlman wrote: post #176
redox99 wrote: post #143

Earlier quoted context omitted.

Almost surely the free model on the web ui. So a dumb model, no harness, and probably a bad prompt.

My point was that the kind of error it made was nothing like the kind of error a contestant would make.

The differences between 'instant' chat models and frontier-grade models are enough to render any such test a waste of electricity.

Re: What sort of maths are LLMs good at?

#178

Post by YeGoblynQueenne »

ozgung wrote: post #164
YeGoblynQueenne wrote: post #115

Earlier quoted context omitted.

>> This is not "brute-force" though. It's an iterative search algorithm. You learn things at each iteration. You also don't search blindly. You use "something" (heuristics, experience, intuition) to come up with "ideas" at each iteration. You don't try 650 random programs. You try 650 different ideas each learning from the results of previous trials. But, learn what? All those ideas where wrong. How does an LLM "lear…

>> In this case, by happy accident, what stuck was an improved bound of the zeroes of the zeta function etc. I’m not familiar with this specific example (or Mathematics) but I assume they keep intermediate results (python functions, lemmas, computations, intermediate proofs etc.) and formulate and explore adjacent ideas. Even with a failed attempt you can learn things. LLMs make a difference here because they can eva…

Thanks, but I can't see that in the article by Anthropic. AFAICT the "650 ideas" that were wrong were all generated independently of each other.

I don't agree that LLMs can evaluate an experiment. There's nothing in LLM training that makes them capable of telling what is e.g. a correct hypothesis from an incorrect one. I know that is a common claim particularly encouraged by AI companies but whenever that claim has been studied systematically and carefully the result is that self-verification doesn't work. For example, see:

On the Self-Verification Limitations of Large Language Models on Reasoning and Planning Tasks

https://arxiv.org/abs/2402.08115

Note also that basically all the mathematical results published so far have to be checked by an external verifier, either human mathematicians or a proof assistant like Lean, or both, and some systems explicitly couple an LLM generator to a traditional solver, like e.g. AlphaProof. None of this would be needed if LLMs could really evaluate their own results in any reliably correct manner.

Re: What sort of maths are LLMs good at?

#179

Post by YeGoblynQueenne »

willmarch wrote: post #145
YeGoblynQueenne wrote: post #115

Earlier quoted context omitted.

>> This is not "brute-force" though. It's an iterative search algorithm. You learn things at each iteration. You also don't search blindly. You use "something" (heuristics, experience, intuition) to come up with "ideas" at each iteration. You don't try 650 random programs. You try 650 different ideas each learning from the results of previous trials. But, learn what? All those ideas where wrong. How does an LLM "lear…

Ask Edison about the light bulb

I beg your pardon?

Re: What sort of maths are LLMs good at?

#180

Post by antonvs »

inigyou wrote: post #165
antonvs wrote: post #151

Earlier quoted context omitted.

> Not in any useful way, though. Theorem provers and proof assistants like Lean, Coq/Rocq, Agda, Idris, NuPRL and Epigram all fundamentally depend on Curry-Howard. And again, the point is not that there’s some magical isomorphism, but that if LLMs are good at coding, they’re also likely to be good at certain classes of proof.

No they don't. They act on proofs, not on stupid conversions of proofs into useless programs.

You should take a look at "The Calculus of Constructions" (1988), which is one of the seminal papers that describes the basis for the Coq (now Rocq) theorem prover: https://www.academia.edu/47789825/The_calculus_of_constructi...

Here's a very relevant quote from the introduction:

> "The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda-expression, typed with propositions of the underlying logic. By removing types we get a pure lambda-expression, expressing its associated algorithm. Computing this lambda-expression corresponds roughly to cut-elimination. It is our thesis that (as already advocated by Martin-L6f [36]) the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of a very high-level functional programming language, with complex polymorphism well-suited for module specification [8]. The notion of type encompasses the usual notion of data type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate."

In other words, proofs are expressed as typed lambda terms, i.e. "proofs are programs". This is literally what such theorem provers are: examples of the Curry-Howard correspondence in action. If the correspondence didn't exist, none of these tools would exist.

Here are a couple of quotes from one of the Lean papers, "Theorem Proving in Lean", https://leanprover.github.io/theorem_proving_in_lean/theorem... :

> "This is the approach followed in the Calculus of Constructions, and hence in Lean as well. The fact that the rules for implication in a proof system for natural deduction correspond exactly to the rules governing abstraction and application for functions is an instance of the Curry-Howard isomorphism, sometimes known as the propositions-as-types paradigm."

> "The match statement is part of Lean’s function definition system, which provides convenient and expressive ways of defining complex functions. Once again, it is the Curry-Howard isomorphism that allows us to co-opt this mechanism for writing proofs as well."

All of the other theorem provers and proof assistants I mentioned rely on a similar approach.

Post reply on HN