MolLean: A Process-Verifiable Language for Chemical Reasoning

AI summary

Overview

Research area: Natural language processing applied to AI-driven chemistry — specifically, making the intermediate reasoning steps of large language models (LLMs) formally checkable rather than free-form text.

Technical level: Intermediate. The paper assumes familiarity with chain-of-thought prompting and basic molecular representations (SMILES, molecular graphs), and it introduces Lean-based verification, but the core ideas are explained concretely enough for a reader with a general machine-learning background.

Scope (one sentence): The paper introduces MolLean, a Lean-backed language in which every chemical reasoning step is a declared operation on an explicit molecular state that is either accepted (committing a new state) or rejected (leaving the state unchanged), and evaluates whole-trace refinement and an interactive tool interface against direct chain-of-thought on 8,800 matched examples across 12 tasks.

What This Paper Is About

When a language model "thinks out loud" about chemistry, its intermediate steps can contain fabricated claims — invoking a functional group the molecule does not have, losing track of a bond, or asserting a property improved without establishing it. Existing chain-of-thought explanations are prose, so nothing forces those claims to correspond to a real structure.

The goal is a reasoning language in which chemical commitments are executable and checkable: each step refers to a maintained molecular state, a verifier decides whether the step is admissible, and only accepted steps change the state. The paper then asks whether generating and repairing such verified traces actually improves task performance over ordinary chain-of-thought.

Key Contributions

1. A state-grounded chemical reasoning language and verification contract. MolLean unifies molecular transitions (constructing, editing, or reorganizing molecules), readouts (observing the state without changing it), and assertions (testing a claim against a readout), with explicit boundaries between native structural checks decided inside Lean and claims that require externally supplied measurements.

2. Two feedback regimes sharing one execution semantics. MolLean Refinement rewrites a rejected complete trace from the initial state; MolLean-MCP is a stateful tool interface where the model inspects the current state, attempts an operation, receives immediate feedback, and only accepted edits commit.

3. An evaluation on 8,800 matched examples across 12 tasks. Every protocol is run on the same examples, spanning molecular generation, editing, optimization, forward reactions, retrosynthesis, and text-to-molecule generation, with trace soundness and answer correctness scored separately.

4. A demonstration that verification transfers to a smaller model. Qwen3-4B, evaluated with the whole-trace protocols on the same task IDs, gains substantially on structural tasks, though reference-based generation remains difficult for it.

Main Findings

• Refinement beats direct chain-of-thought on every task. With Qwen3.6-27B, whole-trace refinement (up to eight revisions) outperforms direct CoT on all 12 tasks, with gains of 12.0–48.2 percentage points under each task's binary success criterion. Atom counts improve by 46.8 points (42.0 to 88.8), bond counts by 48.2 (20.8 to 69.0), and component addition by 44.2 (55.8 to 100.0). Paired 95% bootstrap intervals (4,000 resamples) for Refine-minus-CoT exclude zero in every task.

• Even one-pass verified traces usually help. One-pass improves over CoT on 11 of 12 tasks. The exception is forward reaction prediction, where one-pass reaches 23.6% against CoT's 35.0% — but refinement then raises it to 62.8%, indicating feedback matters most when the initial plan misses the verifier's obligations.

• Repair outweighs damage. Using the shared one-pass completion for a paired comparison, forward prediction recovers 207 answers and loses 11; retrosynthesis recovers 48 and loses two; ChEBI-20 recovers 290 and loses 33, a net gain of 257 correct answers. Among initially unsuccessful answers, the recovered fraction is 54.2% for forward prediction, 10.9% for retrosynthesis, and 11.8% for ChEBI-20.

• Most gains arrive within two revisions. Forward-reaction accuracy rises from 23.6% at zero revisions to 58.0% at two and 62.8% at eight; component addition reaches 100.0% by two revisions. On retrosynthesis and ChEBI-20, later revisions keep raising acceptance (57.4% to 88.2%, and 67.3% to 79.0%) while accuracy moves much less (20.4% to 20.8%, and 31.1% to 33.1%).

• Soundness and correctness are different things. Refinement raises trace soundness over one-pass on all 12 tasks, and MCP matches or exceeds refinement on 10 of them, reaching 98.6% soundness on forward reactions and 98.0% on retrosynthesis. Yet retrosynthesis ends at 88.2% soundness with only 20.8% exact set-match accuracy, and ChEBI-20 at 79.0% soundness with 33.1% answer accuracy. A trace can execute the wrong objective correctly.

• Interactive verification wins on reactions. MCP achieves the best reaction results: 66.4% forward-reaction and 27.4% retrosynthesis accuracy versus 62.8% and 20.8% for refinement. Refinement instead leads on atom counts (88.8% versus 82.6%), bond counts (69.0% versus 56.2%), QED optimization (59.0 versus 49.4 similarity-weighted points), and ChEBI-20 (33.1% versus 23.5%); both reach 100.0% on component addition and 97.0% on component deletion.

• Where acceptance fails to imply success. On ChEBI-20, 1,075 outputs are both sound and correct, 1,533 are sound but incorrect, 17 are correct without certification, and 675 satisfy neither. Atom-count generation shows the opposite profile: 444 of 467 accepted traces meet the task criterion, compared with 1,075 of 2,608 on ChEBI-20 — a count maps directly to a predicate, whereas a textual description requires selecting and combining the right structural obligations.

• The smaller model gains mainly on structural tasks. Qwen3-4B refinement raises atom-count success from 15.8% to 56.8%, component addition from 13.4% to 91.4%, substitution from 15.2% to 53.4%, and the logP optimization score from 14.7 to 60.0. Reference-based generation stays hard: forward-reaction accuracy 1.6% after refinement (one-pass 2.2%), ChEBI-20 1.4%, and retrosynthesis 0.0% under every protocol.

