Research map / Large language models / Alignment and preferences
FormalAlign: Automated Alignment Evaluation for 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.
Proposes FormalAlign, a Mistral-7B evaluator trained jointly with cross-entropy autoformalization loss and a contrastive alignment loss to automatically score informal-formal (Lean 4) statement alignment.
Problem
Autoformalization (informal math to Lean 4) needs semantic alignment checking between informal and formal statements, but current evaluation relies on manual review, compiler checks (only logical validity), or BLEU/BERTScore (surface similarity), which miss subtle misalignments.
Approach
Fine-tune an LLM with a combined loss (autoformalization cross-entropy + contrastive loss between informal and formal hidden states), then score alignment by averaging a generation certainty score and a hidden-state cosine similarity score, with misaligned negatives created by six perturbation strategies.
Key results
- On FormL4-Basic, FormalAlign reaches 99.21% AS versus GPT-4's 88.91%, with 93.65% precision versus 26.33%.
- On MiniF2F-Valid, FormalAlign gets 66.39% AS versus GPT-4's 64.34%, but GPT-4 is higher on MiniF2F-Test (68.31% vs 64.61%).
- In a 80-item human study, FormalAlign reached 65.00% correctness versus 79.58% average for human experts and 47.50% for GPT-4o.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use the combined cross-entropy and contrastive losses instead of cross-entropy loss alone (ablation) | FormalAlign (Mistral-7B) · FormL4-Basic | Alignment Selection: 98.64 -> 99.21 | Helped |
| use the combined cross-entropy and contrastive losses instead of cross-entropy loss alone (ablation) | FormalAlign (Mistral-7B) · FormL4-Random | Alignment Selection: 82.81 -> 85.85 | Helped |
| use the combined cross-entropy and contrastive losses instead of cross-entropy loss alone (ablation) | FormalAlign (Mistral-7B) · MiniF2F-Valid | Alignment Selection: 52.45 -> 66.39 | Helped |
| use the combined cross-entropy and contrastive losses instead of cross-entropy loss alone (ablation) | FormalAlign (Mistral-7B) · MiniF2F-Test | Alignment Selection: 54.32 -> 66.70 | Helped |
| use the combined cross-entropy and contrastive losses instead of contrastive loss alone (ablation) | FormalAlign (Mistral-7B) · MiniF2F-Valid | Alignment Selection: 36.07 -> 66.39 | Helped |
| combine certainty and similarity scores instead of using certainty score alone (ablation) | FormalAlign (Mistral-7B) · MiniF2F-Valid | Alignment Selection: 53.69 -> 66.39 | Helped |
| combine certainty and similarity scores instead of using certainty score alone (ablation) | FormalAlign (Mistral-7B) · MiniF2F-Test | Alignment Selection: 55.55 -> 66.70 | Helped |
| add contrastive learning loss to the autoformalization training objective (ablation) | FormalAlign autoformalization model · FormL4 Basic | Autoformalization performance: 40.92 -> 43.14 | Helped |
| add contrastive learning loss to the autoformalization training objective (ablation) | FormalAlign autoformalization model · FormL4 Random | Autoformalization performance: 35.88 -> 36.02 | Helped |
| fine-tune Mistral-7B as FormalAlign instead of using GPT-4 | automated alignment evaluation · FormL4-Basic | Alignment Selection: 88.91 -> 99.21 | Helped |
| fine-tune Mistral-7B as FormalAlign instead of using GPT-4 | automated alignment evaluation · FormL4-Basic | Precision: 26.33 -> 93.65 | Helped |
| fine-tune Mistral-7B as FormalAlign instead of using GPT-4 | automated alignment evaluation · MiniF2F-Valid | Alignment Selection: 64.34 -> 66.39 | Helped |
Surprising findings
- Cross-entropy-only training is nearly as good as the full model on FormL4 (98.64 vs 99.21 AS on Basic), and the contrastive loss alone performs poorly.
- GPT-4 outperforms FormalAlign on MiniF2F-Test alignment selection (68.31% vs 64.61%) and on recall in several settings.
Limitations
- FormalAlign's correctness ratio (65.00%) is well below human experts (79.58%) on the 80-item study.
- Misalignments are synthetic perturbations of aligned pairs, which may not reflect natural autoformalization errors.
- Reported training details (dataset sizes, exact training data counts) are sparse, and some appendix numbers are inconsistent (e.g., 20 vs 21 negatives, learning rate 2e-6 vs 5e-6).
Experimental setup
Datasets: FormL4 MMA MiniF2F
Benchmarks: FormL4-Basic FormL4-Random MiniF2F-Valid MiniF2F-Test
Metrics: Alignment Selection (AS) precision recall correctness ratio
Baselines: GPT-4 GPT-3.5 GPT-4o BLEU BERTScore Lean 4 compiler
Builds on: Mistral-7B InfoNCE contrastive loss BERTScore FormL4 MiniF2F
Closest papers by meaning
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · similarity 0.90)
- ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.89)
- Multi-language Diversity Benefits Autoformalization (NeurIPS 2024 · similarity 0.86)
- Autoformalizing Euclidean Geometry (ICML 2024 · similarity 0.86)
- APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries (ICML 2026 · similarity 0.85)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
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.