TB-MathModel：把数学建模做成可验证的智能体基准

终端式数学建模评测台：首个智能体化且可验证的数学建模基准

Xiaojun Wu 所属机构：香港科技大学（广州） Cehao Yang 所属机构：香港科技大学（广州） Xuhui Jiang 所属机构：IDEA Research 所属机构：DataArcTech Ltd. Chengjin Xu 所属机构：IDEA Research 所属机构：DataArcTech Ltd. Jia Li Jian Guo

摘要

数学建模把一个开放式的现实问题转化为假设、一个模型、一个解，以及一份经过辩护的建议，而其答案只有在既接近一份可信参照、又在物理上可行时才要紧；现有基准要么给求解器片段打分，要么用大语言模型评审给报告评分，使这些数字处于未核验状态。我们提出 TB-MathModel（Terminal-style Mathematical Modeling Bench），这是首个把完整的竞赛式建模问题同时变成智能体化、可验证且终端化的基准，覆盖 18 道真实的 CUMCM 与 MCM 题目（2023–2025）。每道任务在容器化终端中提供逐字题面、官方附件与图；智能体返回一份 JSON 产物，针对最终问题的数值核心、对照优秀奖论文的一份复现进行评分。两项设计选择使之与众不同：方向感知的单侧评分，它从不因超越锚点而扣分；以及两层可行性验证——覆盖六种可判定不变量形式的程序化门控，外加 624 条 Lean 4 义务——并带有把不可行答案置零的硬门控。每道任务对照一组人类优秀论文而非单篇来评分，因此一个模型必须接近许多被接受的答案；在七个多模态条目（每个三个种子）中，最强者达到多参照 O-Eval 64.58%，而 $2.54 的开源模型以 $1/100$ 的成本保持 59.81%。TB-MathModel 把建模的数值核心变成一种可复现、机器可核验的信号，用于衡量长程建模能力，并用于收集智能体轨迹。源代码见 https://github.com/wxj630/terminal-bench-math-modeling。

1 引言

数学建模竞赛，例如中国的 CUMCM 与国际上的 MCM/ICM，要求队伍在数日之内把一个刻意欠指定的现实问题转化为一个站得住脚的定量答案。交付物不是单个数字，而是一条链：假设 $\rightarrow$ 模型 $\rightarrow$ 解 $\rightarrow$ 灵敏度 $\rightarrow$ 建议。有两项性质使它成为智能体评测的一个有吸引力的目标：它是定量的，因为最终问题以可以核验的数字结束；它是多模态的，因为题面引用图，而附件是电子表格与 CSV。它也不同于求解一个适定问题，其差别在于困难的工作从何处开始——模型本身必须被建立，而且同一情境可以接纳时间序列、优化、动力学、图或多准则表述，其中任何一种都可以是站得住脚的，只要其假设是显式的、其计算是可信的 Giordano et al. (2014) ; Meerschaert (2013)。这正是使建模成为对长程智能体的一场苛刻考验之处：在上下文中持有题面与附件，选择一种表述，编写并运行代码，处理文件与单位，并报告一个自洽的答案。

现有基准覆盖相邻但不同的领域，没有一个闭合我们所关心的回路。代码、终端与助手基准评测仓库编辑、命令行能力与工具使用 Jimenez et al. (2024) ; Merrill et al. (2026) ; Mialon et al. (2024) ; Yao et al. (2025)；闭式数学基准评测的是演绎而非建模 Hendrycks et al. (2021) ; Cobbe et al. (2021) ; Glazer et al. (2024)；运筹学数据集把文字题解析成求解器就绪的表述 Ramamonjison et al. (2023) ; AhmadiTeshnizi et al. (2024) ; Yang et al. (2025)。关于建模本身最接近的先前工作落入两派，两者都不同时是智能体化、可验证、终端化且多模态的。一派停留在面向求解器且范围狭窄，只给单一形式化产物打分 Huang et al. (2025b)。另一派用大语言模型评审给最终报告评分 Qian et al. (2025) ; Liu et al. (2025)，奖赏流畅的行文，却并不确立所报告的数字是正确的、甚至是可接受的。表 1 把这一缺口具体化；TB-MathModel 是首个把这些性质全部结合起来的基准。

表 1：最接近的数学建模基准。只有 TB-MathModel 在一项多模态任务上结合了完整的竞赛题、一次智能体化的终端运行、一个可执行验证器、物理可行性检查，以及一份机器可核验的证明（“评审”：大语言模型给一份报告评分；“求解器”：求解器检查一件形式化产物）。

弥合这一缺口提出了三个塑造该设计的问题。不同队伍做出不同的假设，因此不存在单一真值：与其把一篇论文提升为真理，TB-MathModel 征询每一位人类专家，把每道任务对照一组优秀解来评分，从而使一个模型必须接近许多被接受的答案，而不是匹配其中一篇。锚定造成不对称的失败——一个比该论文做得更好的模型，其得分可以差于一个照抄该论文的模型——因此 TB-MathModel 把每个指标的方向写明，并作单侧评分。而且一个错误但看似合理的答案很容易产生（数字看起来合理，却违反该问题的物理），这是锚定比较所不能抓住的，因此 TB-MathModel 增加一个独立的可行性层。

我们提出 TB-MathModel（Terminal-style Mathematical Modeling Bench），据我们所知，这是首个把完整的竞赛式数学建模问题变成一种智能体化、可验证、终端化评测的基准。其贡献为：

1. 同类中的首个基准，以及其背后的 18 任务数据集。此前没有任何基准把完整的竞赛式建模问题变成带有可执行验证器的容器化终端任务。TB-MathModel 覆盖 CUMCM 与 MCM 2023–2025（每年的 A/B/C 题），含逐字题面、官方附件、从 PDF 裁出的 21 张图，以及每道任务一份 JSON 产物。
2. 带有可审计边界情形规则的方向感知单侧评分。逐指标的语义方向（higher/lower_is_better、target_value、exact_value）；两个所报告的指标（O-Eval、Robust BO-Eval）；针对退化带与未锚定参照单位的显式规则；以及把两项定义性性质锁定下来的契约测试。
3. 一种两层可行性验证设计。一个以六种可判定不变量形式覆盖 18/18 道任务的程序化门控，以及一个由 624 条经内核检查的义务构成的 Lean 4 证书层；这两层判定一个结构化产物所能定夺的每一个可行性问题，并确切说明独立重放从何处接管。
4. 对七个多模态模型/驾具条目的一项实证研究，每一项在三个种子上取平均，含逐任务行为、一项成本–稳健性分析，以及三个案例研究；我们也记录我们发现并加以修复的评分陷阱，并量化其中哪些移动了排行榜。