• Case studies expose specification gaps, not just execution errors. A one-pass edit lowering QED from 0.674 to 0.573 passes the graph edits but fails the property assertion; refinement reaches QED 0.767 with success-weighted similarity 0.743. A valid 27-carbon chain fails an atom-count check requesting 25. A salt proposal that fails the disconnected-proposal check is "repaired" by omitting chloride — producing an accepted but incorrect cation, showing that revision requires a specification that still expresses what the user asked for.

Methodology in Plain English

The design borrows an idea from formal mathematics: in Lean, a model proposes a derivation and a proof assistant checks its obligations, keeping proof construction separate from proof checking. MolLean does the same for chemistry.

Execution starts from an initial state built from the task input, holding active molecules, a "leaving pool" of discarded fragments, atom references, and bookkeeping counters. Molecules are graphs labelled with elements, bonds, charges, radicals, and aromaticity. Seven primitive operations add or remove atoms, form or break bonds, and update bond order, charge, or radicals, checking preconditions and affected valences. Higher-level construction macros (Chain, Ring, AttachGroup) and compound actions (joint bond changes, proton transfer, fragment separation) reduce index bookkeeping, and named reactions expand into these operations.

Each declared operation is sent to the Lean kernel. If it passes its checks the successor state is committed along with an observation or verdict; if it fails, a rejection reason is returned and the previous state remains current — so a rejected edit can never corrupt a later step. Readouts observe the state without changing it, and assertions constrain readouts. Seven structural families are checked natively (atom counts, bond counts, ring counts, molecular formula, aromaticity, built-in functional-group patterns, and retained R/S stereocenters). Descriptor- and knowledge-dependent claims go through a typed witness protocol: Lean issues a typed request, an external provider (for example RDKit, which supplies descriptors, fingerprints, and comparisons) returns typed fields, and Lean applies its predicate to those fields. This keeps "computed from the structure" and "measured by a tool" visibly distinct.

Three inference interfaces sit on this kernel. One-pass submits a complete trace. Refinement starts from that same completion, returns rejection feedback with the failing step and indexed state, and asks for a corrected full trace, restarting each attempt from the initial state within a fixed budget. MolLean-MCP exposes transitions, checks, and readouts as stateful function-calling tools so the model can inspect the state before acting, with rejected proposals leaving the state unchanged.

Evaluation is deliberately strict: all protocols run on the same examples — 500 each for nine S2-Bench tasks, 500 forward and 500 retrosynthesis examples from USPTO-50k, and the full 3,300-example ChEBI-20 test set. Invalid answers and unsuccessful episodes stay in the denominator. Dataset references are used only by an independent scorer, never by the verifier, and process soundness is reported next to answer correctness so the two cannot be conflated.

Why This Matters

Impact on research. The paper reframes chemical chain-of-thought as a process that can be audited rather than a narrative that can only be read. By separating process soundness from task fidelity and answer correctness, it gives the field a vocabulary for a failure mode that accuracy numbers hide: a trace can be internally valid and still solve the wrong problem. It also provides an executable counterpart to prior findings that fluent chemical reasoning can contain fabricated structural claims even alongside correct answers.

Real-world applications:

• Drug discovery and molecular design. Optimization tasks (logP, MR, QED) require edits that provably move a property in the requested direction; witness-checked property assertions make such claims auditable before chemists act on them.
• Synthetic route planning. Reaction and retrosynthesis tasks, where MCP reached the best accuracy, mirror the stepwise, state-dependent nature of planning a synthesis where each operation must be valid given what exists at that moment.
• Cheminformatics pipelines and tool-using agents. MolLean-MCP shows how to wrap existing tools (such as RDKit) in a contract where outputs are typed, requests are explicit, and only verified results commit.
• Auditing and reviewing model-generated chemistry. Accepted traces provide an inspectable record of exactly which operations and obligations were checked, which is useful for review, debugging, and safety triage.

Industry relevance. Teams deploying LLM agents in chemistry need reliability guarantees that raw accuracy does not supply. The paper's architecture — verifier kernel, external witnesses, and two feedback regimes over a shared semantics — is a template for constrained generation in regulated or high-stakes scientific domains, and the finding that a 4B model gains substantially on structural tasks suggests the approach is not limited to frontier-scale models.

Future Directions

• Grounding instructions in explicit constraints. The authors identify instruction-to-constraint grounding as the main lever for further gains, since tasks like ChEBI-20 reach high trace soundness yet modest answer accuracy. The salt case study, where revision silently dropped a required component, makes the problem concrete.
• Combining interactive and whole-trace feedback. Refinement and MCP win on different task families — plan-level revision on counts and optimization, stepwise feedback on reactions. How to choose or interleave the two regimes per task is left open.
• Extending witness coverage. The current split between native Lean predicates and externally witnessed claims covers seven structural families plus RDKit descriptors; richer chemical knowledge providers and more task-relevant obligations are a natural extension.
• Stronger candidate generators for the small-model regime. Reference-based generation stays near zero for Qwen3-4B even after refinement, indicating verification is most effective when paired with a capable proposer — raising the question of how verification quality and proposal quality interact.

Target Audience

Researchers working on LLM reasoning, chain-of-thought faithfulness, and process supervision; AI-for-chemistry and cheminformatics practitioners building tool-using agents; and anyone interested in borrowing formal-verification ideas from Lean for scientific domains. It is also relevant to evaluation specialists, because its separation of soundness, task fidelity, and answer correctness offers a reusable framework for judging reasoning traces rather than just final answers.

Authors’ abstract

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.