🤖 AI

ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction

本文介绍了 ALPS，这是一个通过要求大型语言模型为随机生成的等式法则生成原创且可验证的数学证明或构造，从而严格衡量其有效创造力的创新基准，该研究揭示了当前模型在构造方面存在显著困难，且大多数实例即使是对于先进的自动化证明器而言仍然难以解决。

原作者： Eric Xie, Wenqian Ye, Aidong Zhang

发布于 2026-08-18

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Eric Xie, Wenqian Ye, Aidong Zhang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在现代科学领域，人工智能已开始从数据处理者的角色转向发现者的角色。我们正看到机器能够提出新的化学化合物、建议新型材料，甚至构思人类尚未考虑过的数学猜想。这种转变提出了一个深刻的问题：当机器产生一个看起来像是突破性的答案时，我们如何知道它是真正的创造性，还是仅仅对其训练期间记忆内容的巧妙重复？科学中的真正创造力需要两个条件：解法必须是原创的，即以前从未见过；并且必须是有效的，即它确实起作用并解决了当前的问题。难点在于验证这些品质。在许多领域，判断一个新想法是否有效需要人类专家观察结果并做出判断，这是一个缓慢且具有主观性的过程。在数学中，由于答案可以用绝对的确定性进行检查，挑战则有所不同：问题通常非常复杂，以至于计算机无法简单地通过搜索所有可能性来找到答案，而且问题本身往往是机器可能已经研究过的固定集合。

为了解决这一困境，弗吉尼亚大学的研究人员开发了一种测试人工智能的新方法，他们将这一基准测试称为 ALPS。该系统旨在通过向机器展示一种特定类型的数学谜题来衡量“有效的创造力”，这种谜题无法通过记忆或遵循标准程序来解决。这些谜题基于一组物体如何组合在一起的规则。想象一下，有一组物体以及一条关于如何将其中任意两个混合在一起的规则。研究人员生成了一条特定的规则或定律，描述了这些物体必须如何表现。机器的任务是决定其中之一：要么该规则过于严格，以至于迫使所有物体都变得完全相同；要么该规则允许存在一个满足条件的复杂且无限的物体结构。如果机器声称该结构存在，它必须构建出该结构的描述。如果它声称物体必须是相同的，它必须证明不存在其他可能性。这一设置的精妙之处在于，答案可以由计算机以完美的准确度进行检查，无需任何人类查看结果。此外，该系统可以生成无穷无尽的此类谜题，确保机器始终面临从未见过的新问题。

研究人员使用各种强大的自动推理工具（即专门用于解决逻辑问题的特化计算机程序）对该系统进行了测试。他们针对四千多个生成的定律库运行了这些工具。结果非常悬殊。即使在计算能力大幅增加的情况下，这些自动化工具也只能解决极小比例的问题。具体而言，由八种不同配置的最优证明器组成的组合，仅解决了约 2% 的定律。当研究人员将计算预算增加 20 倍时，他们只发现了极少数额外的解法，而且这些解法都不是他们正在寻找的复杂结构；它们仅仅是证明了物体必须是相同的。这表明，解决这些问题的障碍不在于缺乏计算能力，而在于缺乏一种方法来发明每个独特定律所要求的特定定制结构。机器根本不知道如何从零开始构建正确的无限结构。

研究人员随后转向了大语言模型，即驱动当今许多对话式工具的人工智能类型。他们测试了最强大的推理模型，给它们同样的谜题和同样的机会来证明其答案。在机器需要证明所有物体都相同的任务方面，表现最好的模型在约 14% 的案例中取得了成功，但仅限于较简单的问题。在机器需要构建一个全新的无限结构的任务方面，结果更加发人深省：没有任何模型取得成功。当模型尝试构建结构时，它们一致地以两种方式之一失败：要么它们提出的结构过于僵化，导致所有物体坍缩为一个点，从而未能展示出复杂的解法；要么它们提出的结构过于松散，未能遵循其试图满足的定律规则。在每一种情况下，机器都无法平衡遵循规则与创造新颖复杂事物之间的需求。

