让机器自动将数学理论整体形式化，构建可验证的知识库。
Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
- 从单个命题转向完整数学理论的形式化，构建依赖关系网。
- 提出理论级形式化的框架，支持数学知识的系统性建模。
- 适合数学自动化、形式化证明和知识库建设的研究者。
自动形式化旨在将非形式化的自然语言转化为可被机器验证的形式语言。现有研究多聚焦于孤立命题，而实际形式化工作本质上是理论层级的：需先建立一整套公理、定义与引理，才能陈述目标定理。本文主张推进理论级自动形式化，即以结构化库的形式形式化完整理论及其全部依赖关系。我们探讨这一转变的意义，回应不同观点，识别开放挑战，并提出三条有前景的发展路径。自动形式化研究综述见 https://github.com/marcusm117/Awesome-Autoformalization。
原文摘要 · Abstract (English)
Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward. Our survey of autoformalization is available at https://github.com/marcusm117/Awesome-Autoformalization.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。