将抽象数学结构自动转化为具体定理，提升形式化效率。
SITA: A Framework for Structure-to-Instance Theorem Autoformalization
- 用模块化模板封装抽象结构，支持可复用的形式化
- 在优化问题数据集上实现90%以上定理的正确自动形式化
- 适合数学研究者和形式化验证开发者使用
尽管大型语言模型在数学推理方面取得进展，但在将抽象结构的具体实例形式化为定理时仍面临挑战。为实现研究级数学结果的自动化形式化，我们提出结构到实例的定理自动形式化框架（SITA），系统性地连接抽象数学理论与其在Lean证明助手中的具体应用。形式化的抽象结构作为模块化模板，包含定义、假设、运算和定理，可作为具体实例形式化的可复用指引。给定特定实例后，生成对应的Lean定义与实例声明，利用Lean的类型类机制进行整合，并通过验证结构假设构建已验证定理。结合基于LLM的生成与反馈引导的精炼策略，确保自动化与形式正确性。在优化问题数据集上的实验表明，SITA能有效形式化基于抽象结构的多样化实例。
原文摘要 · Abstract (English)
While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete settings. With the goal of auto-formalizing mathematical results at the research level, we develop a framework for structure-to-instance theorem autoformalization (SITA), which systematically bridges the gap between abstract mathematical theories and their concrete applications in Lean proof assistant. Formalized abstract structures are treated as modular templates that contain definitions, assumptions, operations, and theorems. These templates serve as reusable guides for the formalization of concrete instances. Given a specific instantiation, we generate corresponding Lean definitions and instance declarations, integrate them using Lean's typeclass mechanism, and construct verified theorems by checking structural assumptions. We incorporate LLM-based generation with feedback-guided refinement to ensure both automation and formal correctness. Experiments on a dataset of optimization problems demonstrate that SITA effectively formalizes diverse instances grounded in abstract structures.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。