PaperlayerView exact revision on arXiv

Source-linked AI summary

MolLean: A Process-Verifiable Language for Chemical Reasoning

Jiatong Li, Yatao Bian

arXiv:2610.20459v1cs.CLcs.CEcs.PL

TL;DR

Chemical chain-of-thought can contain unsupported structural and property claims. MolLean grounds reasoning in a maintained molecular state and checks proposed operations and assertions; with Qwen3.6-27B, whole-trace refinement outperforms direct chain-of-thought across all 12 tasks, while MCP has the strongest reaction results.

  • Problem

    Chemical chain-of-thought can contain fabricated structural or property claims, including alongside correct answers.

    Source: §1 · p. 1

  • Method

    MolLean grounds operations and assertions in a maintained molecular state, and MolLean-MCP exposes checks and readouts during generation for stepwise feedback.

    Source: §1 · pp. 1–2

  • Results

    With Qwen3.6-27B, refinement improves over direct chain-of-thought on all 12 tasks, and MCP achieves the highest reaction accuracy.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Explicit molecular commitments can be checked and revised, with whole-trace refinement improving performance across the evaluated tasks and MCP delivering the strongest reaction results.

    Source: §6 · p. 10

    For Qwen3-4B, reference-based generation remains difficult, and verification is most effective when paired with a capable candidate generator.

    Source: §3.5 · p. 8

Abstract

from arXiv · show

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.

1 Introduction

MolLean grounds chemical reasoning in a maintained molecular state so that proposed operations and claims can be checked against explicit referents. Across 12 tasks, refinement improves over direct chain-of-thought, while interactive feedback delivers the strongest reaction results.

1 Introduction

  • Chemical reasoning can include fabricated structural claims or property improvements, even alongside correct answers.These errors concern the stated chemistry itself and are distinct from explanations that misrepresent how an answer was produced.Source: §1 · p. 1
  • MolLean represents transitions, readouts, and assertions against a shared molecular state, with Lean checking admissible transitions and native structural predicates.Descriptor- and knowledge-dependent assertions instead obtain typed witnesses from external providers.Source: §1 · pp. 1–2
  • Accepted edits establish the referent for later checks, while rejected edits leave the maintained state intact.The state determines which atoms later edits address and which molecule a property readout measures.Source: §1 · p. 2
  • Whole-trace refinement revises rejected traces from the input, while MolLean-MCP uses immediate feedback as the model chooses its next action.Both interfaces use the same language and specify what feedback refers to and when a change commits.Source: §1 · p. 2
  • With Qwen3.6-27B, refinement improves over direct chain-of-thought on all 12 tasks; MCP achieves the highest reaction accuracy.On ChEBI-20, refined traces reach 79.0% soundness and 33.1% answer accuracy, identifying task fidelity as a remaining challenge.Source: §1 · p. 2

2 MolLean

MolLean represents chemistry as operations on a maintained molecular state, with checks determining which transitions commit. Its language covers edits, observations, and assertions, while whole-trace and interactive interfaces provide different ways to execute and revise reasoning.

2 MolLean

  • MolLean operations refer to the current molecular state; verification decides admissibility, and only accepted transitions commit a new state.Lean implements the chemical core, while Python handles parsing, state transport, reference resolution, and inference control.Source: §2 · p. 2

2.1 A Language Grounded in Molecular State

  • Execution starts from an initialized state containing active molecules, a leaving pool, atom references, and bookkeeping counters; readouts observe that state without changing it.Assertions constrain readouts, while transitions include edits, construction, candidate introduction, and fragment separation.Source: §2.1 · p. 2

2.2 State Transitions at Different Granularities

  • Primitive edits check preconditions and affected valences, while construction macros, compound actions, and named reactions offer higher-granularity transformations.Concerted bundles apply edits atomically and check resulting valences after the edits apply; terminal checks cover valence, connectivity, aromaticity, and closed-shell rules.Source: §2.2 · p. 3

