7dc2
机械之心报道 编辑:蛋酱、陈陈 这个五一假期,天下顶级数学家是怎样度过的? 菲尔兹奖得主陶哲轩,似乎是忙着宣布自己的开源项目:「我在大模子的协助下编写了一个看法验证软件工具,用于验证涉及恣意正参数的给定预计是否建设(在常数因子规模内)。」 项目地点:https://github.com/teorth/estimates 在这个项目中,陶哲轩开发了一个用于自动(或半自动)证实剖析中预计值的框架。预计值是 X?Y(在渐近记法中体现 X=O (Y))或 X?Y(在渐近符号中体现 X=o (Y))形式的不等式。 为什么要做这样一个工具?这就要从近期陶哲轩和 Bjoern Bringmann(陶哲轩一经的博士生,现为普林斯顿大学助理教授)的讨论提及。 关于代数、微积分和数值剖析等领域的许大都学使命来说,符号数学软件包已经很是「蓬勃」了。但现在还没有类似的重大工具来验证渐近预计 —— 在损失稳固的情形下,关于恣意大的参数都应该建设的不等式。尤其主要的是函数预计,其中参数涉及一个未知函数或序列(保存于某个合适的函数空间,如一个空间)。 陶哲轩将二人的讨论效果写成了一篇博客,重点讨论了更简朴的渐近预计情形,即涉及有限数目的正实数,并使用加、乘、除、指数、最小值和最大值(但不包括减法)等算术运算举行组合。 「我已往曾希望能有一个工具能够自动判断此类预计是否建设(若是建设,则提供证实;若是不建设,则提供渐近反例)。」 现在,这个心愿实现了。 我们都知道,陶哲轩很是喜欢使用大模子来辅助解决数学问题。已往的大大都情形是完成较量简朴的编码使命,例如盘算然后绘制一些稍微重大的数学函数,或者对某些数据集举行一些基本的数据剖析。 这次,他决议给自己一个更具挑战性的使命:编写一个可以处置惩罚上述形式不等式的验证器。 原则上,这类形式的简朴不等式可以通过强力的案例拆分自动解决。单个这类的不等式都不太难手工求解,但有些应用需要磨练大宗这样的不等式,或者将其拆分成大宗案例。这项使命似乎很是适合自动化,尤其是在现代手艺的资助下。 陶哲轩这次用到的 AI 工具仍然是 ChatGPT。经由约莫四个小时的编程,在大模子的频仍协助下,他顺遂做出了一个看法验证工具。 与此同时,陶哲轩还放出了与 ChatGPT 的对话历程,不难发明,对话历程照旧蛮长的。 链接:https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8 一最先,陶哲轩就对 ChatGPT 提出了自己的需求:「我想编写一些 Python 类来操作符号表达式。并且希望有一个体现变量的类,好比 x、y、z…… 你能帮我编写一些具有这种功效的基础类来入门吗?」 ChatGPT 思索了 6 秒钟就给出了谜底。 这一步完成之后,下一轮对话最先,陶哲轩接着追问「我看到你用 add 实现了 + 操作,真棒。那么,实现 * 和 / 的对应要领是什么呢?」 ChatGPT 也给出了回覆: 在整个历程中,陶哲轩一直询问,ChatGPT 也做到了有问必答,不管是简朴的问题,照旧重大的问题,ChatGPT 都给解决了: 「怎样在与目今 python 文件相同的目录下导入 python 文件?」 最终,在 ChatGPT 的鼎力大举协助下,陶哲轩完成了这个看法验证软件工具。 着实,在众多着名数学家中,陶哲轩是较早接受并发明 ChatGPT 这类 AI 大模子数学价值的一个。他曾展望「若是使用适当,到 2026 年,AI 将成为数学研究和许多其他领域值得信托的合著者。」 陶哲轩不止一次借助大模子举行研究,他曾在 GPT-4 的资助下乐成解决了一个数学证实题(GPT4 提出了 8 种要领,其中 1 种乐成解决了问题),还在 AI 的资助下发明了自己论文中的一处隐藏 bug。 陶哲轩还建议各人若是想要开发这类软件,最好是数学家与专业程序员以协作的方法举行,这样才华优势互补。 「这虽然是一个极其不优雅的证实,但优雅并非重点,重点在于它是自动化的。」 回首整个历程,我们可以从陶哲轩的履历中获得一些启发,对大模子的开发使用,或许只是冰山一角,更多的功效等着各人去解锁。 https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/