对照人类小组，两款最新的旗舰领先（GPT-6 Astra + codex 的 O-Eval 为 $64.58\pm 2.93$、Multi-BO 为 $1.132$，Fable 5.1 + claude-code 为 $63.11\pm 1.33$ 与 $1.081$，均为三个种子上的均值），而 $2.54 的 DeepSeek V4.1 Flash + opencode 以 $1/100$ 的成本保持 $59.81\pm 1.25$；仅改变驾具至多使 O-Eval 移动 0.07 个百分点，因此该榜衡量的是模型而非驾具。逐种子偏差达到 $2.9$ 个百分点，因此相邻各行并未被显著分开。一项案例研究颠倒了通常的故事：在 dragon-dance 上，模型是对的，而我们的锚点是错的——这是支持可独立核验的可行性的最尖锐论据。

图 1：为何建模难以评测，以及 TB-MathModel 改变了什么。(a) 在现状中，一个大语言模型评审按组织结构给一份报告评分，而数字从未被核验。(b) TB-MathModel 在一个终端容器中运行题目、附件与图，要求一份结构化产物，对照一份 O 奖复现对其作单侧评分，并用一个门控与 Lean 证书验证可行性——于是一个看似合理但不可行的答案会被抓住。

图

2 相关工作

#### 智能体与助手基准。

软件工程智能体与终端智能体由仓库级任务（SWE-bench Jimenez et al. (2024)）与端到端命令行任务（Terminal-Bench Merrill et al. (2026)）来衡量；助手由诸如 GAIA Mialon et al. (2024) 与 $\tau$-bench Yao et al. (2025) 这样的工具使用套件来衡量。机器学习智能体与数据科学智能体在 Kaggle 式流水线上被衡量 Chan et al. (2025) ; Starace et al. (2025) ; Guo et al. (2024) ; Zhang et al. (2024) ; Gu et al. (2024) ; Hu et al. (2024) ; Li et al. (2024)。这些捕捉了容器之中的工具使用与长程执行——即我们所依托的驾具——但评分的是一个排行榜名次或针对一份交付物的量规，从来不是一份建模产物，并且不附带可行性契约。

#### 数学与优化推理。

闭式数学基准衡量演绎，而非建模 Hendrycks et al. (2021) ; Cobbe et al. (2021) ; Glazer et al. (2024) ; Zheng et al. (2022)。运筹学系统把文字题解析成求解器就绪的表述，并评估给定表述的最优性或可行性 Ramamonjison et al. (2023) ; Xiao et al. (2024) ; AhmadiTeshnizi et al. (2024) ; Yang et al. (2025) ; Huang et al. (2025a) ; Mostajabdaveh et al. (2025) ; Lima et al. (2025) ; Xiao et al. (2025)。它们提供了一个强有力的执行有效性先例——一个求解器认证某个解对于所陈述的模型是可行的或最优的——但不能认证该模型抓住了正确的抽象，而且没有任何一个要求假设、灵敏度分析或一份经过辩护的建议。

#### 数学建模基准与智能体。

最接近的工作形成一个连续谱，其中没有任何一个同时是智能体化、可验证且终端化的。Mamo Huang et al. (2025b) 以求解器为根据：模型产出求解器可消费的产物，而求解器是一个可证伪的检查器，从而在形式片段上、而非在整道竞赛题上给出一个精确但狭窄的信号。ModelingAgent 及其 ModelingBench Qian et al. (2025) 处于报告层面：开放式问题由一个专家风格的大语言模型评审来评分——在生态上丰富，但依赖于评审校准，且不可复现。MM-Agent 与 MM-Bench Liu et al. (2025) 增加了一个分层建模库，然而其主要评测仍然是一份报告量规。TB-MathModel 保留完整的竞赛题面与智能体化工作流，把评测钉在由一个可执行验证器评分的结构化产物上，并增加了一个两派均未提供的可行性层。

#### 评测中的验证。

诸如 Lean 4 de Moura and Ullrich (2021) 配合 Mathlib The mathlib Community (2020) 这样的定理证明器，已经认证了竞赛数学与研究数学，而形式证明上的强化学习已经产出了强证明器 Hubert et al. (2025) ; Xin et al. (2024)。据我们所知，使用一个证明器不是为了寻找答案，而是为了审计一个基准自身的可行性决定，是新的：我们的 Lean 层重新证明程序化门控的不变量，于是一条断言变成一条机器可核验的事实 Sutton (2001)，其代价是整数与有理数算术，内核无需完整的库即可判定。

#### 多模态智能体与复现锚定评分。

使用工具的智能体日益将其状态外化以供复用 Yao et al. (2023) ; Wei et al. (2022) ; Schick et al. (2023) ; Zhou et al. (2026)。TB-MathModel 使视觉证据成为承重的——图从官方 PDF 中裁出——因此带有图像通道与不带图像通道的驾具可以在相同任务上被比较。把一个数值基准锚定在一个已发表的解上是标准做法；我们表明它造成三种少被报告的隐患（方向不对称、退化评分带、未锚定单位），并为每一种给出可审计的规则与测试。

3 TB-MathModel 基准

TB-MathModel（Terminal-style Mathematical Modeling Bench）把每道竞赛题变成一项自包含的终端任务。图 2 概括该构建流水线。一段构建脚本把官方竞赛材料组装成四个部分：(i) 一份带有逐字题面及其图的指令文件；(ii) 一个存放镜像附件与一个输出模式的智能体容器；(iii) 一个存放评分组与一项可执行可行性检查的独立验证器容器；(iv) 一个复现优秀奖（O 奖）论文的预言机。智能体携带这些材料被投入该终端，并且必须返回单一结构化产物。产物下游的一切——评分与可行性——都是机器可执行的。

