理论层面的自动形式化：从孤立陈述到统一形式知识库
Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
浏览论文内容
中文总结 AI 辅助
探讨自动形式化从单个陈述到理论层面的转变，主张将完整理论及其相互依赖关系形式化为结构化库，分析转变意义，回应不同观点，识别挑战并提出三条前进路径。
中文摘要 AI 辅助
自动形式化将非正式自然语言转化为形式化、机器可验证的语言。虽然多数工作聚焦于单个陈述，但实际形式化工作本质上是理论层面的：在陈述目标定理之前，需要一整套公理、定义和引理的网络。在本立场文件中，我们主张理论层面的自动形式化：将完整理论及其所有相互依赖关系形式化为结构化库。我们探讨了这一转变的意义，回应了不同观点，识别了开放挑战，并提出了三条有前景的前进路径。我们关于自动形式化的综述可在该https网址获取。
英文摘要
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.
