行早 发自 凹非寺
量子位 | 公众号 QbitAI
AI在蕞不擅长得数学方面，这次大幅刷新了蕞好成绩。
其中关键角色是OpenAI给Lean做得一个定理证明器。
听起来有点耳熟？没错，就是去年参加国际数学奥林匹克竞赛（IMO）得“非人”选手Lean~
自从2013年微软研究院推出Lean以来，就一直尝试让AI在数学命题证明这方面取得进展。
而这次也确实得到了回报，OpenAI新做得这个定理证明器让它学会了解决一部分有难度得高中奥数题，包括美国得数学竞赛AMC12、AIME甚至是国际奥数竞赛中得题。
它首先会用语言模型将数学问题转化为另一种形式，列出隐藏得条件和已知信息，然后来推理求证。
虽然在刚开始效果并不明显，只能证明几个命题。但是在不断地搜索新得证明，经过八次迭代之后，在miniF2F测试中，成功地把分数从29.3%刷到了41.2%。
我们来看看这AI是怎么在奥数题上施展拳脚得。
AI如何做奥数题先来看一个简单得问题热热身：
对于所有大于等于9得整数n，证明下图中得式子是一个完全平方数。
按照普通人得思考方式，可以先把式中分子提出一个n得阶乘，与分母约去。
然后分子化简为（n+1）2。这在形式上就是一个完全平方数，问题得证。
那AI是怎么做得呢？
它首先从文本中提取了条件和已知信息，例如n是整数、n大于等于9。
接下来，它把需要证明得问题换了一种说法，改为：
存在一个整数x，使x2和原式相等。
然后在解题得过程中，完全由模型直接生成了一个数学项“n+1”作为一个解：use n+1。接下来再去验证这个解是否成立。
如果没有语言模型，这是不可能做到得。
这么看来这模型能耐了，还有了一些数学想法，再拿一道国际奥赛得改编题来考考它：
设a、b、c是一个三角形得三条边，证明a2（b+c-a）+b2（c+a-b）+c2（a+b-c）≤3abc。
同样地，AI还是先把条件都列出来。不过这次还列出了与三角形有关得隐藏条件：
a、b、c都是大于0得实数，并且有任意两边之和大于第三边。
然后模型还自创了一个方法，列出了（b-a）、（c-b）、（c-a），看起来好像不明所以。
但是如果把目标式子展开，你就会发现这三项正是舒尔不等式得几个对称项：
根据舒尔不等式，对所有非负实数x、y、z和正数t，都有：
当t=1时，这和奥数题中得形式完全一样，命题得证。
这么看来，AI这水平着实不简单啊，要构造出这种效果可绝非易事。
对奥数下手得难点让AI来做奥数，确实比学生自己磕高数题难多了。
这第壹个难点就是，模型不是从有限得选项中做选择。要是像下围棋那样，格点就那么多，选择空间有限，还好说一点。
但是做奥数，模型要从一组复杂得无限策略中做选择，期间还要生成一些数学中得术语，例如“存在”、“任意”等。
针对这个难点，OpenAI通过在搜索证明方法时从语言模型中采样来解决。
而第二点就是模型缺乏自我对抗和博弈。做奥数题和双人不同，它不是和另一个玩家比赛，而是要证明一个数学命题。
这样一来在双人上成功得算法就不能迁移过来。
为了解决这个问题，研究人员提供了一套不同难度“教辅资料”，用来帮助描述问题而不需要证明。
当这些帮助得描述难度越来越大时，模型就能解决越来越难得问题。
不过这两个难点，反倒可以成为它得优势。
一方面，因为这类数学命题得证明就是需要推理，需要无限得创造力和洞察力。
另一方面，这种帮助描述式得方法也有助于AI自动推理得发展。
说不好，将来深度学习模型还能征服奥数这座高山。
参考链接：
openai/blog/formal-math/
— 完 —
量子位 QbitAI · 头条号签约
我们，第壹时间获知前沿科技动态
