让大模型在无训练情况下，通过反馈引导探索，提升形式化定理证明成功率。
VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving
- 分两阶段搜索：先采样，再用批评者引导的MCTS利用失败信息优化
- 在miniF2F上达到40.6%正确率，比基线高3.7个百分点
- 适合需要从反馈中迭代推理证明路径的研究者
基于大模型的形式化证明系统常将丰富的验证器信号（语法错误、类型不匹配、部分目标进展）简化为二元通过/失败。我们提出VERITAS，一种零样本框架，通过双阶段协议将每条验证信号反馈回证明搜索：第一阶段进行Best-of-N采样，第二阶段采用批评者引导的MCTS，将第一阶段的失败作为显式负例。该协议保留了第一阶段独立解决的所有定理，因此第二阶段新增的解可归因于反馈驱动的探索。VERITAS在miniF2F上达到40.6%的准确率（独立运行的Best-of-5为36.9%，Portfolio为26.2%），在我们发布的55个组合数学定理的VERITAS-CombiBench上达到7.3%；而Best-of-5仅1.8%，低于Portfolio的3.6%，表明当需从验证反馈中迭代恢复正确引理名时，盲目采样会失效。代码与数据已开源。
原文摘要 · Abstract (English)
LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot framework that routes every verifier signal back into proof search through a two-phase protocol: Best-of-N sampling first, then a critic-guided MCTS pass that ingests Phase 1 failures as explicit negative examples. The protocol preserves every theorem solved by its own Phase 1 sweep, so Phase 2's additional solves are attributable to feedback-driven exploration. VERITAS reaches 40.6% on miniF2F (vs. an independently run Best-of-5 at 36.9%, Portfolio 26.2%) and 7.3% on VERITAS-CombiBench, a 55-theorem combinatorics benchmark we release on which Best-of-5 (1.8%) falls below Portfolio (3.6%), exposing that unguided sampling hurts when correct lemma names must be recovered iteratively from verifier feedback. Artifacts are available on GitHub.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。