VERITAS：用于零样本形式化定理证明的验证器引导式证明搜索

基于大语言模型的形式化证明器常将丰富的验证器信号简化为二元结果。本文提出 VERITAS，一种零样本框架，通过两阶段协议将验证器信号反馈至证明搜索：先进行 Best-of-N 采样，再利用批评者引导的蒙特卡洛树搜索（MCTS）将第一阶段失败案例作为负例。该方法在 miniF2F 基准上达到 40.6% 准确率，并在新发布的组合数学基准上显著优于无引导采样，证明了利用验证器反馈进行迭代探索对复杂逻辑推理的有效性。