终端式数学建模基准：首个智能体化、可验证的数学建模评测 Terminal-style Mathematical Modeling Bench: The First Agentic and Verifiable Benchmark for Mathematical Modeling
把18道竞赛建模真题装进断网终端容器，用单侧计分与双层可行性验证机器可查地评测智能体
前置知识
数学建模竞赛（CUMCM/MCM）
全国大学生数学建模竞赛（CUMCM）与美国大学生数学建模竞赛（MCM/ICM）要求参赛队在几天内把一个开放的真实问题转化为可辩护的定量答案，交付物不是单个数字而是一条链：假设→模型→求解→灵敏度分析→建议。同一个题面可以有时间序列、优化、动力学、图论等多种合理建模方式，只要假设显式、计算可信。两赛事题型互补：CUMCM 偏工程/优化且为中文，MCM 偏建模且为英文，A 题通常是物理/工程，B 题优化/数据，C 题数据科学。
本文的 18 个评测任务就是 2023–2025 年两赛事每年的 A/B/C 真题，理解建模的开放性与多解性是理解其面板计分设计的出发点。
智能体终端评测（Agentic Terminal Evaluation）
把任务装进 Docker 容器，让 LLM 智能体通过 shell、文件读写、代码执行等工具自主完成工作，留下动作-观察轨迹，代表作有 SWE-bench 与 Terminal-Bench。本文沿用该范式，但计分对象从仓库补丁或命令行输出换成一个 schema 约束的结构化 JSON 建模产物，且容器断网、模型流量走本地代理，杜绝在线查答案和运行时装包。
实验中的 harness（codex / claude-code / opencode 等命令行智能体）直接来自这一生态，是理解实验设置与 harness 敏感性分析的基础。
方向感知的单侧计分（One-sided Directional Scoring）
朴素的'离锚点距离'指标隐含惩罚超过锚点的答案：建模题中模型可能做得比参考论文更好却得低分，照抄论文反而占优。单侧计分为每个指标显式声明语义方向（higher_is_better / lower_is_better / target_value / exact_value），并规定方向性指标'达到或超过锚点永远不低于 1.0'，即超越论文绝不扣分；退化计分带、不可比单位、基数不匹配三种高频失效模式另有具名规则。
这是两大计分指标 O-EVAL 与 MULTI-BO 的核心性质，由契约测试锁定；不懂单侧性就无法正确解读排行榜的每一格。
Lean 4 定理证明与内核检验
Lean 4 是交互式定理证明器，每条证明由一个小而可信的内核复核；decide、omega 等战术可在精确整数算术上自动判定命题，因此无需 Mathlib 也能形式化'概率必须在 [0,1] 内''计数必须非负'这类断言。#print axioms 审计能确认证明只依赖标准公理（propext、Quot.sound）而没有 sorryAx（作弊逃逸）或 native_decide（浮点近似）。
可行性验证第二层用 Lean 4 重新证明第一层程序化门控的同一不变式（624 条义务），使'这个答案物理上不可行'成为机器可查的事实而非人工断言。
多参考面板计分（Multi-reference Panel Scoring）
建模题没有唯一正确答案，用单一锚点归一化会把一个队伍的主观选择变成'真值'。面板计分把该题所有可获得的杰出奖（O奖）论文各算一票：对每篇论文，只在它实际报告的字段子集上按权重重归一化计算接近度，再对论文取平均；不完整的报告携带机器可读的排除理由而不是被丢弃。人类专家之间的分歧因此显式可见，而不是被单一锚点掩盖。
O-EVAL 的定义就是对面板取均值；tennis 动量题上 10/11 篇论文与锚点结论相反的例子，正是面板设计必要性的最直接证据。
研究动机
数学建模的自动评测长期停在两个都不闭环的极端。一端是求解器导向的窄评测：如 Mamo（1209 题）只让模型输出求解器可消费的产物，由求解器检验单个形式化片段，信号精确但覆盖不了'假设→模型→求解→灵敏度→建议'的完整竞赛链；ORLM、OptiMUS 等优化建模工作同样只评'给定公式是否可行/最优'。另一端是报告级评测：ModelingBench（68 题）与 MM-Bench（111 题）用专家风格的 LLM 裁判给最终报告打分，奖励流畅的散文却不核实报告里的数字是否正确、甚至是否物理可容许——论文举的例子是，一个看似合理但 $h=1.2$ m 的答案直接违反题面给定的 $h\in[2,6]$ m 约束，裁判毫无察觉。此外，把单篇论文当真值还有方向不对称问题：模型做得比参考论文更好，反而可能比照抄论文的模型得分更低；而'看起来合理但违反物理'的数字又恰恰是锚点比较抓不住的。封闭式数学基准（MATH、GSM8K、FrontierMath）考的是演绎而非建模，Kaggle 类基准（MLE-bench 等）考的是流水线执行也非建模。'完整竞赛题、智能体化、可验证、多模态'四种性质在此前的基准中从未同时成立。
本文的目标是本文要构造第一个同时对完整竞赛式建模问题做到'智能体化、可验证、终端化、多模态'的基准 TB-MathModel，并让它成为可复现、机器可查的长期信号。具体目标：(1) 覆盖 CUMCM 与 MCM 2023–2025 每年 A/B/C 共 18 道真题，逐字保留题面、官方附件（xlsx/csv/pdf）以及从 PDF 裁出的 21 张承重插图，装进容器化终端任务；(2) 智能体只交一个 schema 约束的 JSON 产物，评分完全机器执行——把每题所有可得杰出奖论文组成面板（共 99 篇、94 篇可计分、60 个计分指标），以多参考 O-EVAL 为头条绝对分，以相对 DeepSeek-Flash 基线的 MULTI-BO 为次级指数；(3) 独立于计分做双层可行性验证：覆盖 18/18 任务的六不变式程序化门控，加 624 条 Lean 4 内核检验义务，不可行答案硬性清零；(4) 用 3 种子 × 7 个多模态模型/harness 组合给出带方差的主榜，并实证检验'分数衡量的是模型而非 harness'。
与已有工作不同的是，最接近的先例构成一条连续谱，但没有一个同时具备上述四种性质：Mamo 是求解器导向的窄信号；ModelingAgent/ModelingBench 与 MM-Agent/MM-Bench 是报告级 LLM 裁判，前者依赖裁判校准且不可复现，后者加了分层建模库但主评仍是报告 rubric。本文的独特切入有三点。其一，不把任何一篇论文奉为真值，而是'询问每一位人类专家'：用 O 奖论文面板计分，让人类分歧显式可见（tennis 动量题 10/11 篇与锚点结论相反），并把这类文献分裂任务标记后移出头条排名。其二，直面锚定计分的三个被低估的陷阱——方向不对称、退化计分带、未钉住的单位——逐一给出可审计的规则与契约测试，并公开自己在构建中发现、修正的全部计分陷阱。其三，据作者所知首次'用证明助手不去找答案，而是审计基准自身的可行性判定'：Lean 层重新证明程序化门控的同一不变式，使审计的正确性本身机器可查。正是这条设计让后来 dragon-dance 案例中'基准自己错了、模型是对的'得以被发现并纠正。
核心方法
直觉：把一场数模竞赛的完整体验——读题、看图、处理附件、建模、写代码、算数、自检——原封不动交给断网容器里的 LLM 智能体，只要求它最后交出一份机器可读的 JSON，然后用可执行的评分器与可行性检查器代替人类评委。技术路线分三步。构建：build 脚本把逐字题面（含内嵌插图）、镜像附件与输出 schema 装进任务目录，agent 容器与分离的 verifier 容器各就各位，oracle 是复现某篇 O 奖论文的可运行脚本（覆盖 18/18），溯源字段记录论文 id、PDF/OCR 来源与复现范围。运行：智能体在 python:3.12-slim 容器（2 CPU、8 GB、无 GPU、4 小时超时、断网、模型流量走本地重试代理）里自主行动，必须把结构化产物写到指定路径。评估：verifier 容器按面板计分，独立运行六不变式程序化门控与 624 条 Lean 4 义务，不可行则把该任务 O-EVAL 清零、ROBUST BO-EVAL 记 $-1$。产物之外的一切下游——打分与可行性——都是机器可执行的，这就是'可验证'的确切含义。
本质创新是'把数值核心从不可复核的散文中剥离，同时守住建模的开放性'，落在三个互相咬合的设计上。第一，方向感知的单侧计分：每个指标显式声明语义方向，方向性指标采用非对称奖励——达到或超过锚点永远 $\ge 1.0$——从而'超越论文绝不惩罚'，这与朴素的 distance-to-anchor 有本质区别；退化带（带宽小于量值 2% 时放宽到 5%）、不可比单位（对包括 oracle 在内的所有人一并剔除该指标）、基数不匹配（多余项剔除而非记缺失）三种失效模式均有具名规则。第二，多参考面板：$\text{O-EVAL}(m,t)$ 是对论文面板的加权分均值，每篇论文只在它实际报告的字段上投票，既不神化单一队伍的选择，也不丢弃不完整报告。第三，双层可行性验证独立于计分：第一层程序化门控用六种可判定不变式覆盖 18/18 任务并硬清零违规答案；第二层用 Lean 4 重新证明同一不变式（624 条义务、无 Mathlib、内核判定整数算术），并诚实声明覆盖边界——单位/取值范围（A）与内部一致性（B）两层可判，外部物理真相（C）只在允许独立重放的题目上检验。dragon-dance 案例证明第三层并非冗余：正是恒等式'头速 × 比率 = 2 m/s'让错误锚点现形。
方法步骤详情
第一步，任务构建：选定 CUMCM/MCM 2023–2025 每年 A/B/C 共 18 题（刻意只用近三年，老题先于强 LLM、校准不同），逐字镜像题面与附件，从官方 PDF 裁出 21 张插图（横跨 6 题）随题面内嵌交付；输出 schema 只含字段名与类型；每题配一个 oracle 脚本读附件产出与某篇 O 奖论文一致的 JSON，作为归一化端点（O-EVAL = 100%）。第二步，智能体运行：harness 把题面原样作为提示传入，附加'必需产物'块指定输出路径与 14400 秒时限；容器断网、限 2 CPU / 8 GB；智能体读题、看图、跑 Python、写文件，最终交一个 JSON（多余 CSV/XLSX/PNG 不计分）。第三步，面板计分：抽取各 O 奖论文最终问的数值，得 99 篇面板（94 篇可计分），每题 2–6 个计分指标、共 60 个；每指标带锚点值、方向与权重，按 $$\text{O-EVAL}(m,t)=\frac{1}{|P(t)|}\sum_{p\in P(t)} R(m,S_p)$$ 对论文取均值（$S_p$ 为论文 $p$ 报告的字段集，权重在其上重归一化）；头条指标为多参考 O-EVAL，次级指标 $\text{MULTI-BO}=1+\mathrm{clip}\big((O_t-f_t)/(1-f_t),-1,+1\big)$ 相对 DeepSeek-Flash 基线；缺失产物记 O-EVAL 0、MULTI-BO $-1$。第四步，可行性验证：每题注册一个门控检查，硬错误分支归入六种不变式（定义域/值域、整数/二值、序、精确恒等、有限域、划分求和），违规整题清零；Lean 4 层对每个可检验字段生成义务（共 624 条），由 decide/omega 判定，信任审计仅见 propext/Quot.sound 公理，变异套件十项突变全被拒绝。
技术新颖性
与已有技术的具体区别：(1) 相对 Mamo 等求解器基准，本文保留完整竞赛题面与建模自由度，只在'最终问的数值核心'上收口，而非评单个形式化片段；(2) 相对 ModelingBench/MM-Bench 的 LLM 裁判，每个分数可复现、可上诉——契约测试锁定 oracle 自洽（每个复现恰得 1.0）与单侧性两条不变量，全部评分公式公开；(3) 面板计分虽借人类同行评审的多解思想，但'只在每篇论文实际报告的字段上重归一化投票 + 机器可读排除理由（五种：仅图、仅数值、仅图先验、无数值估计、分析单位不同）'是新设计；(4) 用证明助手审计基准自身据称是首次——Lean 层与程序化门控证明同一不变式，二者职责边界用三级可行性表（A 取值范围 / B 内部一致性 / C 物理真相）显式声明，缺证据的义务记为 witnessed gap 而非静默通过；(5) 全程无浮点容差：数值缩放为整数后由内核精确判定，唯一例外（复合指数）的容差本身作为被审计假设写进谓词。这些设计把'评分器的正确性'也变成了可检验对象，而不仅是'模型答案的正确性'。
实验结果
主榜（Table 2，7 个多模态组合 × 18 题 × 3 种子）：GPT-6 Astra + codex 以 O-EVAL 64.58±2.93%、MULTI-BO 1.132、$246.41 居首，Fable 5.1 + claude-code 以 63.11±1.33%、1.081、$272.80 次之；$2.54 的开源 DeepSeek V4.1 Flash + opencode 拿到 59.81±1.25%（定义 MULTI-BO = 1.000），以 1/100 成本只落后 4.77 分。五个发现：(1) 旗舰领先但每种子标准差达 2.93 pp，相邻名次（如两位旗舰间 1.5 pp）不显著；(2) 成本买到真实但有界的差距；(3) 开源梯队 Kimi K3 58.23、GLM-5.3 57.78、Qwen3.8 Flash 52.66 全部低于基线；(4) 更多推理算力非单调——DeepSeek-Flash 开最高推理档跌到 48.11%、MULTI-BO 0.864；(5) 固定模型换 4 种 harness，O-EVAL 只动 0.07 pp（59.81–59.88），榜单衡量模型而非 harness。分套件看（Table 6 / Figure 3）：CUMCM–MCM 鸿沟大且依赖模型——GPT-6 为 82.9 vs 46.2，GPT-5.5 为 79.7 vs 39.8；smoke 与 submersible 全员 100%，tennis 连旗舰也不到 40%。计分审计修正了若干陷阱：退化带放宽改一格（72.67→73.52，+0.35 pp）；剔除不可比单位指标使所有条目 +0.05–2.62 pp（系统性计分缺陷的签名）；最关键的是 dragon-dance 锚点本身不可行——论文值与比率相乘得 $1.406276\times1.604793=2.2568$ m/s，超过 2 m/s 上限，修正为连续时间值 1.246266 m/s 后，对齐错误锚点的 2 个模型从 100% 跌落、12 个'被扣分'的模型实则正确。可行性门控硬清零 7 格（heliostat 4 格违反功率 ≥60 MW 或镜面 ≥2 m、smoke-screen、Juneau、Olympic 各 1），其余排名保持稳定——外科手术式而非地毯式惩罚。案例研究还显示：crop-planting 论文约束联合不可行，锚点改用可复现的精确 MILP 最优（40,418,877 / 58,718,967 元），两模型分列两侧；Juneau 的可持续性分数被报在不同单位量表（锚点 1.007 vs Fable 的 79.1）。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 18 道 CUMCM/MCM 建模真题（多参考面板计分） | O-EVAL (%)，3 种子均值 | GPT-6 Astra + codex：64.58 ± 2.93 | DeepSeek V4.1 Flash + opencode：59.81 ± 1.25（开源低成本基线） | +4.77 pp（成本 $246.41 vs $2.54，约 1/100） |
| 18 道 CUMCM/MCM 建模真题 | MULTI-BO（相对 Flash 基线的差距收敛指数） | GPT-6 Astra：1.132 ± 0.02 | DeepSeek-Flash：1.000（定义基线） | 收闭 Flash 距人类面板剩余差距的 13.2% |
| 18 道 CUMCM/MCM 建模真题 | O-EVAL (%) | Fable 5.1 + claude-code：63.11 ± 1.33 | GPT-5.5 xhigh + codex：59.75 ± 1.55 | +3.36 pp（MULTI-BO 1.081，收闭剩余差距的 8.1%） |
| 开源低成本梯队（18 题） | O-EVAL (%) / MULTI-BO | Kimi K3 58.23/0.953；GLM-5.3 57.78/0.941；Qwen3.8 Flash 52.66/0.803 | DeepSeek-Flash 59.81（MULTI-BO = 1.000） | 均为负增益，无一开源模型超过基线指数 |
| harness 敏感性（固定 DeepSeek-Flash） | O-EVAL (%) | 4 种 harness：59.81–59.88 | opencode 参考 harness：59.81 ± 1.25 | 仅 0.07 pp 波动，远小于种子方差 → 榜单衡量模型而非 harness |
| 推理算力档位（DeepSeek-Flash） | O-EVAL (%) / MULTI-BO | 最高推理档：48.11% / 0.864 | 默认档：59.81% / 1.000 | −11.70 pp，更多思考预算反而更差且更贵 |
| 可行性硬门控（18 题全部提交） | 被清零单元格数 | 7 格（heliostat×4、smoke-screen、Juneau、Olympic 各 1） | 无门控时这些违反约束的答案照常计分 | 剔除违规格后其余排名保持稳定（外科手术式惩罚） |
局限与改进
作者承认的局限：每题归一化端点仍是一篇可复现 O 奖论文的复现（Limitations 一节的表述甚至仍把多论文面板称作'自然扩展'，与正文 3.2 节已实现的面板计分存在版本不一致的痕迹）；两层验证只能裁决'结构化产物能回答的可行性问题'（取值范围 A 与内部一致性 B），外部物理真相（C，如镜场是否真发 60 MW）属于世界而非产物，只在允许独立重放的题目上检验，缺证据的义务记为 witnessed gap 而非默认通过；面板规模随杰出论文数波动（每题 1–18 篇、中位数 4）；人类自身分歧的文献分裂任务（tennis）被移出头条排名；分数是 3 种子均值。我的补充观察：仅 18 题且只评最终问的数值核心，部分任务已饱和（2025 smoke 与 2024 submersible 全员 100%）而部分全或无（tennis 旗舰 <40%），分辨率两极化；大量低分源于参考量的尺度/范围未在 schema 中钉死（lamprey 的 $10^{80}$ 量级原始指数、Juneau 的 1.007 vs 79.1），这与其说是模型失败不如说是任务契约的缺口，却计入了模型分数；CUMCM/MCM 历年真题与部分 O 奖论文在社区公开流传，存在数据污染风险；效率维度只剩美元成本，未报告各模型的墙钟时间分布。
独立分析的弱点
独立分析四点弱点。第一，任务量与饱和度：18 题中至少 2 题（2025 smoke、2024 submersible）已无区分力，题型锁定三年 A/B/C 模板，长期会被'刷穿'；改进方向是逐年滚动加入新题、纳入中间问与灵敏度指标、按题目区分度加权合成总分。第二，schema 欠约束把记分问题转嫁给模型：剔除两个不可比单位指标让所有条目 +0.05–2.62 pp，说明存在系统性计分缺陷而非模型差异；Juneau 案例中 Fable 在自报的 0–100 量表上给 79.1 并无错误却被相对扣分。改进方向是把每个数值字段的单位、量纲与合法范围写进输出 schema（作者也承认这是'修任务而非修评分器'），并训练模型先声明单位再报数。第三，数据污染：CUMCM 题解与 O 奖论文在中文社区广泛流传，旗舰模型很可能见过题面甚至范文，82.9 vs 46.2 的 CUMCM–MCM 差距部分可能源于此；改进方向是建立赛后全新题目的保密评测通道、嵌入 canary 字符串检测记忆性。第四，面板投票可能测到'统计检验选择'而非建模能力：tennis 上按多数派回答得 0.909、对齐锚点仅 0.091，说明该题分数反映的是模型选了哪种有效检验；这类文献分裂任务虽被移出排名，但仍提示应把'结论是否被某种有效检验支持'与'数值接近度'拆成不同指标族分别报告。
未来方向
作者提出的方向：(1) 把 18 题的任务外壳推广到工程与交叉学科问题，持续扩大纯评测集；(2) 把基准变成训练信号——门控通过、oracle 归一化的分数是可执行、可复现的 RL 奖励：今天就能做拒绝采样（按 O-EVAL 排序保留过闸轨迹），也可做组相对策略优化（GRPO）并把门控当硬乘子，教模型'先满足物理再追参考'；dragon-dance 案例说明模型缺的是自检——奖励中的验证器正好训练这一点；(3) 训练模型主动产出'可行性见证'（逐镜布局、峰值邻域采样等），把 Level-C 类失败转化为可检查的证据，同时提高得分与可验证性。基于成果可延伸的方向：把面板从'均值'升级为'分布'，报告对多个可接受解的 spread 而非单点；钉死单位/范围后重评全榜，量化分数水位变化；把 624 条义务的不变式库作为课程化自检训练数据；在 MULTI-BO 类相对指数下做成本感知的帕累托调度；以及用无区分力任务（全员满分的 submersible）反推任务难度分层设计。
复现评估
复现条件较好。代码开源：https://github.com/wxj630/terminal-bench-math-modeling。任务材料全部来自官方竞赛（逐字题面、附件、PDF 裁图），O 奖论文本身不再分发，但每题锚点是'从公开语料推导的可运行脚本 + 已提交的期望结果'，并带论文 id、PDF/OCR 来源、复现范围等溯源字段，任何锚点都可重新推导（附录 D）。环境完全钉死：python:3.12-slim 加固定版本的科学栈（NumPy 2.0.2 / pandas 2.2.2 / SciPy 1.14.1 / scikit-learn 1.5.2 等），2 CPU / 8 GB / 无 GPU / 4 小时超时，断网加本地重试代理，成本用固定价格快照避免漂移。Lean 层无 Mathlib、干净构建约 1 秒，且可对已提交的 O 奖参考直接运行、无需保存的智能体产物。算力门槛低（纯推理评测、无训练），主要成本是模型 API：复现旗舰行需 $246–273/轮，复现开源基线约 $2.54/轮。注意两点：GPT-6 Astra 与 Fable 5.1 两行由第三方运行、作者用统一评分器重算过；指令文件在部分试验后被修订，复现时应引用试验日志中捕获的提示。总体属中等偏低复现难度：工程上开箱即用，瓶颈只在 API 预算与第三方模型行的可及性。
论文图表
左右对比两幅流程图：(a) 现状——智能体写完报告后由 LLM 裁判按'结构良好 8.5/10'打分，报告里的数字无人核查，一个看似合理但 h=1.2 m 违反 h∈[2,6] m 的答案照样得分；(b) TB-MathModel——题面+附件+插图进终端容器，智能体交一个 JSON 产物，按单侧计分对照 O 奖复现打分，程序化门控加 Lean 4 独立验证可行性，不可行直接清零。
一张图讲清论文的问题意识与全部设计回应，是理解动机（报告级评测为什么不可信）与方法（产物级评测如何闭环）的最短入口。
对比四个最接近的建模基准：Mamo（1209 题，求解器检验）、ModelingBench（68 题，LLM 裁判）、MM-Bench（111 题，LLM 裁判）与 TB-MathModel（18 题、21 图、可执行验证器），后三者列比较了智能体化、物理可行性、Lean 证明与多模态四个维度。
一表定位论文的空缺：只有本文在'完整竞赛题 × 智能体终端 × 可执行验证器 × 物理可行性 × 机器可查证明 × 多模态'上全打勾，是相关工作对比的核心证据。
主结果表：七个多模态模型/harness 组合在 18 题上的 O-EVAL（%）、MULTI-BO 与单轮美元成本，均为 3 种子均值±标准差。GPT-6 Astra 64.58±2.93 居首，$2.54 的 DeepSeek-Flash 以 59.81±1.25 只落后 4.77 pp。
这是论文的头条结果表，成本-精度权衡与旗舰/开源分层全部来自此表，引用本文必引此表。