Researchers prove LLM-verifier systems always terminate using 4/δ latency bound; 90,000 trials confirm Markov Chain model ensures reliable software verification for safety-critical applications.

The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

View PDF HTML (experimental) Abstract:The integration of Formal Verification tools with Large Language Models (LLMs) offers a path to scale software verification beyond manual workflows. However, current methods remain unreliable: without a solid theoretical footing, the refinement process acts as a black box that may oscillate, loop, or diverge. This work bridges this critical gap by developing an LLM-Verifier Convergence Theorem, providing the first formal framework with provable guarantees fo...