图 2：TB-MathModel 的构建与评测流水线。构建：官方题面、附件与 PDF 图被编译进一个任务目录。运行：智能体在一个网络隔离的终端容器内工作，并写出一份 JSON 产物。评测：该产物由一个方向感知的单侧评分组对照一份 O 奖复现来评分，并由一个程序化可行性门控加上一个 Lean 4 证书层独立检查；门控失败则把该任务置零。

图

#### 任务选取与来源。

TB-MathModel 包含 18 道任务：2023–2025 年每一年 CUMCM 与 MCM 的 A、B、C 题。我们有意限定在最近三年：更早的题目早于有能力的 LLM，并且是针对软件辅助评分员校准的，因此它们的任务组合与评审标准不同于 LLM 之后的体制，而近年的版本更难、也更有区分度。两项竞赛彼此互补——CUMCM 偏工程/优化且为中文，MCM 偏建模风格且为英文——而取每年的全部三道题，便覆盖了标准的“A = 物理/工程，B = 数据/优化，C = 数据科学”划分，且不做择优挑选。题面与附件被逐字镜像；题面中的图从官方 PDF 裁切而来（图稿加上它的图注），以内联方式并在稳定的容器路径上交付。跨 6 道任务的 21 幅互不相同的图是承重的：题面引用它们，以给出正文中并未重述的几何（例如舞龙掉头曲线，它确定最终的龙头速度），因此一个没有图像通道的运行框架无法把它恢复出来——多模态评测由此而来。TB-MathModel 是一个纯评测集，没有训练划分，也没有难度分层（附录 A）。

#### 产物契约与 oracle 锚点。

被评分的对象是每道任务一个 JSON 文件，其模式（仅字段名与类型）被交给智能体；额外的 CSV/XLSX/PNG 产物不计分。正是受模式约束的 JSON 使自动评分成为可能，其代价是把一次自由形式的努力映射到具名的数值字段上——这一张力我们在第 4.3 节重新讨论。每道任务锚定于一篇 O 奖论文，并被重新实现为一个读取附件并输出同一 JSON 的脚本；该复现即归一化端点（O-Eval $=100\%$），并设定逐指标面板，覆盖为 18/18。来源是一等字段——论文 id、PDF/OCR 来源，以及复现范围——因此任一锚点都可以被重新推导出来（附录 D）；正是这一点让我们在一个不可行的舞龙锚点进入榜单之前发现并修正了它。

3.1 评分：方向感知、单侧、可审计

一个朴素的到锚点距离指标会无声地奖励照抄并惩罚改进，因此 TB-MathModel 通过一块带有显式语义方向的逐指标面板来为每道任务评分。每道任务附带一块由 2–6 个计分指标组成的面板（共计 60 个），每个指标都有一条进入产物的路径、一个锚点值 $O$、一个方向，以及一个权重。一个指标是 higher_is_better、lower_is_better、target_value（最接近 $O$ 者胜出）或 exact_value，其设定依据该量的建模语义，而不是其数值的正负号。方向性指标使用非对称的、单侧的奖励：达到或超过锚点时，得分从不低于 $1.0$，因此对论文的改进从不受到惩罚（完整公式见附录 G）。

有三种失败模式反复出现，其频繁程度足以配得上具名规则。（i）退化带：一条窄于数值量级 2% 的带无法作出区分，因此我们把它放宽到 5%——这改动了一个单元格（stair-wear，$72.67\!\to\!73.52$）。（ii）不可比的单位：当锚点是一个没有被模式钉住单位的任意原始指数（宿主鱼指数为 1080）时，模型把同一量归一化到 $[0,1]$ 后加以报告并不算错，因此此类指标由一条仅配置的规则，对每一个模型以及 oracle 予以剔除。（iii）基数不匹配：多余的条目被排除，而不是被计为缺失。域外的值（一个落在 $[-1,1]$ 之外的相关、一个负的计数）得零分，并记录原因。

设 $R$、$F$、$O$ 分别为一份提交、DeepSeek V4 Flash 基线以及 oracle 的加权面板原始分。我们报告在各任务上取平均的 O-Eval $=\mathrm{clamp}(R/O,0,1)$（头条绝对得分），以及当 oracle 与基线的差距超过 $0.10$ 时、经缺口补偿的 Robust BO-Eval $=\mathrm{clip}((R-F)/(O-F),\pm 1)$，否则为截断后的原始增益 $R-F$；产物缺失时 $\textsc{Robust BO-Eval}=-1$（完整公式见附录 G）。有两条性质由契约测试锁定：oracle 自洽（每一次复现的得分都恰好为 $1.0$）以及单侧性（达到或高于锚点从不算作失败）。一道未通过的可行性门把该任务的 O-Eval 置为 $0$，并把 Robust BO-Eval 置为 $-1$。

3.2 多参考评测

建模并不存在单一的正确答案，因此一个相对一篇论文做归一化的基准，会无声地把一支队伍的选择变成真值。TB-MathModel 改为去询问每一位人类专家。对每道任务，我们抽取该题所有可获得的 Outstanding 奖论文所报告的末问数值，得到 99 篇面板论文，其中 94 篇给出被计分的量。覆盖为 18/18 道任务，并且所有可获得的 outstanding 论文都被使用——每道任务 1 到 18 篇（中位数为 4），因为 O 奖报告的数量因题目而异。每篇论文是一票。

设 $M(t)$ 为任务 $t$ 的计分指标，$P(t)$ 为其论文面板，$S_{p}\subseteq M(t)$ 为论文 $p$ 实际报告的字段。记 $R(m,S)$ 为提交 $m$ 限制在 $S$ 上的加权面板得分（权重在 $S$ 上重新归一化），则任务得分是面板均值

$$ \textsc{O-Eval}(m,t)\;=\;\frac{1}{\lvert P_{\neq}(t)\rvert}\sum_{p\in P_{\neq}(t)}R(m,S_{p}), $$

（1）

其中 $P_{\neq}(t)=\{p\in P(t):S_{p}\neq\emptyset\}$。于是每篇论文恰好贡献“模型在这个人所报告的字段上，离这一人类答案有多近”。因为 $R(p,S_{p})=1$，每篇论文都与它自己相一致，并且该复现把该面板复现了出来。等权重使一份人类解答保持为一票，而一篇只报告单一字段的论文充当一次单字段检查，而不是被丢弃——这是对一份不完整报告的诚实处理。

