NUS 发布 MolLean：基于 Lean 的过程可验证化学推理语言，抑制模型幻觉

新加坡国立大学团队提出 MolLean，以 Lean 内核将化学推理锚定在显式分子状态上；在 8800 个样本、12 项任务上，Qwen3.6-27B 的全轨迹修正优于直接思维链并降低幻觉。MolLean-MCP 支持状态转移、检查和拒绝读取，被拒动作不改变状态。类型化 witness 协议区分结构检查与外部测量数据。