MerLean：一个用于量子计算自动形式化的代理框架
MerLean: An Agentic Framework for Autoformalization in Quantum Computation
AI总结：
MerLean通过自动化形式化框架将量子计算论文中的数学语句转化为Lean代码并回译为可读格式，实现端到端验证，为同行评审和合成数据训练提供实用工具。
摘要：
我们介绍了MerLean，一个完全自动化的代理框架，用于量子计算中的自动形式化。MerLean从LaTeX源文件中提取数学语句，将其形式化为基于Mathlib的已验证Lean~4代码，并将结果翻译回人类可读的LaTeX进行语义审查。我们在三篇理论量子计算论文上评估MerLean，总共生成2,050个Lean声明，来自114个语句。MerLean在所有三篇论文上实现了端到端的形式化，将验证负担仅限于新引入的定义和公理。我们的结果表明，代理自动形式化可以扩展到前沿研究，既提供了一个实用的机器验证同行评审工具，也提供了一个可扩展的引擎，用于挖掘高质量合成数据以训练未来推理模型。我们的方法也可以推广到数学和理论物理的其他严谨研究中。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