研究得出结论，尽管这些人工智能系统在遵循指令和检查自身工作方面正在变得更好，但它们仍然在科学发现的核心行为上挣扎：即发明一个符合一系列约束条件的全新结构。研究人员向公众发布了他们的整个系统，包括创建谜题的生成器和检查答案的自动评判器。这使得其他科学家可以在不耗尽新鲜问题的情况下，继续测试和改进这些模型。研究结果表明，人工智能在科学领域的未来路径可能不在于给机器更多的数据或更多的时间，而在于教它们如何在创造与验证的循环中提出并完善自己的想法。在机器能够可靠地构建这些定制化解决方案之前，它们在科学发现中的作用将受到限制，无法跨越从处理信息到生成真正有效的、原创知识之间的鸿沟。

技术摘要：ALPS —— 通过数学构建衡量大语言模型的有效创造力

1. 问题陈述

当前针对科学领域（如定理证明、分子设计）的大语言模型（LLM）评估，难以区分有效创造力与单纯的记忆或常规执行。只有当一个解决方案同时满足以下两个准则时，才被视为“有效创造”：

原创性（Originality）： 解决方案并非对训练数据或已知通用程序的重复。
有效性（Effectiveness）： 解决方案在客观上是正确的，并能为特定任务提供价值。

现有的基准测试无法可靠地衡量这种结合，因为它们至少缺失了以下三个必要属性中的一个：

可验证性（Verifiability）： 解决方案必须是可客观检查的（而非主观判断）。
可再生性（Renewability）： 必须能够无限生成新的问题实例，以防止训练数据污染。
构建性（Constructiveness）： 任务必须要求针对特定实例量身定制解决方案，从而防止通过记忆或标准算法求解。

静态语料库（如 MATH, miniF2F）缺乏可再生性；合成谜题（如随机 SAT）通常缺乏构建性（因为可以通过已知程序求解）；而开放式发现任务（如分子设计）通常由于主观人类判断而缺乏可验证性。

2. 方法论：ALPS 基准测试

作者引入了 ALPS（Austin-Law Proof-Synthesis，奥斯汀定律证明合成），这是一个旨在同时满足上述三个属性的基准测试，其领域设定在等式理论（equational theory）中。

问题形式化：

领域： ALPS 运行在 magmas（具有单个二元运算 $\diamond$ 的集合）和等式律（全称量化的恒等式）之上。
任务： 每个实例是一个形式为 $x = T[x, y, z, \dots]$ 的律 $L$ ，其中 $T$ 是一个五阶或更高阶的项。
二分性： 对于任何此类律，恰好存在以下两种情况之一：
1. 平凡性（Trivial）： 该律蕴含 $x = y$ ，导致每个模型都坍缩为单个元素。
2. 奥斯汀性（Austin）： 该律具有非平凡模型，且该模型必然是无限的（因为所有有限的非平凡模型都已被基准测试的认证过程排除）。
挑战： 求解器必须要么提供演绎证明证明 $L \models x=y$ （平凡侧），要么构造一个满足 $L$ 的无限 magma（奥斯汀侧）。

语料库构建：

生成： 语料库通过一个扩展引擎进行生长。从已知的奥斯汀律开始，递归地将项 $T$ 中的变量替换为新的运算（例如， $v \to v \diamond w$ ）。这确保了可以无限生成新鲜且未见过的题目。
筛选与容许性： 候选题目经过严格的筛选流程：
1. 有限模型过滤器： 剔除具有非平凡有限模型的律。
2. 容许性证明器： 使用自动化证明器来认证不存在非平凡有限模型。这依赖于有限性的一个逻辑推论：在有限载体上，单射映射必为满射。证明器尝试从该律和子项的满射性中导出矛盾，从而证明任何模型都必须是无限的。
3. 去重： 等价的律（相互蕴含）被归类到等价类中，以确保题目数量的独立性。
最终池： 从初始生成的候选题目中，作者产生了一个包含 4,141 个未解决律的池（“困难层级”）以及一个较小的“经认证易解”的集合。

