Pith. sign in

REVIEW 5 major objections 3 minor 97 references

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

T0 review · 5 major / 3 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that a four-stage absorbing Markov chain with per-stage success probability δ predicts the latency of LLM-assisted verification pipelines: the process terminates almost surely and needs 4/δ attempts on average.

desk verdict The 4/δ mean is correct but textbook; the paper's advertised exponential tail bound is false and the 90k-trial 'stress test' is circular, so the core contribution does not survive scrutiny. read the letter →

arxiv 2512.02080 v3 pith:2U3SD226 submitted 2025-11-30 cs.AI cs.FLcs.LGcs.SE

Pierre Dantas , Lucas Cordeiro , Youcheng Sun , Waldir Junior This is my paper
classification cs.AIcs.FLcs.LGcs.SE MSC 60J2068Q60
keywords formalverificationlargelanguagemodelsabsorbingMarkovchainconvergencetheoremboundedmodelcheckingSMTsolvingexpectediterationbounddynamiccalibration
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that an LLM-plus-verifier repair loop, when decomposed into the four engineering stages CodeGen, Compilation, InvariantSynth, and SMTSolving, behaves like a sequential absorbing Markov chain: at each stage the next attempt succeeds with probability δ and otherwise retries the same stage. On that model, the paper proves a convergence theorem with three parts: the system reaches the absorbing Verified state almost surely for any δ>0; the expected number of iterations starting from the first stage is exactly 4/δ; and the probability that convergence takes more than k iterations decays exponentially. The paper supports the theorem with 90,000 vectorized Monte Carlo trials across δ values from 0.1 to 0.9, reporting that every run converges and that empirical means track 4/δ with a conservative factor near 1.0. If the theorem holds for real systems, verification pipelines stop being unpredictable black boxes: engineers could budget 4/δ attempts, set timeouts from the exponential tail, and choose models based on which operating region their δ falls into.

What carries the argument

The load-bearing object is the sequential absorbing Markov chain with the canonical transition matrix P = [[Q, R], [0, I]]. Q is a 4×4 upper-triangular matrix with diagonal 1−δ and superdiagonal δ; its fundamental matrix N=(I−Q)^{-1} gives expected visits, and the geometric sojourn time M_j ∼ Geom(δ) in each stage—mean 1/δ—makes E[τ]=4/δ by linearity of expectation. The spectral radius of Q, 1−δ, is used to claim the exponential tail bound. Supporting machinery includes a vectorized Monte Carlo simulator that samples the four geometric residence times directly and a sliding-window estimator of δ for runtime calibration.

What would settle it

Compute P(τ>k) for the four-stage chain explicitly: τ is the sum of four independent Geom(δ) variables, so its survival function contains a k^3 polynomial factor alongside (1−δ)^k; if the claimed bound P(τ>k) ≤ α(1−δ)^k with a single constant α is checked numerically across all k, it fails for large k. A complementary experiment: instrument a real LLM-plus-verifier pipeline to log per-stage success rates and retry counts; if the measured δ_i differ across stages or correlate across attempts, the predicted mean 4/δ will not match.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1, the LLM-Verifier Convergence Theorem. For a five-state chain with transient states s1 through s4 and absorbing state s5 = Verified, where each attempted transition advances with probability δ and stays with probability 1−δ, the paper proves P(τ<∞)=1, E[τ | X0=s1]=4/δ, and P(τ>k) ≤ α(1−δ)^k with α=||(I−Q)^{-1}||. The proof treats the time in each stage as a geometric random variable with mean 1/δ and sums the four independent sojourn times; the tail bound uses the spectral radius of the upper-triangular transient matrix Q, whose diagonal entries are all 1−δ. The empirical campaign—10,000 trials per δ in {0.1,...,0.9}—finds 100% convergence, empirical means with

Load-bearing premise

The whole theorem depends on the assumption—stated in Section 4.1 and conceded in Sections 6.2.1 and 6.2.2—that the LLM-verifier process is a time-homogeneous absorbing Markov chain with the same constant δ at every stage and independent, memoryless retries; if real LLM behavior is non-stationary or stage-correlated, E[τ]=4/δ no longer follows.

Editorial extensions

If this is right

  • Systems modeled this way are guaranteed to terminate almost surely; no infinite oscillation between syntax errors and logical failures under the stated assumptions.
  • Expected pipeline latency is 4/δ attempts, so δ becomes a budgeting parameter rather than a guess.
  • The exponential tail gives a principled way to set timeouts: choose k so that α(1−δ)^k is below the acceptable failure probability.
  • δ thresholds define operating regions (marginal below 0.3, practical 0.3–0.6, high-performance above 0.6), guiding model selection and effort allocation.
  • Runtime monitoring of δ with a sliding window lets engineers trigger corrective actions, such as context resets or temperature changes, when performance drifts.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An analogous m-stage pipeline would have expected time m/δ, so splitting or merging verification stages is a direct design lever on latency, an implication the paper leaves implicit.
  • If per-stage success probabilities are unequal (δ1,...,δ4), the same argument gives E[τ]=Σ 1/δ_i; measuring stage-level success rates would let practitioners test whether the uniform-δ assumption matters in practice.
  • The model abstracts away token-level generation cost; converting 4/δ iterations into dollars or wall-clock time requires multiplying by per-attempt cost, a step the paper does not take.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 3 minor

Summary. The paper models LLM-verifier refinement as a four-stage absorbing Markov chain with per-stage success probability δ and states an 'LLM-Verifier Convergence Theorem' (Section 4.2): almost-sure absorption, E[τ|X0=s1]=4/δ, and an exponential tail bound P(τ>k)≤α(1−δ)^k. It reports a 90,000-trial Monte Carlo campaign, claims the empirical ratio Cf≈1.0 confirms the 4/δ bound, and proposes operational regions and dynamic calibration.