一篇论文从不会被无声地丢弃。当它无法提供被计分的量时，它带有一个机器可读的 exclusion_reason，其中出现五种形式：number_only_in_figure、figure_only、figure_only_logistic_prior、no_numeric_estimate 以及 different_unit_of_analysis；它们构成位于面板之外的 99 篇中的那 5 篇。数值从不向既有锚点作插值或调整，而一篇论文不同但等价的单位会被显式换算并加以注明。当一块面板为空时——当一份 MCM 答案仅为散文或仅为图时便可能如此——该任务回退到那一个被复现的锚点，而一份缺失的产物得分为 $0$，因此分母始终是固定的 18 道任务。

一块面板还使人类之间的分歧变得可见，而不是把它藏在一个锚点背后。在 mcm-2024-c-tennis-momentum 上，11 篇 outstanding 论文中有 10 篇断定动量得到支持，而复现锚点——它本身就是一份 O 奖报告——断定并非如此；在该任务上，模型若与多数一致地作答则得 $0.909$，若与锚点相符则得 $0.091$，因此该分数反映的是模型选择了哪一种有效的统计检验，而不是建模质量。我们显式标记此类文献分裂的任务，并把它们排除出任何头条排名，同时仍把它们保留在面板之中：它们是最清楚的证据，表明一个单锚点分数本来会是任意的。

相对单锚点榜单而言，这把 Robust BO-Eval 变成了一个针对 DeepSeek V4.1 Flash 基线、锚定在 $1.0$ 的多参考增益指数：

$$ \textsc{Multi-BO}\;=\;1+\mathrm{clip}\!\left(\frac{O_{t}-f_{t}}{1-f_{t}},\,-1,\,+1\right), $$

（2）

其中 $f_{t}$ 是 Flash 在任务 $t$ 上的得分，$O_{t}$ 是模型的得分，并在各任务上取平均；当剩余余量 $1-f_{t}$ 低于 $0.10$ 时，我们回退到 $1+\mathrm{clip}(O_{t}-f_{t},\pm 0.10)$，而一份缺失的产物得分为 $-1$。因此，取值 $1.0$ 意味着“与 Flash 持平”，$1.08$ 意味着“弥合了到达人类面板的剩余差距的 8%”；它是一个比值，不是一个百分比，并且不可与 O-Eval 相比较。

3.3 可行性验证：两层

接近一个锚点并不意味着一个答案在物理上是可容许的：一份提交可以在一个字段上匹配参考值，同时在另一个字段上违反一条已经写明的约束。TB-MathModel 独立于评分来验证可行性，分为信任基础各不相同的两层。

#### 第 1 层：覆盖六种可判定形式的程序化门。

每一道任务登记一项可行性检查，并且该登记表覆盖 18/18 道任务；每一条硬错误分支都落入六种可判定形式之一（附录表 12）。检查要么是结构性的/定义域界限（比率、相关、概率、非负计数、求和为 100 的分布、峰值 $\geq$ 平均值），要么是约束重放（定日镜额定功率 $\geq 60$ MW 且安装高度 $\in[2,6]$ m，舞龙头速 $\times$ 放大比 $\leq 2$ m/s，一条受需求封顶的收入上限，一段并集时长 $\leq$ 其各部分之和）。三条契约使这道门保持诚实：覆盖（一道任务不能在未设门的情况下交付）、oracle 自洽（O 奖参考必须通过它自己的检查），以及区分（合成的违规与真实字段上的违规都必须被拒绝，而一份空产物给出警告，而不是硬失败）。四条需要独立重放而非字段检查的约束被记作整题惩罚（附录 G）。

#### 第 2 层：Lean 证书。

为使这道门自身的正确性可以被检查，第 2 层把同样的不变量重新证明为 Lean 4 定理，于是审计依托于内核。它在全部 18 道任务上生成 624 条义务，由 decide 或 omega 加以消去。不使用 Mathlib——这些命题在精确整数上是可判定的——并且数值被缩放到整数，因此不存在浮点容差；唯一的例外是一个复合指数，它在谓词中被声明，因为该容差本身就是被审计假设的一部分。一次信任审计（#print axioms）只报告 [propext, Quot.sound] 或无，没有 sorryAx，也没有 native_decide（经 grep 核对）。一套区分测试每次只变异一个数值叶子，并要求构建失败且点名该字段；遍及全部六种形式的十次变异均被拒绝。两条软警告变成了证明：一个旅游接受度指数因单位约定而被否证，一个可持续性得分在所声明的预算之内对两种约定都不符合。

#### 验证范围。

这两层判定一个结构化产物在没有物理模型的情况下所能定论的每一个可行性问题（附录表 13）：单位/取值范围（A）以及内部一致性（B）。所报告的数值是否反映真实的物理真相（C）——这片镜场真的产出 $60$ MW 吗？——是世界的性质，而不是产物的性质，因此 TB-MathModel 在题目容许一次独立重放的地方验证它。在此范围之内，这两层是精确的：任何其证据缺席的义务都被报告为一个已被见证的缺口，而不是被无声地满足，因此审计从不过度陈述它所已经证明的东西。

4 实验

4.1 设置

我们评测七个多模态的模型/运行框架条目，其运行框架能够打开那些裁出的图。每个条目在每道任务上以三个种子运行，并被报告为带标准差的均值；若某个模型曾在两个推理档位上运行，我们保留得分较高的那个变体。每一行都用同一个评分器与当前锚点来评分，因此这块榜单共享同一个评分定义（附录 C）。

提示词就是该任务的指令文件，被原样传入：竞赛题面、内联引用的图，以及一个写明输出路径的固定“Required Benchmark Artifact”块（附录 E）。任务在 Docker 容器中运行——python:3.12-slim，带有一套固定的科学计算软件栈，互联网被禁用，模型流量经过一个本地重试代理——因此智能体不能在运行时去获取解答或安装软件包；限制为 2 个 CPU、8 GB、无 GPU，以及 4 小时超时（附录 B）。每个多模态条目在每道任务上运行三次，并被报告为带标准差的均值；那一道适定的任务，舞龙，被额外探测了四次，其间各次答案一致到机器精度（std=$4.6\times 10^{-16}$）。

