arXiv cs.CL· Pengzhen Lin, Ke Zhang, Maziar Raissi, Zhouxing Shi·· 12 小时前AI 评分34
面向 Lean 命题多候选答案的高效证明生成框架
Efficient Proof Generation for Lean Statements with Multiple Candidate Answers
AI 导读
研究者提出一种联合证明框架，将候选答案选择、答案补充与形式化证明生成整合为统一推理过程，训练后的证明器单次调用即可选出或提出新答案并为至少一个答案生成证明。
正文
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.CL · arxiv.org