Logic-gated AI and the stochastic frontier

Executive summary

The strongest version of the logic-gated AI argument is partly right. Large language models generate outputs through statistical inference, while formal methods can prove properties of a precisely specified artefact. That distinction matters in safety-critical work. It does not, however, establish that a universal logic-gated replacement for frontier models exists, or that a one-change artefact demonstration by itself proves a model lacks understanding.

The evidence supports a layered conclusion. Use probabilistic models for broad interpretation and generation. Use schemas, type systems, external tools, tests and formal verification where the domain and risk justify them. The practical boundary is not "stochastic versus deterministic" in the abstract. It is which parts of a system can be specified, checked and kept within a tractable state space.

The claim, stated fairly

The position examined here makes several linked claims. Transformer-based language models are stochastic and do not contain a general SAT or SMT solver. Reasoning layers added above the model are said to be too far from the system's foundation to provide dependable guarantees. A proposed diagnostic is to ask a model to create an artefact and then change exactly one named property while preserving everything else. If the result drifts, the argument says, the model lacks repeatable artefact construction. The proposed alternative is to logic-gate domains with semantic systems, knowledge graphs and formal constraints, while accepting that exhaustive reasoning is feasible only in bounded domains.

That is a serious engineering argument, but it combines four different questions: how text is sampled, whether an artefact is edited locally, whether an output is semantically correct, and whether a system can be formally verified. Those questions must be separated, because the evidence for each is different and the answers do not transfer between them.

What the evidence shows

1. Generation is not the same thing as verification

At non-zero temperature, token sampling is an explicit source of variation. Even at temperature zero, serving infrastructure can remain non-bit-reproducible, because small numerical differences can change the selected token when competing logits are close.

Two studies bear on this directly. Atil and colleagues tested five models across eight tasks over ten runs under settings expected to be deterministic, and reported accuracy variations of up to 15 per cent across naturally occurring runs, concluding that none of the models consistently delivered repeatable accuracy, "much less identical output strings". Yuan and colleagues traced a mechanism: floating-point arithmetic is non-associative under limited precision, so evaluation batch size, GPU count and GPU version change results. They measured up to 9 per cent variation in accuracy and a 9,000 token difference in response length under bfloat16 from those factors alone.

These findings support a narrower claim than the original argument needs: identical prompts do not guarantee identical text under every production configuration. They do not, by themselves, prove that a model cannot perform a localised edit.

A genuine edit-consistency test needs a fixed artefact, a precisely named field or span to change, a preservation rule for all other content, repeated trials, and an independent structural diff. Without those controls, a changed wrapper, formatting choice or regenerated section could be generation variance rather than edit drift. The fleet test conducted during this research did not produce a valid cross-model comparison, because the two agents involved turned out to be running the same model. Its raw evidence is therefore not treated as settled here, and no claim about it is made.

That test did produce one operational finding worth stating plainly. When agents were asked which model was executing them, their answers could not be relied upon, and the platform's own execution ledger contradicted them. A model's self-report is not evidence about the system running it. That information belongs in the execution record, written by the infrastructure rather than by the model. This is a small result, but it is the same shape as the larger argument: verification has to live outside the thing being verified.

2. Formal methods work when the object and property are specified

Formal verification is not a branding layer added to a general conversation. It is a proof or decision procedure applied to a formal model, program, specification or constrained output. SAT and SMT solvers are powerful precisely because they operate over defined representations and properties. Their usefulness does not require a language model to contain the solver internally. A model can propose a candidate, and an external solver can reject it or certify a property.

The research record contains mature examples. The seL4 project reports a mathematical proof that a specified kernel implementation satisfies a functional-correctness property, while also documenting the scope and assumptions of that proof. This is strong evidence for domain-scoped assurance, not evidence that every system can be made fully proof-producing at reasonable cost.

Theorem-proving research illustrates the same pattern. HyperTree Proof Search reported 65.4 per cent accuracy on a held-out Metamath set for a model trained on annotated proofs, against a previous state of the art of 56.5 per cent, with online training on unproved theorems raising that to 82.6 per cent. On the Lean-based miniF2F-curriculum dataset the same work improved the state of the art from 31 per cent to 42 per cent.

DeepSeek-Prover reported 46.3 per cent whole-proof generation accuracy with 64 samples on the Lean 4 miniF2F test, and 52 per cent cumulatively, against 23.0 per cent for GPT-4 at the same sample count and 41.0 per cent for a tree-search reinforcement learning method. On the Lean 4 Formalized International Mathematical Olympiad benchmark it proved 5 of 148 problems, where GPT-4 proved none.

Those are meaningful advances, and the comparative margins are real. They are also benchmark results for proof search in formal languages, not a general guarantee of correct reasoning in open-ended work. A system that proves 46 per cent of competition problems is not thereby a system that can be trusted to preserve every unstated invariant in an arbitrary document.

3. General exhaustive logic is constrained by the problem, not by rhetoric

The intuition behind the tractability claim is sound but needs precision. Many verification and satisfiability problems have worst-case complexity that grows rapidly with the size of the model, and non-trivial semantic properties of arbitrary programs are undecidable in the general case. In practice, engineers obtain useful guarantees by restricting the language, decomposing the system, using abstractions, accepting conservative approximations and proving only selected properties.

That is why industrial assurance programs are scoped. seL4 verifies a defined kernel against defined specifications. DO-178C is a software assurance and certification framework for airborne systems, not a promise that every possible behaviour of arbitrary software is exhaustively proved. The practical lesson is not that formal methods fail. It is that assurance depends on boundaries, assumptions and cost.

4. Knowledge graphs improve grounding, not truth by magic

