MolLean: A Process-Verifiable Language for Chemical Reasoning
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
| Task | 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 |
| 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] |
| Task | 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 |
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 |
| 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 |
| 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 |
| Sound | Not sound | ||||
|---|---|---|---|---|---|
| Task | Success | Failure | Success | Failure | |
| 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 |
| 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 |