Research map / Large language models / Agents, code and math
Herald: A Natural Language Annotated Lean 4 Dataset
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Builds Herald, a Lean 4 Mathlib4 natural-language-annotated dataset via structure-aware (Lean-Jixia) hierarchical RAG informalization plus tactic-based and LLM-based augmentation, and fine-tunes the Herald translator (DeepSeek-Prover-V1.5-Base 7B) for statement autoformalization.
Problem
Parallel natural language–Lean 4 data is scarce, limiting LLM autoformalization of mathematics; existing NL-FL pair generation suffers from LLM errors and ignores Lean's structural information.
Approach
Provide the LLM with structural Lean context (head statements, kind, docstrings, neighbor statements, dependent theorems), informalize in dependency-level order, retrieve similar annotated examples, and augment data by decomposing tactic proof states and by LLM-based informal rewriting, then SFT a statement formalizer on the result.
Key results
- Herald translator reaches 96.7% on miniF2F-test (Pass@128) vs 73.0% for InternLM2-Math-Plus-7B and 50.1% for TheoremLlama.
- On the internal graduate-level Extract Theorem set, Herald achieves 23.5% vs 7.5% (InternLM2-Math-Plus-7B) and 4.0% (TheoremLlama).
- Ablation shows augmentation raises miniF2F-test from 86.8% (original only) to 96.7% with 1:2:1 ratio and 1160k examples.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Fine-tune on Herald rather than use InternLM2-Math-Plus-7B | Statement formalization · miniF2F-test | accuracy: 73.0\% -> 96.7\% | Helped |
| Fine-tune on Herald rather than use InternLM2-Math-Plus-7B | Statement formalization · miniF2F-valid | accuracy: 80.1\% -> 96.3\% | Helped |
| Fine-tune on Herald rather than use InternLM2-Math-Plus-7B | Statement formalization · Extract Theorem | accuracy: 7.5\% -> 23.5\% | Helped |
| Fine-tune on Herald rather than use InternLM2-Math-Plus-7B | Statement formalization · College CoT | accuracy: 6.5\% -> 16.0\% | Helped |
| Add tactic-based and informal augmentation to original pairs (ablation) | Herald translator · MiniF2F-test | accuracy: 86.8\% -> 91.4\% | Helped |
| Add tactic-based and informal augmentation to original pairs (ablation) | Herald translator · ProofNet-valid | accuracy: 50.0\% -> 68.3\% | Helped |
| Add tactic-based and informal augmentation to original pairs (ablation) | Herald translator · Extract-Theorem | accuracy: 15.0\% -> 17.5\% | Helped |
| Use more tactic-based augmentation and omit informal augmentation (ablation) | Herald translator · MiniF2F-test | accuracy: 91.4\% -> 95.1\% | Helped |
| Use more tactic-based augmentation and omit informal augmentation (ablation) | Herald translator · ProofNet-valid | accuracy: 68.3\% -> 74.7\% | Helped |
| Use more tactic-based augmentation and omit informal augmentation (ablation) | Herald translator · Extract-Theorem | accuracy: 17.5\% -> 19.0\% | Helped |
| Add informal augmentation to the 1:2:0 tactic-augmentation mixture (ablation) | Herald translator · MiniF2F-test | accuracy: 95.1\% -> 93.2\% | Hurt |
| Add informal augmentation to the 1:2:0 tactic-augmentation mixture (ablation) | Herald translator · ProofNet-valid | accuracy: 74.7\% -> 78.6\% | Helped |
Surprising findings
- Human evaluation found that validation-passed Herald outputs still include major errors (26 of 151), showing the NLI pipeline yields false positives.
- The NLI check can produce false negatives, so some correct translations are rejected.
Limitations
- Validation via Lean compile check and LLM back-translation NLI check admits false positives and negatives.
- Prover (DeepSeek-Prover-V1.5-RL) could only prove one simple theorem in the Stacks Project case study, limiting end-to-end formalization of advanced topics.
- Translating abstract and diagram-based theorems remains challenging.
Experimental setup
Datasets: Mathlib4 OpenHermes2.5 miniF2F ProofNet
Benchmarks: miniF2F-test miniF2F-valid Extract Theorem College CoT ProofNet-valid
Metrics: pass@128 accuracy (compiler check plus back-translation NLI human-evaluated correct/minor/major error rates
Baselines: TheoremLlama InternLM2-Math-Plus-7B Llama3-instruct
Builds on: Lean Workbook Lean-Jixia DeepSeek-Prover-V1.5 TheoremLlama Lean-STaR
Closest papers by meaning
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems (NeurIPS 2024 · similarity 0.92)
- ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.87)
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.87)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.86)
- Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.86)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.