Outside of [coding], I don’t know of it being more than a somewhat better google
I’ve recently tried heavily leveraging o3 as part of a math-research loop.
I have never been more bearish on LLMs automating any kind of research than I am now.
And I’ve tried lots of ways to make it work. I’ve tried telling it to solve the problem without any further directions, I’ve tried telling it to analyze the problem instead of attempting to solve it, I’ve tried dumping my own analysis of the problem into its context window, I’ve tried getting it to search for relevant lemmas/proofs in math literature instead of attempting to solve it, I’ve tried picking out a subproblem and telling it to focus on that, I’ve tried giving it directions/proof sketches, I’ve tried various power-user system prompts, I’ve tried resampling the output thrice and picking the best one. None of this made it particularly helpful, and the bulk of the time was spent trying to spot where it’s lying or confabulating to me in its arguments or proofs (which it ~always did).
It was kind of okay for tasks like “here’s a toy setup, use a well-known formula to compute the relationships between A and B”, or “try to rearrange this expression into a specific form using well-known identities”, which are relatively menial and freed up my working memory for more complicated tasks. But it’s pretty minor usefulness (and you have to re-check the outputs for errors anyway).
I assume there are math problems at which they do okay, but that capability sure is brittle. I don’t want to overupdate here, but geez, getting LLMs from here to the Singularity in 2-3 years just doesn’t feel plausible.
[disclaimer, not a math guy, only barely knows what he’s talking about, if this next thought is stupid I’m interested to learn more]
I don’t expect this to fix it right now, but, one thing I don’t think you listed is doing the work in lean or some other proof assistant that lets you check results immediately? I expect LLMs to first be able to do math in that format because it’s the format you can actually do a lot of training in. And it’d mean you can verify results more quickly.
My current vague understanding is that lean is normally too cumbersome to be a reasonable to work in, but, that’s the sort of thing that could change with LLMs in the mix.
I did actually try a bit of that back in the o1 days. What I’ve found is that getting LLMs to output formal Lean proofs is pretty difficult: they really don’t want to do that. When they’re not making mistakes, they use informal language as connective tissue between Lean snippets, they put in “sorry”s (a placeholder that makes a lemma evaluate as proven), and otherwise try to weasel out of it.
This is something that should be solvable by fine-tuning, but at the time, there weren’t any publicly available decent models fine-tuned for that.
We do have DeepSeek-Prover-V2 now, though. I should look into it at some point. But I am not optimistic, sounds like it’s doing the same stuff, just more cleverly.
(I had a bit of an epistemic rollercoaster making this prediction, I updated “by the time someone makes an actually worthwhile Math AI, even if lean was an important part of it’s training process, it’s probably not that hard to do additional fine tuning that gets it to output stuff in a more standard mathy format. But, then, it seemed like it was still going to be important to quickly check it wasn’t blatantly broken as part of the process)
(Disclaimer: only partially relevant rant.)
I’ve recently tried heavily leveraging o3 as part of a math-research loop.
I have never been more bearish on LLMs automating any kind of research than I am now.
And I’ve tried lots of ways to make it work. I’ve tried telling it to solve the problem without any further directions, I’ve tried telling it to analyze the problem instead of attempting to solve it, I’ve tried dumping my own analysis of the problem into its context window, I’ve tried getting it to search for relevant lemmas/proofs in math literature instead of attempting to solve it, I’ve tried picking out a subproblem and telling it to focus on that, I’ve tried giving it directions/proof sketches, I’ve tried various power-user system prompts, I’ve tried resampling the output thrice and picking the best one. None of this made it particularly helpful, and the bulk of the time was spent trying to spot where it’s lying or confabulating to me in its arguments or proofs (which it ~always did).
It was kind of okay for tasks like “here’s a toy setup, use a well-known formula to compute the relationships between A and B”, or “try to rearrange this expression into a specific form using well-known identities”, which are relatively menial and freed up my working memory for more complicated tasks. But it’s pretty minor usefulness (and you have to re-check the outputs for errors anyway).
I assume there are math problems at which they do okay, but that capability sure is brittle. I don’t want to overupdate here, but geez, getting LLMs from here to the Singularity in 2-3 years just doesn’t feel plausible.
Nod.
[disclaimer, not a math guy, only barely knows what he’s talking about, if this next thought is stupid I’m interested to learn more]
I don’t expect this to fix it right now, but, one thing I don’t think you listed is doing the work in lean or some other proof assistant that lets you check results immediately? I expect LLMs to first be able to do math in that format because it’s the format you can actually do a lot of training in. And it’d mean you can verify results more quickly.
My current vague understanding is that lean is normally too cumbersome to be a reasonable to work in, but, that’s the sort of thing that could change with LLMs in the mix.
I agree that it’s a promising direction.
I did actually try a bit of that back in the o1 days. What I’ve found is that getting LLMs to output formal Lean proofs is pretty difficult: they really don’t want to do that. When they’re not making mistakes, they use informal language as connective tissue between Lean snippets, they put in “sorry”s (a placeholder that makes a lemma evaluate as proven), and otherwise try to weasel out of it.
This is something that should be solvable by fine-tuning, but at the time, there weren’t any publicly available decent models fine-tuned for that.
We do have DeepSeek-Prover-V2 now, though. I should look into it at some point. But I am not optimistic, sounds like it’s doing the same stuff, just more cleverly.
Relevant: Terence Tao does find them helpful for some Lean-related applications.
yeah, it’s less that I’d bet it works now, just, whenever it DOES start working, it seems likely it’d be through this mechanism.
⚖ If Thane Ruthenis thinks there are AI tools that can meaningfully help with Math by this point, did they first have a noticeable period (> 1 month) where it was easier to get work out of them via working in lean-or-similar? (Raymond Arnold: 25% & 60%)
(I had a bit of an epistemic rollercoaster making this prediction, I updated “by the time someone makes an actually worthwhile Math AI, even if lean was an important part of it’s training process, it’s probably not that hard to do additional fine tuning that gets it to output stuff in a more standard mathy format. But, then, it seemed like it was still going to be important to quickly check it wasn’t blatantly broken as part of the process)