2.3 State Readouts and External Witnesses

  • Native readouts cover structural families such as atom and bond counts, formula, aromaticity, functional groups, and retained stereocenter annotations; external providers supply descriptors and knowledge-dependent information.A typed witness separates requesting provider evidence from Lean’s application of a predicate to that response.Source: §2.3 · pp. 3–4

2.4 Process Soundness and Task Fidelity

  • Process soundness requires all declared trace operations to be accepted and closing obligations to hold, while task fidelity asks whether the representation and obligations capture the instruction.Answer correctness is independently scored, so the paper reports process soundness and task scores separately.Source: §2.4 · p. 4

2.5 Whole-Trace and Interactive Inference

  • One-pass submits a complete trace, refinement revises a rejected trace from the initial state, and MCP lets the model inspect state and choose operations interactively.MCP rejected proposals leave the state unchanged, and finish invokes closing gates; dataset references are reserved for the independent scorer.Source: §2.5 · p. 4

3 Experiments

Across 12 tasks, whole-trace refinement improves over direct chain-of-thought, while interactive verification performs best on reaction tasks. The experiments also distinguish accepted traces from correct answers and test whole-trace refinement with a smaller model.

3. Experiments

  • The evaluation compares Direct CoT, One-pass, Refinement, and MCP on matched examples, using task-specific success metrics and trace soundness.The main comparison uses Qwen3.6-27B and includes 8,800 examples across 12 task types.Source: §3 · p. 4, §3.1 · p. 5

3.2 Whole-Trace Refinement Improves Task Performance

  • Refinement improves over Direct CoT on all 12 task types, with gains of 12.0–48.2 percentage points under each task’s binary success criterion.For optimization, the reported range uses direction-only success; similarity-weighted scores show the same gains.Source: §3.2 · p. 5, Table 1 · p. 5
  • Most refinement gains arrive within two revisions, though acceptance can continue rising with little accuracy change on reference-based tasks.Forward-reaction accuracy rises from 23.6% at k = 0 to 58.0% at k = 2 and 62.8% at k = 8; retrosynthesis accuracy moves from 20.4% to 20.8% between k = 2 and k = 8.Source: §3.2 · p. 6, Figure 3 · p. 7

3.3 Soundness Separates Execution from Task Fidelity

  • Refinement raises soundness over One-pass on all 12 tasks, but accepted traces do not always yield correct answers, especially when instructions are incompletely grounded in constraints.On ChEBI-20, 1,533 outputs are sound but incorrect, while 1,075 are both sound and correct; atom-count generation has 444 correct outputs among 467 accepted traces.Source: §3.3 · pp. 6–7, Table 2 · p. 7, Figure 3 · p. 7

3.4 Interactive Verification Strengthens Reaction Prediction

  • MCP achieves the best reaction results, with 66.4% forward-reaction and 27.4% retrosynthesis accuracy, versus 62.8% and 20.8% for Refinement.Refinement leads on several structural and optimization tasks, while both protocols reach 100.0% on component addition and 97.0% on component deletion.Source: Figure 2 · p. 6, §3.4 · pp. 7–8

3.5 Whole-Trace Inference with Qwen3-4B

  • With Qwen3-4B, refinement improves several structural-task scores over Direct CoT, but reference-based generation remains difficult.For example, atom-count success rises from 15.8% to 56.8%, while retrosynthesis remains at 0.0% under every protocol.Source: §3.5 · p. 8, Table 3 · p. 8

4 Case Studies: Repairs and Specification Gaps

The cases show how verification can reject invalid operations or candidates that miss requested properties, and how revision can repair them. They also show that an accepted trace may still fail when its revised description omits a required component.

Valence and attachment sites

  • A carbonate edit is rejected when its sequential operations create carbon valence five; a joint bond-change operation repairs it.For aldehyde addition, changing the attachment site from aromatic carbon 10 to carbon 11 makes the revised trace pass its checks.Source: §4 · p. 8, Figure 4 · p. 9

Measured properties and explicit counts

  • A valid candidate can fail the requested property check: refinement raises QED from 0.573 to 0.767 and changes a 27-carbon chain to the requested 25-carbon chain.RDKit supplies the QED measurement, while atom count is checked natively from the graph.Source: §4 · p. 8, Figure 4 · p. 9

