本文为1656字，建议阅读4分钟
这两天Google DeepMind 推出一项名为AlphaGeometry的人工智能系统，其在《自然》杂志上发表论文称,在解决国际数学奥林匹克(International Mathematical Olympiad, IMO)中的几何问题上的表现,已接近甚至超过人类选手的平均水平。这标志着人工智能高级推理一个里程碑式进步
国际数学奥林匹克是世界上最负盛名的高中生数学竞赛。其中尤其以几何题最难,需要选手在有限时间内解决无限可能解法空间中的推理问题。AlphaGeometry系统由谷歌DeepMind的特里休·特林(Trieu H. Trinh)博士率领研发,通过与符号引擎相结合的神经网络语言模型,实现了几何定理自动推理。
在最新发表的论文中,AlphaGeometry系统被考验30道国际数学奥林匹克中的经典几何难题,其中成功解决了25道,超过了历史上平均获得金牌的人类选手的表现。这一成绩也远远超过了之前最强的计算机几何定理证明程序,后者最多只能解决10道题。
无人标注数据的挑战
长期以来,神经网络语言模型难以应用于自动定理证明领域的一个主要障碍,在于人类提供并标注的定理证明训练数据稀缺。尤其在几何领域,由于其图形表示翻译到机器可读语言的难度,使得可供模型训练的证明数量更少。
为解决训练数据不足的问题,AlphaGeometry系统采用了全新的数据生成方案。该系统自动随机生成了1亿条几何定理命题和相应的证明,构建成长度高达200多步的合成训练数据,其中90%为纯符号引擎推导步骤,10%带有辅助构造。这充分覆盖了奥林匹克几何题中必要的复杂构造和演绎推理。
在庞大的人造训练数据上预训练后,AlphaGeometry中的神经网络模型成功学会了符号引擎的行为,并在搜索证明过程中主动进行关键的辅助构造,从而找到难题的解法。这种不依赖人类数据标注的全自动方法,为更多数学定理自动证明领域提供了范例。
神经符号系统 引擎协同
AlphaGeometry系统采用了神经符号框架,即将神经网络与符号逻辑引擎有机结合。其中前者擅长直觉性地探索构造空间,后者擅长严谨地进行演绎推理。
证明搜索过程中,符号引擎先尝试直接推导,当无法继续前进时,语言模型则会输出一句新的辅助构造,如“过C作D的平行线”“E为三角形ABC的内心”等,从而扩展了引擎的演绎闭包,为找到定理的证明提供更多可能性。两者循环协同工作,直至发现完整的证明。
业界评价
AlphaGeometry系统的测试结果获得了业界的广泛关注。多位专家学者对其技术方式给予肯定,同时也提出了进一步改进的建议。
加州大学洛杉矶分校数学家陶哲轩(Terence Tao)认为这项工作成果“出人意料地强”,但他也指出,要将方法推广至更为创造性的数学领域还有一定差距。
英国爱丁堡大学历史学家迈克尔·巴拉尼(Michael Barany)则质疑仅以奥林匹克题目作为评判标准的意义。他说,大多数数学家的日常工作远比这更富创造性。
此外,高中生数学教练陈启天(Evan Chen)和几何学专家希瑟·麦克贝丝(Heather Macbeth)都对AlphaGeometry的证明结果进行了验证。他们肯定了其正确性,同时也对神经网络搜索方式充满好奇。
前谷歌AI研究员克里斯蒂安·塞格迪(Christian Szegedy)则指出,这一方法尚难以推广到其他数学领域,仍有很多问题有待解决
未来展望
尽管外界反响正面,AlphaGeometry的作者特里休·特林仍保持着谦逊的态度。他表示,这只是一个证明概念的初步实践,距离真正理解人类解题思维还很遥远。
特林博士的下一步计划是进一步加强系统的视觉感知能力,并尝试将这一框架方法推广至更多数学和逻辑推理领域。他希望能从中获得一些普适的启发,为建立更加智能和可信的AI系统提供帮助。
从1959年“几何定理机”(Geometry Theorem Prover, GTP)项目启动至今,自动几何推理研究已经走过60个年头。AlphaGeometry系统的出现无疑推进了这一领域的新进展。我们也期待见证人工智能在更加创造性的数学研究中大放异彩的那一天
结语
想要深入理解看这里
blog：https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/?utm_source=twitter&utm_medium=social
paper：https://www.nature.com/articles/s41586-023-06747-5
code：https://github.com/google-deepmind/alphageometry
作者本人视频解释：https://www.youtube.com/watch?v=TuZhU1CiC0k
⭐星标AI寒武纪，好内容不错过⭐
用你的赞和在看告诉我～
AI越来越强👇👇