OpenAI 发布模型实现自动定理证明，妈妈再也不用担心我的数学？
文章插图
作者 | 八宝粥
出品 | 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 这种惊人能力让人想到了当年的印度天才拉马努金 ， 他从来没有经历专业的数学训练 。 凭借自己的天赋 ， 用自己的符号和方式证明了很多已经存在的定理 。 著名的数学家哈代发现了他的天赋 ， 将其带往英国 ， 后发现了拉马努金猜想、整数分割和θ函数等著名的数学定理 。 如果机器真的都能变成一个个拉马努金 ， 那么不久的将来在数学甚至信息学界就会发生翻天覆地的变化 。
推荐阅读
- LG发布LG UltraFine OLED Pro显示器 首次引入OLED面板
- Kensington发布StudioDock 将iPad Pro扩展坞与无线充电器相结合
- 金士顿发布Workflow Station - 为内容创作者设计的模块化底座
- 微软新Surface Pro 7 Plus发布 拥有更大的电池、可拆卸的SSD和LTE模组
- 三星公司发布2021款数字座舱 集成诸多高科技
- 搭载骁龙888处理器+120W超充 横屏性能旗舰iQOO 7正式发布
- 499元！魅族新耳机正式发布：这外观太熟悉了
- 3798元起！iQOO 7正式发布：120W快充+骁龙888
- iQOO 7手机发布：首款120W快充骁龙888旗舰、120Hz全感触控
- “性能旗舰”iQOO 7正式发布：感受全感操控3798元起