AI 又对奥数下手，刷题刷出“模考”最好成绩

图片地址：https://img.ithome.com/newsuploadfiles/2022/2/58e88170-49a6-4cbc-a8e5-6524d8a12adf.png

AI 在最不擅长的数学方面，这次大幅刷新了最好成绩。其中关键角色是 OpenAI 给 Lean 做的一个定理证明器。听起来有点耳熟？没错，就是去年参加国际数学奥林匹克竞赛（IMO）的“非人”选手 Lean~自从 2013 年微软研究院推出 Lean 以来，就一直尝试让 AI 在数学命题证明这方面取得进展。而这次也确实得到了回报，OpenAI 新做的这个定理证明器让它学会了解决一部分有难度的高中奥数题，包括美国的数学竞赛 AMC12、AIME 甚至是国际奥数竞赛中的题。它首先会用语言模型将数学问题转化为另一种形式，列出隐藏的条件和已知信息，然后来推理求证。虽然在刚开始效果并不明显，只能证明几个命题。但是在不断地搜索新的证明，经过八次迭代之后，在 miniF2F 测试中，成功地把分数从 29.3% 刷到了 41.2%。我们来看看这 AI 是怎么在奥数题上施展拳脚的。AI 如何做奥数题先来看一个简单的问题热热身：对于所有大于等于 9