4.2 主要结果：多模态榜单

表 2 是主要结果：七个多模态条目在全部 18 道任务上的结果，每一项都是三种子均值（$\pm$ std）；逐条目的配置见附录表 7。O-Eval 是首要指标：即第 3.2 节的多参考得分，也就是在人类论文面板上，对模型离每一个被接受的答案有多近取均值。Multi-BO 是次要的相对指数，即这同一个得分相对于 DeepSeek V4.1 Flash 基线的指数，逐单元格固定在 $1.000$：$1.08$ 意味着该模型弥合了 Flash 到达该面板所余差距的 $8\%$，因此它是对照基线来读的，并且不是一个百分比。有五项发现十分突出。

1. 最新的旗舰居于领先。GPT-6 Astra + codex（$64.58\pm 2.93$）与 Fable 5.1 + claude-code（$63.11\pm 1.33$）位居榜首，大约分别高出 GPT-5.5 xhigh + codex（$59.75\pm 1.55$）4.8 分与 3.4 分，并且二者分别以剩余差距的 $13.2\%$ 与 $8.1\%$ 超越 Flash 基线。
2. 成本买到的是真实但有界的差距。两位领先者每次运行花费 246–273 美元，而最便宜的强条目 DeepSeek-Flash + opencode 以 2.54 美元达到 $59.81\pm 1.25$——大约落后领先者 4.8 分，成本大致为前者的 $1/100$。
3. 廉价的开放模型聚集在旗舰之下。在低成本条目之中，DeepSeek-Flash（59.81）、Kimi K3（58.23）、GLM-5.3（57.78）与 Qwen3.8 Flash（52.66）的跨度约为 7 分，并且只有两位旗舰超过基线指数（$1.132$ 与 $1.081$）；DeepSeek-Flash 把它定义在 $1.000$，其余每一个条目都落在其下。
4. 很小的差距尚不是已经裁定的排名。逐种子的偏差达到 $2.93$ 个百分点，因此两位领先者之间、以及 GPT-5.5 与 Flash 之间约 $\sim 1.5$ 个百分点的间隔，落在一个标准差之内；我们报告这一次序，但不声称相邻行之间存在显著差别。
5. 更多的推理计算并不单调。把 DeepSeek-Flash 运行在其最高推理档位，会使其多参考得分降到 $48.11\%$，并将其 Multi-BO 降到 $0.864$，远低于默认档位的 $59.81$ 与 $1.000$，而且成本更高：更大的审慎推理预算并不会在这些任务上简单地买到准确度。

表 2：主要结果：七个多模态条目，18 道任务，按 O-Eval 排序。“产物”：具有可评分产物的任务；成本：每完成一次 18 道任务的美元数。O-Eval 是多参考面板得分（%），Multi-BO 是同一得分相对于 DeepSeek V4.1 Flash 基线的值（ 1.000 1.000 = 与 Flash 持平），二者均为三种子均值（ ± \pm std）。

图 3：左：多参考 O-Eval 对成本（对数刻度）——帕累托前沿是被压缩的，接近前沿的得分出现在低两个数量级的成本上。中：每个条目的 O-Eval。右：按套题划分的 O-Eval，显示出 CUMCM–MCM 差距。

图

#### 硬门控与成本。

门控恰好移除那些答案违反既定约束的单元格，并使排名在其余方面保持稳定，因此它是手术式的，而非一刀切的惩罚。成本由每词元价格主导，而非用量：GPT-5.5 的 99.37 美元主要是缓存读取的输入与输出，费率大约为 DeepSeek V4.1 Flash 的 $33\times$/$50\times$，尽管词元数量相当。

#### 驾驭框架敏感性。

每个模型都由一个智能体驾驭框架驱动，因此一个自然的问题是，分数反映的是模型还是驾驭框架。表 3 固定模型并变换驾驭框架，使用 DeepSeek-Flash 与四种驾驭框架。分数基本不变：O-Eval 在全部四种上仅移动 $0.07$ 个百分点（$59.81$–$59.88$），远在逐种子偏差之内，相对指数也在同样狭窄的区间内移动。模型自身的驾驭框架对它的契合略好一些——DeepSeek 的原生驾驭框架给出最高的 O-Eval（$59.88$）与 Multi-BO（$1.092$）——但差异很小。因此，排行榜衡量的是模型，远多于它所包裹于其中的驾驭框架。

表 3：驾驭框架敏感性，固定模型（DeepSeek-Flash，18 项任务，三个种子）。按定义，Multi-BO 对于 opencode 参考驾驭框架为 1.000 1.000。

4.3 分析

四个代表性条目的逐任务 O-Eval 见附录表 6。有三种模式十分突出。（a）CUMCM–MCM 差距很大，且依赖于模型。对较弱的条目，CUMCM 单元格接近 100%，而 MCM 单元格位于 0% 与 60% 之间：工程问题具有定义明确的最终数值，大多数模型都能达到，而 MCM 问题更为开放，其锚点也更可争议。最强的条目仅略微缩小这一差距（GPT-6 在 CUMCM 上为 82.9，对比 MCM 上的 46.2；GPT-5.5 为 79.7，对比 39.8）。相当大一部分任务现在已被近乎完美地求解——这是当前基准所预期的——排行榜的区分力来自开放式的 MCM 问题。（b）两项任务是非全即无的。在 mcm-2024-b-submersible 上，每个条目都得到 100%，而在 mcm-2024-c-tennis 上，即便旗舰模型的得分也低于 40%。这类任务要么完全落在专家组容差之内，要么完全落在其外，因此它们区分的是模型的不同体制，而不是同一体制之内的模型。（c）许多低分反映的是参考的尺度/范围，而非建模误差。若干任务含有模型/专家组比值超过 $5\times$ 的指标：某些论文报告的宿主鱼指数接近 1080，而模型给出的是归一化的 $[0,1]$ 量；可持续性得分接近 1.007，而模型报告的是 0–100 的效用；一个 $6\times 6$ 网格，而模型把同一区域离散成数百个单元；以及一个 $72.67\!\to\!73.52$ 区间，其中论文自身的基线得分为零。

#### 我们发现并修复的评分陷阱。

