Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912445573890048 |
|---|---|
| author | Rajaee, Sara Pratik, Kumar Cesa, Gabriele Behboodi, Arash |
| author_facet | Rajaee, Sara Pratik, Kumar Cesa, Gabriele Behboodi, Arash |
| contents | The most promising recent methods for AI reasoning require applying variants of reinforcement learning (RL) either on rolled out trajectories from the LLMs, even for the step-wise rewards, or large quantities of human-annotated trajectory data. The reliance on the rolled-out trajectory renders the compute cost and time prohibitively high. In particular, the correctness of a reasoning trajectory can typically only be judged at its completion, leading to sparse rewards in RL or requiring expensive synthetic data generation in expert iteration-like methods. In this work, we focus on the Automatic Theorem Proving (ATP) task and propose a novel verifier-in-the-loop design, which, unlike existing approaches that leverage feedback on the entire reasoning trajectory, employs an automated verifier to give intermediate feedback at each step of the reasoning process. Using Lean as the verifier, we empirically show that the step-by-step local verification produces a global improvement in the model's reasoning accuracy and efficiency. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_09730 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving Rajaee, Sara Pratik, Kumar Cesa, Gabriele Behboodi, Arash Artificial Intelligence Computation and Language Machine Learning Logic in Computer Science The most promising recent methods for AI reasoning require applying variants of reinforcement learning (RL) either on rolled out trajectories from the LLMs, even for the step-wise rewards, or large quantities of human-annotated trajectory data. The reliance on the rolled-out trajectory renders the compute cost and time prohibitively high. In particular, the correctness of a reasoning trajectory can typically only be judged at its completion, leading to sparse rewards in RL or requiring expensive synthetic data generation in expert iteration-like methods. In this work, we focus on the Automatic Theorem Proving (ATP) task and propose a novel verifier-in-the-loop design, which, unlike existing approaches that leverage feedback on the entire reasoning trajectory, employs an automated verifier to give intermediate feedback at each step of the reasoning process. Using Lean as the verifier, we empirically show that the step-by-step local verification produces a global improvement in the model's reasoning accuracy and efficiency. |
| title | Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving |
| topic | Artificial Intelligence Computation and Language Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2503.09730 |