数学建模是竞赛题，也是真实工作的接口层。

一道刻意欠定的现实问题丢过来，你得自己定假设、选模型、写代码、跑求解器，最后交出一份站得住的结论。这条链上任何一环断了，答案就是废的。过去两年评测 Agent，测的几乎全是链条末端——代码能不能跑通、答案算得对不对。

新发布的 TB-MathModel 把整条链塞进了评测里。任务本身并不刁钻，2024 年 CUMCM A 题的舞龙任务（dragon-dance），Agent 读题、看图、写代码，最后交出一份 JSON 算末端速度峰值。真正尴尬的是，这套评测在跑的过程中自己先摔了一跤。

论文记录，12 个被测模型给出的峰值 1.246266 m/s 是对的，却因为参考答案本身算错而被压在 49.82%；另有 2 个模型跟着那份错答案走，反而拿了满分。错在哪：人类 O 奖论文对速度做了整数秒取整，跨过了 t=14.48 s 处的连续时间真实峰值，算出 1.406276 m/s，再乘上 1.604793 的放大系数变成 2.2568 m/s，越过了题面规定的 2 m/s 上限——这份"标准答案"物理上根本不可行。

论文团队自己把这个问题挖出来并改了锚点值。论文写道：模型是对的，我们的锚点是错的。

把"建模"变成机器能判的分

TB-MathModel 收了 18 道真实竞赛建模题：CUMCM（中文）和 MCM（英文）2023—2025 每年 A/B/C 三题，各 9 道。题目原文、官方附件和从 PDF 里裁出来的图一起塞进 Docker 容器，Agent 要自己读题、开表格、看图、写代码、跑求解器，最后交一份 JSON。容器限制 2 核、8 GB 内存、无 GPU、4 小时超时、断网。

关键在判分方式。论文把三类已有做法摆在一起对比：Mamo 有 1209 道题但只验 solver 片段；ModelingBench 68 道、MM-Bench 111 道都靠 LLM judge 给报告打分，论文对这类做法的评价是"奖励流畅的散文，却不确认报出来的数字是否正确甚至是否站得住"。TB-MathModel 只判最后一问的数字核心，用可执行 verifier 打分。

还有两个设计比分数更值得看。

一是方向感知的单向打分。每个指标显式标注 higher_is_better、lower_is_better、target_value 还是 exact_value，达到或超过锚点永远不会低于 1.0。锚定式打分的通病是：抄答案的拿高分，比答案更好的反而拿低分。单向打分把这条堵死了。

二是用 99 份人类 O 奖（Outstanding-award）论文做评审团，而不是认准一份"标准答案"。99 份里有 94 份给出了被评的量，每题 1 到 18 份、中位数 4 份，一人一票。数学建模本就没有唯一解，把某一支队伍的选择当成 ground truth 本身就是错的。

可行性交给 Lean 4 审卷

更狠的一层在可行性校验。

外层是程序化闸门，覆盖 18/18 任务，把硬错误归进六类可判定的不变量形式：取值域与范围、整数与二值、序关系、精确恒等、有限域、划分求和。比如定日镜场那题要求额定功率不低于 60 MW、镜面安装高度在 2—6 米之间。

里层是 Lean 4：把同样的不变量重新证一遍，18 道题一共生成 624 条内核检查的 obligation，不用 Mathlib，数值全部缩放成整数因此没有浮点容差；信任审计（#print axioms）只出现 propext 和 Quot.sound，没有 sorryAx，也没有 native_decide。

这不是用 Lean 4 去解题——解题是模型的事。它是用来审 benchmark 自己的：闸门判的每一个决定，都要有一条机器可查的定理托底。

闸门一共硬性作废 7 个格子，集中在定日镜场那题（4 个），另有烟幕、Juneau、奥运各 1 个。

贵的不一定赢，加钱反而更差

七个多模态组合、每题三个种子跑下来，O-Eval 是主指标，Multi-BO 是相对 DeepSeek-Flash 基线的增益指数（1.000 代表与基线持平，1.132 代表追平人类评审团剩余差距的 13.2%）：

  • GPT-6 Astra + codex：64.58%（±2.93），Multi-BO 1.132，246.41 美元
  • Fable 5.1 + claude-code：63.11%（±1.33），Multi-BO 1.081，272.80 美元
  • DeepSeek-Flash + opencode：59.81%（±1.25），Multi-BO 1.000，2.54 美元
  • GPT-5.5 xhigh + codex：59.75%（±1.55），Multi-BO 0.998，99.37 美元
  • Kimi K3 + opencode：58.23%（±1.12），Multi-BO 0.953，23.26 美元
  • GLM-5.3 + opencode：57.78%（±1.30），Multi-BO 0.941，28.15 美元
  • Qwen3.8 Flash + opencode：52.66%（±1.17），Multi-BO 0.803，8.30 美元

两个结论。一是 2.54 美元的 DeepSeek V4.1 Flash 咬住了 59.81%，成本大约是头名的百分之一，落后约 4.8 分——这个性价比组合比单纯比谁分高更值得看。二是给 DeepSeek-Flash 调到最大推理档，多花的钱换来的是掉到 48.11%，Multi-BO 从 1.000 掉到 0.864。更长的思考预算在这些任务上不单调。

还有一组数据专门回应"分数到底是模型的还是壳子的"：固定模型、只换四种 harness，O-Eval 全部加起来只动了 0.07 个百分点（59.81—59.88）。榜基本身测的是模型。

不过作者也自己拆了台：种子间最大偏差到 2.93 个百分点，所以前两名的差距落在噪声里，不构成显著差异。而仓库里的实时榜单（https://github.com/wxj630/terminal-bench-math-modeling）已经翻过一次——按单次跑分排，Fable 5.1 + claude-code 的 64.62% 反而压过 GPT-6 Astra + codex 的 61.47%。仓库自己写着：一两分的差距在种子噪声之内，没有模型越过 65%。

所以呢

TB-MathModel 真正的贡献不是又一张榜单，而是把"可验证"从赛题本身挪到了评测基础设施里：闸门查约束，Lean 4 查闸门，人类评审团查单一锚点的偏见。

模型层越来越强，但只要评测还是 LLM judge 读报告、还是拿一份"标准答案"对齐，测出来的就只是流畅度和抄写能力。真正难的那层——把一团乱的现实压成一个能算、能验、能辩护的模型——目前测得最差。

论文页上的话说得很直接（https://huggingface.co/papers/2611.08237）：离能处理真实世界问题的 Agent 还很远，而那条路需要的正是统一的环境、可验证的奖励，以及一份能复利增长的 agent 轨迹语料。据 AI Weekly 的报道（https://aiweekly.co/alerts/tb-mathmodel-gpt-6-astra-tops-contest-bench-at-6458-o-eval），作者团队来自香港科技大学（广州）、IDEA Research 与 DataArcTech。

这份基准自己也交了一次学费：错的是它。能让基准自己承认自己错的评测，才配拿来衡量模型。