본 논문은 AI 추론에서 강화학습(RL) 기반 방법들의 높은 계산 비용 및 시간 소모 문제를 해결하기 위해, 자동 정리 증명(ATP) 과제에 새로운 검증자-루프(verifier-in-the-loop) 설계를 제안합니다. 기존의 전체 추론 과정에 대한 피드백을 활용하는 방법과 달리, 자동 검증자를 이용하여 추론 과정의 각 단계마다 중간 피드백을 제공하는 방식입니다. Lean을 검증자로 사용하여, 단계별 지역적 검증이 모델의 추론 정확도와 효율성을 전반적으로 향상시킨다는 것을 실험적으로 보여줍니다.
