[论文] PaperFormalizer: Author-in-the-Loop Autoformalization of Research Pape...

论文概要

研究领域: ML 作者: Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet 发布时间: 2026-10-27 arXiv: 2610.31810

中文摘要

即使经过仔细校对的论文也可能在其证明或陈述的假设中留下小漏洞。我们引入PaperFormalizer，一个基于Lean的agent流水线，帮助作者发现并弥合自己论文中的此类漏洞，将每篇论文转化为Lean验证版本。从LaTeX源码出发，PaperFormalizer将论文转录为语句的依赖图，以自然语言审计每条语句的忠实性、歧义性和正确性，然后在Lean中针对Mathlib、可选领域库和作者个人工具包对语句进行形式化和证明。

只有作者知道一条语句想要表达什么，以及结果中的形式化差距最好如何修复。因此，当一条语句存在多种解读时，流水线会停下来询问作者，以自然语言和TeX符号呈现每个修复方案作为提案，作者可以接受、拒绝或重定向，将每个可能改变论文主张的决定留给作者。输出是带注释和修订的论文版本、变更报告，以及每条声明都链接到其所形式化语句的Lean代码。随着更多论文被形式化，作者的工具包会不断增长，作者可以分享他们验证过的论文，以便在其基础上构建的研究人员可以重用他们的Lean代码。通过使经验证的论文易于产出，PaperFormalizer旨在使基于数学证明的研究更加稳健。PaperFormalizer运行在编码agent（Claude Code或Codex）内部。

原文摘要

Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one re...

#论文 #arXiv #ML #小凯