OpenAI 发布模型实现自动定理证明，妈妈再也不用担心我的数学？作者|八宝粥出品|CSDN(ID:CSDNnews)Ope

文章插图
作者 | 八宝粥
出品 | CSDN(ID:CSDNnews)
文章插图
OpenAI 大招频出，染指数学江湖
日前， OpenAI 研究者Stanislas Polu和Ilya Sutskever在社交媒体发布消息，宣布在预印本发布文章，展示了一个基于Transformer 的自动定理证明模型。文章表示，团队在 Metamath 库上取得了新的进展，通过将深度学习和形式系统相结合能带来更好的效果。
文章插图
论文两位作者在社交网络分享发布新模型的喜悦
团队表示， GPT-f 可以自动证明 Metamath 当中23个定理。横向对比上， GPT-f 最佳模型实现 Metamath 56.22% 的保留测试集，而目前最先进的 MetaGen-IL 只有 21.16% 的证明能力。
文章还给出了数据集 set.mm 和证明助手的一个 demo：
文章插图
“自动定理证明”对于饱受数学困扰的同学来说简直就是大杀器，比拟“步步高点读机” ，笔者不禁想到自己中学数学做题时自信地刷刷写下“证明”二字和面对高等数学挠头时候的“这也能证？” ， “要是机器能帮我证明就好了” 。
实际上，在数学界，确实有很多问题需要机器来帮忙。但是 GPT-f 真的是数学界的 AlphaGo 吗？数学家也要望机器兴叹了吗？似乎也并不是这样。
文章插图
数学天才也需要机器
前段时间获得诺贝尔物理学奖的科学家罗杰·彭罗斯，他在数学方面有一个很有趣的贡献，就是彭罗斯密铺， 1976年，他提出采用两种不同的菱形进行密铺，实现对平面的全覆盖。而放眼三维，早在十七世纪，德国天文学家开普勒就对三维欧式空间当中容纳球的方式进行研究，发现三维球堆积的最大密度为：
文章插图
而这个定理直到 1998 年由机器来辅助证明的。就是那种你明明知道却证不出来的感觉。直到 2014年才由黑尔斯的 FlysPeck 项目完成了形式化证明。
说到推理，就肯定会提到计算机界的鼻祖图灵大佬。二战期间，德军采用恩格玛机器加密，给盟军的情报获取造成了极大的打击。为了破解密码，盟军招募大量人力组建团队，对密码机进行研究，后发明“图灵炸弹（Turing Bombe）” ，虽然对恩格玛的破解是波兰人，但是毫无疑问图灵是恩格玛破解的最大功臣。此后“图灵炸弹”在布莱切利继续发挥作用，给密码破译工作加速。图灵以他的名字命名的抽象计算模型——图灵机也是通过机器来模拟人类计算的过程。后来成为计算机历史上具有浓墨重彩的一页。
机器辅助证明已经成为了单独的数学研究方向，而人工智能更多地研究的是让机器自主去发现和探索数学定理。就好比 AlphaGo 或者 AutoML 一样，机器可以自己去探索和研究。人们期待计算机能给人带来更多惊喜。 GPT 这种惊人能力让人想到了当年的印度天才拉马努金，他从来没有经历专业的数学训练。凭借自己的天赋，用自己的符号和方式证明了很多已经存在的定理。著名的数学家哈代发现了他的天赋，将其带往英国，后发现了拉马努金猜想、整数分割和θ函数等著名的数学定理。如果机器真的都能变成一个个拉马努金，那么不久的将来在数学甚至信息学界就会发生翻天覆地的变化。