用工具增强智能体提升自然语言转正式数学代码的准确性
Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
- 结合三种工具：查询微调模型、搜索知识库符号定义、利用编译器反馈验证
- 编译通过率和语义等价性显著提升，比单次提示基线大幅提高
- 首次量化各工具贡献，揭示编译反馈对性能提升最关键
将自然语言数学自动翻译为忠实的 Lean 4 代码受到非形式集合论直觉与严格形式类型论之间根本差异的阻碍。这一差距常导致大语言模型虚构不存在的库定义，造成代码无法编译或语义失真。本文通过系统性的因子分析，研究三类工具增强智能体在该任务中的有效性：微调模型查询（获取专家草稿）、知识搜索（检索符号定义）、编译器反馈（通过 Lean REPL 验证代码）。首先在单次提示基线上进行基准测试，证明在编译成功率和语义等价性上均有显著提升。随后通过因子分解，量化每类工具的独立贡献，明确各工具对整体性能的边际影响。
原文摘要 · Abstract (English)
Automatic translation of natural language mathematics into faithful Lean 4 code is hindered by the fundamental dissonance between informal set-theoretic intuition and strict formal type theory. This gap often causes LLMs to hallucinate non-existent library definitions, resulting in code that fails to compile or lacks semantic fidelity. In this work, we investigate the effectiveness of tool-augmented agents for this task through a systematic factorial analysis of three distinct tool categories: Fine-tuned Model Querying (accessing expert drafts), Knowledge Search (retrieving symbol definitions), and Compiler Feedback (verifying code via a Lean REPL). We first benchmark the agent against one-shot baselines, demonstrating large gains in both compilation success and semantic equivalence. We then use the factorial decomposition to quantify the impact of each category, isolating the marginal contribution of each tool type to overall performance.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。