arXiv · NLP· Pengzhen Lin, Ke Zhang, Maziar Raissi, Zhouxing Shi·· 3 小时前AI 评分34
针对 Lean 4 语句多候选答案的高效证明生成框架
Efficient Proof Generation for Lean Statements with Multiple Candidate Answers
AI 导读
提出一种联合证明框架，将答案选择、补充与形式化证明生成整合为统一流程。 该框架在单次调用中为至少一个答案生成可验证证明，并可复用证明检测语义忠实性错误。 在 MATH-500、AMC 2023 及 AIME 等基准上，该框架以约 1/6 的 token 成本达到与逐个候选证明相同的成功率为，并识别出至少 6.1% 的未忠实形式化语句。
来源：arXiv · NLP · arxiv.org