Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.</p>\n<p>Github: <a href=\"https://github.com/OpenBMB/MathForm\" rel=\"nofollow\">https://github.com/OpenBMB/MathForm</a><br>Model: <a href=\"https://huggingface.co/openbmb/MathForm-8B\">https://huggingface.co/openbmb/MathForm-8B</a><br>Dataset: <a href=\"https://huggingface.co/datasets/openbmb/FormalVerse\">https://huggingface.co/datasets/openbmb/FormalVerse</a></p>\n","updatedAt":"2026-08-19T04:40:45.926Z","author":{"_id":"660e827d996fae1305ba4ec7","avatarUrl":"/avatars/c7ee117e3fdc01e932f12d5d74385097.svg","fullname":"Lushi Pu","name":"daypu","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.84279865026474},"editors":["daypu"],"editorAvatarUrls":["/avatars/c7ee117e3fdc01e932f12d5d74385097.svg"],"reactions":[],"isReport":false}}],"primaryEmailConfirmed":false,"paper":{"id":"2608.14221","authors":[{"_id":"6a829da1b601d59c652814e5","user":{"_id":"660e827d996fae1305ba4ec7","avatarUrl":"/avatars/c7ee117e3fdc01e932f12d5d74385097.svg","isPro":false,"fullname":"Lushi Pu","user":"daypu","type":"user","name":"daypu"},"name":"Lushi Pu","status":"claimed_verified","statusLastChangedAt":"2026-08-17T16:45:04.515Z","hidden":false},{"_id":"6a829da1b601d59c652814e6","name":"Weiming Zhang","hidden":false},{"_id":"6a829da1b601d59c652814e7","name":"Xinheng Xie","hidden":false},{"_id":"6a829da1b601d59c652814e8","name":"Zixuan Fu","hidden":false},{"_id":"6a829da1b601d59c652814e9","name":"Bingxiang He","hidden":false},{"_id":"6a829da1b601d59c652814ea","name":"Hengyu Zhao","hidden":false},{"_id":"6a829da1b601d59c652814eb","name":"Hongya Lyu","hidden":false},{"_id":"6a829da1b601d59c652814ec","name":"Xin Li","hidden":false},{"_id":"6a829da1b601d59c652814ed","name":"Jie Zhou","hidden":false},{"_id":"6a829da1b601d59c652814ee","name":"Yudong Wang","hidden":false}],"publishedAt":"2026-08-14T11:51:12.000Z","submittedOnDailyAt":"2026-08-19T00:00:00.000Z","title":"MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement","submittedOnDailyBy":{"_id":"660e827d996fae1305ba4ec7","avatarUrl":"/avatars/c7ee117e3fdc01e932f12d5d74385097.svg","isPro":false,"fullname":"Lushi Pu","user":"daypu","type":"user","name":"daypu"},"summary":"Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.","upvotes":3,"discussionId":"6a829da1b601d59c652814ef","githubRepo":"https://github.com/OpenBMB/MathForm","githubRepoAddedBy":"user","ai_summary":"MathForm improves autoformalization by retrieving Mathlib knowledge and iteratively refining outputs with verification feedback, yielding a large verified dataset and a high-performing 8B model.","ai_keywords":["autoformalization","Mathlib","retrieval planner","verification-guided iterative refinement","compiler diagnostics","semantic-consistency feedback","FormalVerse","supervised fine-tuning","reinforcement learning","Pass@8"],"ai_summary_model":"thinkingmachines/Inkling-Small","githubStars":3,"organization":{"_id":"633fe81429b5a95f6e16e34a","name":"openbmb","fullname":"OpenBMB","avatar":"https://cdn-avatars.huggingface.co/v1/production/uploads/1670387859384-633fe7784b362488336bbfad.png"}},"canReadDatabase":false,"canManagePapers":false,"canSubmit":false,"hasHfLevelAccess":false,"upvoted":false,"upvoters":[{"_id":"63c1699e40a26dd2db32400d","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63c1699e40a26dd2db32400d/3N0-Zp8igv8-52mXAdiiq.jpeg","isPro":false,"fullname":"Chroma","user":"Chroma111","type":"user"},{"_id":"660e827d996fae1305ba4ec7","avatarUrl":"/avatars/c7ee117e3fdc01e932f12d5d74385097.svg","isPro":false,"fullname":"Lushi Pu","user":"daypu","type":"user"},{"_id":"63ac5701c21e60a3e9b58aa7","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63ac5701c21e60a3e9b58aa7/g6EX7diOpuA94R2ab-rZC.png","isPro":true,"fullname":"Dipankar Sarkar","user":"dipankarsarkar","type":"user"}],"acceptLanguages":["en"],"dailyPaperRank":0,"organization":{"_id":"633fe81429b5a95f6e16e34a","name":"openbmb","fullname":"OpenBMB","avatar":"https://cdn-avatars.huggingface.co/v1/production/uploads/1670387859384-633fe7784b362488336bbfad.png"},"markdownContentUrl":"https://huggingface.co/buckets/huggingchat/papers-content/resolve/2608/2608.14221.md","query":{}}">
MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
Abstract
MathForm improves autoformalization by retrieving Mathlib knowledge and iteratively refining outputs with verification feedback, yielding a large verified dataset and a high-performing 8B model.
Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.
Community
Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.
Github: https://github.com/OpenBMB/MathForm
Model: https://huggingface.co/openbmb/MathForm-8B
Dataset: https://huggingface.co/datasets/openbmb/FormalVerse
Upload images, audio, and videos by dragging in the text input, pasting, or clicking here.
Tap or paste here to upload images
Cite arxiv.org/abs/2608.14221 in a Space README.md to link it from this page.
Discussion (0)
Sign in to join the discussion. Free account, 30 seconds — email code or GitHub.
Sign in →No comments yet. Sign in and be the first to say something.