评估SageMath增强的LLM智能体在计算与实验数学中的应用

# 评估基于 SageMath 增强的 LLM 智能体在计算与实验数学中的表现  
来源：https://arxiv.org/html/2607.06820  

###### 摘要  

近年来，人工智能在数学领域的研究主要集中于自动形式化与定理证明，而计算机代数系统（CAS）在基于智能体的大语言模型工作流中的作用尚未得到充分探索。我们提出了一种 ReAct 风格的智能体框架，将 LLM 推理与来自 SageMath 的可验证反馈相结合，同时借助 Context7 获取最新文档。我们在模拟计算数学研究循环的设置中，利用 RealMath 基准测试中的研究级数学问题，评估了该智能体框架在前沿模型上的表现。我们还对 RealMath 基准测试进行了改进，引入了一个多步骤后处理流程和一个多阶段验证流水线，从而提升了所提取问题集的质量和可靠性。实验结果表明，所有受评估模型在接入 SageMath 后均取得了显著的性能提升，平均提升幅度达 9.7 个百分点，范围从 1.5 到 27.8 个百分点不等，并且缩小了开源模型与闭源模型之间的差距。Qwen 3.7-Max 从 SageMath 中获益最多，而 GPT-5.5 在启用工具的配置中实现了最高的解题率（75.2%）和最低的 token 消耗。我们的发现表明，CAS 增强的智能体是帮助数学家进行计算探索的有前途的方向，并相信这项工作朝着自动猜想发现迈出了一步。项目仓库已在线公开。111https://github.com/Snopoff/Evaluating-SageMath-Augmented-LLM-Agents-for-Computational-and-Experimental-Mathematics  

## 1 引言  

