易坊好文馆

  1. 首页 > 玩科技 >

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

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


我们来看看这 AI 是怎么在奥数题上施展拳脚的 。
AI 如何做奥数题
先来看一个简单的问题热热身：
对于所有大于等于 9 的整数 n，证明下图中的式子是一个完全平方数 。
AI|AI又对奥数下手 刷题刷出“模考”最好成绩
文章图片


按照普通人的思考方式，可以先把式中分子提出一个 n 的阶乘，与分母约去 。
然后分子化简为（n+1）2 。这在形式上就是一个完全平方数，问题得证 。
那 AI 是怎么做的呢？
它首先从文本中提取了条件和已知信息，例如 n 是整数、n 大于等于 9 。
接下来，它把需要证明的问题换了一种说法，改为：
存在一个整数 x，使 x2 和原式相等 。
AI|AI又对奥数下手 刷题刷出“模考”最好成绩
文章图片


然后在解题的过程中，完全由模型直接生成了一个数学项“n+1”作为一个解：use n+1 。接下来再去验证这个解是否成立 。
如果没有语言模型，这是不可能做到的 。
这么看来这模型能耐了，还有了一些数学想法，再拿一道国际奥赛的改编题来考考它：
设 a、b、c 是一个三角形的三条边，证明 a2（b+c-a）+b2（c+a-b）+c2（a+b-c）≤3abc 。
AI|AI又对奥数下手 刷题刷出“模考”最好成绩
文章图片


同样地，AI 还是先把条件都列出来 。不过这次还列出了与三角形有关的隐藏条件：
a、b、c 都是大于 0 的实数，并且有任意两边之和大于第三边 。
AI|AI又对奥数下手 刷题刷出“模考”最好成绩
文章图片


然后模型还自创了一个方法，列出了（b-a）、（c-b）、（c-a），看起来好像不明所以 。
但是如果把目标式子展开，你就会发现这三项正是舒尔不等式的几个对称项：
AI|AI又对奥数下手 刷题刷出“模考”最好成绩
文章图片


根据舒尔不等式，对所有非负实数 x、y、z 和正数 t，都有：
AI|AI又对奥数下手 刷题刷出“模考”最好成绩
文章图片


当 t=1 时，这和奥数题中的形式完全一样，命题得证 。
【AI|AI又对奥数下手 刷题刷出“模考”最好成绩】这么看来，AI 这水平着实不简单啊，要构造出这种效果可绝非易事 。
对奥数下手的难点
让 AI 来做奥数，确实比学生自己磕高数题难多了 。
这第一个难点就是，模型不是从有限的选项中做选择 。要是像下围棋那样，格点就那么多，选择空间有限，还好说一点 。
但是做奥数，模型要从一组复杂的无限策略中做选择，期间还要生成一些数学中的术语，例如“存在”、“任意”等 。
针对这个难点，OpenAI 通过在搜索证明方法时从语言模型中采样来解决 。
而第二点就是模型缺乏自我对抗和博弈 。做奥数题和双人游戏不同，它不是和另一个玩家比赛，而是要证明一个数学命题 。
这样一来在双人游戏上成功的算法就不能迁移过来 。
为了解决这个问题，研究人员提供了一套不同难度“教辅资料”，用来辅助描述问题而不需要证明 。
当这些辅助的描述难度越来越大时，模型就能解决越来越难的问题 。
不过这两个难点，反倒可以成为它的优势 。
一方面，因为这类数学命题的证明就是需要推理，需要无限的创造力和洞察力 。
另一方面，这种辅助描述式的方法也有助于 AI 自动推理的发展 。
说不好，将来深度学习模型还能征服奥数这座高山 。
参考链接：
https://openai.com/blog/formal-math/

    推荐阅读


    上一篇：Apple|iPhone屡次登上热搜榜和畅销榜 问题越多消费者却越爱？

    下一篇：IT|黄健翔呼吁按男足标准奖励中国女足 支付宝已安排