谷歌深度思维公司的明升体育app家开发了一个能解国际数学奥林匹克竞赛级别几何题的人工智能（AI）系统，其表现超过了之前最好的自动化定理证明系统。该研究证明了AI能以接近人类最高水平破解复杂逻辑挑战的潜力——这正是AI研究的一个主要目标。相关研究1月18日发表于《自然》。
奥林匹克水平的数学定理证明需要高水平的逻辑推理和解题能力。然而，当前基于机器学习的AI系统在证明数学定理方面还有困难。机器学习这种AI形式通过向计算机提供参考数据，让计算机学习如何执行特定任务，但由于作为训练数据的人类示范很少，所以定理证明（尤其是几何学定理）很难被掌握。
谷歌深度思维的Trieu Trinh和同事描述了一种不需要人类示范的定理证明方法。该系统名为G0，通过综合复杂程度各异的数百万条定理和证明，利用一个神经语言模型完成自我训练。这种方法结合符号演绎引擎（能搜索难题中的大量分支点），能让G0在无需人类直接输入的情况下学习并解开复杂问题。
研究者用国际数学奥林匹克竞赛（优等高中生参加的数学定理证明大赛）2000~2020年的30个问题测试了该系统。G0解出了其中25题，接近国际数学奥林匹克竞赛金牌选手的平均表现，而之前最优秀的方法只解出了10题。值得一提的是，G0能生成人类可阅读的证明，甚至发现了2004年国际数学奥林匹克竞赛定理的一个新版本。
作者指出，G0目前仅限于几何学，但这种方法或许也能应用于其他数学领域。
相关论文信息：
http://doi.org/10.1038/s41586-023-06747-5
版权声明：凡本网注明“来源：明升官网明升体育app报、明升手机版(明升官网)、明升体育app手机版杂志”的所有作品，网站转载，请在正文上方注明来源和作者，且不得对内容作实质性改动；微信公众号、明升头条号等新媒体平台，转载请联系授权。邮箱：shouquan@stimes.cn。