近年来，LLM 以及将 LLM 推理与确定性、可验证的工具后端（如编译器、定理证明器、SAT/SMT 求解器、类型检查器和物理模拟器）相结合的智能体系统取得了进展，这建立了一种新的神经符号范式，其中生成式推理部分基于可验证的反馈。通过将 LLM 推理与提供真实信号（ground-truth signals）的组件耦合，该范式催生了一类工具，能够自动完成以前需要大量专家经验的任务，并以纯生成方法无法达到的可靠性水平生成答案。该范式一个特别活跃的应用领域是数学。在自动形式化方面取得了重大进展，即将数学陈述转换为用证明助手语言（如 Lean、Coq 和 Isabelle）编写的形式化程序（Wu et al., 2022 (https://arxiv.org/html/2607.06820#bib.bib1)）；在自动定理证明方面也取得了显著进展，基于 LLM 的系统引导形式化证明的搜索（Lin et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib2)），在 2025 年国际数学奥林匹克竞赛中以形式化验证的解决方案达到金牌水平（Achim et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib3)），并且最近自主解决了 Erdős 收藏中的几个开放问题（Sothanaphan, 2026 (https://arxiv.org/html/2607.06820#bib.bib4); Tsoukalas et al., 2026 (https://arxiv.org/html/2607.06820#bib.bib56)），包括著名的单位距离猜想（OpenAI, 2026b (https://arxiv.org/html/2607.06820#bib.bib57)）。这些进展确立了 LLM 与形式化证明助手的集成是数学推理的一个有前途的方向，重点在于证明和形式化已经指定的陈述。  

在数学的许多领域中，计算机代数系统（CAS）和符号引擎被常规地用于假设探索、候选验证和反例搜索。现代数学研究中的常见工作流程，特别是在计算性较强的领域如组合交换代数、代数组合学、图论、有限群论及相关领域，严重依赖 CAS。突出的例子包括 SageMath (The Sage Developers, 2022 (https://arxiv.org/html/2607.06820#bib.bib5))、Macaulay2 (Grayson and Stillman, (https://arxiv.org/html/2607.06820#bib.bib6))、GAP (17 (https://arxiv.org/html/2607.06820#bib.bib7))、Magma (Bosma et al., 1997 (https://arxiv.org/html/2607.06820#bib.bib8))、PARI/GP (The PARI Group, 2023 (https://arxiv.org/html/2607.06820#bib.bib10)) 和 Singular (Decker et al., 2024 (https://arxiv.org/html/2607.06820#bib.bib9))，它们为研究级数学问题的求解提供计算支持。研究人员使用这类系统来发现和修剪猜想空间，通过迭代计算示例、识别模式、制定初步猜想并对其进行计算测试。222 正如 V. I. Arnold 的名言："数学是物理学中实验成本较低的部分。" 这种工作流程在计算性和实验驱动的数学领域非常常见。  

尽管 CAS 被广泛使用，但将其集成到基于 LLM 的数学推理系统中所受到的关注远不如形式化证明助手的集成。特别是，现有工作主要集中在形式化证明的构建上，而基于符号实验和可执行验证的计算工作流程相对未被充分探索。这一差距，加上 LLM 在数学推理方面的最新成功，促使了本研究。我们工作的核心问题是：可验证的符号反馈能在多大程度上提高前沿 LLM 在研究级数学中的表现，并且在智能体设置中是否会改变它们的行为？为了研究这种效应，我们在一个能够访问 SageMath 的智能体设置中评估了前沿 LLM，该设置紧密模拟了数学家的计算工作流程。所提出的设置特别适用于符号计算起核心作用且核心数学结构已在现有软件系统中以算法形式化的任务。我们的贡献有三点：  

- **工具使用智能体评估**：我们提出了一项实证研究，在 ReAct 风格的智能体设置中，通过多轮访问 SageMath 以及通过 Context7 检索最新文档，评估前沿 LLM。我们通过受控的工具访问消融实验，评估来自 CAS 的可验证反馈如何影响模型在研究级数学问题上的表现。  
- **基准改进与评估协议**：基于 RealMath 基准，我们精选了一个评估集，仅限于数值和符号表达式答案。此外，我们使用压缩的上下文信息丰富问题陈述，并引入了一个 LLM 辅助的归一化流水线，用于可执行的符号验证。我们还采用了一种混合验证协议，结合符号等价性检查与 LLM-as-a-Judge 重新评估。  
- **错误与行为分析**：我们补充了定量评估，分析了执行失败、恢复动态和工具调用轨迹，突出了智能体与符号计算工具交互时的模型特定模式。我们还提供了一个案例研究，描述了智能体用于解决其中一个问题所采用的策略。  

## 2 相关工作  

### 2.1 自动形式化与定理证明  

本小节将我们的工作置于最近 AI4Math 更广泛的进展中，重点关注自动形式化和自动定理证明。主导方向是将 LLM 与形式化证明助手相结合。许多工作评估了 LLM 在竞赛数学和形式化证明生成方面的表现。MathArena (Balunović and others, 2025 (https://arxiv.org/html/2607.06820#bib.bib20)) 在数学竞赛结束后立即评估 LLM，以避免污染，并引入了一个证明写作基准，顶级模型在 2025 年美国数学奥林匹克（USAMO）上得分低于 25%。PutnamBench (Tsoukalas et al., 2024 (https://arxiv.org/html/2607.06820#bib.bib23)) 提出了 1,692 个任务的形式化，覆盖 Lean 4、Isabelle、Coq。Herald (Gao et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib11)) 通过反向翻译 Mathlib 构建了一个大型自然语言到 Lean 4 的语料库，并训练了一个自动形式化器，在 miniF2F-test 上达到 96.7% 的准确率。AlphaProof (Google DeepMind AlphaProof and AlphaGeometry teams, 2025 (https://arxiv.org/html/2607.06820#bib.bib12)) 将 Lean 与 AlphaZero 风格的强化学习相结合，并与几何专用系统 AlphaGeometry 2 (Chervonyi et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib13)) 一起在 2024 年 IMO 上达到了银牌水平。DeepSeek-Prover 系列 (Xin and others, 2024 (https://arxiv.org/html/2607.06820#bib.bib14); Ren and others, 2025 (https://arxiv.org/html/2607.06820#bib.bib15)) 通过子目标分解追求开源证明器，V2 在 MiniF2F-test 上达到 88.9%。Kimina-Prover (Wang et al., 2025a (https://arxiv.org/html/2607.06820#bib.bib16)) 和 Seed-Prover (Chen et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib17)) 提出了基于结构化推理和引理式证明（结合迭代 Lean 反馈）的替代方案。  

最近的工作已超越了标准证明搜索训练。DeepSeekMath-V2 (Shao et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib18)) 训练了一个生成器-验证器对，奖励推理步骤，在 2024 年普特南竞赛（Putnam）上得分 118/120。围绕 Lean 编译器编排 LLM 的智能体系统也已出现：AxiomProver (Axiom Math Team, 2025 (https://arxiv.org/html/2607.06820#bib.bib19)) 为所有 2025 年普特南任务生成了完全验证的 Lean 证明。我们建议读者参考 Wang et al. (2025b (https://arxiv.org/html/2607.06820#bib.bib36)) 获取关于 LLM 在数学推理中（特别是工具使用方面）的广泛综述。  

### 2.2 AI4Math 基准测试  

#### 研究级基准测试。  
一个主要的基准测试方向针对来自研究级任务和文献而非竞赛的数学问题。FrontierMath (Glazer and others, 2024 (https://arxiv.org/html/2607.06820#bib.bib25)) 通过由顶尖数学家（包括陶哲轩）创作的数百个未发表问题，提高了难度上限，覆盖许多研究相关领域。到 2026 年年中，最好的推理 LLM 在第 1-3 级上达到超过 50%，在第 4 级上达到 25-40% (Epoch AI, 2026 (https://arxiv.org/html/2607.06820#bib.bib27))。EternalMath (Ma and others, 2026 (https://arxiv.org/html/2607.06820#bib.bib21)) 追求一个完全自动化的、基于定理的流水线，将最新论文转化为可执行、可验证的任务，目标是产生一个可持续更新的基准测试。一个特别相关的工作是 RealMath (Zhang et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib26))，它提出了一种自动数据收集流水线，从 arXiv 和 Math Stack Exchange 中提取研究级问题，并将其呈现为（上下文、问题、答案）三元组，侧重于构造性定理。我们的工作在此基础上进行，我们使用他们流水线提取的数据集的可计算子集，并提出了对基准测试的改进。  

#### 涉及符号计算的基准测试。  
与我们的工作最接近的基准测试涉及符号或 CAS 增强的评估。IMProofBench (Schmitt et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib28)) 在多轮智能体设置中结合工具（Python、SageMath、Bash、网络搜索）评估 LLM，针对 39 个研究级证明生成问题，最好的模型 GPT-5 为 22% 的问题生成了完全正确的证明。与我们的设置不同，IMProofBench 没有通过受控的无工具消融实验来隔离工具访问的效应，且其问题集保持私有。ASyMOB (Shalyet et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib29)) 包含 17,092 个符号任务，涵盖积分、化简、极限和微分方程，通过测量在符号扰动下的性能下降，暴露出高达 70% 的下降，他们使用 SymPy 进行答案验证。IntegralBench (Tang et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib30)) 将范围缩小到 317 个研究生级别的定积分问题，并带有符号和数值真值，说明了紧凑、领域受限的基准测试如何能够隔离特定的失败模式。  

### 2.3 用于数学发现与推理的工具增强智能体  

另一条互补的工作线将智能体与外部符号和计算工具相结合，用于数学推理中的猜想空间发现与修剪。FunSearch (Romera-Paredes et al., 2024 (https://arxiv.org/html/2607.06820#bib.bib31)) 及其后继者 AlphaEvolve (Novikov et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib33)) 通过演化由确定性基于 Python 评估器评分的 Python 程序来遍历假设空间：FunSearch 产生了 caps 集问题的新下界，而 AlphaEvolve 将循环推广到整个代码库演化，并报告了新的 SOTA 构造，包括一个改进的 4×4 复数矩阵乘法方案。该方向的早期工作包括 (Chuharski et al., 2024 (https://arxiv.org/html/2607.06820#bib.bib32))，他们从 LLM 中采样关于群论中“溶化子”（solubilizer）的猜想，并通过 GAP 生成的反例来修剪猜想空间。ToRA (Gou et al., 2024 (https://arxiv.org/html/2607.06820#bib.bib34)) 训练开源模型将推理与 SymPy 工具交替使用，在竞赛级基准测试上显著提高了性能。MathSensei (Das et al., 2024 (https://arxiv.org/html/2607.06820#bib.bib35)) 在规划器驱动的流水线中结合了知识检索器、Python 程序生成器与执行器以及 Wolfram-Alpha，并在 MATH 基准测试上对这些工具进行消融，以隔离它们的互补效应。我们将这种模式推广到一个通用的、基于 CAS 的工具，并在数学问题求解上对其进行评估。  

## 3 实验设置  

我们评估每个模型在两种匹配条件下的表现：无工具基线，其中模型仅通过直接推理来解决每个问题；以及工具增强的智能体设置，其中模型可以迭代地查询 SageMath 和 Context7。除了工具访问和相应的系统提示外，基础模型和问题集保持不变。这种设计隔离了可验证符号反馈在研究级数学中对性能的影响。我们在来自 RealMath 基准测试的精选 133 个问题集上进行评估，并使用一个多阶段协议验证模型输出，该协议结合了符号等价性检查与 LLM-as-a-Judge 阶段。两个流水线的系统提示见附录 F.1 (https://arxiv.org/html/2607.06820#A6.SS1) 和 F.2 (https://arxiv.org/html/2607.06820#A6.SS2)。  

### 3.1 评估数据集  

我们通过执行额外的处理步骤、多阶段过滤和从 RealMath 基准测试 (Zhang et al., 2025 (https://arxiv.org/html/2607.06820#bib.bib26)) 中采样，提取了一个包含 133 个问题的精选子集。RealMath 是一个直接来自当代文献的研究级数学问题数据集。这些额外步骤至关重要，因为我们专注于可执行的数学推理，因此需要问题具有可通过算法验证的解。然而，RealMath 是作为问答基准开发的，其中“答案”字段表示为纯 LaTeX 文本，这阻止了直接自动比较。此外，它在收集时未评估问题的计算视角，因此可能包含不适合在 SageMath 框架内进行符号计算的问题。因此，我们通过以下多阶段流水线构建最终的评估套件（关于数据集构建、过滤标准和注释提示的完整细节见附录 A.2 (https://arxiv.org/html/2607.06820#A1.SS2)）：  

1. 1. 我们只保留 t