据新智元报道,近日热衷于用 GPT-4、Copilot 做研究的数学大神陶哲轩,在 AI 的帮助下发现了自己论文中的一处隐藏 bug。一些数学爱好者粉丝在此帖中惊呼:这太惊人了,很高兴看到 AI 证明助手的传播,为数学研究的未来奠定了更坚实的基础。 陶哲轩对此表示,“这是完全有可能的事。或许在不久的将来,我们就可以在 Lean 之上构建一个 AI 层。只要把证明中的各步描述给 AI,AI 就可以利用 Lean 来执行证明了,过程中还能各种调用计算机代数软件包。” 今年 6 月,陶哲轩就曾在 GPT-4 试用体验的博客中预言:2026 年,AI 将与搜索和符号数学工具相结合,成为数学研究中值得信赖的合著者。这期间,不断有人证明着这一点,比如加州理工、英伟达、MIT 等机构的学者,就构建出一个基于开源 LLM 的定理证明器。
数学大神陶哲轩在 AI 的帮助下发现自己论文中的一处隐藏漏洞
本文来自网络,不代表本站立场,转载请注明出处:https://news9.com.cn/n/a49922.html