(I’m not sure whether I’m supposed to nitpick. If I were nitpicking I’d ask things like: Wait are you allowing it to see preexisting computer-generated proofs? What counts as computer generated? Are you allowing it to see the parts of papers where humans state and discuss propositions and just cutting out the proofs? Is this system somehow trained on a giant human text corpus, but just without the math proofs?)
But if you mean basically “the AI has no access to human math content except a minimal game environment of formal logic, plus whatever abstract priors seep in via the training algorithm+prior, plus whatever general thinking patterns in [human text that’s definitely not mathy, e.g. blog post about apricots]”, then yeah, this would be really crazy to see. My points are trying to be, not minimally hard, but at least easier-ish in some sense. Your thing seems significantly harder (though nicely much more operationalized); I think it’d probably imply my “come up with interesting math concepts”? (Note that I would not necessary say the same thing if it was >25% of IMO problems; there I’d be significantly more unsure, and would defer to you / Sam, or someone who has a sense for the complexity of the full proofs there and the canonicalness of the necessary lemmas and so on.)
I didn’t express this clearly, but yea I meant no pretraining on human text at all, and also nothing computer-generated which “uses human mathematical ideas” (beyond what is in base ZFC), but I’d probably allow something like the synthetic data generation used for AlphaGeometry (Fig. 3) except in base ZFC and giving away very little human math inside the deduction engine. I agree this would be very crazy to see. The version with pretraining on non-mathy text is also interesting and would still be totally crazy to see. I agree it would probably imply your “come up with interesting math concepts”. But I wouldn’t be surprised if like >20% of the people on LW who think A[G/S]I happens in like 2−3 years thought that my thing could totally happen in 2025 if the labs were aiming for it (though they might not expect the labs to aim for it), with your things plausibly happening later. E.g. maybe such a person would think “AlphaProof is already mostly RL/search and one could replicate its performance soon without human data, and anyway, AlphaGeometry already pretty much did this for geometry (and AlphaZero did it for chess)” and “some RL+search+self-play thing could get to solving major open problems in math in 2 years, and plausibly at that point human data isn’t so critical, and IMO problems are easier than major open problems, so plausibly some such thing gets to IMO problems in 1 year”. But also idk maybe this doesn’t hang together enough for such people to exist. I wonder if one can use this kind of idea to get a different operationalization with parties interested in taking each side though. Like, maybe whether such a system would prove Cantor’s theorem (stated in base ZFC) (imo this would still be pretty crazy to see)? Or whether such a system would get to IMO combos relying moderately less on human data?
I’d probably allow something like the synthetic data generation used for AlphaGeometry (Fig. 3) except in base ZFC and giving away very little human math inside the deduction engine
IIUC yeah, that definitely seems fair; I’d probably also allow various other substantial “quasi-mathematical meta-ideas” to seep in, e.g. other tricks for self-generating a curriculum of training data.
But I wouldn’t be surprised if like >20% of the people on LW who think A[G/S]I happens in like 2-3 years thought that my thing could totally happen in 2025 if the labs were aiming for it (though they might not expect the labs to aim for it), with your things plausibly happening later
Mhm, that seems quite plausible, yeah, and that does make me want to use your thing as a go-to example.
whether such a system would prove Cantor’s theorem (stated in base ZFC) (imo this would still be pretty crazy to see)?
This one I feel a lot less confident of, though I could plausibly get more confident if I thought about the proof in more detail.
Part of the spirit here, for me, is something like: Yes, AIs will do very impressive things on “highly algebraic” problems / parts of problems. (See “Algebraicness”.) One of the harder things for AIs is, poetically speaking, “self-constructing its life-world”, or in other words “coming up with lots of concepts to understand the material it’s dealing with, and then transitioning so that the material it’s dealing with is those new concepts, and so on”. For any given math problem, I could be mistaken about how algebraic it is (or, how much of its difficulty for humans is due to the algebraic parts), and how much conceptual progress you have to do to get to a point where the remaining work is just algebraic. I assume that human math is a big mix of algebraic and non-algebraic stuff. So I get really surprised when an AlphaMath can reinvent most of the definitions that we use, but I’m a lot less sure about a smaller subset because I’m less sure if it just has a surprisingly small non-algebraic part. (I think that someone with a lot more sense of the math in general, and formal proofs in particular, could plausibly call this stuff in advance significantly better than just my pretty weak “it’s hard to do all of a wide variety of problems”.)
(I’m not sure whether I’m supposed to nitpick. If I were nitpicking I’d ask things like: Wait are you allowing it to see preexisting computer-generated proofs? What counts as computer generated? Are you allowing it to see the parts of papers where humans state and discuss propositions and just cutting out the proofs? Is this system somehow trained on a giant human text corpus, but just without the math proofs?)
But if you mean basically “the AI has no access to human math content except a minimal game environment of formal logic, plus whatever abstract priors seep in via the training algorithm+prior, plus whatever general thinking patterns in [human text that’s definitely not mathy, e.g. blog post about apricots]”, then yeah, this would be really crazy to see. My points are trying to be, not minimally hard, but at least easier-ish in some sense. Your thing seems significantly harder (though nicely much more operationalized); I think it’d probably imply my “come up with interesting math concepts”? (Note that I would not necessary say the same thing if it was >25% of IMO problems; there I’d be significantly more unsure, and would defer to you / Sam, or someone who has a sense for the complexity of the full proofs there and the canonicalness of the necessary lemmas and so on.)
I didn’t express this clearly, but yea I meant no pretraining on human text at all, and also nothing computer-generated which “uses human mathematical ideas” (beyond what is in base ZFC), but I’d probably allow something like the synthetic data generation used for AlphaGeometry (Fig. 3) except in base ZFC and giving away very little human math inside the deduction engine. I agree this would be very crazy to see. The version with pretraining on non-mathy text is also interesting and would still be totally crazy to see. I agree it would probably imply your “come up with interesting math concepts”. But I wouldn’t be surprised if like >20% of the people on LW who think A[G/S]I happens in like 2−3 years thought that my thing could totally happen in 2025 if the labs were aiming for it (though they might not expect the labs to aim for it), with your things plausibly happening later. E.g. maybe such a person would think “AlphaProof is already mostly RL/search and one could replicate its performance soon without human data, and anyway, AlphaGeometry already pretty much did this for geometry (and AlphaZero did it for chess)” and “some RL+search+self-play thing could get to solving major open problems in math in 2 years, and plausibly at that point human data isn’t so critical, and IMO problems are easier than major open problems, so plausibly some such thing gets to IMO problems in 1 year”. But also idk maybe this doesn’t hang together enough for such people to exist. I wonder if one can use this kind of idea to get a different operationalization with parties interested in taking each side though. Like, maybe whether such a system would prove Cantor’s theorem (stated in base ZFC) (imo this would still be pretty crazy to see)? Or whether such a system would get to IMO combos relying moderately less on human data?
IIUC yeah, that definitely seems fair; I’d probably also allow various other substantial “quasi-mathematical meta-ideas” to seep in, e.g. other tricks for self-generating a curriculum of training data.
Mhm, that seems quite plausible, yeah, and that does make me want to use your thing as a go-to example.
This one I feel a lot less confident of, though I could plausibly get more confident if I thought about the proof in more detail.
Part of the spirit here, for me, is something like: Yes, AIs will do very impressive things on “highly algebraic” problems / parts of problems. (See “Algebraicness”.) One of the harder things for AIs is, poetically speaking, “self-constructing its life-world”, or in other words “coming up with lots of concepts to understand the material it’s dealing with, and then transitioning so that the material it’s dealing with is those new concepts, and so on”. For any given math problem, I could be mistaken about how algebraic it is (or, how much of its difficulty for humans is due to the algebraic parts), and how much conceptual progress you have to do to get to a point where the remaining work is just algebraic. I assume that human math is a big mix of algebraic and non-algebraic stuff. So I get really surprised when an AlphaMath can reinvent most of the definitions that we use, but I’m a lot less sure about a smaller subset because I’m less sure if it just has a surprisingly small non-algebraic part. (I think that someone with a lot more sense of the math in general, and formal proofs in particular, could plausibly call this stuff in advance significantly better than just my pretty weak “it’s hard to do all of a wide variety of problems”.)