Research map / Large language models / Instruction and fine-tuning
Multi-language Diversity Benefits Autoformalization
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.
Creates MMA, a 332K informal-formal dataset by using GPT-4 to informalise Isabelle AFP and Lean4 mathlib4 statements, and fine-tunes LLaMA-33B and Mistral 7B on it for multi-language autoformalization.
Problem
Autoformalization needs large parallel informal-formal data, which is scarce; existing work relies on small manually curated corpora or few-shot prompting, which suffers from data scarcity and formal-language difficulty.
Approach
Reverse-direction distilled back-translation: use GPT-4 to informalise existing formal statements from two proof libraries (Isabelle AFP and Lean4 mathlib4) into natural language, then fine-tune open LLMs to formalise, and show that jointly training on multiple formal languages beats single-language training.
Key results
- Mistral 7B fine-tuned on Isabelle+Lean4 MMA produced 29% (Isabelle) and 31% (Lean4) of formalisations acceptable with minimal corrections; base models produced 0%.
- Jointly fine-tuned LLaMA-33B reached 18% (Isabelle) and 16% (Lean4) acceptable-with-minimal-correction formalisations.
- Joint multi-language fine-tuning gave lower average correction effort than single-language fine-tuning for both languages, with non-overlapping 95% confidence intervals for Isabelle.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Fine-tune LLaMA on both Isabelle and Lean4 MMA data instead of Isabelle-only data (ablation) | LLaMA-33B autoformalization · miniF2F + ProofNet, Isabelle | acceptable with minimal corrections: 6% -> 18% | Helped |
| Fine-tune LLaMA on both Isabelle and Lean4 MMA data instead of Lean4-only data (ablation) | LLaMA-33B autoformalization · miniF2F + ProofNet, Lean4 | acceptable with minimal corrections: 10% -> 16% | Helped |
| Fine-tune Mistral on both Isabelle and Lean4 MMA data instead of Isabelle-only data (ablation) | Mistral 7B autoformalization · miniF2F + ProofNet, Isabelle | acceptable with minimal corrections: 20% -> 29% | Helped |
| Fine-tune Mistral on both Isabelle and Lean4 MMA data instead of Lean4-only data (ablation) | Mistral 7B autoformalization · miniF2F + ProofNet, Lean4 | acceptable with minimal corrections: 26% -> 31% | Helped |
| Fine-tune on MMA instead of using the base model | LLaMA-33B and Mistral 7B autoformalization · miniF2F + ProofNet, Isabelle and Lean4 | acceptable with minimal corrections: 0% -> 6–31% | Helped |
| Train on both Isabelle and Lean4 rather than Isabelle only (ablation) | Autoformalization models · 200 evaluation samples, Isabelle | average correction effort: 2.785 -> 2.415 | Helped |
| Train on both Isabelle and Lean4 rather than Lean4 only (ablation) | Autoformalization models · 200 evaluation samples, Lean4 | average correction effort: 2.67 -> 2.495 | Helped |
| Fine-tune on Isabelle and Lean4 MMA data instead of using the base model | Autoformalization models · 200 evaluation samples, Isabelle | average correction effort: 4 -> 2.415 | Helped |
| Fine-tune on Isabelle and Lean4 MMA data instead of using the base model | Autoformalization models · 200 evaluation samples, Lean4 | average correction effort: 3.995 -> 2.495 | Helped |
Surprising findings
- Fine-tuning on both Isabelle and Lean4 was more data-efficient, outperforming single-language models even though it saw fewer tokens of each language.
- Compilation rate is a poor proxy for usefulness: Isabelle-only models achieved high compilation rates via untyped variables while producing less useful formalisations.
Limitations
- GPT-4 informalisations are noisy: about 26% of a sample contained errors such as misunderstood concepts or hallucinations, so MMA is not perfect.
- Evaluation is manual on only 50 problems per benchmark per model, with limited statistical power and no automatic correctness check.
- Only two formal languages (Isabelle and Lean4) and two base models were studied, and the data-ratio sweep was not performed due to budget.
Experimental setup
Datasets: MMA (Isabelle AFP and Lean4 mathlib4 informal-formal pairs) miniF2F ProofNet
Benchmarks: miniF2F ProofNet
Metrics: compilation rate human correction effort level (0-4 Likert) share of formalisations acceptable with minimal corrections validation loss and token accuracy
Baselines: base LLaMA-33B (no fine-tuning) base Mistral 7B (no fine-tuning) single-language fine-tuned models (Isabelle only, Lean4 only)
Builds on: back-translation Codex-based autoformalization (Azerbayev et al.) instruction prompting
Closest papers by meaning
- ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.88)
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · similarity 0.87)
- FormalAlign: Automated Alignment Evaluation for Autoformalization (ICLR 2025 · similarity 0.86)
- Automating Dataset Updates Towards Reliable and Timely Evaluation of Large Language Models (NeurIPS 2024 · similarity 0.86)
- Beyond Autoregression: Fast LLMs via Self-Distillation Through Time (ICLR 2025 · similarity 0.86)
- Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks (ICLR 2025 · similarity 0.85)
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.