Graph-based retrieval can help a system organise entities, relationships and higher-level summaries. Microsoft Research's GraphRAG work describes a pipeline combining text extraction, network analysis and LLM prompting, and reports comparative improvements on its evaluation tasks. The project documentation also warns that using GraphRAG out of the box may not produce the best results.

That is the right interpretation. A graph can make provenance and relationships more explicit, but extraction errors, incomplete source material, incorrect edges and poor query decomposition remain possible. A graph is a structured evidence layer, not a proof that every generated conclusion is true.

5. The strongest counter-argument is architectural, not philosophical

A frontier model does not need to be deterministic internally to participate in a reliable system. Structured output contracts can reject malformed responses. A compiler, type checker, test suite, SAT or SMT solver, proof assistant or policy engine can validate a proposed result. Multiple samples and test-time selection can improve empirical performance, although they do not turn a probabilistic proposal into a proof.

This produces a hybrid architecture. Probabilistic components search a large space, and deterministic components constrain, test or verify the parts for which a formal property has been defined. The approach is less rhetorically pure than replacing the model, but it aligns with what the evidence actually demonstrates.

Where the logic-gated position holds

The position holds most strongly in bounded domains with stable semantics, high consequence of error and a manageable verification surface. Examples include portions of kernels, cryptographic components, hardware blocks, safety monitors, restricted programming languages and rule engines. In these settings, a model can assist with specification, code or proof search, while an independent checker remains authoritative.

It also holds as an architectural warning. A system that lets a stochastic generator directly perform irreversible actions without validation, authority boundaries or receipts is relying on a capability that has not been proved. External governance can contain the consequences of error, but containment is not correctness.

Where it is overstated

The available evidence does not establish that all useful AI must be logic-gated, that semantic systems and knowledge graphs can make arbitrary domains fully formal, or that a single artefact-edit failure demonstrates an absence of understanding. Nor does it support treating formal verification as a universal substitute for broad language understanding, open-world retrieval or exploratory generation.

Attribution is also unresolved. This research could not verify the identity of the speaker who advanced the position, the organisation behind the claimed "GS system", or the meaning and implementation of "Diff" as used in that argument. Those terms are not presented here as established products or technologies, and no claim in this article rests on them.

Several quantitative claims in the initial research report were excluded from this article because their primary sources could not be independently verified. The same rule applies to claimed commercial products, funding figures and future-dated benchmarks. A source list is not evidence unless the source exists and supports the specific proposition attributed to it.

What remains open

The most useful unresolved experiment is a controlled, harness-recorded edit-consistency benchmark. It should use at least two genuinely different model pins, record provider and model identity from the execution ledger rather than from agent self-report, preserve the exact prompt pair, compare complete before and after artefacts structurally, and repeat across temperature, infrastructure and task types. It should separate formatting drift, wrapper drift, semantic drift and outright failure to make the requested edit.

A second open question is economic. Formal assurance can be valuable without being universal, but the cost depends on the domain, specification quality, toolchain, proof obligations, maintenance burden and certification target. Public evidence is stronger for research prototypes and bounded systems than for a general commercial market in fully logic-gated AI.

What would falsify this analysis

This analysis would be weakened by replicated evidence that a broadly applicable logic-gated architecture can maintain formally specified correctness across open-ended domains at materially lower cost and latency than hybrid alternatives, while also matching their breadth.

It would also be weakened by a controlled, independently logged edit benchmark showing that frontier models reliably preserve all non-target content across varied artefacts and deployment conditions, removing the practical need for external structural checks.

Conversely, a localised edit failure alone would not falsify the broader case for probabilistic models. It would establish only a property of that system, that task and that harness.

Sources

Every figure quoted above was checked against the primary source listed here on 11 August 2026. Where a number appears in this article, it appears in the cited paper's own abstract in the form given.

• Lample, G., Lachaux, M.-A., Lavril, T., Martinet, X., Hayat, A., Ebner, G., Rodriguez, A., and Lacroix, T. (2022). HyperTree Proof Search for Neural Theorem Proving. arXiv:2205.11491. https://arxiv.org/abs/2205.11491
• Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., and Liang, X. (2024). DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. arXiv:2405.14333. https://arxiv.org/abs/2405.14333
• Atil, B., Aykent, S., Chittams, A., Fu, L., Passonneau, R. J., Radcliffe, E., Rajagopal, G. R., Sloan, A., Tudrej, T., Ture, F., Wu, Z., Xu, L., and Baldwin, B. (2024). Non-Determinism of "Deterministic" LLM Settings. arXiv:2408.04667. https://arxiv.org/abs/2408.04667
• Yuan, J., Li, H., Ding, X., Xie, W., Li, Y.-J., Zhao, W., Wan, K., Shi, J., Hu, X., and Liu, Z. (2025). Understanding and Mitigating Numerical Sources of Nondeterminism in LLM Inference. arXiv:2506.09501. https://arxiv.org/abs/2506.09501
• Microsoft Research. GraphRAG: Unlocking LLM discovery on narrative private data. https://www.microsoft.com/en-us/research/blog/graphrag-unlocking-llm-discovery-on-narrative-private-data/
• Microsoft Research. GraphRAG project. https://www.microsoft.com/en-us/research/project/graphrag/
• seL4. Verification. https://sel4.systems/Verification/
• RTCA. DO-178. https://www.rtca.org/do-178/

Correction log

An earlier draft of this article attributed the 65.4 per cent HyperTree Proof Search result to performance after online training. That is incorrect. The 65.4 per cent figure is for a model trained on annotated proofs; online training on unproved theorems raises it to 82.6 per cent. The error was caught during source verification before publication and is recorded here rather than silently amended.