基于锚点的基准，其可信度仅与其锚点相当，因此我们审计了每一条评分规则和每一个锚点，并报告审计改变了什么（附录 G）。两处门控假阳性被移除，且没有移动任何分数；退化区间的拓宽影响了一个单元格（$+0.35$ 个百分点）。排除两项单位不可比的指标，使每个条目提高 0.05–2.62 个百分点——这是系统性评分效应而非模型差异的标志。影响最为重大的是，审计将舞龙锚点标记为物理上不可行，而我们予以纠正（第 4.2 节）。

#### 可行性层捕捉到了什么。

门控将 7 个单元格硬性判为无效，集中于定日镜（额定功率低于 60 MW，或一面镜子低于 2 m 的最小值），外加烟幕、Juneau 与 Olympic 各一个单元格。Lean 层把两条软警告转化为证明，并通过在拒绝所报告制品的那个谓词之下接受一份经纠正的制品，来证明非空洞性。在那一项数值上适定的任务上，各次运行一致到机器精度；就整体而言，逐种子偏差相对于条目之间的散布仍然很小（表 2），因此排名不依赖于种子。

4.4 从发现到模型开发

TB-MathModel 旨在改进模型，而不仅仅是对它们排名。上述发现引出三条杠杆，每一条都可以用 TB-MathModel 已经产生的信号来训练。

面向强化学习的可验证奖励。可行的、经预言机归一化的分数是一项可执行、可复现的奖励——每一份提交都通过门控与 Lean 层。拒绝采样（保留门控所接受的轨迹，并按 O-Eval 排序）如今即可使用；以门控作为硬乘数的组相对策略优化，教会模型在追逐参考之前先满足物理约束。舞龙案例为此提供了动机：十二个模型算出了正确的峰值，却受到惩罚，因此它们所缺少的是自检——而这正是奖励中的验证器所提供的。

针对所观察到的失败的目标。发现（a）——开放式的 MCM 套件区分质量，而 CUMCM 已经饱和——说明应当训练假设、建模表述与敏感性，而不是闭式求解；发现（c）——许多失分是单位与尺度不匹配——说明应当在给出一个数之前陈述并核验单位、范围与模式。二者都由制品契约直接给予奖励。

制品能够检查的可行性。舞龙审计暴露了取值范围检查无法发现的失败：一个自洽的答案在物理上不可接受，因为制品省略了证据（没有逐镜布局，没有峰值邻域样本）。训练模型输出该见证，既提高分数，又使它们可被检查，从而达到 C 级。

#### 案例研究。

三种角色——一个顶级专有智能体、预言机，以及低成本开放智能体——在附录 F 的三个问题上进行比较。在舞龙上，三者都收敛，而论文的数值是不可行的离群点，因此模型是对的，我们的锚点是错的。在作物种植上，论文的约束联合起来不可行，因此我们锚定于一个可复现的精确 MILP 最优解。在 Juneau 上，可持续性得分以不同的单位尺度被报告，这就是为什么必须由任务模式、而不是评分器，来钉住一个字段的范围。

5 结论

我们提出了 TB-MathModel，这是首个针对 18 道真实数学建模问题的、智能体化且可验证的终端基准。它的区别在于方向感知的单侧评分——这种评分从不惩罚对锚点的超越——以及两层可行性验证，后者把覆盖六种可判定不变量形式的门控，与 624 条经内核检查的 Lean 义务结合起来。

对照由人类优秀论文组成的专家组为每项任务评分，最新的旗舰在七个多模态条目中领先（GPT-6 Astra 的 O-Eval 为 $64.58\%$，Fable 5.1 为 $63.11\%$），而 2.54 美元的开放模型 DeepSeek-Flash 以 $1/100$ 的成本保持 $59.81\%$。我们记录了所修复的评分陷阱，并展示了一个基准本身是错的、而模型是对的案例。

两层设计是可迁移的思想：快速门控覆盖每一项任务，证明助手使审计自身的正确性可被机器检查，同时陈明二者都不能回答什么。因为 TB-MathModel 给出可复现的奖励，它的轨迹也是训练材料，而第 4.4 节把这些发现转化为方向。

致谢

我们感谢 OpenRefinery（https://openrefinery.ai/）提供大语言模型 API 访问与评测支持，使我们得以开展 GPT-6-Astra 与 Claude-Fable-5.1 的实验。我们特别感谢 OpenRefinery 的 Kai Du 与 Ding Fan 所提供的协助。他们的基础设施与支持，对开展本文所报告的模型评测至关重要。此处表达的任何意见、发现与结论均为作者的观点，并不必然反映 OpenRefinery 的观点。

局限性

TB-MathModel 针对一份可复现的优秀奖解答对每项任务进行归一化，并附有逐锚点来源，从而使任何参考都能被重新推导；由于建模并不承认单一正确答案，自然的扩展是一个多论文专家组，报告各个被接受解答上的散布。两层验证裁定结构化制品所能解决的每一个可行性问题（单位/取值范围与内部一致性）；外部物理真理是世界的属性，因此仅在某个问题允许独立重放之处才加以检查，而任何缺少证据的义务都会被报告，而不是被静默放过。专家组规模随每个问题的优秀报告篇数而变化（1 至 18 篇论文），而在人类自身也意见不一之处——如网球动量检验，11 篇论文中有 10 篇得出与锚点相反的结论——我们把该任务标记为文献分裂，并将其排除在头条排名之外。分数是三个种子的均值，并且该任务外壳可沿用于工程问题与跨学科问题。

伦理考量

陈述、附件与图是用于研究评测的 CUMCM 与 MCM 官方材料；我们不重新分发优秀奖解答，复现代码衍生自带有逐任务来源的公开语料库。用户应当为自己的再分发确认许可条款。TB-MathModel 衡量并改进大语言模型智能体的建模工作流，而不是把被呈现为某一团队自己成果的工作加以自动化，完全自动化的评测则使广泛参与的成本保持较低。

大语言模型的使用

大语言模型充当被测系统——表 2 中的每一个条目都是一个大语言模型智能体，亦即测量的对象——并充当写作助手，帮助起草正文，并检查 LaTeX 与数字的内部一致性。基准构建、评分规则、可行性检查与 Lean 义务，均由作者加以规定、实现并验证，全部数值结果都由已发布的脚本产生。

参考文献

• A. AhmadiTeshnizi、W. Gao 与 M. Udell

OptiMUS：借助 (MI)LP 求解器与大语言模型进行可扩展的优化建模。

载于 Proceedings of the 41st International Conference on Machine Learning (ICML)，

Proceedings of Machine Learning Research，第 235 卷，第 577–596 页。

外部链接：2402.10172

被引于：§1， §2。

• J. S. Chan、N. Chowdhury、O. Jaffe、J. Aung、D. Sherburn、E. Mays、G. Starace、K. Liu、L. Maksin、T. Patwardhan、L. Weng 与 A. Mądry

MLE-bench：在机器学习工程上评测机器学习智能体。

说明：The Thirteenth International Conference on Learning Representations (ICLR)，口头报告

外部链接：2410.07095， 链接（https://arxiv.org/abs/2410.07095）

被引于：§2。

• K. Cobbe、V. Kosaraju、M. Bavarian、M. Chen、H. Jun、L. Kaiser、M. Plappert、J. Tworek、J. Hilton、R. Nakano 等

训练验证器以求解数学文字题。

arXiv 预印本 arXiv:2110.14168。

被引于：§1， §2。

• L. de Moura 与 S. Ullrich

Lean 4 定理证明器与编程语言。

载于 Automated Deduction – CADE 28，

Lecture Notes in Computer Science，第 625–635 页。

外部链接：文档（https://dx.doi.org/10.1007/978-3-030-79876-5%5F37）

被引于：§2。

• F. R. Giordano、W. P. Fox 与 S. B. Horton

数学建模入门课程。

第 5 版，Brooks/Cole。

被引于：§1。

• E. Glazer、E. Erdil、T. Besiroglu、D. Chicharro、E. Chen、A. Gunning、C. Falkman Olsson、J. Denain、A. Ho、E. de Oliveira Santos 等

FrontierMath：评测人工智能中高级数学推理的基准。

外部链接：2411.04872， 链接（https://arxiv.org/abs/2411.04872）

被引于：§1， §2。

• K. Gu、R. Shang、R. Jiang、K. Kuang、R. Lin、D. Lyu、Y. Mao、Y. Pan、T. Wu、J. Yu 等

BLADE：为数据驱动科学对语言模型智能体进行基准评测。

arXiv 预印本 arXiv:2408.09667。

被引于：§2。

• S. Guo、C. Deng、Y. Wen、H. Chen、Y. Chang 与 J. Wang

DS-Agent：通过以基于案例的推理增强大语言模型，实现自动化数据科学。

载于 Proceedings of the 41st International Conference on Machine Learning (ICML)，

被引于：§2。

• D. Hendrycks、C. Burns、S. Kadavath、A. Arora、S. Basart、E. Tang、D. Song 与 J. Steinhardt

用 MATH 数据集衡量数学问题求解。

载于 Advances in Neural Information Processing Systems (NeurIPS)，

外部链接：2103.03874

被引于：§1， §2。

• X. Hu、Z. Zhao、S. Wei、Z. Chai、Q. Ma、G. Wang、X. Wang、J. Su、J. Xu、M. Zhu 等

InfiAgent-DABench：在数据分析任务上评测智能体。

arXiv 预印本 arXiv:2401.05507。

被引于：§2。

• C. Huang、Z. Tang、S. Hu、R. Jiang、X. Zheng、D. Ge、B. Wang 与 Z. Wang

ORLM：一种为自动化优化建模而训练大模型的可定制框架。

Operations Research 73（6），第 2986–3009 页。

外部链接：文档（https://dx.doi.org/10.1287/opre.2024.1233）

被引于：§2。

• X. Huang、Q. Shen、Y. Hu、A. Gao 与 B. Wang

面向数学建模的大语言模型：迈向弥合自然语言与数学语言之间的差距。

载于 Findings of the Association for Computational Linguistics: NAACL 2025，

第 2678–2710 页。

外部链接：文档（https://dx.doi.org/10.18653/v1/2025.findings-naacl.146）， 链接（https://aclanthology.org/2025.findings-naacl.146/）

被引于：表 1， §1， §2。

• T. Hubert、R. Mehta、L. Sartran、M. Z. Horváth、G. Žǔžić、E. Wieser、A. Huang、J. Schrittwieser 等

借助强化学习的奥林匹克水准形式化数学推理。

Nature 651，第 607–613 页。

外部链接：文档（https://dx.doi.org/10.1038/s41586-025-09833-y）

被引于：§2。

• C. E. Jimenez、J. Yang、A. Wettig、S. Yao、K. Pei、O. Press 与 K. Narasimhan

SWE-bench：语言模型能否解决真实世界的 GitHub 问题？

载于 The Twelfth International Conference on Learning Representations (ICLR)，

外部链接：链接（https://openreview.net/forum?id=VTF8yNQM66）

被引于：§1， §2。

• Z. Li、Q. Zang、D. Ma、J. Guo、T. Zheng、X. Niu、X. Yue、Y. Wang、J. Yang、J. Liu 等

AutoKaggle：面向自主数据科学竞赛的多智能体框架。

arXiv 预印本 arXiv:2410.20424。

被引于：§2。

• V. Lima、D. T. Phan、J. Kalagnanam、D. Patel 与 N. Zhou

经由可验证的合成数据生成，走向可信的优化建模智能体。

外部链接：2508.03117， 链接（https://arxiv.org/abs/2508.03117）

被引于：§2。

• F. Liu、Z. Yang、C. Liu、T. Song、X. Gao 与 H. Liu

MM-Agent：把大语言模型作为智能体，用于真实世界的数学建模问题。

外部链接：2505.14148， 链接（https://arxiv.org/abs/2505.14148）

被引于：表 1， §1， §2。

• M. Meerschaert

数学建模。

Academic Press。

被引于：§1。

• M. A. Merrill、A. G. Shaw、N. Carlini、B. Li、H. Raj、I. Bercovich、L. Schmidt 等

Terminal-Bench：在命令行界面中困难且真实的任务上对智能体进行基准评测。

说明：项目页面：https://www.tbench.ai/

外部链接：2601.11868， 链接（https://arxiv.org/abs/2601.11868）

被引于：§1， §2。

• G. Mialon、C. Fourrier、C. Swift、T. Wolf、Y. LeCun 与 T. Scialom