Interactive recovery and incomplete specifications

  • MCP repairs a refused attachment without changing state, but a revised salt description omits chloride and its count obligation, yielding an accepted but incorrect cation.The MCP episode finishes correctly after four counted calls, including the refusal.Source: §4 · p. 9, Figure 4 · p. 9

5 Related Work

Related work spans language and molecular representations, executable and formal reasoning, and feedback-driven tool use. MolLean is positioned among these approaches as a language for checking chemical commitments against molecular state.

5 Related Work

  • Chemical-language work ranges from text–molecule retrieval and translation to instruction-driven tasks, while SELFIES targets string validity and structural reasoning targets molecular understanding.ChemBench evaluates chemical knowledge and reasoning more broadly.Source: §5 · p. 9
  • XDL expresses synthesis procedures for compilation into laboratory instructions, providing an executable chemical-language example distinct from MolLean’s reasoning focus.The passage identifies XDL as an executable chemical language.Source: §5 · p. 10
  • Formal approaches make different parts of reasoning checkable, including proof checking, learned process evaluation, and execution-grounded computation.The passage contrasts Lean-based proof checking with learned verification and executable programs.Source: §5 · p. 10
  • Tool-use approaches ground feedback in external tools or interleaved actions, with chemistry systems applying tools to planning, automation, and catalyst search.The cited examples include CRITIC, ReAct, ChemCrow, Coscientist, and ChemReasoner.Source: §5 · p. 10

6 Conclusion

MolLean grounds chemical reasoning in a maintained molecular state, combining Lean-checked obligations with explicit external witnesses. Whole-trace refinement improves performance across 12 tasks, while MolLean-MCP delivers the strongest reaction results.

6 Conclusion

  • Whole-trace refinement improves Qwen3.6-27B performance across all 12 tasks, while MolLean-MCP delivers the strongest reaction results.Source: §6 · p. 10
  • MolLean grounds chemical reasoning in a maintained molecular state, combining Lean-checked obligations with explicit external witnesses.Source: §6 · p. 10
  • Qwen3-4B gains substantially on structural tasks, and grounding instructions in explicit constraints is presented as the next step toward verifiable, task-faithful chemical reasoning.Source: §6 · p. 10

A Implementation Details

This section describes MolLean’s implementation, including its Lean–Python orchestration, typed external evidence, molecular-state and reference management, and prompts for whole-trace and stateful MCP interaction. It also presents the shared vocabulary for verified operations and assertions, with worked examples showing verifier feedback guiding trace revision.

A Implementation Details

  • Lean proves native molecular assertions over the returned proof-carrying object, while external providers supply evidence for checks without native definitions.Native assertion-boundary proofs cover AtomCount, BondCount, RingCount, HasAromatic, FGCount, and FormulaMatch; hydrogen counts include graph and implicit hydrogens, and formula matching rejects duplicate element entries.Source: A Implementation Details · p. 13

A.1 Represented State and Reference Resolution

  • MultiMolState tracks active molecules, a leaving pool, step count, and initial atom and charge bookkeeping, with indexed molecular graphs and references.Virtual hydrogens contribute to element and formula readouts, while the leaving pool is excluded from the answer but remains in the atom-count ledger; reference remapping differs across whole-trace execution, compound bundles, and MCP feedback.Source: §A.1 · p. 13

A.2 Action Dispatch and Commit Semantics

  • The runtime translates model calls into shared step representations and updates maintained state only after Lean accepts an action.Rejections return structured errors and leave state unchanged; primitive edits check preconditions and affected valences, concerted bundles validate joint outcomes, and closing checks charge, radical bookkeeping, and task-dependent terminal obligations.Source: §A.2 · p. 14

A.3 A Concrete Typed Witness

  • Lean counts represented atoms itself for native AtomCount, while PropertyChange(qed) requests RDKit measurements of current and bound initial molecules, requiring computable=1 and comparing out x1000 with in x1000 in the requested direction.Source: §A.3 · p. 14