Significance. The expectation and almost-sure parts of the theorem are correct for the stated abstract chain, and the paper is clear about the model and makes its simulator code available. However, the advertised exponential tail bound is false for the paper's own chain, and the empirical campaign is circular: the simulator generates M_{i,j}∼Geom(δ) and sums four such variables, exactly the quantity whose mean the theorem computes. Consequently, the paper's central claim of a provable, empirically confirmed convergence guarantee for LLM-verifier systems is not established. The value of the contribution, if the theorem were corrected, would be modest: a standard negative-binomial calculation for a stylized four-stage retry process.

major comments (5)
  1. [§4.2, Theorem 1, Part 3] The tail bound P(τ>k|X0=s1)≤α(1−δ)^k is false for the stated chain. The proof passes from the spectral radius of Q to a norm bound, but Q is non-normal, so ρ(Q)^k does not bound ||Q^k||. In fact τ is a sum of four independent Geom(δ) variables, so P(τ>k)=∑_{n=k+1}^{∞} C(n−1,3)δ^4(1−δ)^{n−4}; this negative-binomial tail is asymptotically c_δ k^3(1−δ)^k. No finite α can dominate this polynomial factor for all k. The exact statement is a polynomial-prefactor tail, not α(1−δ)^k.
  2. [Table 8 and §6.1.4] The paper's own data contradict Part 3 of Theorem 1. At δ=0.1, Table 8 reports P99=97, so roughly 1% of trials have τ>97. With α=||(I−Q)^{−1}||=4/δ=40, the claimed bound gives 40·(0.9)^97≈1.4×10^{−3}, an order of magnitude below the observed tail. Similar checks hold at δ=0.2 (P99=47). Thus the empirical tail analysis, which is used to justify reliable timeouts, actually refutes the stated bound.
  3. [§5.2.2, Eq. (8) and §6.2.2] The empirical 'stress test' is circular. Eq. (8) samples residence times M_{i,j}∼Geom(δ) and defines T_i as their sum over four stages; Theorem 1's E[τ]=4/δ is exactly the mean of that sum. Cf≈1.0 is therefore a property of the random-number generator, not evidence about LLM-verifier systems. Section 6.2.2 concedes that only simulated behavior was tested and real API validation is future work, yet the abstract and conclusions describe conclusive support for the framework's applicability to real systems.
  4. [§3.1.3, Eq. (7)] The paper contains an internal inconsistency in the central expected value. Eq. (7) states E[n]=(4−3δ)/δ=4/δ−3 for 'the specific chain structure analyzed in this paper', while Theorem 1 and Table 8 use E[τ]=4/δ. These cannot both describe the same chain. For the chain defined in §4.1, with each of four transient states occupied for a Geom(δ) sojourn, the correct mean is 4/δ; Eq. (7) should be corrected or removed.
  5. [§4.1 and §6.2.1] The theorem's applicability to actual LLM-verifier systems depends on assumptions that are asserted but never tested: time-homogeneous per-stage success probability δ, independence of sojourns across stages, and memoryless retries. Section 6.2.1 acknowledges non-stationarity and Section 8.1 defers real API validation to future work. This would be acceptable if the paper were framed purely as an analysis of a stylized retry model, but the title, abstract, and conclusions claim guarantees for 'LLM-verifier systems' and 'formal method guarantee'. That external-validity gap is load-bearing for the paper's stated contribution.
minor comments (3)
  1. [Table 8] The first row is typeset as '0.140.000'; it should presumably be '0.1 40.000'. The header alignment should be fixed.
  2. [§5.1 and §6.1.4] The methodology repeatedly states P(n>k)∝e^{−cδk} without defining c and without reconciling this form with the theorem's α(1−δ)^k or with the negative-binomial tail acknowledged in §7.3. These three tail statements should be unified.
  3. [§5.2.3] Defining 'Success' as τ≤1000 and reporting 100% success in Table 8 is uninformative because a sum of four geometric variables with δ≥0.1 has P(τ>1000) astronomically small; this metric cannot validate or illustrate almost-sure convergence.

Circularity Check

3 steps flagged · score 8.0 of 10

Empirical 'stress test' is the theorem's own generative model: Eq. (8) samples M_i,j ~ Geom(δ) and sums four per trial, so C_f≈1.0 is forced by construction; the paper itself concedes real LLM/API validation is future work.

  1. self definitional [Section 5.2.2 (Eq. 8) vs. Section 4.2, Theorem 1 Part 2 (Eq. 4 and proof)]
    "Each element M_{i,j} represents the residence time in stage j for trial i, sampled independently from a Geometric distribution, as defined in Eq. (8). M_{i,j} ∼ Geom(δ) ∀i∈[1,N], j∈[1,4] ... The total convergence time T_i for the i-th trial is computed via row-wise summation, T_i = Σ_{j=1}^{4} M_{i,j}."

    Theorem 1 derives E[τ|X0=s1]=4/δ by writing τ=Σ_{j=1}^{4} M_j with M_j∼Geom(δ). The simulator generates exactly this: four independent Geom(δ) draws summed per trial. Therefore the empirical mean is produced by the same distributional identity the theorem states, and C_f=(4/δ)/µ≈1.0 is an artifact of the sampler rather than a test of any LLM-verifier system. The abstract calls this a 'stress-tested prediction' and Section 7.1 calls it 'decisive confirmation,' but no real system data enters the loop.

  2. self definitional [Section 7.3, RQ4 discussion]
    "The structure of the empirical data strongly confirms that the convergence time follows a Negative Binomial distribution with parameter r=4. Since a Negative Binomial(r, p) distribution describes the sum of r independent Geometric variables, this empirical fit mathematically validates our modeling assumption that the process consists of exactly four independent, sequential refinement stages."

    The empirical data were generated by Eq. (8) as row-wise sums of four independent Geom(δ) variables. A Negative Binomial fit is therefore guaranteed by the simulation construction. Citing that fit as 'mathematically validating' the four-stage independent-Geometric assumption restates the simulator's input rather than providing independent evidence for the Markovian model.

