2 ms·
> Sampling is what AI is good at. You might think so, but I tried asking ChatGPT to solve one of the puzzles from https://en.wikipedia.org/wiki/Countdown_(game
by zahlman 3mo ago
> Sampling is what AI is good at.
You might think so, but I tried asking ChatGPT to solve one of the puzzles from https://en.wikipedia.org/wiki/Countdown_(game_show) https://en.wikipedia.org/wiki/Countdown_(game_show) (which a Python script can brute-force on my 12-year-old hardware in half a second) and it made an elementary arithmetic error that's decidedly not human-like.
- TuringTest 3mo agoLLMs are terrible at anything systematic. They're incredibly good at anything heuristic, so it makes sense that they can explore wide mathematical spaces fast and converge towards interesting regions. 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. You need to combine them with a proper logical problem solver to get the best parts of both.
- wyager 3mo ago> 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 operating procedure for any LLM math discovery!
- deleted 3mo ago[deleted]
- TuringTest 3mo agoYeah 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 tooling is a must, the statistical essential nature of generating content from weights is 1) error prone and 2) not suitable for chains of systematic reasoning that are longer than the attention span. The proofs will be only as good as the framework for linking successive instances of reasoning.
- black_knight 3mo agoNot 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’t!
- zahlman 2mo agoThe thread title is "What sort of maths are LLMs good at?" The codebase you describe would be an external tool in GP's conception.
- black_knight 2mo agoIf I walked outside, I would also be an external tool. So, I don't.
- wyager 2mo agoEvery LLM harness released in the last year has handled this gracefully via delegation, structured memory systems, etc.
- deleted 2mo ago[deleted]
- CamperBob2 3mo ago"ChatGPT" could mean anything from Instant to Pro. What was the prompt, and which model(s) did you try?
- redox99 3mo agoAlmost surely the free model on the web ui. So a dumb model, no harness, and probably a bad prompt.
- nullsanity 3mo ago[dead]
- zahlman 2mo agoMy point was that the kind of error it made was nothing like the kind of error a contestant would make.
- CamperBob2 2mo agoThe differences between 'instant' chat models and frontier-grade models are enough to render any such test a waste of electricity.