B.1 Direct CoT and Whole-Trace Generation

  • Direct CoT receives no verifier state or feedback, whereas One-pass and Refinement share a prompt for generating a typed whole trace before sequential execution.The whole-trace prompt’s claim that each step is checked describes execution after the model generates the complete trace, not stepwise feedback during generation.Source: §B.1 · p. 15

B.2 Whole-Trace Revision Feedback

  • After rejection, Refinement receives the first failed step, its error, and the state at failure, then is asked for a corrected complete trace executed from the original input.Feedback can include the live atom map, but contains no correctness score or held-out target; an unparseable later revision stops refinement at the last parseable outcome.Source: §B.2 · p. 16

B.3 Stateful MCP Prompt and Schemas

  • MCP maintains molecular state across function calls and appends verifier responses to later turns; rejected edits leave the state unchanged.Schemas distinguish action arguments from measured evidence, and descriptor values come from a provider; atom indices are taken from the kernel’s latest reply.Source: §B.3 · pp. 16–17

B.4 Shared Whole-Trace Vocabulary

  • The shared whole-trace vocabulary distinguishes proposing whole molecules for synthesis from proposing fragments for transformations, which are attached and must end as one molecule.Task setup and runtime checks determine applicable proposals and closing conditions; the implementation allocates new atom indices after the largest current index.Source: §B.4 · pp. 17–18
  • Compound operations apply mechanism-level changes to groups of atoms or bonds, desugar to verified primitives, and check conservation across the whole step.The vocabulary includes concerted bond formation and cleavage; because the state addresses only heavy atoms, proton shifts require adding and bonding an explicit hydrogen first.Source: §B.4 · pp. 18–19
  • Macro operations compactly build chains, rings, and attached groups while expanding to individually verified primitives and avoiding atom-index bookkeeping errors.Chain and ring indices follow the next free indices, and ring construction closes the loop.Source: §B.4 · p. 19
  • The vocabulary supports assertions about atom, bond, and ring counts, functional groups, names, property changes, and outcomes, with stereocenter claims limited to untouched centers.The stereochemistry rule is conservative: edits at a center drop its annotation, so only centers not touched by edits should be claimed.Source: §B.4 · pp. 19–20

C Worked Examples

  • The eight worked examples show submitted operations, verifier feedback, and saved outcomes, including multi-molecule retrosynthesis and a native functional-group assertion.Whole-trace listings retain unexecuted steps after a rejection, while MCP listings retain function calls and verifier replies; free-form deliberation is omitted.Source: C Worked Examples · p. 20

C.1 Acylation: Changing the Verification Unit

  • The corrected acylation trace uses BondFormBreak to form and cleave bonds together, then removes chlorine; all three steps are accepted and the final product is correct.The initial separate bond-formation edit was rejected because it would give the acyl carbon effective valence x2 of 10, above the allowed 8; later steps were not executed.Source: §C.1 · pp. 20–21

C.2 QED Optimization: A Valid Edit Can Move the Wrong Way

These examples show that MolLean checks whether accepted edits satisfy the task’s stated obligations, and that refinement can repair a failed property check or attachment. They also expose a boundary: a trace can be accepted after dropping a requirement and still produce the wrong task answer.

C.2 QED Optimization: A Valid Edit Can Move the Wrong Way

  • QED fell from 0.674 to 0.573 after accepted edits, then refinement reached approximately 0.767.The initial property assertion was rejected; the revision removed chlorine and attached hydroxyl.Source: §C.2 · p. 22

C.3 Aldehyde Attachment: Repairing the Referent

  • The aldehyde attachment at atom 10 was rejected; moving the AttachGroup anchor to atom 11 let the group-count and input-similarity assertions pass.The repair changed the molecular referent.Source: §C.3 · p. 23

C.4 MCP Phenyl Attachment: Continuing After a Refusal

  • One of four counted MCP calls was refused, yet the final answer was correct; the model then attached phenyl at nitrogen 1 and passed two checks.The first attachment attempt targeted carbon 5; the later checks tested benzene-ring count increase and input similarity.Source: §C.4 · p. 25

