验证 LLM 生成数学解答的流水线

随着大型推理模型日益流行及其在解决数学问题上的成果，衡量其能力变得至关重要。我们提出一个支持自动与交互式验证的流水线，作为仅核对答案（目前基准测试最流行的做法）的更准确替代方案。该流水线还可用作形式语言与非形式语言下正确解答的生成器。其结构中包含 3 个可按基准需求选择的 AI 智能体。关键思想是使用提示获得特定形式的解答，从而便于用证明助手验证，并可能使用小模型（≤8B）。在多个数据集上的实验表明误报概率很低。开源实现及服务器搭建说明见 https://github.com/LogicEnj/lean4_verification_pipeline。