LLM과 형식 검증 도구의 결합을 통해 소프트웨어 검증을 확장하는 아이디어는 있지만, 현재 방법은 신뢰성이 부족하다. 본 연구는 LLM-Verifier 수렴 정리(LLM-Verifier Convergence Theorem)를 개발하여 종료 및 수렴에 대한 증명 가능한 보장을 제공하는 최초의 공식 프레임워크를 제공하여 이러한 문제를 해결한다. LLM과 검증기의 상호 작용을 오류 감소 확률($\delta$)에 의해 결정되는 상태 전환을 갖는 이산 시간 마르코프 체인으로 모델링한다. 검증된 상태에 도달하는 절차는 $\delta > 0$에 대해 거의 확실하게 프로그램이 종료됨을 보여주며, 예상 반복 횟수는 $\mathbb{E}[n] \leq 4/\delta$로 제한된다. 90,000회 이상의 실험을 통해 이 예측을 검증했으며, 실험 결과는 이론과 일치했고 모든 실행에서 검증에 도달했다. 결과적으로, 워크플로우를 marginal, practical, high-performance의 세 가지 운영 영역으로 나누는 것이 가능하다.
