What question did this study set out to answer?

The study aims to critique existing arguments about integrating large language models with formal specification and proof, identifying mathematical flaws.

May 15, 2026Open Access

Algorithm Almost Correctness, Almost Uselessness? A Probabilistic-Formal Synthesis for the LLM Era

Key Points

The study aims to critique existing arguments about integrating large language models with formal specification and proof, identifying mathematical flaws.
Evaluated mathematical premises of existing arguments regarding module independence and system reliability.
Proposed models for correlated failure and extended definitions for correctness.
Developed a verification framework for guarantees on LLM-generated outputs.
Identified flaws in the assumption of per-module independence affecting system reliability assessments.
Introduced a model capturing correlated failures that enhances understanding of system robustness.
Demonstrated empirically that under certain conditions, hallucination rates in AI can be controlled and reduced.

Abstract

In his Communications of the ACM article and the May 2026 ACM TechTalk Software Ver-ication in the Age of Articial Intelligence, Mey26 argues that since modern generativeAI is statistical, while professional software requires categorical correctness, the only viablefuture is a marriage of large language models (LLMs) with formal specication and proof.We endorse the directional claim but show that three of the load-bearing premises of theargument are mathematically defective. First, the Dijkstra-style compounding argumentpN, which Meyer deploys to motivate exponential decay of system reliability with modulecount, presupposes per-module independence of failure events, an assumption empiricallyrefuted by KL86 and structurally incompatible with the way modules in real systems areconstructed, deployed, and defended. Second, the binary works/useless dichotomy thatanchors the A/B/C taxonomy conates per-input total correctness in the sense of Hoa69with distributional reliability on a non-trivial input measure μ; once disambiguated, al-most correct is not only meaningful but is the dominant operating regime for the entireB class. Third, the claim that hallucinations are essential, not accidental to modern AIbegs the question by xing the generator's training objective and decoding regime; underverier-conditioned generation, hallucination rates are by construction zero relative to theverier's logic, as demonstrated empirically by Alp25, Yan+25, and SYA25. We replacethe defective scaolding with (i) a correlated-failure model with architectural fault contain-ment, (ii) a denition of ε-correctness extending Hoare logic to distributional reliability, and(iii) a conformal-verication framework that delivers nite-sample correctness guaranteeson LLM-generated artifacts. The synthesis preserves Meyer's central insight while quanti-fying the genuine open problem: the correlated stochastic verication that arises when bothspecication and implementation are generated by statistically dependent models.

Read Full Paperexternally

Mark Helpful

Bookmark

Relay

View Full Paper