Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910142453252096 |
|---|---|
| author | Zhang, Ke Gallardo, Patricio Raissi, Maziar Murthy, Sudhir |
| author_facet | Zhang, Ke Gallardo, Patricio Raissi, Maziar Murthy, Sudhir |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_16538 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis Zhang, Ke Gallardo, Patricio Raissi, Maziar Murthy, Sudhir Software Engineering Artificial Intelligence Machine Learning Programming Languages 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. |
| title | Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis |
| topic | Software Engineering Artificial Intelligence Machine Learning Programming Languages |
| url | https://arxiv.org/abs/2604.16538 |