MolLean：让化学推理从“会解释”走向“可验证执行”

导语

大语言模型能够用自然语言描述化学推理，却不代表它真的完成了可靠的结构计算。一个模型可能在分子编辑时漏数原子、虚构官能团，或声称某项性质得到改善，却没有给出测量依据。MolLean 试图改变这种“先生成解释、再由人判断是否可信”的工作方式：它把化学推理表示为一串可执行的操作，并让每一步都围绕一个明确的分子状态展开。

核心要点

• 显式状态是推理基础。 MolLean 不把分子仅当作文本中的名称或描述，而是持续维护一个分子状态。模型提出的图编辑、结构变换和相关断言，都需要与该状态保持一致。
• 分层内核负责检查。 系统使用基于 Lean 的分层验证内核，从基础图操作一直检查到更复杂的复合变换，并验证模型对分子读数提出的声明。
• 区分结构事实与外部测量。 其类型化见证协议将可以由系统原生检查的结构性质，与需要外部工具提供的测量结果分开处理。这意味着“结构已经改变”和“某个性质变好了”不再被混为一谈。
• 支持多种运行方式。 MolLean 可以执行一次性推理轨迹，也可以对完整轨迹进行校正；配套的 MolLean-MCP 则提供有状态的交互式接口。模型每次行动后都能收到检查反馈，若操作被拒绝，分子状态不会被悄然修改。

论文展示的例子包括把乙醇编辑为 1-丙醇、满足精确的 25 个碳原子约束、依据测得反馈进行 QED 优化，以及在一次交互过程中拒绝不合法的苯基连接并保留原状态。这些例子说明，验证机制不仅能指出错误，还能为下一步操作提供明确边界。

实验与意义

研究者在 8800 个匹配样例上比较了直接思维链、一次性轨迹执行、全轨迹校正和 MolLean-MCP 交互推理，任务覆盖分子生成、编辑、优化与反应等 12 类场景。使用 Qwen3.6-27B 时，全轨迹校正在全部 12 类任务上超过直接思维链；MolLean-MCP 则以逐步反馈补充完整轨迹校正，并在反应任务中取得更好的表现。

这项工作的价值不只是给化学模型增加一个检查器，更在于重新定义了化学推理的输出形式：模型不应只给出听起来合理的结论，还应提交一条可以执行、复核和修正的过程。对于分子设计和反应规划而言，这种机制有望降低结构幻觉与无依据属性判断的风险。不过，当前材料主要报告了框架和基准实验，项目页面显示代码仍计划发布，因此其在更广泛数据、真实实验闭环及不同模型上的表现仍有待进一步验证。

Hugging Face Daily Papers