PaperFormalizer：基于 Lean 的作者在环研究论文自动形式化系统
英文标题：PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
研究人员提出了 PaperFormalizer，这是一个基于 Lean 形式化证明语言的 Agent 自动化流水线。该系统采用“作者在环”（Author-in-the-Loop）机制，旨在协助学术论文作者发现并弥补其论文证明及预设假设中的细微漏洞。通过将自然语言论文逐步转化为经机器严格验证的形式化代码，PaperFormalizer 有效提升了论文论证的严密性。对于开发者和科研人员而言，这一工具显著降低了形式化验证的门槛，展现了 AI Agent 在辅助学术验证与自动化定理证明领域的应用价值。
打开原文相关 2.4 · 机会 0
2.0 KB
640 B
612 B
380 B
24.2 KB
34.7 KB
中文
PaperFormalizer：基于 Lean 的作者在环研究论文自动形式化系统
- arXiv 编号：arXiv:2610.31810v1
- 公告类型：new
摘要
即使是经过仔细校对的论文，在论证过程或给出的前提假设中也难免会出现细微漏洞。我们提出了 PaperFormalizer，这是一个基于 Lean 的 Agent 流水线（agentic pipeline），可帮助作者在自己的论文中发现并弥合这些漏洞，并将整篇论文转化为经过 Lean 验证的形式化表述。
English / 原文
BibTeX formatted citation
×