MathModelingAgent

一个闭环科学建模 Agent：持续观测、验证和纠偏，而不是一次性生成答案。 模型负责提出，工具负责验证，证据决定结论。

MathModelingAgent 面向开放式数学建模、预测、优化、估计、仿真和机制分析。它把人与智能体的协作组织成一个可追问、可复检、可恢复的科学闭环：

提出模型 → 执行计算 → 观测结果 → 独立验证 → 发现偏差 → 修正模型 → 再验证

直到结论获得足够证据支持，或者系统明确返回 CONDITIONAL、INCONCLUSIVE、REFUTED 等非确定状态。

为什么需要闭环建模

LLM 作为数学建模辅助工具，能够帮助理解题目、提出候选模型、编写代码和整理报告，但它也可能在题意、公式、边界条件、代码结果、引用或常识判断上产生幻觉。一个“看起来完整”的答案，不等于一个可信的数学结论。

数学建模论文的本质，不只是给出一个可能正确的数字，而是把问题、数据、假设、推导、计算、验证和局限有条理地描述清楚。没有人能够理解、追问和复核的答案，即使碰巧正确，也很难成为重要的科学交付。

普通的 LLM + Python 流程通常是开环的：

理解题目 → 建模 → 写代码 → 得到结果 → 输出答案

其中代码 exit 0、优化器返回一个解、图像看起来合理、solver 报告 feasible，或 LLM 认为结果符合直觉，都只能说明某个局部环节完成了，不能单独证明最终结论成立。

MathModelingAgent 把它改造成闭环：

             ┌────── 验证与反例 ──────┐
             ↓                       │
问题 → 建模 → 计算 → 结果 → 鲁棒性 → 结论
 ↑       ↑      ↑      ↑             │
 └────── 修正、降级、换方向 ─────────┘

如果观测结果与题目要求、数学约束或现实解释不一致，系统不会继续把答案写得更完整，而是回到相应阶段，修正假设、增加验证、换模型或降低结论强度。

从控制论看 MathModelingAgent

这里的“控制”不是指用控制算法解决所有建模题，而是用反馈、观测、误差、约束和纠偏来组织 Agent 自己的建模过程：

| 闭环概念 | MathModelingAgent 中的对应物 | | --- | --- | | 目标 | 题目要求、约束和需要回答的问题 | | 系统状态 | 当前假设、模型、主张、证据、失败和未解决问题 | | 观测 | 数值结果、验证结果、反例、误差和审计 finding | | 控制动作 | 重算、修改假设、换模型、增加实验、补验证、降低结论 | | 反馈 | PASS / FAIL / INCONCLUSIVE 与新的科学证据 | | 边界 | 数学约束、数据条件、验证义务和阶段门禁 | | 终态 | SOLVED / CONDITIONAL / INCONCLUSIVE / REFUTED 等 |

人与智能体的边界也因此变得清晰：智能体可以自主执行可逆的计算、整理和检查；凡是改变问题理解、全局假设、模型方向或结论强度的决定，都必须留下可读的依据和变化记录，并在需要时交由人确认。每个阶段都有明确的输入、输出、检查方式和下一步，而不是把关键判断藏在一个无法解释的答案里。

这也是本项目的三层定位：

• 一句话： 一个闭环科学建模 Agent。
• 核心机制： Claim → Obligation → Evidence。
• 核心原则： 模型负责提出，工具负责验证，证据决定结论。

工作方式

1. 题目与数据：明确问题目标、输入、约束、缺失信息与歧义。
2. 理解与拆解：拆成可验证的子问题，登记假设、候选模型与关键主张。
3. 建模与执行：提出候选方案，用数值计算、优化、仿真、符号计算、文献、形式验证执行并保留产物。
4. 证据验证：独立重算、检查单位量纲、对照公式与代码、查找数据泄漏、比较基线、做敏感性分析、构造反例、查引用与可复现性。证据不足就回去修正，而不是硬通过。
5. 结果交付：说明哪些结论已支持、哪些有条件、哪些无法判断，以及如何复现、当前运行为何结束。

Chat-first 输出顺序

每个重点环节都会先把完整、可读、可追问的文本直接输出在聊天正文中，再等待用户纠正或确认；确认后才写入 artifact，并允许 run-state 进入下一阶段。适用范围包括 D0/D-R、数据画像、全局假设、候选方向、SP1…、模型、计算结果、验证、鲁棒性、评价和 D4。

