Automated Formalization via Conceptual Retrieval-Augmented LLMs

摘要

交互式定理证明器（ ITP ）需要手动形式化，这是劳动密集型的，需要专业知识。虽然自动化形式化提供了一种潜在的解决方案，但它面临两大挑战：模型幻觉（例如，未定义的谓词、符号滥用和版本不兼容）以及自然语言描述中模糊或缺少前提导致的语义差距。 为了解决这些问题，我们提出了CRAMF ，这是一个概念驱动的检索增强数学形式化框架。CRAMF通过检索核心数学概念的正式定义来增强基于LLM的自形式化，在代码生成期间提供上下文基础。 然而，由于缺乏结构化知识库，数学概念的多态性以及形式检索所需的高精度，在此环境中应用检索增强生成（ RAG ）并非易事。 我们引入了一个用于从Mathlib4自动构建概念定义知识库的框架， Mathlib4是精益4定理证明器的标准数学库，索引了26,000多个形式定义和1,000多个核心数学概念。为了解决概念多态性，我们提出了使用域级和应用级信号的上下文查询增强。 此外，我们设计了一种具有重新排序的双通道混合检索策略，以确保准确和相关的定义检索。在miniF2F、ProofNet和我们新提出的AdvancedMath基准上的实验表明， CRAMF可以无缝集成到基于LLM的自动形式化器中，从而在翻译准确性方面实现了一致的提高，最高可达62.1% ，平均相对提高29.9%。