5 ms·
LLMs are terrible at anything systematic. They're incredibly good at anything heuristic, so it makes sense that they can explore wide mathematical spaces fast a
by TuringTest 1mo ago
LLMs 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 1mo 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 1mo ago[deleted]
- TuringTest 1mo 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 1mo 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 1mo 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 1mo agoIf I walked outside, I would also be an external tool. So, I don't.
- wyager 1mo agoEvery LLM harness released in the last year has handled this gracefully via delegation, structured memory systems, etc.
- deleted 1mo ago[deleted]