1 more flagged steps
  1. other [Section 6.2.2, External Validity]
    "Experiments use modeled behavior (sum of independent Geometric distributions); validation with real LLM and application programming interfaces (APIs) is future work."

    This is the paper's own admission that the 90,000-trial campaign was not an empirical test of real LLM-verifier pipelines. Combined with Eq. (8), it confirms that the claimed validation of E[n]≤4/δ and C_f≈1.0 is a check of the model against itself: the 'prediction' and the 'data' share the same definitional distribution. This makes the central empirical claim circular by construction.

full rationale

The theoretical derivation itself is not circular: given a four-stage absorbing Markov chain with per-stage success δ, E[τ]=4/δ follows from E[Geom(δ)]=1/δ and linearity of expectation. That conditional statement is a standard mathematical result, and the paper's Markovian modeling assumptions are at least stated explicitly. The circularity is in the validation loop. Section 5.2.2's simulator instantiates M_{i,j}∼Geom(δ) and sums four such draws per trial, which is precisely the construction Theorem 1 uses to compute E[τ]=4/δ. Hence the empirical mean, C_f≈1.0, and the Negative Binomial fit are forced by the simulator's definition; they cannot confirm that real LLM-verifier behavior follows the model. Section 6.2.2 concedes exactly this: 'validation with real LLM and APIs is future work.' The false tail bound in Theorem 1 Part 3 is a genuine mathematical error—the negative-binomial tail has a k^3(1−δ)^k factor, so no constant α suffices—but I did not count it as circularity because it is unsoundness rather than a definitional reduction. The score of 8 reflects that the paper's headline empirical confirmation is equivalent, by construction, to its own input distribution, while the underlying Markov-chain calculation itself is not circular.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The model's load-bearing input is a single fixed δ per stage, plus the Markov/stationarity assumptions. No new physical or mathematical entities are introduced. The false norm assumption in the tail bound is an ad hoc technical premise that breaks the theorem as stated.

free parameters (1)
  • δ
    Per-stage success probability; assumed identical across four stages and stationary. Not estimated from real LLM runs; swept 0.1-0.9 in simulation. The entire E=4/δ bound is inversely proportional to this one number.
assumptions (4)
  • domain assumption LLM-verifier refinement is a time-homogeneous absorbing Markov chain with exactly four transient stages and self-loop retries (CodeGen, Compilation, InvariantSynth, SMTSolving).
    Invoked in Section 4.1 to define Theorem 1; no real-system data show transitions are memoryless or that retries stay in the same stage.
  • domain assumption A single fixed success probability δ governs all four stages and remains constant over time.
    Theorem 1 states 'fixed success probability δ∈(0,1]'; Section 6.2.1 concedes non-stationarity and stage differences are future work.
  • standard math Standard absorbing Markov chain facts: absorption is almost sure when the absorbing state is reachable, and expected absorption time is N1.
    Used in Section 3.1.3 and proof of Theorem 1 Parts 1-2.
  • ad hoc to paper The transient matrix Q satisfies ||Q^k|| ≤ ρ(Q)^k = (1−δ)^k.
    Assumed in Theorem 1 Part 3 proof; false for this non-normal upper-triangular Q, whose true tail has polynomial factor k^3(1−δ)^k.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee." pith.science (2026). https://pith.science/paper/2U3SD226

@misc{pith2026251202080,
  author       = {Pith},
  title        = {Pith review of: The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2U3SD226}},
  note         = {Machine review of arXiv:2512.02080}
}
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 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: \texttt{CodeGen}, \texttt{Compilation}, \texttt{InvariantSynth}, and \texttt{SMTSolving}. We prove that for any non-zero stage success probability ($\delta > 0$), the system reaches the \texttt{Verified} state almost surely. Furthermore, because of the sequential nature of the pipeline, we derive a precise latency bound of $\mathbb{E}[n] \leq 4/\delta$. 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 $C_f\approx 1.0$, confirming that the $4/\delta$ 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.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

97 extracted references · 16 canonical work pages

  1. [1]

    Computer51(11), 14–23 (2018) https://doi.org/10.1109/mc

    Cofer, D., Gacek, A., Backes, J., Whalen, M.W., Pike, L., Foltzer, A., Podhradsky, M., Klein, G., Kuz, I., Andronick, J., Heiser, G., Stuart, D.: A Formal Approach to Construct- ing Secure Air Vehicle Software. Computer51(11), 14–23 (2018) https://doi.org/10.1109/mc. 2018.2876051

    arXiv 2018

  2. [2]

    In: 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, pp

    Hatcliff, J., King, A., Lee, I., Macdonald, A., Fernando, A., Robkin, M., Vasserman, E., Weininger, S., Goldman, J.M.: Rationale and Architecture Principles for Medical Application Platforms. In: 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, pp. 3–12. IEEE, Beijing, China (2012). https://doi.org/10.1109/iccps.2012.9

    doi:10.1109/iccps.2012.9 2012

  3. [3]

    ACM Computing Surveys52(5), 1–41 (2019) https://doi.org/10.1145/3342355

    Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal Specification and Ver- ification of Autonomous Robotic Systems: A Survey. ACM Computing Surveys52(5), 1–41 (2019) https://doi.org/10.1145/3342355

    doi:10.1145/3342355 2019

  4. [4]

    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs, pp. 193–207. Springer, Berlin, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    doi:10.1007/3-540-49059-0_14 1999

  5. [5]

    In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

    Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an Industrial-Strength C Model Checker. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. ASE’18, pp. 888–891. ACM, Manchester, UK (2018). https://doi.org/10.1145/3238147.3240481

    arXiv 2018

  6. [6]

    IEEE Transactions on Software Engineering38(4), 957–974 (2012) https://doi.org/10.1109/tse.2011.59

    Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based Bounded Model Checking for Embed- ded ANSI-C Software. IEEE Transactions on Software Engineering38(4), 957–974 (2012) https://doi.org/10.1109/tse.2011.59

    doi:10.1109/tse.2011.59 2012

  7. [7]

    Springer, Cham, Switzerland (2018)

    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Cham, Switzerland (2018). https://doi.org/10.1007/978-3-319-10575-8

    doi:10.1007/978-3-319-10575-8 2018

  8. [8]

    ACM Computing Surveys41(4), 1–36 (2009) https://doi.org/10.1145/1592434

    Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal Methods: Practice and Experience. ACM Computing Surveys41(4), 1–36 (2009) https://doi.org/10.1145/1592434. 1592436

    doi:10.1145/1592434 2009

