用AI管道自动验证大模型数学解题，提升准确性。
Pipeline for Verifying LLM-Generated Mathematical Solutions
- 设计三类AI代理，通过特定提示生成可验证的解题格式。
- 在多个数据集上测试，误判率极低，结果可信。
- 适合研究者用于评测或生成正确数学解答。
随着大型推理模型在解决数学问题上的广泛应用，衡量其能力变得至关重要。本文提出一种自动与交互式结合的验证流程，作为目前仅检查答案这一主流方法的更准确替代方案。该流程可生成正式与非正式语言的正确解法，包含三个可选的AI代理。核心思路是通过提示工程使解题结果以特定形式输出，便于使用证明助手验证，并支持调用小模型（≤8B参数）进行辅助。在多个数据集上的实验表明，错误接受率（假阳性）极低。开源代码及服务器部署说明已发布于https://github.com/LogicEnj/lean4_verification_pipeline。
原文摘要 · Abstract (English)
With the growing popularity of Large Reasoning Models and their results in solving mathematical problems, it becomes crucial to measure their capabilities. We introduce a pipeline for both automatic and interactive verification as a more accurate alternative to only checking the answer which is currently the most popular approach for benchmarks. The pipeline can also be used as a generator of correct solutions both in formal and informal languages. 3 AI agents, which can be chosen for the benchmark accordingly, are included in the structure. The key idea is the use of prompts to obtain the solution in the specific form which allows for easier verification using proof assistants and possible use of small models ($\le 8B$). Experiments on several datasets suggest low probability of False Positives. The open-source implementation with instructions on setting up a server is available at https://github.com/LogicEnj/lean4_verification_pipeline.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。