Lean 数学命题多候选答案的高效证明生成框架
Efficient Proof Generation for Lean Statements with Multiple Candidate Answers
AI 导读
一项研究提出面向 Lean 4 形式化数学问题的联合证明框架，把候选答案选择、答案补充与形式化证明生成整合进统一推理过程，由训练的 prover 单次调用完成答案选择与新证明生成。
正文 · 原文
Abstract:In formal systems such as Lean 4, efficiently finding answers to mathematical problems and generating verifiable proofs is an important task in automated mathematical reasoning. In the traditional way where an upstream solver provides multiple candidate answers, the common workflow requires searching for proofs for each candidate separately, incurring redundant computational cost. To this end, we propose a joint proof framework that integrates candidate answer selection, answer supplementation, and formal proof generation into a unified reasoning process. At its core is a trained prover that selects given or proposes new answers and generates a proof for at least one answer in a single call. Joint proof can also reuse generated proofs to check for faithfulness errors. For problems with a unique answer, if two distinct answers both obtain verifiable proofs under the same formal statement, this confirms the statement does not faithfully preserve the original problem semantics. On MATH-500, AMC 2023, and AIME 2024/2025/2026, our framework achieves the same formal proof success rate as per-candidate proof generation with about one sixth of the token cost, and identifies at least 6.1% of the formalized statements as unfaithful without requiring additional judges. Our model and code are available at this https URL.
| Comments: | Code and model: this https URL |
| Subjects: | Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG) |
| Cite as: | arXiv:2610.34490 [cs.CL] |
| (or arXiv:2610.34490v1 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2610.34490 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Pengzhen Lin [view email]
[v1]
Sun, 25 Oct 2026 18:32:39 UTC (1,113 KB)
来源：arXiv cs.AI · arxiv.org