MolLean：面向化学推理的过程可验证语言

MolLean 提出一种用于化学推理的过程可验证语言，借助显式分子状态、基于 Lean 的验证和交互式工具反馈，以减少生成与反应任务中的模型幻觉。其分层 Lean 内核检查状态转换与断言，MolLean-MCP 状态化工具接口在生成时暴露状态转换、检查与分子读数，模型据反馈决定下一动作，被拒绝的动作不改变状态；框架支持单次轨迹执行、整条轨迹修订和交互式推理。