The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
Not on the map. Why?
Abstract (arXiv)
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 for termination in multi-stage verification pipelines. We model the interaction not as a generic loop, but as a sequential absorbing Markov Chain comprising four essential engineering stages: textttCodeGen, textttCompilation, textttInvariantSynth, and textttSMTSolving. We prove that for any non-zero stage success probability (δ > 0), the system reaches the textttVerified state almost surely. Furthermore, because of the sequential nature of the pipeline, we derive a precise latency bound of mathbbE[n] ≤ 4/δ. We stress-tested this prediction in an extensive empirical campaign comprising over 90,000 trials. The results match the theory with striking consistency: every run reached verification, and the empirical convergence factor clustered tightly around Cf≈ 1.0, confirming that the 4/δ bound accurately mirrors system behavior rather than serving as a loose buffer. Based on this data, we identify three distinct operating zones -- marginal, practical, and high-performance -- and propose a dynamic calibration strategy to handle parameter drift in real-world environments. Together, these contributions replace heuristic guesswork with a rigorous architectural foundation, enabling predictable resource planning and performance budgeting for safety-critical software.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 42 of its 108 references that are in the map. First posted on arXiv 30 Nov 2025.
Builds on
42 of 108 references.
References · 42
- 2017Attention Is All You Needcited by 59,932
- 2020Language Models are Few-Shot Learnerscited by 32,199
- 2021LoRA: Low-Rank Adaptation of Large Language Modelscited by 14,084
- 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
- 2015Distilling the Knowledge in a Neural Networkcited by 10,076
- 2023QLoRA: Efficient Finetuning of Quantized LLMscited by 3,355
- 2022Emergent Abilities of Large Language Modelscited by 2,483
- 2023Code Llama: Open Foundation Models for Codecited by 2,105
- 2022GPTQ: Accurate Post-Training Quantization for Generative Pre-trained Transformerscited by 1,838
- 2022Least-to-Most Prompting Enables Complex Reasoning in Large Language Modelscited by 1,397
- 2023SparseGPT: Massive Language Models Can Be Accurately Pruned in One-Shotcited by 1,090
- 2021Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributionscited by 417
30 more
- 2023LLMLingua: Compressing Prompts for Accelerated Inference of Large Language Modelscited by 279
- 2023A Survey on Model Compression for Large Language Modelscited by 263
- 2017A Survey of Machine Learning for Big Code and Naturalnesscited by 220
- 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
- 2023A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validationcited by 91
- 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
- 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
- 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
- 2023A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verificationcited by 42
- 2024PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generationcited by 36
- 2023Finding Inductive Loop Invariants using Large Language Modelscited by 35
- 2024Large Language Models as Markov Chainscited by 33
- 2023The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verificationcited by 32
- 2024AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMscited by 30
- 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
- 2023Using LLMs to Facilitate Formal Verification of RTLcited by 17
- 2024VerifierQ: Enhancing LLM Test Time Compute with Q-Learning-based Verifierscited by 14
- 2016Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraintscited by 12
- 2023Leveraging Large Language Models for Automated Proof Synthesis in Rustcited by 11
- 2025LLM4CVE: Enabling Iterative Automated Vulnerability Repair with Large Language Modelscited by 9
- 2024How Well Do Large Language Models Serve as End-to-End Secure Code Agents for Python?cited by 7
- 2025Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overviewcited by 7
- 2025Supporting Software Formal Verification with Large Language Models: An Experimental Studycited by 6
- 2025Optimizing Singular Spectrum for Large Language Model Compressioncited by 4
- 2021Model Checking C++ Programscited by 3
- 2024Automated Repair of AI Code with Large Language Models and Formal Verificationcited by 3
- 2025When Compression Meets Model Compression: Memory-Efficient Double Compression for Large Language Modelscited by 3
- 2023ESBMC v7.3: Model Checking C++ Programs using Clang ASTcited by 1
- 2025Enhancing Large Language Model Efficiencyvia Symbolic Compression: A Formal Approach Towards Interpretabilitycited by 1
- 2025LLM For Loop Invariant Generation and Fixing: How Far Are We?cited by 1
Built on by
Citing papers per year: 2026: 1.
1 paper.