GAIA：面向通用人工智能助手的基准。

载于 The Twelfth International Conference on Learning Representations (ICLR)，

外部链接：2311.12983， 链接（https://openreview.net/forum?id=fibxvahvs3）

被引于：§1， §2。

• M. Mostajabdaveh、T. T. L. Yu、S. C. B. Dash、R. Ramamonjison、J. S. Byusa、G. Carenini、Z. Zhou 与 Y. Zhang

用 ORQA 评测运筹学领域中的大语言模型推理。

载于 Proceedings of the AAAI Conference on Artificial Intelligence，

第 39 卷，第 24902–24910 页。

被引于：§2。

• C. Qian、H. Du、H. Wang、X. Chen、Y. Zhang、A. Sil、C. Zhai、K. McKeown 与 H. Ji

ModelingAgent：架起大语言模型与数学建模之间的桥梁，以应对真实世界挑战。

外部链接：2505.15068， 链接（https://arxiv.org/abs/2505.15068）

被引于：表 1， §1， §2。

• R. Ramamonjison、T. T. Yu、R. Li、H. Li、G. Carenini、B. Ghaddar、S. He、M. Mostajabdaveh、A. Banitalebi-Dehkordi、Z. Zhou 与 Y. Zhang

NL4Opt 竞赛：根据其自然语言描述来表述优化问题。

载于 Proceedings of the NeurIPS 2022 Competitions Track，

Proceedings of Machine Learning Research，第 220 卷，第 189–203 页。

外部链接：2303.08233

被引于：§1， §2。

• T. Schick、J. Dwivedi-Yu、R. Dessì、R. Raileanu、M. Lomeli、E. Hambro、L. Zettlemoyer、N. Cancedda 与 T. Scialom

Toolformer：语言模型能够教会自己使用工具。

Advances in Neural Information Processing Systems 36，第 68539–68551 页。

被引于：§2。

• G. Starace、O. Jaffe、D. Sherburn、J. Aung、J. S. Chan、L. Maksin、R. Dias、E. Mays、B. Kinsella、W. Thompson、J. Heidecke、A. Glaese 与 T. Patwardhan

PaperBench：评测人工智能复现人工智能研究的能力。

说明：PMLR 267:56843–56873

外部链接：2504.01848， 链接（https://arxiv.org/abs/2504.01848）

被引于：§2。

• R. S. Sutton

验证，人工智能的关键。

说明：http://www.incompleteideas.net/IncIdeas/KeytoAI.htmlEssay，2001 年 11 月 15 日

被引于：§2。

• The mathlib Community

Lean 数学库。

载于 Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)，

第 367–381 页。

外部链接：文档（https://dx.doi.org/10.1145/3372885.3373824）， 链接（https://doi.org/10.1145/3372885.3373824）

被引于：§2。

• J. Wei、X. Wang、D. Schuurmans、M. Bosma、B. Ichter、F. Xia、E. H. Chi、Q. V. Le 与 D. Zhou

思维链提示激发大语言模型中的推理。

载于 Advances in Neural Information Processing Systems (NeurIPS)，

被引于：§2。

• Z. Xiao、J. Xie、L. Xu、S. Guan、J. Zhu、X. Han、X. Fu、W. Yu、H. Wu、W. Shi 等

优化建模遇见大语言模型综述：进展与未来方向。

外部链接：2508.10047， 链接（https://arxiv.org/abs/2508.10047）

被引于：§2。

• Z. Xiao、D. Zhang、Y. Wu、L. Xu、Y. J. Wang、X. Han、X. Fu、T. Zhong、J. Zeng、M. Song 与 G. Chen

专家链：当大语言模型遇见复杂的运筹学问题。

载于 The Twelfth International Conference on Learning Representations (ICLR)，

外部链接：链接（https://openreview.net/forum?id=HobyL1B9CZ）

被引于：§2。

• H. Xin、Z. Z. Ren、J. Song、Z. Shao、W. Zhao、H. Wang、B. Liu、L. Zhang、X. Lu、Q. Du 等

DeepSeek-Prover-V1.5：利用证明助手反馈进行强化学习与蒙特卡洛树搜索。

说明：The Thirteenth International Conference on Learning Representations (ICLR)，海报

外部链接：2408.08152， 链接（https://arxiv.org/abs/2408.08152）

被引于：§2。

• Z. Yang、Y. Wang、Y. Huang、Z. Guo、W. Shi、X. Han、L. Feng、L. Song、X. Liang 与 J. Tang

OptiBench 遇见 ReSocratic：衡量并改进用于优化建模的大语言模型。

载于 The Thirteenth International Conference on Learning Representations (ICLR)，

外部链接：2407.09887， 链接（https://arxiv.org/abs/2407.09887）

被引于：§1， §2。

• S. Yao、N. Shinn、P. Razavi 与 K. Narasimhan

$\tau$-bench：真实世界领域中工具–智能体–用户交互的基准。

载于 The Thirteenth International Conference on Learning Representations (ICLR)，

外部链接：2406.12045， 链接（https://arxiv.org/abs/2406.12045）

被引于：§1， §2。

• S. Yao、J. Zhao、D. Yu、N. Du、I. Shafran、K. R. Narasimhan 与 Y. Cao

ReAct：使语言模型中的推理与行动协同起来。

载于 The Eleventh International Conference on Learning Representations (ICLR)，

被引于：§2。

• Y. Zhang、Q. Jiang、X. Han、N. Chen、Y. Yang 与 K. Ren

对数据科学智能体进行基准评测。

arXiv 预印本 arXiv:2402.17168。

被引于：§2。

• K. Zheng、J. M. Han 与 S. Polu

miniF2F：面向形式化奥林匹克水准数学的跨系统基准。

载于 International Conference on Learning Representations (ICLR)，

外部链接：2109.00110， 链接（https://arxiv.org/abs/2109.00110）

被引于：§2。

• C. Zhou、H. Chai、W. Chen、Z. Guo、R. Shan、Y. Song、T. Xu、Y. Yang、A. Yu、W. Zhang 等

大语言模型智能体中的外化：记忆、技能、协议与驾驭工程的统一综述。

arXiv 预印本 arXiv:2604.08224。

被引于：§2。