A proof of concept tool to verify estimates

Source | HN Comments

文章介绍了一个概念验证工具，用于验证数学中的渐近估计。该工具基于 Python，利用了大型语言模型辅助编程。它能够处理涉及正实数算术运算的简单不等式，并提供证明或反例。文章展示了该工具验证不等式的示例，并讨论了其局限性。作者认为，该工具可以扩展，并设想了更复杂的应用，例如验证函数估计和多元线性表达式。作者还探讨了未来开发的方向，包括协作项目、与现有平台的整合以及 AI 在验证过程中的应用。

验证估计的 Proof of Concept 工具

2025年5月1日，发布于 math.AP, math.CA | 标签: Software | 作者：Terence Tao

这篇文章的灵感来自于最近与 Bjoern Bringmann 的一些讨论。符号数学软件包在许多数学任务（如代数、微积分和数值分析等领域）中得到了高度发展。然而，据我所知，我们没有类似复杂的工具来验证渐近估计——对于任意大的参数都应该成立的不等式，并带有常数损失。特别重要的是函数估计，其中参数涉及到一个未知的函数或序列（存在于一些合适的函数空间中，例如 ${L^p}$ 空间）；但在这篇文章中，我将重点关注更简单的情况，即涉及有限数量的正实数的渐近估计，这些正实数通过算术运算（如加法、乘法、除法、指数运算以及最小值和最大值（但没有减法））组合在一起。这里的一个典型不等式可能是弱算术平均-几何平均不等式：

$\displaystyle (abc)^{1/3} \lesssim a+b+c \ \ \ \ \ (1)$

其中 ${a,b,c}$ 是任意正实数，并且这里的 ${\lesssim}$ 表示我们愿意在估计中损失一个未指定的常数。

