基于循环验证器的局部前瞻引导用于自动定理证明
人工智能
2025-06-25 v2 计算与语言
机器学习
计算机科学中的逻辑
摘要
AI推理中最具前景的近期方法需要在大语言模型（LLM）展开的轨迹上应用强化学习（RL）的变体，即使对于逐步奖励也是如此，或者需要大量人工标注的轨迹数据。对展开轨迹的依赖使得计算成本和时间高得难以承受。特别地，推理轨迹的正确性通常只能在其完成时才能判断，这导致RL中的稀疏奖励，或在专家迭代类方法中需要昂贵的合成数据生成。在本工作中，我们聚焦于自动定理证明（ATP）任务，并提出了一种新颖的循环验证器设计，与现有利用整个推理轨迹反馈的方法不同，该设计采用自动验证器在推理过程的每一步提供中间反馈。使用Lean作为验证器，我们通过实证表明逐步局部验证产生了模型推理准确性和效率的全局提升。
引用
@article{arxiv.2503.09730,
title = {Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving},
author = {Sara Rajaee and Kumar Pratik and Gabriele Cesa and Arash Behboodi},
journal= {arXiv preprint arXiv:2503.09730},
year = {2025}
}
备注
Accepted at the Findings of ACL 2025, Accepted at ICLR 2025 Workshop on Reasoning and Planning for Large Language Models