量子科技中心_量科网

该研究团队推出了MerLean——一个用于量子计算领域自动形式化的全自动化智能框架。该系统能从LaTeX源文件中提取数学陈述，将其形式化为基于Mathlib验证的Lean 4代码，并将结果转译回人类可读的LaTeX格式以供语义审查。研究人员在3篇理论量子计算论文上评估了MerLean，共从114个陈述中生成了2050条Lean声明。该框架成功实现了三篇论文的端到端形式化，将验证负担仅局限于新引入的定义和公理。结果表明，这种智能自动形式化方法能扩展到前沿研究领域，既为机器验证的同行评审提供了实用工具，也为挖掘高质量合成数据训练未来推理模型构建了可扩展引擎。该工作的方法论也可推广至数学与理论物理等其他需要严格论证的研究领域。