KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment

📄 arXiv: 2507.08665v1 📥 PDF

作者: Jiyao Zhang, Chengli Zhong, Hui Xu, Qige Li, Yi Zhou

分类: cs.CL, cs.AI

发布日期: 2025-07-11

备注: Accepted by the ICML 2025 AI4MATH Workshop. 22 pages, 16 figures, 2 tables

💡 一句话要点

KELPS：一种基于语义-句法对齐的可验证多语言自动形式化框架

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动形式化 神经符号 多语言翻译 知识方程 形式化验证

📋 核心要点

  1. 现有方法在自动形式化方面面临多语言平行语料库匮乏的挑战，限制了模型性能。
  2. KELPS框架通过引入知识方程（KEs）作为中间表示，实现自然语言到多种形式化语言的精确转换。
  3. 实验结果表明，KELPS在MiniF2F数据集上超越了现有SOTA模型，验证了其有效性。

📝 摘要（中文）

现代大型语言模型（LLMs）在将非形式化数学转化为机器可验证定理方面展现出令人鼓舞的进展。然而，由于多语言平行语料库的数量和质量有限，这些方法仍然面临瓶颈。本文提出了一种新颖的神经符号框架KELPS（基于知识方程的逻辑处理系统）来解决这些问题。KELPS是一个迭代框架，用于将非形式化数据翻译、合成和过滤成多种形式化语言（Lean、Coq和Isabelle）。首先，我们将自然语言翻译成知识方程（KEs），这是一种我们设计的新语言，理论上基于断言逻辑。接下来，我们通过严格定义的规则将其转换为目标语言，这些规则保留了句法结构和语义意义。这个过程产生了超过60,000个问题的平行语料库。我们的框架在MiniF2F上实现了88.9%的句法准确率（pass@1），优于SOTA模型，如Deepseek-V3（81%）和Herald（81.3%）。所有数据集和代码都在补充材料中提供。

🔬 方法详解

问题定义：论文旨在解决将非形式化数学语言自动转化为多种形式化语言（如Lean、Coq、Isabelle）的问题。现有方法依赖于有限且质量参差不齐的多语言平行语料库，导致翻译准确率不高，难以满足形式化验证的需求。现有方法难以保证翻译过程中的语义一致性，容易引入错误。

核心思路：论文的核心思路是引入一种中间表示——知识方程（KEs），作为自然语言和形式化语言之间的桥梁。KEs基于断言逻辑，能够精确地捕捉自然语言的语义信息。通过将自然语言先翻译成KEs，再将KEs转换成目标形式化语言，可以有效地保证翻译过程中的语义一致性和句法准确性。这种方法类似于一种“枢纽语言”策略，降低了多语言翻译的复杂度。

技术框架：KELPS框架包含以下几个主要阶段：1) 自然语言到KEs的翻译：使用LLM将自然语言数学问题翻译成KEs。2) KEs到形式化语言的转换：通过预定义的规则，将KEs转换成目标形式化语言（Lean、Coq、Isabelle）。这些规则旨在保持句法结构和语义意义。3) 数据过滤与迭代：对生成的平行语料库进行过滤，去除不准确或不符合要求的样本。整个过程是迭代进行的，不断优化翻译规则和模型。

关键创新：最重要的技术创新点在于知识方程（KEs）的引入。KEs作为一种中间表示，具有以下优势：1) 语义精确：基于断言逻辑，能够准确地表达自然语言的语义信息。2) 结构化：具有清晰的结构，易于进行句法分析和转换。3) 多语言通用：可以作为多种形式化语言的通用中间表示，降低了多语言翻译的复杂度。与直接进行自然语言到形式化语言的翻译相比，KELPS通过KEs实现了更精确和可控的翻译过程。

关键设计：KEs的设计是关键。论文中详细定义了KEs的语法和语义规则，确保其能够准确地表达自然语言的数学含义。KEs到形式化语言的转换规则也经过精心设计，以保证句法结构和语义意义的保留。论文中使用了LLM进行自然语言到KEs的翻译，并对LLM进行了微调，以提高翻译的准确率。具体参数设置和损失函数等技术细节在论文的补充材料中提供（未知）。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

KELPS框架在MiniF2F数据集上取得了显著的性能提升，句法准确率（pass@1）达到88.9%，优于Deepseek-V3（81%）和Herald（81.3%）等SOTA模型。这表明KELPS框架在自动形式化方面具有很强的竞争力，能够有效地提高翻译的准确性和可靠性。该框架生成的平行语料库包含超过60,000个问题，为后续研究提供了宝贵的数据资源。

🎯 应用场景

KELPS框架可应用于自动定理证明、形式化验证、数学教育等领域。通过自动将非形式化数学知识转化为机器可验证的形式，可以提高定理证明的效率和可靠性。在形式化验证领域，KELPS可以帮助验证软件和硬件系统的正确性。在数学教育领域，KELPS可以辅助学生理解和掌握形式化数学知识，并提供自动化的习题解答和验证工具。

📄 摘要（原文）

Modern large language models (LLMs) show promising progress in formalizing informal mathematics into machine-verifiable theorems. However, these methods still face bottlenecks due to the limited quantity and quality of multilingual parallel corpora. In this paper, we propose a novel neuro-symbolic framework KELPS (Knowledge-Equation based Logical Processing System) to address these problems. KELPS is an iterative framework for translating, synthesizing, and filtering informal data into multiple formal languages (Lean, Coq, and Isabelle). First, we translate natural language into Knowledge Equations (KEs), a novel language that we designed, theoretically grounded in assertional logic. Next, we convert them to target languages through rigorously defined rules that preserve both syntactic structure and semantic meaning. This process yielded a parallel corpus of over 60,000 problems. Our framework achieves 88.9% syntactic accuracy (pass@1) on MiniF2F, outperforming SOTA models such as Deepseek-V3 (81%) and Herald (81.3%) across multiple datasets. All datasets and codes are available in the supplementary materials.