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

arXiv: https://arxiv.org/abs/2512.02080 · HTML: https://mlsanity.com/paper/2512.02080/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 42 of its 108 references that are in the map.
- First posted on arXiv 30 Nov 2025.

## Builds on (most cited first, 30 of 42)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Distilling the Knowledge in a Neural Network](https://mlsanity.com/paper/1503.02531/) (2015)
- [QLoRA: Efficient Finetuning of Quantized LLMs](https://mlsanity.com/paper/2305.14314/) (2023)
- [Emergent Abilities of Large Language Models](https://mlsanity.com/paper/2206.07682/) (2022)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [GPTQ: Accurate Post-Training Quantization for Generative Pre-trained Transformers](https://mlsanity.com/paper/2210.17323/) (2022)
- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [SparseGPT: Massive Language Models Can Be Accurately Pruned in One-Shot](https://mlsanity.com/paper/2301.00774/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [LLMLingua: Compressing Prompts for Accelerated Inference of Large Language Models](https://mlsanity.com/paper/2310.05736/) (2023)
- [A Survey on Model Compression for Large Language Models](https://mlsanity.com/paper/2308.07633/) (2023)
- [A Survey of Machine Learning for Big Code and Naturalness](https://mlsanity.com/paper/1709.06182/) (2017)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Large Language Models as Markov Chains](https://mlsanity.com/paper/2410.02724/) (2024)
- [The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification](https://mlsanity.com/paper/2307.02192/) (2023)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Using LLMs to Facilitate Formal Verification of RTL](https://mlsanity.com/paper/2309.09437/) (2023)
- [VerifierQ: Enhancing LLM Test Time Compute with Q-Learning-based Verifiers](https://mlsanity.com/paper/2410.08048/) (2024)
- [Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints](https://mlsanity.com/paper/1601.04943/) (2016)

## Built on by (most cited first, 1 of 1)

- [Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization](https://mlsanity.com/paper/2606.09449/) (2026)

## 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.