In training AlphaProof, it didn't actually matter whether the auto-formalization of a problem was correct, because asking the model to prove or disprove the statement worked either way — an incorrectly formalized (false) statement simply gets 'proved false,' so it remains usable as training data.
Thomas Ahle explains a key trick behind AlphaProof: since the model is trained to prove OR disprove a formalized statement, an incorrect auto-formalization still yields usable training signal, so correctness only needed to be checked by hand for the final IMO submissions. ✦ AI generated
Thomas Ahle · Machine Learning Street Talk · 2026-06-28 · original ↗
starts at this moment · 24:38
I think it's actually really trick in alpha proof was that when they did the formalization of the proof, it didn't really matter if they got it right or wrong because um if they just asked the model to provide a proof or a disproof. So if they if they got it wrong and it was no longer true then it would just prove that it was not true or like it would they would like you you could still use it.
verbatim transcript · starts at 24:38
24:38like AUM for example they're very focused on this part right like they and also in some sense alpha proof that's also the main thing it did was it started with a formalization um and then the hard part was training the model to provide a proof uh or a disproof I think it's actually really trick in alpha proof was that when they did the formalization of the proof, it
25:01didn't really matter if they got it right or wrong because um if they just asked the model to provide a proof or a disproof. So if they if they got it wrong and it was no longer true then it would just prove that it was not true or like it would they would like you you could still use it. uh of course like when they actually did the uh IMO uh
25:21challenges uh they wanted the form auto formalization to be correct um so then they did it by hand um but they didn't need it for the training which I think helps scale it up um I think yeah so we can do a similar thing with uh hardware by the way it's it's pretty easy to just take some chip design and then you know you can basically just come up with some
25:44properties that may and may not be true and then you can train the model to try and prove or disprove that this thing holds. Uh so then but that's all about creating the proof but then the autoformalization in some sense it's harder because um yeah it's it's all like because it's harder to to create the the training data for it right like I think that's kind of also a story about uh AI in the
26:05last two years since reinforcement learning like anything you can create good um RL environment for you can probably learn but anything else is like out of reach right now and so some of these chips have thousands of pages of specifications Um, and if you want to turn that you yeah you're turning that into a into a formal model. Um, it's not it doesn't really like if you got just a
26:29couple of words wrong somewhere or a couple of numbers um then it doesn't work like then what you prove is not uh is not important or it's not relevant. Um, and I think I mean it's always been an issue for in the chip industry like um that and they've kind of tried to solve it by having orthogonal teams. So they have one team that's designing the chip and one team that's designing the