我过去一直希望（例如，[在这个 MathOverflow 回答中](https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/https:/mathoverflow.net/questions/463937/what-mathematical-problems-can-be-attacked-using-deepminds-recent-mathematical/463940#463940））有一个工具可以自动确定这样的估计是否为真（如果为真，则提供证明；如果为假，则提供渐近反例）。原则上，这种形式的简单不等式可以通过暴力案例拆分自动解决。例如，对于 (1)，首先观察到 ${a+b+c}$ 在常数范围内与 ${\max(a,b,c)}$ 相当，因此只需确定是否：

$\displaystyle (abc)^{1/3} \lesssim \max(a,b,c). \ \ \ \ \ (2)$

接下来，为了解决最大值，可以分为三种情况： ${a \gtrsim b,c}$ ； ${b \gtrsim a,c}$ ；和 ${c \gtrsim a,b}$ 。例如，假设 ${a \gtrsim b,c}$ 。那么要证明的估计简化为：

$\displaystyle (abc)^{1/3} \lesssim a,$

这（在取对数后）是假设 ${a \gtrsim b}$ ， ${a \gtrsim c}$ 的一个正线性组合。确定这种线性组合的任务是一个标准的线性规划任务，为此存在许多计算机软件包。

任何单个这样的不等式都不难手工解决，但在某些应用中，需要检查大量这样的不等式，或者拆分为大量情况。我将从我的一篇旧论文中随机选取一个例子（改编自公式 (51) 之后，并为了简单起见忽略了一些 epsilon 项）：我想建立估计：

$\displaystyle \frac{\langle N_2 \rangle^{1/2}}{\langle N_1 \rangle^{1/4} L_1^{1/2} L_2^{1/2} } L_{\min}^{1/2} N^{-1} (N_1 N_2 N_3)^{1/2} \lesssim 1 \ \ \ \ \ (3)$

对于任何满足以下约束的 ${N_1,N_2,N_3,L_1,L_2,L_3 > 0}$ ：

$\displaystyle N_{\max} \sim N_{\mathrm{med}} \sim N; \quad L_{\max} \sim L_{\mathrm{med}} \gtrsim N_1 N_2 N_3$

其中 ${N_{\max}}$ ， ${N_{\mathrm{med}}}$ 和 ${N_{\min}}$ 分别是 ${N_1, N_2, N_3}$ 的最大值、中位数和最小值， ${L_{\max}}$ ， ${L_{\mathrm{med}}}$ 和 ${L_{\min}}$ 也是如此，并且 ${\langle N \rangle := (1+N^2)^{1/2}}$ 。这个特定的界限可以通过一些更简单的不等式在三四行内解决；但想出这些不等式花了一些时间，而且我不得不做十几个这种类型的不等式。这是一个似乎非常适合自动化的任务，特别是使用现代技术。

最近，我比过去做了更多的编码（主要是用 Python），这得益于大型语言模型在为许多不同任务生成初始代码示例或自动完成部分编写的代码方面的卓越能力。在大多数情况下，我将自己限制在相当简单的编码任务中，例如计算然后绘制一些稍微复杂的数学函数，或者对某些数据集进行一些基本的数据分析。但我决定给自己一个更具挑战性的任务，即编写一个可以处理上述形式的不等式的验证器。经过大约四个小时的编码，并在 LLM 的频繁帮助下，我能够为此生成一个概念验证工具，该工具可以在此 GitHub 存储库中找到。例如，要验证 (1)，相关的 Python 代码是：

  a = Variable("a")
  b = Variable("b")
  c = Variable("c")
  assumptions = Assumptions()
  assumptions.can_bound((a * b * c) ** (1 / 3), max(a, b, c))

验证不等式的（有点冗长的）输出是：

Checking if we can bound (((a * b) * c) ** 0.3333333333333333) by max(a, b, c) from the given axioms.
We will split into the following cases:
[[b <~ a, c <~ a], [a <~ b, c <~ b], [a <~ c, b <~ c]]
Trying case: ([b <~ a, c <~ a],)
Simplify to proving (((a ** 0.6666666666666667) * (b ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1.
Bound was proven true by multiplying the following hypotheses :
b <~ a raised to power 0.33333333
c <~ a raised to power 0.33333333
Trying case: ([a <~ b, c <~ b],)
Simplify to proving (((b ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1.
Bound was proven true by multiplying the following hypotheses :
a <~ b raised to power 0.33333333
c <~ b raised to power 0.33333333
Trying case: ([a <~ c, b <~ c],)
Simplify to proving (((c ** 0.6666666666666667) * (a ** -0.3333333
333333333)) * (b ** -0.3333333333333333)) >= 1.
Bound was proven true by multiplying the following hypotheses :
a <~ c raised to power 0.33333333
b <~ c raised to power 0.33333333
Bound was proven true in all cases!

当然，这是一种极其笨拙的证明，但重点不是优雅；而是自动化。（另请参阅 Heather Macbeth 的这篇最新文章，了解在形式证明助手等自动化工具存在的情况下，证明写作风格如何变化。）

该代码几乎也可以处理更复杂的估计，例如 (3)；目前，我还没有编写代码来正确处理诸如 ${N_{\max} \sim N_{\mathrm{med}} \sim N}$ 这样涉及复杂表达式（如 ${N_{\max} = \max(N_1,N_2,N_3)}$ ）的假设，而不是只涉及原子变量（如 ${N_1}$ ， ${N_2, N_3}$ ）的假设，但我至少可以处理我要验证的估计的左右两边的此类复杂表达式。

无论如何，这段代码是 LLM 生成的代码和我自己基本的 Python 技能的混合物，很难说是高效或优雅编码的典范，我相信有许多专业的程序员可以做得更好。但我认为这是一个概念验证，可以更容易地创建一个更复杂的此类工具来执行更高级的任务。这样的一个例子任务是我在上面的 MathOverflow 问题中给出的，即能够自动验证诸如：

$\displaystyle \sum_{d=0}^\infty \frac{2d+1}{2h^2 (1 + \frac{d(d+1)}{h^2}) (1 + \frac{d(d+1)}{h^2m^2})^2} \lesssim 1 + \log(m^2)$

对于所有 ${h,m > 0}$ 。另一个任务是自动验证估计各种函数的多元线性表达式的能力，根据这些函数在标准空间（如 Sobolev 空间）中的范数；这是一项在 PDE 和调和分析中尤其普遍的任务（而且坦率地说，手工完成会有些乏味）。正如在该 MO 帖子中推测的那样，人们最终可能希望利用 AI 来协助验证过程，例如通过建议各种涉及的求和或积分的可能拆分，但这将是一个长期目标。

这种软件开发可能最好作为一个协作项目来执行，其中涉及数学家和专业程序员。我对如何最好地进行此类项目感兴趣（例如，将此类工具合并到现有平台（如 SageMATH）中是否有意义），以及对于数学家来说，通用估计验证器最需要哪些功能。我愿望清单上的一件事是能够给工具一个要估计的表达式（例如某些未知函数的多元线性积分），以及一组固定的工具来限制该积分（例如，将积分分成几部分、分部积分、使用 Hölder 和 Sobolev 不等式等），并让计算机尽最大努力优化它可以产生的界限（并为其输出提供一些独立可验证的证明证书）。人们还可以想象这些工具可以选择以形式证明助手语言（如 Lean）输出其证明证书。但也可能读者希望提出其他有用的功能。