自动将量子计算论文转化为可验证的代码，提升研究可信度。
MerLean: An Agentic Framework for Autoformalization in Quantum Computation
- 用智能代理自动提取公式并转为可验证的Lean代码
- 从114个数学陈述生成2050个代码声明，三篇论文全部成功转化
- 适合需要机器验证的理论物理与数学研究者
我们提出MerLean，一个完全自动化的智能框架，用于量子计算中的自动形式化。MerLean从LaTeX源文件中提取数学陈述，将其形式化为基于Mathlib的可验证Lean 4代码，并将结果转换回人类可读的LaTeX以供语义审查。我们在三篇理论量子计算论文上评估该框架，共生成2050个Lean声明，源自114个原始陈述。MerLean在所有三篇论文上实现端到端形式化，仅需验证新引入的定义和公理。结果表明，智能体式自动形式化可扩展至前沿研究，既可用于机器验证同行评审，也可作为训练未来推理模型的高质量合成数据引擎。该方法还可推广至数学与理论物理等其他严谨领域。
原文摘要 · Abstract (English)
We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \LaTeX{} source files, formalizes them into verified Lean~4 code built on Mathlib, and translates the result back into human-readable \LaTeX{} for semantic review. We evaluate MerLean on three theoretical quantum computing papers producing 2,050 Lean declarations from 114 statements in total. MerLean achieves end-to-end formalization on all three papers, reducing the verification burden to only the newly introduced definitions and axioms. Our results demonstrate that agentic autoformalization can scale to frontier research, offering both a practical tool for machine-verified peer review and a scalable engine for mining high-quality synthetic data to train future reasoning models. Our approach can also be generalized to any other rigorous research in mathematics and theoretical physics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。