MolLean: A Process-Verifiable Language for Chemical Reasoning
Jiatong Li, Yatao Bian
cs.CL, cs.CE, cs.PL
2026-10-15
MolLean checks LLM chemical reasoning against a Lean-verified molecular state; whole-trace refinement beats direct CoT on all 12 tasks with Qwen3.6-27B, gaining 12-48 points.
Chemical chain-of-thought has a stubborn failure mode: the final answer can look right while the reasoning cites a functional group that is not on the molecule, loses track of a bond, or claims a property improvement nobody computed. The authors' own earlier analysis found fabricated structural claims sitting next to correct answers. The root cause is that intermediate steps are free-form text with no machine-checkable meaning. Mathematics set the precedent with Lean: the model proposes a derivation, a proof assistant checks it. Chemistry was missing the equivalent, a shared molecular referent for every step plus an explicit acceptance condition. MolLean supplies both.
Everything rests on one contract: an operation refers to the current molecular state, a verifier decides whether it is admissible, and only an accepted transition commits a new state. A rejected operation leaves the state untouched. The state holds active molecules, a leaving pool for fragments excluded from the answer, atom indices, and bookkeeping counters for atoms, charge, and radical parity.
Operations come in three kinds:
Two design choices matter. A Concerted bundle validates a group of edits atomically and checks valence once at the end, so forming one bond before breaking another no longer trips over a transiently over-valent carbon; the acylation case in the appendix is exactly this repair. And the boundary between natively checkable structure and externally witnessed measurement is explicit, backed by theorems for six assertion families.
Three inference interfaces share these semantics. One-pass submits a complete trace with no feedback. Refinement takes rejection feedback and rewrites the whole trace, up to eight times, each attempt restarting from the initial state. MolLean-MCP exposes transitions, checks, and readouts as stateful tools in the inference loop: the model inspects the current state, attempts an action, and a rejected call changes nothing.
Main evaluation: Qwen3.6-27B on 8,800 matched examples across 12 tasks, with nine S2-Bench tasks at 500 examples each, 500 forward and 500 retrosynthesis reactions from USPTO-50k, and the full 3,300-example ChEBI-20 test set.
| Task | CoT | One-pass | Refine | MCP |
| Atom counts | 42.0 | 61.4 | 88.8 | 82.6 |
| Add component | 55.8 | 93.6 | 100.0 | 100.0 |
| Forward reaction | 35.0 | 23.6 | 62.8 | 66.4 |
| Retrosynthesis | 3.0 | 11.6 | 20.8 | 27.4 |
| ChEBI-20 text to molecule | 18.1 | 25.3 | 33.1 | 23.5 |
Refinement beats direct CoT on all 12 tasks, with gains of 12.0 to 48.2 percentage points; paired 95% bootstrap intervals from 4,000 resamples exclude zero everywhere. The forward-reaction column carries the most information: One-pass scores 23.6, which is 11.4 points below bare CoT at 35.0. Writing a fully admissible trace in one shot is a heavy burden, and the paper's own reading is that feedback matters most when the initial plan misses the verifier's obligations. Eight rewriting rounds lift it to 62.8, with most of the gain arriving within two revisions (58.0 at k=2).
The second story: an accepted trace is not a correct answer. Retrosynthesis ends at 88.2% trace soundness against 20.8% accuracy; ChEBI-20 at 79.0% versus 33.1%, where 1,533 of 2,608 accepted traces give wrong answers. Between k=2 and k=8, ChEBI-20 acceptance climbs from 67.3% to 79.0% while accuracy moves only from 31.1% to 33.1%. Late revisions repair the obligations the model chose to state, not the task.
Qwen3-4B shows the same split at smaller scale. Structural tasks jump (atom counts 15.8 to 56.8, component addition 13.4 to 91.4), but retrosynthesis is 0.0% under every protocol and forward reaction lands at 1.6%. A verifier cannot rescue a proposer without the chemical knowledge to supply candidates, and the authors say so themselves.
The work swaps trained process verifiers for a deterministic checker: no annotation pipeline, no reward hacking. Teams doing molecular editing or counting-style tasks get near-ceiling numbers they can adopt directly, and the MCP design, where a refused call costs one call and leaves the state untouched, is a clean pattern for tool-use agents generally. Reporting trace soundness and answer accuracy separately is a measurement discipline worth copying. To be clear about the increment: Lean, RDKit, MCP, and tool-use all exist; the contribution is cutting evidence sources and commit semantics cleanly inside one vertical domain.
The authors' own list: acceptance does not imply task fidelity, and the hydrochloride case in the appendix has a revision drop the chloride and its count obligation, then get accepted while missing the salt; instruction-to-constraint grounding is named the next bottleneck; the 4B model collapses on reference-based tasks; MCP was not run on 4B because small models interact poorly.
Open questions from the reading. Many assertions use referents the model picked itself, since OutcomeMatch compares against the model's own SMILES, which comes close to a self-graded exam and matches the symptom of rising acceptance with flat accuracy. External witnesses are trusted by the protocol, which checks types, not truth. Only two Qwen models were tested, so the benefit of verification has not been shown outside one family. And on optimization tasks the headline gain range uses direction-only success; the similarity-weighted numbers are much lower in absolute terms (QED: 92.2% direction success against a weighted score of 59.0).