Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

本周二,我们报道了菲尔兹奖得主陶哲轩的一个开源项目 —— 在大模型的协助下编写了一个概念验证软件工具,来验证涉及任意正参数的给定估计是否成立(在常数因子范围内)。

本周二,我们报道了菲尔兹奖得主陶哲轩的一个开源项目 —— 在大模型的协助下编写了一个概念验证软件工具,来验证涉及任意正参数的给定估计是否成立(在常数因子范围内)。

在项目中,他开发了一个用于自动(或半自动)证明分析中估计值的框架。估计值是 X≲Y(在渐近记法中表示 X=O (Y))或 X≪Y(在渐近符号中表示 X=o (Y))形式的不等式。

这才几天的时间,这个估计验证工具的 2.0 版本就来了!

Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

陶哲轩对该工具进行了两次全面改进。

首先,他将其改造成一个基础的证明助手(proof assistant),同时能够处理一些命题逻辑;接着,他根据评论者的反馈,将其改造成一个更加灵活的证明助手(在几个关键方面特意模仿了 Lean 证明助手),它也由功能强大的 Python 符号代数包 sympy 提供支持。

陶哲轩认为现在得到了一个稳定的框架,并可以进一步扩展该工具。他最初的目标只是自动化(或半自动化)标量函数渐近估计的证明,但原则上可以继续向该工具添加策略、新的 sympy 类型和引理,以处理范围广泛的其他数学任务。

该证明助手的 2.0 版本已经上传到了 GitHub。同样地,与自己以前的编码一样,陶哲轩最终「严重」依赖大语言模型的帮助来理解 Python 和 sympy 的一些细节,其中 Github Copilot 的自动补全功能尤其有用。

虽然该工具支持全自动证明,但陶哲轩决定现在更多地关注半自动交互式证明,其中人类用户提供高级「策略」,然后证明助手执行必要的计算,直到证明完成。

Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

GitHub 地址:https://github.com/teorth/estimates

根据项目简介,这是一个利用 Python 开发的轻量级证明助手,其功能远逊于 Lean、Isabelle 或 Rocq 等完整证明助手,但希望它能够轻松用于证明一些简短而繁琐的任务,例如验证一个不等式或估计是否由其他不等式或估计推导出来。该助手的一个具体目标是为渐近估计(asymptotic estimates)提供支持。

具体实现过程

下载相关文件后,即可在 Python 中启动证明助手,只需输入「from main import *」并加载一个预先制作的练习即可。以下是其中一个练习:

Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

这是证明助手对以下问题的形式化描述:如果 x, y, z 是正实数,且 x<2y 且 y<3z+1,则证明 x<7z+2。

证明助手的工作方式是:用户指示助手使用各种「策略」来简化问题,直到问题得到解决。在本例中,该问题可以通过线性算法求解,具体形式化为「Linarith ()」策略:

Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

如果有人想更详细地了解线性算法的工作原理,可以使用「verbose」标志(flag)来运行此策略。

Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

有时,证明过程会涉及情况拆分,最终的证明会呈现出树状结构。这里有个例子:其务是证明假设 (x>-1)∧(x<1) 且 (y>-2)∧(y<2) 蕴涵 (x+y>-3)∧(x+y<3):

Copilot上大分,仅数天,陶哲轩的估计验证工具卷到2.0!刚刚又发数学形式化证明视频

这里,根据使用的三种策略对证明进行「伪精益」描述:策略「cases h」 1 对假设「 h1」进行情况拆分,然后在两种情况下分别应用「simp_all」策略来简化。

该工具支持渐近估计。陶哲轩找到了一种在 Sympy 中实现量级形式化的方法。事实证明,Sympy 在某种意义上已经可以原生实现非标准分析:它的符号变量有一个「is_number」标志,基本上对应于非标准分析中「标准」数的概念。

举例而言,数字 3 的「sympy」版本「S (3)」有「S (3).is_number == True」,因此是标准的;而整数变量「n = Symbol (\”n\”, integer=true)」有「n.is_number == False 」,因此是非标准的。

在「sympy」中,他能够构建各种(正)表达式「X」的数量级「Theta (X)」,其属性「 Theta (n)=Theta (1)」如下:如果「n」是标准数,然后使用这个概念来定义渐近估计,例如

AI新闻资讯

Manus 背后的重要 Infra,E2B 如何给 AI Agents 配备“专属电脑”?

2025-5-11 15:33:09

AI新闻资讯

字节Seed首次开源代码模型,拿下同规模多个SOTA,提出用小模型管理数据范式

2025-5-11 15:33:15

0 条回复 A文章作者 M管理员
欢迎您,新朋友,感谢参与互动!
    暂无讨论,说说你的看法吧
个人中心
购物车
优惠劵
今日签到
私信列表
搜索