如果某一阶段只生成了文件、工具摘要或一句结论，而没有在聊天中展示完整内容，它不算完成，真实 run 会停在当前阶段。

模式、算力消耗与组合建议

模式预算是一次 run 的执行上限，不代表一定会全部消耗。粗略可以用下面的模型理解总成本：

C_total ≈ A × (C_model + C_compute + C_verify) + Q × C_research

• A：允许的尝试轮数；
• C_model：每轮模型分析、代码生成和报告整理的成本；
• C_compute：每轮数值计算、优化或仿真的成本；
• C_verify：每轮独立重算、反例、鲁棒性和一致性检查的成本；
• Q：文献/方法检索次数；
• C_research：每次检索、阅读和整理的成本。

当前默认预算如下。计算预算只表示工具执行上限，不等同于模型 token 费用；实际消耗取决于问题复杂度、是否触发修正、工具耗时和证据缺口。

| 模式 | 最大尝试轮数 | 文献检索预算 | 计算预算上限 | 相对 Fast 的计算预算 | | --- | ---: | ---: | ---: | ---: | | Fast | 2 | 0 | 60 秒 | 1× | | Standard | 12 | 12 | 1800 秒 | 30× | | High-Assurance | 24 | 30 | 7200 秒 | 120× |

High-Assurance 还要求独立审计和更严格的终态门禁，因此通常比表中的计算预算比例更慢；但它不是“必然正确”，只是给验证、反例和修正留下更多预算。

推荐组合

1. Fast → Standard：先用低成本判断题目类型和可行方向，再对选定方向完整建模。适合普通练习题。
2. Standard → High-Assurance：先完成 Q1 → Q2 → Q3，再只对最终候选做高保证复核。适合数学建模竞赛和论文交付，通常最划算。
3. Fast → Standard → High-Assurance：先筛选，再完整求解，最后审计。适合问题复杂、验证成本高或需要提交论文的任务。
4. 直接 High-Assurance：只在结论风险高、问题依赖多或必须尽量减少遗漏时使用；不建议对尚未稳定的早期方向直接使用。

模式在 run 初始化时确定。需要升档时创建新的 run 或 correction lineage，可以复用输入快照，但不能静默修改原 run 的历史结果。

核心：Claim → Obligation → Evidence

Claim（主张）：影响结论的重要陈述，如"C1：该方案是全局最优解"、"C2：模型可泛化到训练数据之外"。

Obligation（义务）：按主张类型要求证据——

• 数值结果：独立重算 + 容差 + 误差界 + 输入配置一致
• 最优性：精确搜索 / 可证上下界 / KKT / 对偶 / 形式证明；只有启发式优化结果时只能说"当前搜索下的最佳解"，不能升级为"全局最优"
• 预测能力：防泄漏划分 + 基线 + 验证/测试集 + 校准 + 不确定性

Evidence（证据）：记录方法、工具、命令、环境、输入输出哈希、退出码、产物、容差、局限与支持的主张；等级：

LEGACY_UNVERIFIED → DERIVED → EXECUTED → VERIFIED → INDEPENDENTLY_VERIFIED → EXTERNALLY_VALIDATED

原则：证据强度不能弱于主张强度。

验证协议

验证不是让另一个 LLM 再"看一遍答案"，而是按固定顺序攻击：

1. 任务覆盖：是否真回答原问题、是否偷换代理指标、是否漏子问题
2. 数学与约束：单位、量纲、定义域、边界、约束、推导
3. 推导与实现一致性：公式 ↔ 代码 ↔ 参数 ↔ 结果
4. 数据与实验设计：标签、划分、数据泄漏、后验参数、来源
5. 模型可信度：基线、不确定性、敏感性、鲁棒性、外部效度、更简单替代
6. 可复现性：版本、种子、配置、命令、引用真实性
7. 反例攻击：边界案例、失败案例、更简单解释

裁决只有三态：

• PASS：可复现证据支持
• FAIL：矛盾 / 反例 / 无效方法 / 复现失败
• INCONCLUSIVE：证据不足——不能因为"看起来合理"升级为 PASS

终态与进展

