提升数学文本自动形式化的一致性，让AI更可靠地构建数学库。
Consistent Autoformalization for Constructing Mathematical Libraries
- 用相似检索增强生成+去噪+语法纠错三机制协同优化
- 在多个模型上实现语法、术语、语义一致性显著提升
- 适合构建大规模数学形式化库的科研人员使用
自动形式化是将自然语言撰写的数学内容自动转换为形式语言表达的任务。大型语言模型（LLMs）在语言理解尤其是形式语言处理方面的能力不断增强，降低了自动形式化的门槛。然而，仅靠LLMs难以在复杂和专业化程度高的领域保持一致且可靠的输出。随着该领域向系统性构建大规模数学库的方向发展，对句法、术语和语义控制的需求日益增强。本文提出协同使用三种机制：最相似检索增强生成（MS-RAG）、去噪步骤以及基于语法错误反馈的自动纠错（Auto-SEF），以提升自动形式化质量。实证分析表明，这些机制在不同模型上均能显著提高输出在语法、术语和语义层面的一致性。该方法可跨多种LLM应用，并在不同模型类型中均表现出改进效果。
原文摘要 · Abstract (English)
Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. The growing language interpretation capabilities of Large Language Models (LLMs), including in formal languages, are lowering the barriers for autoformalization. However, LLMs alone are not capable of consistently and reliably delivering autoformalization, in particular as the complexity and specialization of the target domain grows. As the field evolves into the direction of systematically applying autoformalization towards large mathematical libraries, the need to improve syntactic, terminological and semantic control increases. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality. The empirical analysis, across different models, demonstrates that these mechanisms can deliver autoformalizaton results which are syntactically, terminologically and semantically more consistent. These mechanisms can be applied across different LLMs and have shown to deliver improve results across different model types.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。