KELPS框架实现多语言数学命题自动形式化，提升准确率至88.9%
KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment
- 用知识方程作为中间语言，实现自然语言到形式语言的语义-语法对齐
- 构建超6万条多语言并行数据集，在MiniF2F上达到88.9%语法准确率
- 适合形式化验证、AI辅助数学推理等研究者使用
现代大语言模型在将非形式化数学转化为可机器验证的定理方面展现出良好进展，但受限于多语言平行语料的数量与质量。本文提出新型神经符号框架KELPS（基于知识方程的逻辑处理系统），用于将非形式化数据迭代翻译、合成并过滤为多种形式语言（Lean、Coq、Isabelle）。首先，将自然语言转化为我们设计的、基于断言逻辑的新型语言——知识方程（KEs）；随后通过严格定义的规则转换为目标语言，确保语法结构与语义一致性。该流程生成了超过60,000个问题的并行语料库。在MiniF2F数据集上，本框架达到88.9%的语法准确率（pass@1），优于Deepseek-V3（81%）和Herald（81.3%）等现有模型。所有数据集与代码已包含在补充材料中。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。