MolLean: A Process-Verifiable Language for Chemical Reasoning

Jiatong Li; Yatao Bian

cs.CLOct 14, 2026

MolLean: A Process-Verifiable Language for Chemical Reasoning

Authors: Jiatong Li, Yatao Bian

Organizations: National University of Singapore

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.

Figures & tables

Figure 1: MolLean’s language, execution contract, and inference interfaces. (a) The state, transition families, and read-only queries; native predicates are decided in Lean, while witnessed claims apply a Lean predicate to a typed provider response. (b) The adapter holds

S_{0}=\operatorname{init}(x)

, sends each operation to the Lean kernel, and commits only accepted successors; witness requests and responses pass through the adapter. In the example, generation starts empty, admits ethanol as

S_{1}

, and attaches methyl to obtain 1-propanol as

S_{2}

; a false carbon count is rejected and

S_{2}

is unchanged. (c) One-pass executes one trace; refinement rewrites a rejected trace from

S_{0}

; MCP continues from the current state. Dataset references are used only by an independent scorer.

Task	$N$	CoT	One-pass	Refine	MCP
Atom counts	500	42.0	61.4	88.8	82.6
Bond counts	500	20.8	39.8	69.0	56.2
Functional groups	500	25.6	38.8	41.8	37.2
Add component	500	55.8	93.6	100.0	100.0
Delete component	500	85.0	94.6	97.0	97.0
Substitute component	500	81.0	94.2	96.0	95.4

Table 1: Qwen3.6-27B task performance on matched examples. Refine permits eight whole-trace revisions; MCP uses interactive verification. Bold marks the highest score.

\dagger

denotes

100\times

success-weighted similarity.

Figure 2: Repair, specification gaps, and interactive verification. (a) Refine recovers more One-pass failures than it loses successes, as fractions of each task’s examples. (b) Joint Refine outcomes separate accepted traces from correct answers. (c) MCP-minus-Refine primary-score differences show task-dependent benefits. Optimization appears below the dashed line: (a,b) use direction-only success, while (c) uses similarity-weighted score points. Other task differences are percentage points.

Figure 3: Whole-trace refinement across revision budgets for all 12 tasks. Each panel uses the complete Qwen3.6-27B task cohort (

N=500

; ChEBI-20

N=3{,}300

). Solid curves show trace acceptance and dashed curves the primary answer score;

\dagger

marks

100\times

success-weighted similarity.

k=0

is One-pass and

k=8

is the Refine column of Table 1 .

	Soundness (%)			Refine $-$ CoT
Task	One-pass	Refine	MCP	95% interval
Atom counts	61.6	93.4	96.6	[42.2, 51.6]
Bond counts	52.8	84.8	90.4	[43.8, 52.8]
Functional groups	84.0	97.6	98.2	[12.8, 19.6]
Add component	93.6	100.0	100.0	[39.6, 48.6]
Delete component	85.2	99.8	98.8	[8.8, 15.2]

Table 2: Qwen3.6-27B trace soundness and uncertainty. Soundness is the percentage of examples with an accepted trace (Equation 3 ); intervals are paired 95% bootstrap intervals (4,000 resamples) for the primary Refine-minus-CoT score.

Task	$N$	CoT	One-pass	Refine
Atom counts	500	15.8	39.6	56.8
Bond counts	500	9.6	13.4	22.4
Functional groups	500	11.8	12.2	16.6
Add component	500	13.4	41.2	91.4
Delete component	500	59.0	56.4	64.2
Substitute component	500	15.2	21.6	53.4

Table 3: Qwen3-4B task performance. The tasks and example IDs match the main evaluation.

\dagger

denotes

100\times

success-weighted similarity; other scores are success percentages.

Figure 4: Molecular cases of repair and incomplete specification. (a,c) Refinement changes action granularity or the attachment site. (b,e) A property or count assertion rejects an otherwise valid candidate. (d) MCP repairs an edit within the same maintained state. (f) A revised salt description drops a required component, giving an accepted but incorrect answer. Molecular drawings use the saved structures; numbers in (c,d) denote input atom indices. Refinement restarts from the task input, whereas MCP continues within its episode.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Component	Implemented check	Execution semantics
Molecule validator	Proved valence and connectivity soundness; conditional aromaticity	Validation of represented molecular graphs
Native assertions	Graph predicates; six assertion-boundary theorems	Checks on explicitly stated obligations
Edits and bundles	Preconditions, valences, bundle outcomes	Atomic validation of a concerted bundle’s outcome
Bookkeeping	Atoms, charge, radical parity across both pools	Additions and removals update the ledger
External witnesses	Typed request and predicate on returned fields	Provider and witness binding trusted
Python orchestration	Parsing, reference translation, serialization, control flow	State transport and inference control

Appendix

Table 4: Verification components and execution semantics.

Family	Supplied input	Requested construction and checks
Atom, bond, and group generation	Natural-language specification; empty state	Construct or propose; assert requested counts
Add, delete, and substitute	Input SMILES and indexed atom/bond map	Edit in place; group-count change and input similarity
logP, MR, and QED optimization	Input molecule and requested direction	Property-changing edits; direction and input similarity
Forward reaction	Reactants, reaction class, and atom maps	Transform loaded reactants; check proposed outcome
Retrosynthesis	Product, reaction class, and atom map	Disconnect and modify fragments; check proposed outcome
Text to molecule	Molecular description; empty state	Propose or construct; assert explicit structural requirements

