MolLean: A Process-Verifiable Language for Chemical Reasoning

MolLean. A Process-Verifiable Language for Chemical Reasoning. By Jiatong Li and one other, from the National University of Singapore. Published on the fourteenth of October. Its code repository is a placeholder: a readme, and nothing to run yet.

When a language model reasons about chemistry step by step, the chain of thought can contain hallucinated claims about structure and about properties. Written as free-form explanation, those claims sit there unchecked, and nothing in the text itself distinguishes a correct commitment from an invented one. A step that says a group was added, or that a property now holds, reads exactly the same whether it is true or not. The reasoning has no state underneath it to be held against.

MolLean is a process-verifiable language that grounds chemical reasoning in an explicit molecular state. Instead of describing a molecule in prose, the reasoning acts on a state, and every step becomes something that can be checked.

The checking is done by a layered kernel built on Lean. It verifies state transitions and assertions over molecular readouts, at every level from primitive graph edits up to compound transformations. Alongside it, a typed witness protocol keeps two kinds of evidence apart: structural checks the system performs natively, and measurements supplied from outside.

MolLean-MCP is a stateful tool interface that exposes these transitions, checks and readouts while the model is generating. The model receives feedback and uses it to decide its next action, and any rejected action leaves the state unchanged. A bad step, in other words, is refused rather than silently absorbed into what follows. In total MolLean supports three modes: one-pass trace execution, whole-trace refinement, and interactive reasoning through MolLean-MCP.

All three modes are evaluated against direct chain-of-thought on eight thousand eight hundred matched examples. These span twelve tasks covering molecular generation, editing, optimization and reactions. With Qwen3.6-27B, whole-trace refinement outperforms direct chain-of-thought on all twelve tasks. MolLean-MCP complements refinement with stepwise verification feedback, and reaches better performance on the reaction tasks. The two are presented as working together rather than competing: refinement revises a whole trace, while the interactive mode checks each step as it is taken.

The broader argument is about where chemical commitments live. In ordinary chain-of-thought they live only in explanation. Here they become operations on a state that can be executed, checked, and revised, which the authors present as an executable foundation for chemical reasoning.