But, learn what? All those ideas where wrong. How does an LLM "learn" from incorrect proofs that it has generated itself? What does it learn? Can you explain how this mechanism works?
But, learn what? All those ideas where wrong. How does an LLM "learn" from incorrect proofs that it has generated itself? What does it learn? Can you explain how this mechanism works?
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 evaluate an experiment and hypothesize what went wrong or what should stick. So the search space is dynamically evolving unlike pre-LLM algorithms.
Karpathy’s Autoresearch provides a proof of concept for this method.
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.
An empirical paper from 2024 that doesn't give a principled reason why LLMs will always be bad at self-verification.
Which is to say, I think your criticism is unfair and an attempt to avoid engaging with the arguments in the paper.