Show all 97 references
  1. [9]

    In: Proceedings 2025 Network and Distributed System Security Symposium (2025)

    Liu, Y., Xue, Y., Wu, D., Sun, Y., Li, Y., Shi, M., Liu, Y.: PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation. In: Proceedings 2025 Network and Distributed System Security Symposium (2025). https: //doi.org/10.14722...

    2025

  2. [10]

    In: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, pp

    Pirzada, M.A.A., Reger, G., Bhayat, A., Cordeiro, L.C.: LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. In: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, pp. 1395–1407 (2024). https: //doi.org/10.1145/3...

    2024

  3. [11]

    In: 2025 IEEE/ACM International Conference on Automation of Software Test (AST), pp

    Tihanyi, N., Charalambous, Y., Jain, R., Ferrag, M.A., Cordeiro, L.C.: A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification. In: 2025 IEEE/ACM International Conference on Automation of Software Test (AST), pp. 136–147 ...

    2025

  4. [12]

    arxiv (2017)

    Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L., Polosukhin, I.: Attention Is All You Need. arxiv (2017). https://doi.org/10.48550/arxiv.1706. 03762

    2017 doi

  5. [13]

    arxiv (2022)

    Wei, J., Tay, Y., Bommasani, R., Raffel, et al.: Emergent Abilities of Large Language Models. arxiv (2022). https://doi.org/10.48550/arxiv.2206.07682 30

    2022 doi arXiv

  6. [14]

    Beckert, B., Klamroth, J., Pfeifer, W., Röper, P., Teuber, S.: Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification, pp. 242–257. Springer, Cham, Switzerland (2024). https://doi.org/10.1007/978-3-031-75387-9_15

    2024 doi

  7. [15]

    arxiv (2023)

    Huang, X., Ruan, W., Huang, W., Jin, G., Dong, et al.: A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation. arxiv (2023). https: //doi.org/10.48550/arxiv.2305.11391

    2023 doi arXiv

  8. [16]

    Neural Information Processing Systems (2024) https://doi.org/10.48550/arxiv.2406.14408

    Lin, X., Cao, Q., Huang, Y., Wang, H., Lu, J., Liu, Z., Song, L., Liang, X.: FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. Neural Information Processing Systems (2024) https://doi.org/10.48550/arxiv.2406.14408

    2024 doi arXiv

  9. [17]

    https://doi.org/10.48550/arxiv.2410.02724

    Zekri, O., Odonnat, A., Benechehab, A., Bleistein, L., Boullé, N., Redko, I.: Large Language Models as Markov Chains (2024). https://doi.org/10.48550/arxiv.2410.02724

    2024 doi arXiv

  10. [18]

    https://doi.org/10.48550/arxiv.2410.08048

    Qi, J., Tang, H., Zhu, Z.: VerifierQ: Enhancing LLM Test Time Compute with Q-Learning- based Verifiers (2024). https://doi.org/10.48550/arxiv.2410.08048

    2024 doi arXiv

  11. [19]

    Software Testing, Verification and Reliability32(1) (2021) https://doi.org/10.1002/stvr.1793

    Monteiro, F.R., Gadelha, M.R., Cordeiro, L.C.: Model Checking C++ Programs. Software Testing, Verification and Reliability32(1) (2021) https://doi.org/10.1002/stvr.1793

    2021 doi

  12. [20]

    arxiv.org (2023) https://doi.org/10.48550/arxiv.2309.09437

    Orenes-Vera, M., Martonosi, M., Wentzlaff, D.: Using LLMs to Facilitate Formal Verification of RTL. arxiv.org (2023) https://doi.org/10.48550/arxiv.2309.09437

    2023 doi arXiv

  13. [21]

    In:Proceedings of the31st ACM JointEuropean Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp

    First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: Whole-Proof Generation and Repair with Large LanguageModels. In:Proceedings of the31st ACM JointEuropean Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1229–1241 (2023). https:/...

    2023

  14. [22]

    arxiv (2024) https://doi.org/10.48550/arxiv.2406.08467

    Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M.R.H., Amin, N., Tegmark, M.: DafnyBench: A Benchmark for Formal Software Verification. arxiv (2024) https://doi.org/10.48550/arxiv.2406.08467

    2024 doi arXiv

  15. [23]

    Proceedings of the ACM on Software Engineering1, 812–835 (2024) https://doi.org/ 10.1145/3643763

    Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards AI-Assisted Synthesis of Verified Dafny Methods. Proceedings of the ACM on Software Engineering1, 812–835 (2024) https://doi.org/ 10.1145/3643763

    2024 doi

  16. [24]

    https: //doi.org/10.48550/arxiv.2201.11903

    Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E., Le, Q., Zhou, D.: Chain-of-Thought Prompting Elicits Reasoning in Large Language Models (2022). https: //doi.org/10.48550/arxiv.2201.11903

    2022 doi arXiv

  17. [25]

    arxiv (2024)

    Charalambous, Y., Manino, E., Cordeiro, L.C.: Automated Repair of AI Code with Large Language Models and Formal Verification. arxiv (2024). https://doi.org/10.48550/arxiv.2405. 08848

    2024 doi

  18. [26]

    arxiv (2025)

    Fakih, M., Dharmaji, R., Bouzidi, H., Araya, G.Q., Ogundare, O., Faruque, M.A.A.: LLM4CVE: Enabling Iterative Automated Vulnerability Repair with Large Language Models. arxiv (2025). https://doi.org/10.48550/arxiv.2501.03446

    2025 doi arXiv

  19. [27]

    arxiv.org (2025) https://doi.org/10.48550/ arxiv.2507.04857

    Wang, W., Farrell, M., Cordeiro, L.C., Zhao, L.: Supporting Software Formal Verification with Large Language Models: An Experimental Study. arxiv.org (2025) https://doi.org/10.48550/ arxiv.2507.04857

    2025 doi arXiv

  20. [28]

    Sensors 25(9), 2683 (2025) https://doi.org/10.3390/s25092683

    Deng, L., Zhong, Q., Song, J., Lei, H., Li, W.: LLM-Based Unknown Function Automated Modeling in Sensor-Driven Systems for Multi-Language Software Security Verification. Sensors 25(9), 2683 (2025) https://doi.org/10.3390/s25092683

    2025 doi

  21. [29]

    arxiv.org (2023) https://doi.org/10.48550/arxiv.2311.03739

    Yao, J., Zhou, Z., Chen, W., Cui, W.: Leveraging Large Language Models for Automated Proof 31 Synthesis in Rust. arxiv.org (2023) https://doi.org/10.48550/arxiv.2311.03739

    2023 doi arXiv

  22. [30]

    arxiv (2023)

    Jiang, H., Wu, Q., Lin, C.-Y., Yang, Y., Qiu, L.: LLMLingua: Compressing Prompts for Accel- erated Inference of Large Language Models. arxiv (2023). https://doi.org/10.48550/arxiv.2310. 05736

    2023 doi

  23. [31]

    Transactions of the Association for Computational Linguistics12, 1556–1577 (2024) https://doi.org/10.1162/tacl_a_00704

    Zhu, X., Li, J., Liu, Y., Ma, C., Wang, W.: A Survey on Model Compression for Large Language Models. Transactions of the Association for Computational Linguistics12, 1556–1577 (2024) https://doi.org/10.1162/tacl_a_00704

    2024 doi

  24. [32]

    In: Findings of the Association for Computational Linguistics: EMNLP 2024, pp

    Wang, W., Mao, Y., Dongdong, T., Hongchao, D., Guan, N., Xue, C.J.: When Compression Meets Model Compression: Memory-Efficient Double Compression for Large Language Models. In: Findings of the Association for Computational Linguistics: EMNLP 2024, pp. 16973–16983. Association ...

    2024

  25. [33]

    Applied Intelligence54(22), 11804–11844(2024) https://doi.org/10.1007/s10489-024-05747-w

    Dantas, P.V., Silva, W., Cordeiro, L.C., Carvalho, C.B.: A Comprehensive Review of Model Compression Techniques in Machine Learning. Applied Intelligence54(22), 11804–11844(2024) https://doi.org/10.1007/s10489-024-05747-w

    2024 doi

  26. [34]

    ACM Computing Surveys57(10), 1–39 (2025) https: //doi.org/10.1145/3728636

    Kim, G.I., Hwang, S., Jang, B.: Efficient Compressing and Tuning Methods for Large Language Models: A Systematic Literature Review. ACM Computing Surveys57(10), 1–39 (2025) https: //doi.org/10.1145/3728636

    2025 doi

  27. [35]

    Scientific Reports15(1) (2025) https://doi.org/10.1038/ s41598-025-92586-5

    Belhaouari, S.B., Kraidia, I.: Efficient Self-attention with Smart Pruning for Sustain- able Large Language Models. Scientific Reports15(1) (2025) https://doi.org/10.1038/ s41598-025-92586-5

    2025

  28. [36]

    https://doi.org/10.48550/arxiv.2502.15092

    Li, D., Shen, T., Zhou, Y., Yang, B., Liu, Z., Yang, M., Ghanem, B., Yang, Y., Zhong, Y., Yang, M.-H.: Optimizing Singular Spectrum for Large Language Model Compression (2025). https://doi.org/10.48550/arxiv.2502.15092

    2025 doi arXiv

  29. [37]

    Complex & Intelligent Systems11(9) (2025) https://doi.org/ 10.1007/s40747-025-02019-z

    Dantas, P.V., Cordeiro, L.C., Junior, W.S.S.: A Review of State-of-the-art Techniques for Large Language Model Compression. Complex & Intelligent Systems11(9) (2025) https://doi.org/ 10.1007/s40747-025-02019-z

    2025 doi

  30. [38]

    arxiv (2025)

    Tihanyi, N., Bisztray, T., Ferrag, M.A., Cherif, B., Dubniczky, R.A., Jain, R., Cordeiro, L.C.: Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview. arxiv (2025). https://doi.org/10.48550/arxiv.2503. 10784

    2025 doi

  31. [39]

    https://doi.org/10.48550/arxiv.2310.04870

    Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating Large Language Models in Automated Program Verification (2023). https://doi.org/10.48550/arxiv.2310.04870

    2023 doi arXiv

  32. [40]

    https://doi.org/10.48550/arxiv.2501.18657

    AI, L., School, T.N..M., Ji, S., Song, Z., Zhong, F., Jia, J., Wu, Z., Cao, Z., Xu, T.: Enhanc- ing Large Language Model Efficiencyvia Symbolic Compression: A Formal Approach Towards Interpretability (2025). https://doi.org/10.48550/arxiv.2501.18657

    2025 doi arXiv

  33. [41]

    Proceedings of the AAAI Conference on Artificial Intelligence28(1) (2014) https://doi.org/ 10.1609/aaai.v28i1.8843

    Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Designing Fast Absorbing Markov Chains. Proceedings of the AAAI Conference on Artificial Intelligence28(1) (2014) https://doi.org/ 10.1609/aaai.v28i1.8843

    2014 doi

  34. [42]

    Health Economics11(1), 33–42 (2002) https://doi.org/10.1002/hec.654

    Craig, B.A., Sendi, P.P.: Estimation of the Transition Matrix of a Discrete-Time Markov Chain. Health Economics11(1), 33–42 (2002) https://doi.org/10.1002/hec.654

    2002 doi

  35. [43]

    Clarke, E.M.: Model Checking, pp. 54–56. Springer, Berlin, Heidelberg, Germany (1997). https: //doi.org/10.1007/bfb0058022 32

    1997 doi

  36. [44]

    arxiv (2022) https://doi.org/10.48550/arxiv.2205.10625

    Zhou,D.,Schärli,N.,Hou,L.,Wei,J.,Scales,N.,Wang,X.,Schuurmans,D.,Cui,C.,Bousquet, O., Le, Q., Chi, E.: Least-to-Most Prompting Enables Complex Reasoning in Large Language Models. arxiv (2022) https://doi.org/10.48550/arxiv.2205.10625

    2022 doi arXiv

  37. [45]

    In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

    Staton, S., Yang, H., Wood, F., Heunen, C., Kammar, O.: Semantics for Probabilistic Program- ming: Higher-order Functions, Continuous Distributions, and Soft Constraints. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. LICS’16, pp. 525–534. ...

    2016

  38. [46]

    Communications of the ACM59(7), 107–115 (2016) https://doi.org/10.1145/2936726

    Gogate, V., Domingos, P.: Probabilistic theorem proving. Communications of the ACM59(7), 107–115 (2016) https://doi.org/10.1145/2936726

    2016 doi

  39. [47]

    Springer, Berlin, Heidelberg, Germany (2016)

    Kroening, D., Strichman, O.: Decision Procedures. Springer, Berlin, Heidelberg, Germany (2016). https://doi.org/10.1007/978-3-662-50497-0

    2016 doi

  40. [48]

    Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs, pp. 168–176. Springer, Berlin, Heidelberg, Germany (2004). https://doi.org/10.1007/978-3-540-24730-2_15

    2004 doi

  41. [49]

    Communications of the ACM9(5), 366–371 (1966) https://doi.org/10.1145/ 355592.365646

    Böhm, C., Jacopini, G.: Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules. Communications of the ACM9(5), 366–371 (1966) https://doi.org/10.1145/ 355592.365646

    1966

  42. [50]

    Rozier, K.Y., Dureja, R., Irfan, A., Johannsen, C., Nukala, K., Shankar, N., Tinelli, C., Vardi, M.Y.: MoXI: An Intermediate Language for Symbolic Model Checking, pp. 26–46. Springer, Cham, Switzerland (2024). https://doi.org/10.1007/978-3-031-66149-5_2

    2024 doi

  43. [51]

    Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branch- ing Time Temporal Logic, pp. 52–71. Springer, Berlin, Heidelberg, Germany (1982). https: //doi.org/10.1007/bfb0025774

    1982 doi

  44. [52]

    Clarke, E.M.: The Birth of Model Checking, pp. 1–26. Springer, Berlin, Heidelberg, Germany (2008). https://doi.org/10.1007/978-3-540-69850-0_1

    2008 doi

  45. [53]

    In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp

    Pnueli, A.: The Temporal Logic of Programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46–57. IEEE, Providence, RI, USA (1977). https://doi.org/ 10.1109/sfcs.1977.32

    1977 doi

  46. [54]

    Sometimes

    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: on Branching versus Linear Time (Preliminary Report). In: Proceedings of the 10th ACM SIGACT-SIGPLAN Sym- posium on Principles of Programming Languages - POPL’83. POPL’83, pp. 127–140. ACM Press, New York, NY...

    1983

  47. [55]

    Proceedings of the IEEE103(11), 2021–2035 (2015) https://doi.org/10

    Vizel, Y., Weissenbacher, G., Malik, S.: Boolean Satisfiability Solvers and Their Applications in Model Checking. Proceedings of the IEEE103(11), 2021–2035 (2015) https://doi.org/10. 1109/jproc.2015.2455034

    2021

  48. [56]

    IEEE Transactions on ComputersC–35(8), 677–691 (1986) https://doi.org/10.1109/tc.1986.1676819

    Bryant: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on ComputersC–35(8), 677–691 (1986) https://doi.org/10.1109/tc.1986.1676819

    1986

  49. [57]

    Formal Methods in System Design19(1), 7–34 (2001) https://doi.org/10.1023/a: 1011276507260

    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design19(1), 7–34 (2001) https://doi.org/10.1023/a: 1011276507260

    2001 doi

  50. [58]

    Menezes, R.S., Aldughaim, M., Farias,et al.: ESBMC v7.4: Harnessing the Power of Intervals: (Competition Contribution), pp. 376–380. Springer, Luxembourg City, Luxembourg (2024). https://doi.org/10.1007/978-3-031-57256-2_24

    2024 doi

  51. [59]

    Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model Checking and the State Explosion 33 Problem, pp. 1–30. Springer, Berlin, Heidelberg, Germany (2012). https://doi.org/10.1007/ 978-3-642-35746-6_1

    2012

  52. [60]

    In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp

    Dhaussy, P., Roger, J.-C., Boniol, F.: Reducing State Explosion with Context Modeling for Model-Checking. In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp. 130–137. IEEE, Boca Raton, FL, USA (2011). https://doi.org/10.1109/hase. 2011.24

    2011 doi

  53. [61]

    Mukherjee, R., Tautschnig, M., Kroening, D.: v2c – A Verilog to C Translator, pp. 580–586. Springer, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_38

    2016 doi

  54. [62]

    Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software Verification Using k-Induction, pp. 351–368. Springer, Berlin, Heidelberg (2011). https://doi.org/10.1007/ 978-3-642-23702-7_26

    2011

  55. [63]

    Barrett, C., Tinelli, C.: Satisfiability Modulo Theories, pp. 305–343. Springer, Cham, Switzer- land (2018). https://doi.org/10.1007/978-3-319-10575-8_11

    2018 doi

  56. [64]

    In: 2011 Brazilian Symposium on Computing System Engineering, pp

    Barreto, R., Cordeiro, L., Fischer, B.: Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker. In: 2011 Brazilian Symposium on Computing System Engineering, pp. 46–52. IEEE, Los Alamitos, CA, USA (2011). https://doi.org/10. 1109/sbesc.2011.19

    2011

  57. [65]

    Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, pp. 174–177. Springer, Berlin, Heidelberg, Germany (2009). https://doi.org/10.1007/ 978-3-642-00768-2_16

    2009

  58. [66]

    In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp

    Ho, Y.-S., Chauhan, P., Roy, P., Mishchenko, A., Brayton, R.: Efficient Uninterpreted Function Abstraction and Refinement for Word-Level Model Checking. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 65–72. IEEE, Mountain View, CA, USA (2016). https: //doi.org/1...

    2016

  59. [67]

    Electronic Notes in Theoretical Computer Science75, 95–113 (2003) https://doi.org/10.1016/s1571-0661(04)80781-3

    Tabuchi, N., Sumii, E., Yonezawa, A.: Regular Expression Types for Strings in a Text Processing Language. Electronic Notes in Theoretical Computer Science75, 95–113 (2003) https://doi.org/10.1016/s1571-0661(04)80781-3

    2003 doi

  60. [68]

    arxiv (2020) https://doi.org/10.48550/arxiv.2005.14165

    Brown, T.B., Mann, B., Ryder, N., Subbiah, M., Kaplan,et al.: Language Models are Few-Shot Learners. arxiv (2020) https://doi.org/10.48550/arxiv.2005.14165

    2020 doi arXiv

  61. [69]

    Pearce, H., Ahmad, B., Tan, B., Dolan-Gavitt, B., Karri, R.: Asleep at the Keyboard? Assess- ing the Security of GitHub Copilot’s Code Contributions, vol. 68, pp. 96–105. Association for Computing Machinery (ACM), San Francisco, CA, USA (2025). https://doi.org/10.1145/ 3610721

    2025

  62. [70]

    Zheng, S., Huang, C., Yu, F., Yao, J., Ye, J., Chen, T., Luo, Y., Ding, N., BAI, L., Cui, G., Ye, P.: SCI-Verifier: Scientific Verifier with Thinking (2025) https://doi.org/10.48550/arxiv.2509. 24285

    2025 doi

  63. [71]

    ACM Computing Surveys51(4), 1–37 (2018) https://doi.org/10.1145/ 3212695

    Allamanis, M., Barr, E.T., Devanbu, P., Sutton, C.: A Survey of Machine Learning for Big Code and Naturalness. ACM Computing Surveys51(4), 1–37 (2018) https://doi.org/10.1145/ 3212695

    2018

  64. [73]

    In: 2023 IEEE/ACM 45th International 34 Conference on Software Engineering (ICSE), pp

    Lemieux, C., Inala, J.P., Lahiri, S.K., Sen, S.: CodaMosa: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models. In: 2023 IEEE/ACM 45th International 34 Conference on Software Engineering (ICSE), pp. 919–931. IEEE, Melbourne, VIC, Australia (202...

    2023

  65. [74]

    arxiv (2022) https://doi.org/10.48550/arxiv

    Frantar, E., Ashkboos, S., Hoefler, T., Alistarh, D.: GPTQ: Accurate Post-Training Quanti- zation for Generative Pre-trained Transformers. arxiv (2022) https://doi.org/10.48550/arxiv. 2210.17323

    2022 doi arXiv

  66. [75]

    arxiv (2023) https://doi.org/10.48550/arxiv.2305.14314

    Dettmers, T., Pagnoni, A., Holtzman, A., Zettlemoyer, L.: QLoRA: Efficient Finetuning of Quantized LLMs. arxiv (2023) https://doi.org/10.48550/arxiv.2305.14314

    2023 doi arXiv

  67. [76]

    arxiv (2023) https://doi.org/10.48550/arxiv.2301.00774

    Frantar, E., Alistarh, D.: SparseGPT: Massive Language Models Can Be Accurately Pruned in One-Shot. arxiv (2023) https://doi.org/10.48550/arxiv.2301.00774

    2023 doi arXiv

  68. [77]

    arxiv (2015) https://doi.org/10.48550/arxiv.1503.02531

    Hinton, G., Vinyals, O., Dean, J.: Distilling the Knowledge in a Neural Network. arxiv (2015) https://doi.org/10.48550/arxiv.1503.02531

    2015 doi arXiv

  69. [78]

    arxiv (2021) https://doi.org/10.48550/arxiv

    Hu, E.J., Shen, Y., Wallis, P., Allen-Zhu, Z., Li, Y., Wang, S., Wang, L., Chen, W.: LoRA: Low-Rank Adaptation of Large Language Models. arxiv (2021) https://doi.org/10.48550/arxiv. 2106.09685

    2021 doi arXiv

  70. [79]

    In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis

    Brauße, F., Shmarov, F., Menezes, R., Gadelha, M.R., Korovin, K., Reger, G., Cordeiro, L.C.: ESBMC-CHERI: Towards Verification of C programs for CHERI Platforms with ESBMC. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA’...

    2022

  71. [80]

    Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver, pp. 337–340. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    2008 doi

  72. [81]

    In: International Conference on Predictive Models in Software Engineering (2023)

    Tihanyi, N., Bisztray, T., Jain, R., Ferrag, M.A., Cordeiro, L., Mavroeidis, V.: The For- mAI Dataset: Generative AI in Software Security through the Lens of Formal Verification. In: International Conference on Predictive Models in Software Engineering (2023). https: //doi.org...

    2023

  73. [82]

    https://doi.org/10.48550/arxiv.2308.05649

    Song, K., Gadelha, M.R., Brauße, F., Menezes, R.S., Cordeiro, L.C.: ESBMC v7.3: Model Checking C++ Programs using Clang AST (2023). https://doi.org/10.48550/arxiv.2308.05649

    2023 doi arXiv

  74. [83]

    International Journal on Software Tools for Technology Transfer23(6), 857–861 (2020) https://doi.org/10.1007/s10009-020-00571-2

    Gadelha, M.R., Menezes, R.S., Cordeiro, L.C.: ESBMC 6.1: Automated Test Case Genera- tion Using Bounded Model Checking. International Journal on Software Tools for Technology Transfer23(6), 857–861 (2020) https://doi.org/10.1007/s10009-020-00571-2

    2020 doi

  75. [84]

    https://doi.org/10.48550/ arxiv.2408.10495

    Gong,J.,Duan,N.,Tao,Z.,Gong,Z.,Yuan,Y.,Huang,M.:HowWellDoLargeLanguageMod- els Serve as End-to-End Secure Code Agents for Python? (2024). https://doi.org/10.48550/ arxiv.2408.10495

    2024 doi arXiv

  76. [85]

    https://doi.org/10.48550/arxiv.2511.06552

    Akhond, M.R., Chakraborty, S., Uddin, G.: LLM For Loop Invariant Generation and Fixing: How Far Are We? (2025). https://doi.org/10.48550/arxiv.2511.06552

    2025 doi

  77. [86]

    https://doi.org/10.48550/arxiv.2311.07948

    Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding Inductive Loop Invariants using Large Language Models (2023). https://doi.org/10.48550/arxiv.2311.07948

    2023 doi arXiv

  78. [87]

    In: Proceedings of the 30th Asia and South Pacific Design Automation Conference

    Yan, Z., Fang, W., Li, M., Li, M., Liu, S., Xie, Z., Zhang, H.: AssertLLM: Generating Hard- ware Verification Assertions from Design Specifications via Multi-LLMs. In: Proceedings of the 30th Asia and South Pacific Design Automation Conference. ASPDAC’25, pp. 614–621. ACM, Tok...

    2025

  79. [88]

    Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.-C., Tian, C.: Enchanting 35 Program Specification Synthesis by Large Language Models Using Static Analysis and Pro- gram Verification, pp. 302–328. Springer, Cham, Switzerland (2024). https://doi.org/10.1007...

    2024

  80. [89]

    Routledge, New York, NY (2013)

    Cohen, J.: Statistical Power Analysis for the Behavioral Sciences. Routledge, New York, NY (2013). https://doi.org/10.4324/9780203771587

    2013 doi

  81. [90]

    Springer, New York, NY (2010)

    Robert, C., Casella, G.: Introducing Monte Carlo Methods with R. Springer, New York, NY (2010). https://doi.org/10.1007/978-1-4419-1576-4

    2010 doi

  82. [91]

    The American Statistician52(2), 119–126 (1998) https://doi.org/10.1080/ 00031305.1998.10480550

    Agresti, A., Coull, B.A.: Approximate is Better than “Exact” for Interval Estimation of Bino- mial Proportions. The American Statistician52(2), 119–126 (1998) https://doi.org/10.1080/ 00031305.1998.10480550

    1998 arXiv

  83. [92]

    Statistical Science16(2) (2001) https://doi.org/10.1214/ss/1009213286

    Brown, L.D., Cai, T.T., DasGupta, A.: Interval Estimation for a Binomial Proportion. Statistical Science16(2) (2001) https://doi.org/10.1214/ss/1009213286

    2001

  84. [93]

    Oxford University Press, Oxford, UK (2013)

    Boucheron, S., Lugosi, G., Massart, P.: Concentration Inequalities: A Nonasymptotic Theory of Independence. Oxford University Press, Oxford, UK (2013). https://doi.org/10.1093/acprof: oso/9780199535255.001.0001

    2013

  85. [94]

    Quantitative Finance20(10), 1591–1594 (2020) https://doi.org/10.1080/ 14697688.2020.1813475

    Papaspiliopoulos, O.: High-Dimensional Probability: An Introduction with Applications in Data Science. Quantitative Finance20(10), 1591–1594 (2020) https://doi.org/10.1080/ 14697688.2020.1813475

    2020

  86. [95]

    Technometrics39(3), 338–338 (1997) https://doi.org/10.1080/00401706.1997.10485133

    Wasserstein, R.L.: Monte Carlo: Concepts, Algorithms, and Applications. Technometrics39(3), 338–338 (1997) https://doi.org/10.1080/00401706.1997.10485133

    1997

  87. [96]

    Cambridge University Press, Cambridge, UK (2019)

    Durrett, R.: Probability: Theory and Examples. Cambridge University Press, Cambridge, UK (2019). https://doi.org/10.1017/9781108591034

    2019 doi

  88. [97]

    https://doi.org/10.48550/ARXIV.2308.12950

    Rozière, B., Gehring, J., Gloeckle, et al.: Code Llama: Open Foundation Models for Code (2023). https://doi.org/10.48550/ARXIV.2308.12950

    2023 doi arXiv

  89. [98]

    Foun- dations and Trends®in Theoretical Computer Science1(3), 237–354 (2006) https://doi.org/ 10.1561/0400000003 36

    Montenegro, R., Tetali, P.: Mathematical Aspects of Mixing Times in Markov Chains. Foun- dations and Trends®in Theoretical Computer Science1(3), 237–354 (2006) https://doi.org/ 10.1561/0400000003 36

    2006 doi

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.