让化学AI把推理过程写成可检查的账本
AI 做化学推理时，经常一本正经地编造分子结构和性质——它说出来的中间步骤，没人能验证真假。这篇把推理过程变成一套可执行、可检查的「账本」:每一步对分子的改动、每个读出的性质，都必须经过一个类似数学证明器的内核验证，错了就当场驳回、状态不变。模型不再只是写一段自由发挥的文字，而是边推理边被反馈纠错。在 12 个化学任务、8800 个样本上，这种「整段回溯修正」的方式全面超过直接思维链，反应类任务里配合逐步验证效果更好。它不是你明天就能用的工具，但它指向一个更可信的方向：让 AI 的化学推理从「说给你听」变成「做给你看」。
📄 原文摘要(英文)
Chemical chain-of-thought can contain hallucinated structural and property claims. We thereby introduce MolLean, a process-verifiable language that grounds chemical reasoning in an explicit molecular state. A layered Lean-based kernel checks state transitions and assertions over molecular readouts, from primitive graph edits to compound transformations. Meanwhile, a typed witness protocol separates native structural checks from externally supplied measurements. We further introduce MolLean-MCP, a stateful tool interface that exposes these transitions, checks, and readouts during generation: the model receives feedback to decide its next action, and rejected actions leave the state unchanged. MolLean supports one-pass trace execution, whole-trace refinement, and interactive reasoning through MolLean-MCP. We evaluate these three modes with direct chain-of-thought on 8,800 matched examples across 12 tasks spanning molecular generation, editing, optimization, and reactions. With Qwen3.6-27B, whole-trace refinement outperforms direct chain-of-thought on all 12 tasks. MolLean-MCP complements whole-trace refinement with stepwise verification feedback, reaching better performance in reaction tasks. Together, these results highlight an executable foundation for chemical reasoning, in which explicit chemical commitments can be checked and revised rather than remaining solely in free-form explanations.