不只有 SOLVED：PARTIAL 部分解决 / CONDITIONAL 结论依赖条件 / INCONCLUSIVE 证据不足 / REFUTED 被反驳 / INFEASIBLE 不可行 / UNIDENTIFIABLE 信息不足 / BLOCKED 外部阻塞 / CANCELLED 取消。ATTEMPT 永远不能直接跳到 SOLVED。

算进展：关闭一条义务、新增可复现证据、反驳候选、收紧界或区间、移除阻塞、修复问题、正确降低结论强度。 不算进展：换说法、同参数重跑、写更长、exit 0、模型说"有信心"。 连续多轮无进展 → 换方向 / 请求用户决策 / 以非 SOLVED 状态暂停。

SOLVED 硬门禁：范围冻结 + 必选 verification 通过并聚合为 SATISFIED 的 obligations + SUPPORTED claims + 关键对抗检查通过 + 可复现材料齐全 + 局限已声明；High-Assurance 还需独立审计（审计器只读产物，不依赖求解过程的私有推理）。

当前版本：v0.5.2 Evidence-driven pipeline

本版本新增：v3 run/ledger evidence graph；独立的 verification / obligation / claim / run 状态；inputs/raw 冻结快照和 SHA-256 校验；typed verification recipes；真实输出量化后的硬约束复检；九段科学报告、symbols 和 Answer Coverage；结构化失败启发；PROJECT_INITIAL_REVIEW 与 PAPER_FINAL_REVIEW 两种论文质量评审；以及不修改父 run 的 correction lineage。

PASS 只表示某条 verification recipe 通过，不自动表示 claim SUPPORTED 或 run SOLVED。用户 waiver、未证明全局最优和部分证据只能进入 CONDITIONAL。CUMCM/MCM/ICM 评分是 paper-quality proxy，不是官方 CUMCM/COMAP 评分。

两个 Skill

• math-modeling-agent：建立和推进模型。目标不是"写一篇看似完整的答案"，而是把问题推进到有证据支持的结论，或清晰可恢复的科学状态。
• math-modeling-audit：独立审计已有模型/论文，逐条回答哪些主张 PASS / FAIL / INCONCLUSIVE 以及为什么；不替作者修改。

工具：可插拔，缺失就降级

工具只是产生证据的方式，可以替换，工作流不变。

本插件保留原 GitHub 项目的核心行为：问题/附件探查、子问题顺序求解、Modeler → Analyzer → Correction 迭代、逐轮日志和可恢复运行；对应关系见 skills/math-modeling-agent/references/original-project-parity.md。

数学计算后端扩展位于 skills/math-modeling-agent/scripts/computation/：它只负责探测可调用后端、生成能力快照和校验计算记录，不捆绑 Mathematica/SageMath 等外部引擎。

• Python 可选（推荐）：需要计算时在运行目录内创建隔离环境（数值计算、数据分析、优化、仿真、绘图、独立重算）
• Lean 可选：形式化验证；不自动安装；形式命题被证明 ≠ 现实主张被证明
• Wolfram 可选：符号计算、解析推导、恒等式验证
• 文献研究：未知方法、证据缺口、参数依据不足、换方向时检索；私有原始数据不进检索

工具缺失不会伪装成验证成功：记录缺失 → 降低证据等级 → 降低结论强度 → 保留未满足的义务。

可恢复运行

默认运行目录 math-modeling-runs/<task-id>/：

run.json  ledger.json  events.jsonl   # 原子状态 + 契约（interactions/decisionStack）+ 日志
problem-brief.md  inputs.json         # 冻结的问题重述 + 输入清单
inputs/raw/  inputs/manifest.json      # 自包含输入快照 + SHA-256 校验
attempts/<n>/                         # 每轮：report.md + code/ + data/ + plots/ + _drafts/
failed/directions/<id>/               # 方向级失败：wall memo + 代码 + 放弃理由
failed/code-drafts/<attempt>-<name>/  # 实现级失败：bug 版/超时版/弃用版（不删除）
failed/failures.jsonl + failed/issues.md # 结构化失败与索引（DATA/TOOL/IMPLEMENTATION/MODEL/VALIDATION/EVIDENCE/RESEARCH_GAP）
research/  walls/                     # 文献检索 / 突破备忘录
reproducibility.json  final-report.md

