MolLean: A Process-Verifiable Language for Chemical Reasoning
Jiatong Li, Yatao Bian
cs.CL, cs.CE, cs.PL
2026-10-15
把化学推理落到 Lean 逐步验证的分子状态上，被拒操作不改变状态；Qwen3.6-27B 用整轨迹修正后 12 项分子任务全部超过直接思维链。
化学思维链有个顽固的失败模式：答案看着对，中间步骤却引用分子上不存在的官能团、弄丢一根键，或宣称 QED 提升了却从没算过。作者团队前期的分析在正确答案旁边照样找到捏造的结构断言。根因是中间步骤为自然语言，机器无法检查。Lean 在数学证明里给出过范式：模型提推导，证明助手查推导。化学缺的是给每一步一个共享的分子指称对象和明确的接受条件，MolLean 补的就是这块。
整个语言建立在一个契约上：操作指向当前分子状态，验证器判定能否接纳，只有被接纳的转换才提交新状态，被拒的操作原状态不动。状态装着活动分子、leaving pool(分离后不计入答案的片段)、原子索引和记账计数。操作分三类：
两处设计有讲究。Concerted 把一组编辑打包原子化、总价一次检查，「先成键再断键」不会卡在瞬时超价上，附录的酰化案例正是改成 BondFormBreak 一步完成才通过。断言的证据来源被显式分层：结构计数原生判定，测量值必须外部作证，这条边界有六个断言族的定理背书。
接口有三种，共享同一套执行语义：One-pass 一次交完整轨迹；Refinement 拿拒绝反馈后整条重写，最多 8 次，每次从初始状态重启；MolLean-MCP 把转换、检查、读出做成有状态工具接进推理循环，模型先看当前状态再选下一步，被拒的调用不改变状态。
主实验用 Qwen3.6-27B,8,800 条匹配样本、12 项任务：9 项 S2-Bench 各 500 条，USPTO-50k 正逆反应各 500 条，ChEBI-20 全测试集 3,300 条。
| 任务 | CoT | One-pass | Refine | MCP |
| 原子数生成 | 42.0 | 61.4 | 88.8 | 82.6 |
| 加基团 | 55.8 | 93.6 | 100.0 | 100.0 |
| 正向反应 | 35.0 | 23.6 | 62.8 | 66.4 |
| 逆合成 | 3.0 | 11.6 | 20.8 | 27.4 |
| ChEBI-20 文到分子 | 18.1 | 25.3 | 33.1 | 23.5 |
Refine 对 CoT 的 12 项配对差全部显著(4,000 次 bootstrap 的 95% 区间不含零)，涨幅 12.0 到 48.2 个百分点。正向反应那列信息量最大：One-pass 只有 23.6%,比裸 CoT 的 35.0% 低 11.4 个点，一次性写对整条轨迹的负担很重，反馈的价值主要在补救初稿没写对的义务；给 8 次重写后到 62.8%,大半收益在前两轮到账(k=2 已 58.0%)。
第二组数字讲另一件事：轨迹被接纳不等于答案对。逆合成最终 88.2% 的轨迹过验证，答案准确率 20.8%;ChEBI-20 是 79.0% 对 33.1%,2,608 条被接纳的轨迹里 1,533 条答案错误。从 k=2 到 k=8,ChEBI-20 接受率从 67.3% 爬到 79.0%,准确率只从 31.1% 挪到 33.1%:后期修订修的是模型自己声明的义务，不是任务。
Qwen3-4B 上结构类任务涨幅可观(原子数 15.8 到 56.8,加基团 13.4 到 91.4),逆合成所有协议都是 0.0%,正向反应 1.6%。验证器救不了缺乏化学知识的提议器，作者自己也这么写。
这份工作把 process supervision 从「训练一个 verifier」换成「写一个确定性检查器」：不用标注，也不会被 reward hacking。做分子编辑、计数类任务的团队可以直接拿走接近满分的收益；MCP 那套「被拒调用只花一次调用、状态不动」的设计，对任何 tool-use agent 都是好抄的模式。soundness 与答案准确率分开报，本身就有测量学价值。也要说清：Lean、RDKit、MCP、tool-use 都是现成件，新意在垂直域里把证据来源和提交语义切干净，性质上属渐进改进。
作者自认的：可接受不等于忠于任务，附录的盐案例中，重写版丢掉氯离子及其计数义务，轨迹被接受、答案错误，指令到约束的落地被点名为下一个瓶颈；4B 模型在参照类任务上崩溃；MCP 没在 4B 上跑，理由是小模型交互能力弱。
读下来还有几处要打问号。断言的参照很多由模型自己定，OutcomeMatch 拿模型自己写的 SMILES 当目标，接近自己出题自己判，后期接受率涨而准确率不涨正是症状。外部 witness 被默认可信，协议管类型不管真伪。模型只测了 Qwen 两档，没有其他家族对照，「验证普遍有效」还立不住。优化任务的涨幅区间用方向性成功口径，相似度加权的绝对值低不少(QED 方向成功率 92.2%,加权分 59.0)。