在训练AlphaProof时，问题的自动形式化（auto-formalization）是否正确其实并不重要，因为无论如何，让模型去证明或证伪这个命题都是有效的——一个被错误形式化（即实际为假）的命题，只会被'证明为假'，因此仍然可以作为训练数据使用。

Thomas Ahle解释了AlphaProof背后的一个关键技巧：由于模型被训练来证明或证伪一个形式化命题，即便自动形式化出错，依然能产生可用的训练信号，因此只有在最终提交IMO答案时才需要人工核实正确性。 ✦ AI 生成 · 平台预翻

Thomas Ahle · Machine Learning Street Talk · 2026-06-28 · English original →

我觉得AlphaProof里其实有一个很巧妙的技巧，就是他们在做证明的形式化的时候，其实做对做错都无所谓，因为呃，只要他们让模型去提供一个证明或者证伪就行。所以如果他们做错了，命题不再成立，那模型就会去证明它不成立，或者说……反正你还是可以拿它来用。

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.

回到原声 ↗逐字转录 · 起于 24:38 · 中文为平台译文