MolLean: A "Type Checker" for Chemical Reasoning That Makes LLM Chemistry Verifiable
A Dangerous Hallucination
Ask a large language model to design a synthesis route: "Starting from ethanol, add a methyl group to get 1-propanol."
The model confidently replies: "Sure, first step, attach a methyl group to ethanol's hydroxyl group..."
Wait—a methyl group on the hydroxyl? That would give methyl ethyl ether (CH₃-O-CH₂CH₃), not 1-propanol (CH₃CH₂CH₂OH). The model got the attachment site wrong.
This is not a hypothetical scenario. The paper's authors analyzed many chemical reasoning chains and found that LLMs make three classes of errors:
1. Citing nonexistent functional groups — claiming a molecule has a carboxyl group when it doesn't 2. Losing track of bonds — modifying one site while forgetting what else is connected 3. Claiming property improvements without verification — saying "this modification improves solubility" without checking whether it actually does
These errors are nearly impossible to detect automatically in free-text reasoning. It's like writing code without a compiler—syntax errors and logic errors are mixed together, and you have no idea where things went wrong.
MolLean's solution: install a "type checker" for chemical reasoning.
What Is MolLean?
MolLean comes from Jiatong Li and Yatao Bian at the National University of Singapore, with the paper released on October 14, 2026. Its core idea: turn chemical reasoning from free text into executable, stateful programs.
If you've used Lean (an interactive theorem prover), MolLean's design will feel familiar. If not, think of it this way:
Imagine writing code. You define a variable x: int, then try to compute x + "hello". The compiler immediately errors—type mismatch. You don't need to run the code; the error is caught at compile time.
MolLean does the same thing, except "types" become molecular structures and "operations" become chemical transformations.
Three Core Designs
1. Explicit Molecular State
In MolLean, reasoning is not "writing a paragraph describing a reaction" but "executing a sequence of operations on molecular state."
The initial state S₀ = init(x)—for example, an empty molecule or a starting molecule. Each operation acts on the current state:
- Add a component: S₁ = add(S₀, "ethanol")
- Attach a methyl group: S₂ = attach(S₁, "methyl", "position-1")
- Count atoms: count(S₂, "carbon") → should return 3
- Full-trace refinement (Refine) beat direct CoT on all 12 tasks
- MolLean-MCP further improved reaction-type tasks
- Extending MolLean to biochemistry (proteins, nucleic acids)
- Combining RL to optimize reasoning that is "not just sound, but correct"
- Integrating experimental validation into a "computational verification → experimental verification" pipeline
If an operation is invalid—say, attaching a group at a nonexistent position—the Lean kernel rejects it, and the state remains unchanged.
It's like a Git commit—only changes that pass checks get "committed" to the molecular state.
2. Typed Witness Protocol
This is MolLean's most elegant design.
Chemistry has two kinds of verification:
Native structural checks: Are atom counts right? Is bond valence valid? Do functional groups actually exist? These can be judged purely by the Lean kernel, without external information. Like a compiler checking types—int + int is legal, int + string is not.
External measurement verification: Solubility, logP (lipophilicity), molecular weight, etc. These require external tools and cannot be judged by pure logic. MolLean handles them with "typed witnesses"—external tools return a typed proof, and the Lean kernel verifies that the proof's type matches.
The cleverness here: structural correctness is "free" (judged directly by the kernel), while property verification comes at a "cost" (calling external tools), but both are managed through the same verification framework.
It's like the relationship between TypeScript's type and runtime checks—type errors are caught by the compiler, runtime errors need asserts. MolLean unifies both in one framework.
3. MolLean-MCP: A Stateful Tool Interface
MolLean isn't just a language—it also has an interactive interface. The model can:
1. Propose an operation 2. Receive validation feedback (accepted or rejected) 3. If rejected, the state is unchanged and the model can retry
This is fundamentally different from traditional "one-shot generation." Traditional CoT writes the whole reasoning chain in one go; MolLean-MCP is "write a step, verify a step, fix it if wrong."
Rejected operations don't change the molecular state—like Git's staging area, where only code passing CI checks can merge into the main branch.
The Numbers: 12 Tasks, Comprehensive Gains
On 8,800 matched samples covering 12 tasks (molecule generation, editing, optimization, reactions), using Qwen3.6-27B as the base model:
Overall Results
Soundness—Is the Reasoning Chain Itself Correct?
| Task | One-pass | Refine | MCP | |------|----------|--------|-----| | Atom counting | 61.6% | 93.4% | 96.6% | | Bond counting | 52.8% | 84.8% | 90.4% | | Functional groups | 84.0% | 97.6% | 98.2% | | Component addition | 93.6% | 100.0% | 100.0% | | Forward reaction | 23.8% | 88.2% | 98.6% | | Retrosynthesis | — | — | 98.0% |
Forward-reaction soundness jumped from 23.8% to 98.6%—meaning about 76% of reasoning chains originally contained structural errors, and MolLean fixed nearly all of them.
A Key Distinction: Soundness ≠ Task Correctness
The paper's most profound finding: a reasoning chain can be fully sound (every step legal) while the final answer is still wrong.
On the ChEBI-20 dataset, refined reasoning chains reached 79.0% soundness, but answer accuracy was only 33.1%.
It's like code that compiles but has buggy logic—type checking catches syntax errors, not algorithmic errors.
The significance: it splits "chemical reasoning failures" into two classes—"execution errors" (the chain itself is flawed) and "task errors" (the chain is correct but the answer is wrong). MolLean fixes the former; the latter needs deeper improvements.
Small Models Benefit Too
MolLean isn't just for large models. Tested with Qwen3-4B (a 4B-parameter model), it delivered significant gains on structural tasks. This shows verifiable reasoning doesn't depend on model scale—even a small model makes fewer mistakes with a type checker.
Good news for resource-limited researchers: you don't need a 70B model; a 4B model plus MolLean can do chemical reasoning.
Relation to Other Work
MolLean sits at the intersection of several trends:
1. Formal verification + LLM: Using theorem provers like Lean/Coq to constrain LLM reasoning has been hot in mathematical reasoning (e.g., DeepSeek-Prover). MolLean extends this to chemistry. 2. Tool-augmented reasoning: MolLean-MCP is essentially a stateful tool interface, in the same lineage as ReAct and Toolformer, but with an added "state validation" layer. 3. Executable reasoning chains: Turning reasoning from "text descriptions" into "executable programs" resembles Program-aided Language Models (PAL), but MolLean's "programs" are chemical operations rather than Python code.
MolLean's unique contribution: it doesn't make LLMs write chemical equations—it makes them program in a typed chemical language. The former only checks the final answer; the latter checks every step.
Limitations and Outlook
The paper candidly discusses several limitations:
1. Task correctness remains the bottleneck: soundness improved, but answer accuracy has a long way to go 2. External tool dependence: property verification depends on the accuracy of external tools 3. Task scope: currently 12 tasks; more complex synthesis route planning is untested
Future directions may include:
Implications for the Industry
MolLean's significance goes beyond chemistry:
1. For agent engineering: the "stateful tool interface" pattern of MolLean-MCP can extend to other domains requiring verification—legal reasoning, financial analysis, engineering design 2. For AI safety: the Typed Witness Protocol offers a "layered verification" approach—structural correctness by the kernel, property correctness by external tools, both managed in one unified framework 3. For evaluation: the soundness vs. task-correctness distinction reminds us—when evaluating LLMs, don't just look at the final answer; check whether the reasoning process is legal
Core takeaway: When you turn an LLM's free-text reasoning into executable, stateful programs, you can verify every step. This doesn't make the LLM smarter—it makes the LLM's errors easier to detect and fix.
Just as compilers didn't make programmers smarter, but made programs more reliable.
---
Paper: https://arxiv.org/abs/2610.20459
HTML version: https://arxiv.org/html/2610.20459v1
Open-source code: https://github.com/phenixace/Open-MolLean