Pith. sign in

REVIEW 6 cited by

Multilingual Mathematical Autoformalization

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2311.03755 v2 pith:RUQSDTU7 submitted 2023-11-07 cs.CL cs.LG

Albert Q. Jiang , Wenda Li , Mateja Jamnik This is my paper · ORCID
classification cs.CLcs.LG
keywords languageautoformalizationtextttformalmodelsmultilingualdatadataset
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
abstract

Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a sizeable dataset consisting of informal-formal pairs expressing the same essence. Existing methods tend to circumvent this challenge by manually curating small corpora or using few-shot learning with large language models. But these methods suffer from data scarcity and formal language acquisition difficulty. In this work, we create $\texttt{MMA}$, a large, flexible, multilingual, and multi-domain dataset of informal-formal pairs, by using a language model to translate in the reverse direction, that is, from formal mathematical statements into corresponding informal ones. Experiments show that language models fine-tuned on $\texttt{MMA}$ produce $16-18\%$ of statements acceptable with minimal corrections on the $\texttt{miniF2F}$ and $\texttt{ProofNet}$ benchmarks, up from $0\%$ with the base model. We demonstrate that fine-tuning on multilingual formal data results in more capable autoformalization models even when deployed on monolingual tasks.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 6 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  2. Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

    cs.AI 2025-10 conditional novelty 6.0 of 10

    A graph-of-thought agent with retrieval and a term-grounded semantic checker auto-formalizes research-level math statements in Lean, hitting 68.5% on ProofNet and 6/14 homological conjectures where baselines score 0.

  3. FormaRL: Enhancing Autoformalization with no Labeled Data

    cs.AI 2025-08 conditional novelty 6.0 of 10

    A reinforcement learning framework improves autoformalization without labeled data by rewarding outputs that pass Lean syntax and LLM consistency checks.

  4. Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization

    cs.LG 2025-07 conditional novelty 6.0 of 10

    GTED uses tree edit distance on operator trees of standardized Lean statements to evaluate autoformalization, ranking top on miniF2F and joint-top on ProofNet.

  5. Mathesis: Towards Formal Theorem Proving from Natural Languages

    cs.AI 2025-06 conditional novelty 6.0 of 10

    An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.

  6. Integrating Rules and Semantics for LLM-Based C-to-Rust Translation

    cs.SE 2025-08 unverdicted novelty 5.0 of 10

    IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.

Pith tools