答案验证（自动化裁判）：
裁判通过两个完全不同的全自动渠道验证提交结果，无需人工参与：

平凡侧： LLM 提交一条等式链。一个框架将其自动形式化为 Lean 证明（由 Lean 内核检查），以验证 $L \implies \forall a, b: a=b$ 。
构造侧： LLM 提交一组有限方程 $E$ $E$ （一个表示）。裁判使用自动化定理证明器（如 Vampire, E, Twee）验证两个主张：
- 推导性： $E \vdash L$ （ $E$ 的每个模型都满足 $L$ ）。
- 可满足性： $E \cup \{a \neq b\}$ 是可满足的（存在一个包含至少两个不同元素的 $E$ 模型）。
- 如果两者均成立，则该实例的容许性证书保证了该模型是无限的。

3. 核心贡献

双向构造任务： 一个每个实例都被认证具有确定答案（要么是平凡的，要么是无限的）的基准测试，从而隔离了对创造性构造的需求。
可再生语料库与生成器： 一个公开的生成器，可以无限制地产生新鲜实例，确保评估永远不会受到训练数据污染。
自动化裁判： 一个系统，通过独立的渠道（利用 Lean 进行平凡性验证，利用自动化证明器证书进行构造验证）来认证提交结果，无需人类裁判。
强自动化基线： 一个由八种领先证明器（Vampire, E, Twee）配置组成的组合，确立了当前自动化能力的“方法论极限”。

4. 实验结果

自动化证明器表现：

一个由八种配置组成的证明器组合仅解决了 4,141 个律评估池中 2.2% 的问题。
将计算预算增加 20 倍仅额外解决了 0.6% 的律（均为平凡性证明，未发现新模型）。
97.2% 的池仍未被任何测试配置解决，这表明障碍在于缺乏构造定制化无限结构的方法，而非计算量不足。
侧面发现： 作者解决了一个此前由等式理论项目（ETP）留下的五阶律，通过饱和法确认了无限模型的存在。

LLM 表现：

平凡侧： 在 63 个“经认证易解”的律上，测试的最强模型 (o3) 在使用路标（由证明器导出的引理）时实现了 14% 的通过率（9 个解法），不使用路标时为 9.5%。GPT-4.1 和 o4-mini 的通过率为 0%。
- 失败模式： LLM 主要因提交包含无效步骤（无法从该律中导出的步骤）的链条而失败，这些步骤被框架拒绝。
构造侧： 在 25 个“困难层级”样本（自动化无法解决）上，没有任何 LLM 产生了经过验证的解决方案。
- 失败模式： 提交的结果要么过强（蕴含了该律但坍缩为单个元素，导致无法通过差异性检查），要么过弱（允许不同元素但未能蕴含该律）。
- o3 在所有 25 个律中恰好通过了其中一项检查。o4-mini 和 GPT-4.1 在许多律上两项检查均失败。

5. 意义与主张

论文声称 ALPS 通过消除记忆和常规执行的干扰，成功隔离了有效创造力。

创造力的必要性： 自动化证明器和 LLM 在“困难层级”上的高失败率表明，这些问题无法通过现有的通用程序或暴力搜索来解决。
失败性质： 特定的失败特征（平凡证明中的无效步骤；构造侧“过强/过弱”的表示）凸显了当前模型在约束下的创造性生成方面存在困难。它们虽然可以起草一个结构，但难以在不坍缩为退化解的情况下平衡全局规范。
科学并行性： 论文将此与科学发现（如分子设计）中的“指定–构造–验证”循环进行了类比，指出 ALPS 使每一个阶段都具备了机器可检查性。
未来方向： 作者建议，未来的路径在于验证与精炼循环（类似于基于反例引导的归纳合成，CEGIS），即求解器起草结构，接收来自自动化的反馈，并据此修订结构。

作者保持了谦逊的态度，指出虽然最强的 LLM 在简单实例上展现了一定的能力，但目前在处理困难实例时仍无法构造有效的无限结构，且该基准测试在很大程度上仍处于未解决状态。