C.5 Atom Count: The Count Obligation Guides the Correction

  • A graph-valid 27-carbon chain failed the requested count of 25; refinement proposed a 25-carbon chain and passed the native AtomCount check.No external measurement was needed for the rejection or repair.Source: §C.5 · p. 26

C.6 Hydrochloride Description: Acceptance After Dropping a Requirement

  • The initial hydrochloride proposal was rejected, but revision dropped both chloride and its count obligation, yielding an accepted molecule that missed the required salt.The self-proposed OutcomeMatch could not recover the omitted requirement, exposing a specification gap.Source: §C.6 · pp. 27–28

C.7 Retrosynthesis: The Answer Is the Full Active Set

  • Retrosynthesis retained both fragments after cutting the amide bond, then formed a carboxylic-acid precursor; the saved acid and aniline-derivative reactant set was correct.Reaction scoring compares the complete active set, unlike an OutcomeMatch assertion referring only to molecule 0.Source: §C.7 · p. 28

D.1 Task Setup and Scoring

The evaluation defines task-specific initialization and scoring, then compares direct CoT with MolLean protocols under specified inference budgets. Whole-trace refinement is also examined across revision budgets, retaining accepted traces as the budget increases.

D.1 Task Setup and Scoring

  • Tasks initialize from an empty state, input molecule, reactants, or product; non-reaction tasks score the first active molecule, while reactions score the full active set.ChEBI-20 uses its supplied test split; USPTO evaluation uses 500 examples per direction, with forward and reverse versions kept on the same side.Source: §D.1 · p. 29

D.2 Inference Settings

  • Refinement allows up to eight revisions; MCP allows two attempts and 30 counted action/check calls per attempt, with measure, show state, and finish excluded.Refinement uses a 32,768-token context; MCP uses 65,536 tokens and 4,096 output tokens per call.Source: §D.2 · pp. 29–30

E.1 Whole-Trace Refinement Across Budgets

  • Across revision budgets, accepted traces are retained, unsuccessful examples remain in each task denominator, and stopping uses verifier feedback alone.Figure 3 reports accepted-trace rate and answer score after at most k revisions, with k = 0 denoting the shared One-pass completion.Source: §E.1 · p. 30

E.2 Interaction-Length Distribution in MolLean-MCP

Selected MCP attempts are usually short, though interaction length varies by task and some generation tasks have long tails. The accompanying analyses distinguish trace certification from task success and describe paired outcomes between One-pass and refinement.

E.2 Interaction-Length Distribution in MolLean-MCP

  • Median MCP calls range from three for addition, deletion, logP, MR, and QED to six for ChEBI-20; QED and atom-count generation have appreciable mass beyond ten calls.Reaction medians are four for forward prediction and five for retrosynthesis; ChEBI-20’s interquartile range is four to ten calls. Figure 5 bins counted calls and separates accepted from unaccepted episodes.Source: §E.2 · p. 30, Figure 5 · p. 31

E.3 Certification and Statistical Uncertainty

  • Table 2 reports trace acceptance and paired 95% bootstrap intervals for primary Refine-minus-CoT scores, using 4,000 paired resamples per task.The intervals describe variation across examples conditional on model outputs.Source: §E.3 · p. 32

E.4 Joint and Paired Outcomes

  • Table 7 separates Refinement acceptance from binary task success, while Table 8 groups paired One-pass-to-Refinement outcomes into recovered, lost, and unchanged statuses.Optimization success in Table 7 means improvement in the requested property direction; each Table 8 row sums to N.Source: §E.4 · p. 32, Table 7 · p. 32, Table 8 · p. 32

E.5 Qwen3-4B Whole-Trace Results

The smaller-model evaluation uses the same task IDs and whole-trace evaluation structure, but does not include MCP experiments.

E.5 Qwen3-4B Whole-Trace Results

  • Qwen3-4B is evaluated with CoT, One-pass, and Refinement; MCP is omitted because 4B models have relatively poor interactive capability.The evaluation uses the same task IDs and whole-trace structure.Source: §E.5 · p. 33

Related papers

Loading 2610.20459v1…