Appendix

Table 5: Task-specific prompt content. All whole-trace templates append the same operator vocabulary. Reference structures for editing and optimization are the input molecule, not a held-out answer.

Objective	CoT	One-pass	Refine	MCP
logP optimization	59.8	95.8	99.8	99.4
MR optimization	60.6	93.2	99.8	99.6
QED optimization	54.2	65.6	92.2	77.0

Appendix

Table 6: Qwen3.6-27B optimization direction success (%). Each task contains 500 examples; input similarity is not included in this table.

Figure 5: Distribution of counted MCP action/check calls in the selected attempt. Bars sum to 100% within each complete task cohort, including unaccepted and no-result examples. Colors separate accepted from unaccepted episodes. Each panel reports its median. Bins span zero, 1–5, 6–10, 11–15, 16–20, 21–25, and 26–30 calls. Counts exclude measure , show_state , and finish , as well as earlier attempts.

Task	$N$	Success	Failure	Success	Failure
		Sound		Not sound
Atom counts	500	444	23	0	33
Bond counts	500	345	79	0	76
Functional groups	500	209	279	0	12
Add component	500	500	0	0	0
Delete component	500	485	14	0	1

Appendix

Table 7: Joint outcomes for Qwen3.6-27B Refinement.

Task	Both succeed	Recovered	Lost	Both fail
Atom counts	307	137	0	56
Bond counts	199	146	0	155
Functional groups	194	15	0	291
Add component	468	32	0	0
Delete component	472	13	1	14
Substitute component	471	9	0	20

Appendix

Table 8: One-pass to Refinement transitions for Qwen3.6-27B. Each row sums to

N

; categories use binary task success.

Chemical Reasoning in LLMs

See all 13 papers

From Answers to States: Verifiable Process-Level Evaluation of Chemical Reasoning in Large Language Models
Jun 2, 2026Hongyu Guo, Hao Li, He Cao +2LLM Evaluation Chemical Reasoning in LLMs
Peking University, Shenzhen Graduate School · International Digital Economy Academy (IDEA)
Chemical Chain-of-Thought Functions as a Hallucination-Prone Molecular Scratchpad
Jul 23, 2026Jiatong Li, Yuxuan Ren, Weida Wang +2CoT Faithfulness Chemical Reasoning in LLMs
Blue Whale Lab, National University of Singapore · Fudan University · Hong Kong Polytechnic University
Localize, Then Reason: Visual Latent Structural Reasoning for Molecular Properties and Edits
Aug 13, 2026Xingqiao Lin, Junmei Wang, Haocheng TangLatent Visual Reasoning Structured Reasoning
Department of Chemical Engineering, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, United States · Department of Pharmaceutical Sciences and Computational Chemical Genomics Screening Center, School of Pharmacy, University of Pittsburgh, Pittsburgh, PA, USA · Khoury College of Computer Science, Northeastern University, Boston, MA, USA

Jun 2, 2026J/K move · Enter open · S save

From Answers to States: Verifiable Process-Level Evaluation of Chemical Reasoning in Large Language Models

Hongyu Guo, Hao Li, He Cao, Gongbo Zhang+1

Peking University, Shenzhen Graduate School · International Digital Economy Academy (IDEA)

LLM Evaluation Chemical Reasoning in LLMs Chemical Reaction Prediction LLM Reasoning

Open paper AskPDF arXiv

Large language models are increasingly used as chemistry assistants, yet most chemistry benchmarks still score only final answers. This masks a critical failure mode: a model may output the correct molecule, product, or option while its reasoning violates chemical logic. Existing process-level evaluators are hard to scale because LLM judges and human step-level process annotation are costly, inconsistent, and vulnerable to hallucination. We introduce ChemCoTBench-V2, a rule-verifiable diagnostic benchmark for low-cost, auditable evaluation of structured, verifier-addressable chemical reasoning traces. It spans molecular understanding, molecule editing, molecular optimization, and reaction prediction, with 5,620 evaluation samples across 18 reporting tasks. Models must expose key intermediate steps in expert-designed templates, and those steps are checked with deterministic chemistry rules and, for closed-answer tasks, reference traces rather than another LLM judge. Open-ended molecular optimization is evaluated with oracle-verifiable state constraints rather than strict trace matching. The benchmark reports three separate signals: final-answer correctness, template adherence, and step-wise verifier correctness over expert-refined intermediate commitments. Experiments on frontier models reveal a persistent gap between final-answer success and structured-reasoning-state consistency: models often follow the requested format while failing chemical-step checks, or answer correctly with weak supporting reasoning. ChemCoTBench-V2 enables fine-grained model comparison and identifies the concrete step at which the trace first violates the verifier.

Abstract

Chemical Reasoning in LLMs

Explore similar work

From Answers to States: Verifiable Process-Level Evaluation of Chemical Reasoning in Large Language Models

Chemical Chain-of-Thought Functions as a Hallucination-Prone Molecular Scratchpad

Localize, Then Reason: Visual Latent Structural Reasoning for Molecular Properties and Edits