Research map / Large language models / Agents, code and math
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
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 scoring k LLM autoformalization candidates with symbolic equivalence (via Isabelle tactics, Z3, CVC5) and semantic consistency (BERT similarity of back-translated statements), combined via log/linear/quadratic strategies, to close the pass@1 vs pass@k gap on MATH and miniF2F.
Problem
LLM autoformalization of math statements shows a large gap between pass@1 and pass@k, and standard self-consistency (answer matching or test-based execution) does not transfer to formal statements.
Approach
Rank k autoformalization candidates by two complementary self-consistency signals: symbolic equivalence among formal statements checked by automated theorem provers after variable standardization and bipartite variable matching, and semantic consistency measured as embedding similarity between the informalized candidate and the original text; combine them with a tuned alpha.
Key results
- On MATH with GPT-4, SymEq reaches 42.0% 1@10 versus 37.5% for the baseline, and log-comb adds further gains; the combination improves 1@k by 2.3% to 22.6% across LLMs and datasets.
- On miniF2F, GPT-4 with SymEq achieves 41.1% 1@10 versus 32.9% baseline.
- Log-comb gives relative labeling efficiency of 17.7% to 21.6% on MATH and up to 21.9% on miniF2F with GPT-4.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Rank generated candidates by symbolic equivalence (SymEq) instead of the strongest of Baseline, Naïve, or Cluster | Mistral-7B, Llemma-34B, DeepSeek-v2, Codex, and GPT-4 autoformalization · MATH | 1@k accuracy: 18.1 -> 26.7; 33.4 -> 41.1; 37.3 -> 42.4; 43.8 -> 46.1; 39.7 -> 42.0 | Helped |
| Rank generated candidates by symbolic equivalence (SymEq) instead of the strongest of Baseline, Naïve, or Cluster | Mistral-7B, Llemma-34B, DeepSeek-v2, Codex, and GPT-4 autoformalization · miniF2F | 1@k accuracy: 7.5 -> 14.5; 21.3 -> 32.0; 28.0 -> 28.4; 30.0 -> 36.5; 34.8 -> 41.1 | Helped |
| Rank generated candidates by semantic consistency (SemCo) | MATH autoformalization · MATH | 1@k accuracy: 0.8%-3.9% improvement over the baseline | Helped |
| Use semantic consistency rather than symbolic equivalence to select candidates | GPT-4 autoformalization · MATH categories | 1@k accuracy | Mixed |
| Combine symbolic equivalence and semantic consistency scores using log combination | Autoformalization across the evaluated LLMs · MATH and miniF2F | n@k accuracy: 2.3%-22.6% | Helped |
| Add log-combination ranking to SymEq | GPT-4 autoformalization · MATH | 1@k accuracy: 3.3% | Helped |
| Add log-combination ranking to SymEq | GPT-4 autoformalization · miniF2F | 1@k accuracy: 2.5% | Helped |
| Use log combination instead of linear or quadratic combination (ablation) | Combining symbolic equivalence and semantic consistency scores · MATH and miniF2F | autoformalization accuracy | Helped |
| Use the limited equivalence checker with only auto and simp tactics, removing the other tactics and SMT solvers (ablation) | SymEq with GPT-4 · MATH | 1@k accuracy: 2.13 vs. 2.33 per problem on average | Hurt |
| Use stronger ATPs rather than the limited equivalence checker (ablation) | SymEq with GPT-4 · MATH | 1@k accuracy | No clear effect |
Surprising findings
- Increasing ATP capability (more tactics and SMT solvers) yields only narrow gains in symbolic-equivalence-based performance.
- Naive filtering by ATP proof success underperforms the log-probability baseline for most models, with negative relative efficiency on MATH.
Limitations
- Semantic consistency with embeddings may miss nuanced notation differences.
- ATPs are not strong enough to prove many high-school level problems or symbolic equivalences automatically.
- MATH correctness was judged manually, and no statistical significance or error bars are reported.
Experimental setup
Datasets: MATH miniF2F
Benchmarks: MATH miniF2F
Metrics: n@k accuracy relative labeling efficiency
Baselines: log-probability ranking ATP filtering (Naive) adaptive k-means clustering (Cluster)
Builds on: self-consistency Isabelle/HOL Sledgehammer adaptive k-means
Closest papers by meaning
- ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.92)
- FormalAlign: Automated Alignment Evaluation for Autoformalization (ICLR 2025 · similarity 0.90)
- Autoformalizing Euclidean Geometry (ICML 2024 · similarity 0.90)
- Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization (ICLR 2024 · similarity 0.89)
- Multi-language Diversity Benefits Autoformalization (NeurIPS 2024 · similarity 0.87)
- Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · 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.