每个会改变模型结构的决策在对话中交互确认并写入 ledger（D0 重述/D1 路由/D2 子问题假设/ D3 方向/D4 裁决），run-state.mjs gate 在每次状态转移前强制校验；终态前强制鲁棒性 敏感度分析；失败尝试按类归档到独立目录。

崩溃恢复：跨进程互斥锁 + stale 锁与 reclaim guard 回收 + Windows 共享冲突重试；已完成且输入未变的工作不重跑；任何失败都保留最佳候选与原始产物。

MCM / ICM 终审（audit Skill）

模拟终审框架（非 COMAP 官方评分表）：一票否决与奖项封顶 → 七类 100 分评分 → 模型逐个审计 → 关键结果审计 → MCM A/B/C 与 ICM D/E/F 专项 → 固定 14 节终审报告。评分不修改建模侧的 SOLVED 判定。

快速开始

安装：

dsh plugin --profile web add github:yohanchen1/MathModelingAgent#v0.5.2
dsh --profile web --dump-config   # 检查组合层（应看到 dsh-math-modeling-agent-skills 行）
dsh web                          # 重启以加载插件

（npm 源通道：dsh plugin --profile web add dsh-math-modeling-agent —— 从 npm registry 拉最新版； dsh plugin 会在 profile 目录执行 pnpm 安装并自动把插件注册进 dsh.profile.bundles， 不要用 npm install 代替，那会装到错误位置。如本机镜像源同步滞后，可显式走官方源： dsh plugin --profile web add dsh-math-modeling-agent --registry=https://registry.npmjs.org/）

维护者在发布后应分别核对 GitHub 解包目录、npm tarball 解包目录和 profile 安装目录：

node skills/math-modeling-agent/scripts/distribution-parity.mjs <source-root> <candidate-root>

该命令比较 package.json files allowlist 内所有文件的 SHA-256；它不把 AI 解题中的偶发失败当作分发失败。dsh --profile web --dump-config 用于检查组合， 但新版 DSH 可能重写 profile 的空 cordis.yml，不是严格只读操作。

开始建模——直接描述任务即可。每个环节都是人与 LLM 的深度信息交换：LLM 给出带依据链的 完整分析（题面原句/数据证据/文献/显式判断标记），你纠正、补充背景或提供自己的参考文献， LLM 更新并展示差异。建模前必须先做文献调研（AI 检索原理与方法文献，你可增删），每个候选 方向都有文献出处；每轮在对话直接输出 runlog 式摘要（问题重述/分析/假设/建模求解/验证/鲁棒性/ 评价改进/参考文献），失败尝试按类归档，终态前强制鲁棒性敏感度分析：

建立这个数学建模问题的模型，先分析题目和数据。
任何"最优""显著""泛化"的结论都必须提供相应证据，证据不足不要强行确定。

独立审计——给已有论文/模型/代码：

独立审计这份结果，逐条给出 PASS / FAIL / INCONCLUSIVE，不要帮我修改原文。

项目结构

skills/
├── math-modeling-agent/   # 建模、执行、修正、生成证据
└── math-modeling-audit/   # 独立复算、反例攻击、证据审查、MCM/ICM 终审
assets/                    # README 工作流总览图
tests/                     # 状态机、锁与恢复、验证协议、打包完整性、MCM 评分
cordis.patch.yml  package.json  README.md  LICENSE

卸载

dsh plugin --profile web remove dsh-math-modeling-agent

然后重启当前 DSH host。

设计原则

1. 模型可以提出结论，但不能自己给自己判卷。
2. exit 0 只是程序状态，不是数学结论。
3. 不确定性是合法答案：INCONCLUSIVE 优于编造。
4. 结论强度必须匹配证据强度。
5. 失败应该被保留：反例与失败方向防止下一轮重蹈覆辙。
6. 结果应可被他人复检：数据、代码、命令、哈希、验证记录、局限。

方法论来源

继承"问题分解 + 多轮尝试 + 失败后换方向"的 Agent 建模思想（受 IMO25 等启发）。核心变化：把验证裁决从 LLM 主观评价中拿出来——不是"分析者觉得 4/5 分可以通过"，而是 Claim → Obligation → 工具/独立检查 → Evidence → PASS / FAIL / INCONCLUSIVE。LLM 可以提出主张、攻击主张，但不能仅凭自己的判断宣布主张已被证明。

License

MIT