Fine-tuned 0.6B LLMs with beam search achieve 85% success on 60 test Shannon entropy inequalities (n=10-15), outperforming GPT-5.5 (1.7%) and Psitip (33.3%).
Process-driven autoformalization in lean 4
13 Pith papers cite this work. Polarity classification is still indexing.
13
Pith papers citing it
abstract
Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing efforts are limited to formal languages with substantial online corpora and struggle to keep pace with rapidly evolving languages like Lean 4. To bridge this gap, we propose a new benchmark \textbf{Form}alization for \textbf{L}ean~\textbf{4} (\textbf{\name}) designed to evaluate the autoformalization capabilities of large language models (LLMs). This benchmark encompasses a comprehensive assessment of questions, answers, formal statements, and proofs. Additionally, we introduce a \textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier (\textbf{PSV}) model that leverages the precise feedback from Lean 4 compilers to enhance autoformalization. Our experiments demonstrate that the PSV method improves autoformalization, enabling higher accuracy using less filtered training data. Furthermore, when fine-tuned with data containing detailed process information, PSV can leverage the data more effectively, leading to more significant improvements in autoformalization for Lean 4. Our dataset and code are available at \url{https://github.com/rookie-joe/PDA}.
citation-role summary
baseline 1
dataset 1
citation-polarity summary
years
2026 13representative citing papers
A new benchmark of 9,415 Lean 4 specifications derived from 2,772 scraped Python property-based tests, plus a three-agent LLM transpilation pipeline and proof-generation baselines.
CAM-Bench is a new Lean 4 theorem-proving benchmark of 1,000 problems in computational and applied mathematics, built from textbook exercises using a dependency-recovery pipeline to reconstruct local context.
Paraphrase sensitivity in Lean 4 autoformalization is dominated by code-generation failures that differ between undergraduate and Olympiad datasets across multiple models.
LLMs display clear performance stratification on formal language tasks aligned with Chomsky hierarchy complexity levels, limited by severe efficiency barriers rather than absolute capability.
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
A 400-entry benchmark and protocol shows tool-augmented agents reach 89.5% compilation but only 60.5% consensus faithfulness, with a 29-point gap; elaboration feedback improves validity most but increases unfaithful compiles.
The signal-coverage matrix stratifies autoformalization outputs into true success, type-only, semantic-only, and both-fail cells, showing type-correctness gains are mostly type-stratum recovery with semantic errors largely unchanged.
Lean-GAP is a dataset of 430 graduate algebra problems formalized in Lean 4 from Dummit and Foote, with a described pipeline for autoformalization and verification plus analysis of challenges.
A minimal agentic system achieves competitive performance in automated theorem proving with a simpler design and lower cost than state-of-the-art methods.
AI for mathematics is best described as a supervision ladder — final answers, programs, process rewards, proof-assistant kernels — culminating in verified-discovery workflows.
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.
citing papers explorer
-
Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search
Fine-tuned 0.6B LLMs with beam search achieve 85% success on 60 test Shannon entropy inequalities (n=10-15), outperforming GPT-5.5 (1.7%) and Psitip (33.3%).
-
FVSpec: Real-World Property-Based Tests as Lean Challenges
A new benchmark of 9,415 Lean 4 specifications derived from 2,772 scraped Python property-based tests, plus a three-agent LLM transpilation pipeline and proof-generation baselines.
-
CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
CAM-Bench is a new Lean 4 theorem-proving benchmark of 1,000 problems in computational and applied mathematics, built from textbook exercises using a dependency-recovery pipeline to reconstruct local context.
-
Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization
Paraphrase sensitivity in Lean 4 autoformalization is dominated by code-generation failures that differ between undergraduate and Olympiad datasets across multiple models.
-
Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy
LLMs display clear performance stratification on formal language tasks aligned with Chomsky hierarchy complexity levels, limited by severe efficiency barriers rather than absolute capability.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
A 400-entry benchmark and protocol shows tool-augmented agents reach 89.5% compilation but only 60.5% consensus faithfulness, with a 29-point gap; elaboration feedback improves validity most but increases unfaithful compiles.
-
The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
The signal-coverage matrix stratifies autoformalization outputs into true success, type-only, semantic-only, and both-fail cells, showing type-correctness gains are mostly type-stratum recovery with semantic errors largely unchanged.
-
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
Lean-GAP is a dataset of 430 graduate algebra problems formalized in Lean 4 from Dummit and Foote, with a described pipeline for autoformalization and verification plus analysis of challenges.
-
A Minimal Agent for Automated Theorem Proving
A minimal agentic system achieves competitive performance in automated theorem proving with a simpler design and lower cost than state-of-the-art methods.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
AI for mathematics is best described as a supervision ladder — final answers, programs, process rewards, proof-assistant kernels — culminating in verified-discovery workflows.
-
AI for Mathematics: Progress, Challenges, and Prospects
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.
- Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics