Research report · 2026-08-03
What machine reasoning is, what has been built, and what the evidence supports.
This report accompanies the post What People Mean When They Say AI Cannot Reason. The concepts behind it ship as a portable Open Knowledge Format bundle you can hand to your own assistant.
This document explains what machine reasoning is, what has been built, what has been deployed, and what the evidence supports. It is written for a professional who is not an AI researcher and who has heard the claim that AI cannot really reason. Researchers checking the numbers will find each claim traced to a named source.
Reasoning, in engineering, means deriving conclusions from premises by rules you can state and check. Three forms of inference matter.
Deduction moves from premises to a conclusion that must hold if the premises hold. If every patient with condition A has finding B, and this patient has condition A, then this patient has finding B. Deduction preserves truth.
Induction moves from observations to a general rule. The rule can be wrong even when every observation was correct. Machine learning is mostly induction.
Abduction moves from an observation to the best explanation of it. Diagnosis is abduction. So is fault-finding in a machine. Abduction is not truth-preserving either, and the quality of the answer depends on the space of explanations considered.
Two properties tell you what an inference procedure is worth.
Soundness means the procedure never derives anything false from true premises. If a sound program says a proof exists, a proof exists.
Completeness means the procedure derives everything that follows. If a complete program says no proof exists, no proof exists.
Entailment is the underlying relation. A set of statements entails a conclusion when every situation making the statements true also makes the conclusion true. An inference procedure is an algorithm for detecting entailment.
The point that distinguishes this material from general talk about intelligence is that these properties have tests attached. Soundness and completeness are theorems, proved or not proved about a specific algorithm. Termination has a complexity class attached, so you can promise a customer that a computation finishes. Calibration, defined later, is a measured quantity. When a system claims a property in this family, someone can check it.
1955. The phrase “artificial intelligence” first appears in a proposal dated 31 August 1955, written by John McCarthy of Dartmouth College, Marvin Minsky of Harvard, Nathaniel Rochester of IBM and Claude Shannon of Bell Telephone Laboratories to request Rockefeller Foundation funding for “a 2 month, 10 man study” in the summer of 1956. The document circulated in typescript and was first published in AI Magazine volume 27 number 4, in 2006.
1955 to 1957. Allen Newell, J. C. Shaw and Herbert Simon built the Logic Theorist. It searched for proofs in the propositional calculus of Whitehead and Russell’s Principia Mathematica and proved 38 of the first 52 theorems in Chapter 2. For Theorem 2.85 it found a shorter proof than the published one, which Simon showed to Bertrand Russell.
1959. The same three authors reported the General Problem Solver at the IFIP congress. It separated the problem statement from the solving method and drove search by means-ends analysis: compare the current state to the goal, name the difference, apply an operator that reduces it. Planning systems still use that control loop.
1965. J. A. Robinson published the resolution principle in the Journal of the ACM, volume 12 number 1, pages 23 to 41, replacing the many rules of a textbook proof system with one rule a machine can apply repeatedly. The same paper gave the first widely known unification algorithm, which finds the most general substitution making two logical terms identical. Unification is why a program can apply a general rule to a specific case without a human choosing the instantiation.
1965. DENDRAL began at Stanford with Edward Feigenbaum and Joshua Lederberg, inferring organic molecular structure from mass spectrometry data. Bruce Buchanan joined in 1966, and Carl Djerassi’s mass-spectrometry group was recruited afterwards as the source of domain expertise. Its architecture separated an editable knowledge base from inference code. Its authors later called it “the first major application of heuristic programming to experimental analysis in an empirical science.”
1972 to 1974. Philippe Roussel implemented the first Prolog system in Algol-W in Marseille in the autumn of 1972, working from Robinson’s resolution and from the SL-resolution refinement of Robert Kowalski and Donald Kuehner. Kowalski’s “Predicate logic as a programming language” appeared in the IFIP Congress proceedings in 1974, pages 569 to 574.
1974 to 1979. Marvin Minsky circulated “A Framework for Representing Knowledge” as MIT AI Laboratory Memo 306 in June 1974. Amir Pnueli introduced temporal logic to computer science in 1977, receiving the 1996 Turing Award for it, and Patrick and Radhia Cousot published abstract interpretation at POPL 1977. In 1979 Victor Yu and colleagues published a blinded evaluation of MYCIN in JAMA.
1981 to 1982. Model checking was founded. Edmund Clarke and E. Allen Emerson published “Design and synthesis of synchronization skeletons using branching time temporal logic” at the Logic of Programs Workshop, Yorktown Heights, in May 1981. Independently in France, Jean-Pierre Queille and Joseph Sifakis published “Specification and verification of concurrent systems in CESAR” at the 5th International Symposium on Programming in April 1982.
1985 to 1996. Ronald Brachman and James Schmolze described KL-ONE in Cognitive Science in 1985, with a classifier that placed a new description in an existing taxonomy. Judea Pearl published belief propagation in 1986 and introduced the do-calculus in Biometrika in 1995. João Marques-Silva and Karem Sakallah published GRASP at ICCAD in 1996, introducing conflict-driven clause learning. On 10 October 1996 William McCune’s EQP prover settled the Robbins conjecture, an open question since the 1930s, after about eight days of search.
2001 to 2016. Chaff made clause learning fast at DAC 2001. Astrée proved the absence of runtime errors in Airbus flight control code in November 2003. OWL became a W3C Recommendation on 10 February 2004 and OWL 2 on 27 October 2009. Z3 appeared at TACAS 2008 and the seL4 microkernel proof at SOSP in October 2009. Pearl received the 2011 ACM A.M. Turing Award. AWS engineers began using TLA+ in 2011. Marijn Heule, Oliver Kullmann and Victor Marek settled the Boolean Pythagorean triples problem in 2016 with a proof certificate of almost 200 terabytes.
2020 to 2026. Retrieval-augmented generation was published in May 2020. Chain-of-thought prompting was posted on 28 January 2022. AlphaGeometry appeared in Nature on 17 January 2024. DeepSeek published a full reinforcement-learning recipe for reasoning models on 22 January 2025. Vampire, a direct descendant of the resolution line, won all eight divisions of the CADE ATP System Competition at CASC-30 in 2025. The organisers described it as the first clean sweep in the competition’s history.
Two branches grew from resolution. One optimises for search power. The other optimises for trust.
The search branch produced first-order provers that run unattended. Vampire’s 2025 sweep is the current benchmark. Terence Tao’s Equational Theories Project, launched 25 September 2024, resolved all 22,028,942 implications among 4,694 magma equational laws, with every result validated in Lean; the write-up with 33 named collaborators went to arXiv on 9 December 2025. Tao reports that Vampire, Prover9 and Mace4, the older resolution-lineage tools, were more cost-effective than modern AI tools for most of the core reasoning work.
The trust branch produced proof assistants, where a human directs the proof and a small program checks every step. Robert Boyer and J Strother Moore began in Edinburgh in 1971 on what became Nqthm; Natarajan Shankar used it in 1986 for a machine-checked proof of Gödel’s first incompleteness theorem. Nqthm is the ancestor of ACL2, still used in hardware verification. Andrzej Trybulec designed Mizar in 1973. Coq began in 1984 at INRIA-Rocquencourt as Thierry Coquand and Gérard Huet’s implementation of the Calculus of Constructions, extended by Christine Paulin to inductive constructions in 1991; it won the ACM Software System Award in 2013 and is now the Rocq Prover. Lawrence Paulson released Isabelle in 1986.
HOL Light, first released by John Harrison in 1996 in CAML Light and later ported to OCaml, shows the architecture clearly. Its logical kernel is roughly 400 lines of OCaml built on ten primitive inference rules and three axioms. Following the LCF approach, users can add new inference rules without compromising soundness, because every theorem is constructed through that kernel. Correctness of the whole system reduces to a few hundred lines a person can read.
The results are dated and checkable. Georges Gonthier, with Benjamin Werner, completed a Coq proof of the Four Colour Theorem in 2005; Appel and Haken had proved the theorem in 1976 with a computer search mathematicians could not fully audit, and Gonthier removed both the hand-checked combinatorics and the unverified custom program. On 20 September 2012 Gonthier’s team with Assia Mahboubi and Laurent Théry finished a Coq proof of the Feit-Thompson odd order theorem, about six years and roughly 170,000 lines of work. Thomas Hales proved the Kepler conjecture in 1998 with Samuel Ferguson, and the Annals of Mathematics referees could not certify the computational parts; the Flyspeck project he launched in 2003 was announced complete in August 2014, and the official account, with 22 authors, appeared in Forum of Mathematics Pi volume 5, e2, on 29 May 2017.
The tradition is current. Lean was launched by Leonardo de Moura at Microsoft Research in 2013 and described at CADE-25 in Berlin, 1 to 7 August 2015, by de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer; all five received the CADE Skolem Award at CADE-30 in July 2025. As of 2026-08-03 Lean’s Mathlib library reports 283,802 theorems and 134,897 definitions from 772 contributors. The Isabelle Archive of Formal Proofs reports 1,012 entries by 604 authors, about 323,000 lemmas and roughly 5.3 million lines.
In November 2023 a crowd-sourced Lean 4 project, launched by Terence Tao less than a week before 18 November 2023 and coordinated with Patrick Massot’s Blueprint tool, formalized the proof of the polynomial Freiman-Ruzsa conjecture over F_2 in roughly three weeks; the dependency graph was fully green by early December 2023. Yael Dillies and Bhavik Mehta were the most active of roughly twenty contributors. The underlying mathematics is arXiv:2311.05762, “On a Conjecture of Marton,” by W. T. Gowers, Ben Green, Freddie Manners and Terence Tao, submitted 9 November 2023.
Description logics are languages for defining concepts and relations so that a program can compute what follows. The discipline was created by negative results. Ronald Brachman and Hector Levesque showed at AAAI-84 that the cost of computing subsumption is extremely sensitive to small changes in the description language, so that adding one apparently innocent constructor can turn a cheap problem into an intractable one. Manfred Schmidt-Schauss then proved at KR-89 that subsumption in KL-ONE is undecidable outright. The field had to define restricted languages and prove things about them. Schmidt-Schauss and Gert Smolka did that in 1991 for the logic ALC: deciding coherence and subsumption of ALC concept descriptions is PSPACE-complete, with a decision procedure running in linear space. With general TBoxes, meaning arbitrary axioms relating concepts, the same problems become EXPTIME-complete. Working ontology systems mostly operate in the second setting, so the distinction matters.
The W3C standardised chosen points on that trade-off curve. OWL became a Recommendation on 10 February 2004, with OWL DL defined for “maximum expressiveness while retaining computational completeness and decidability.” OWL 2 followed on 27 October 2009, with a Second Edition on 11 December 2012; its Direct Semantics is compatible with the model theory of the description logic SROIQ. OWL 2 defines three profiles with stated guarantees. EL decides consistency, subsumption and instance checking in polynomial time. QL answers conjunctive queries in LOGSPACE with respect to data size, using ordinary relational databases. RL runs on rule engines over RDF triples. RDF 1.1 Concepts and Abstract Syntax became a Recommendation on 25 February 2014; SPARQL 1.1 on 21 March 2013.
A reasoner does four mechanical jobs. Subsumption asks whether every instance of concept A must also be an instance of B. Classification runs subsumption across the whole vocabulary and returns the inferred hierarchy. Consistency checking asks whether any model satisfies all axioms at once, and coherence checking asks whether a named class has been defined so that it can never have an instance. Instance retrieval returns every individual that provably belongs to a concept. Every answer is an entailment: if the axioms hold, the answer holds. There is no confidence score.
The implementations have published algorithms. FaCT++ (Dmitry Tsarkov and Ian Horrocks, IJCAR 2006) implements a tableau decision procedure for SHOIQ. Pellet (Evren Sirin and colleagues, 2007) was described by its authors as the first sound and complete OWL-DL reasoner. HermiT (Birte Glimm, Ian Horrocks, Boris Motik, Giorgos Stoilos and Zhe Wang, 2014) uses a hypertableau calculus and is fully compliant with OWL 2 Direct Semantics. ELK (Yevgeny Kazakov, Markus Krötzsch and František Simančík, 2014) targets OWL 2 EL and classifies SNOMED CT, with around 300,000 classes, in under four seconds on a laptop.
SNOMED CT is the production case. SNOMED International describes it as the most comprehensive multilingual clinical healthcare terminology in the world, with more than 360,000 concepts, released monthly, in use in more than eighty countries. It ships two views. The stated view holds only what human authors asserted. The inferred view is, in SNOMED’s own specification, “logically derived by applying a description logic classifier to the stated view.” The OWL 2 Profiles specification names the case directly: EL “provides class constructors that are sufficient to express the very large biomedical ontology SNOMED CT.”
Biology runs the same machinery. ROBOT (Rebecca Jackson and colleagues, BMC Bioinformatics 20:407, 2019) makes reasoning a routine release step: its reason command performs logical validation and automatic classification and requires the ontology to be coherent, using ELK for large ontologies such as the Gene Ontology and HermiT for richly axiomatised ones. The UniProt SPARQL endpoint reports 232,509,129,690 triples for release 2026_02. In regulated finance, the Financial Industry Business Ontology is written in OWL, based on description logic, published by the EDM Council and standardised through the Object Management Group.
Validation is a separate capability and the standards keep it separate. SHACL became a W3C Recommendation on 20 July 2017. It validates RDF graphs against shapes and derives no new facts; data and shapes graphs stay immutable during validation, so validation is idempotent. Inference adds triples. Validation reports violations. Confusing the two is the most common modelling error in this area.
The commercial “semantic layer” in business intelligence takes the governance idea without the entailment. dbt’s Semantic Layer moves metric definitions out of the BI tool into the modelling layer so that, in dbt’s words, “different business units are working from the same metric definitions, regardless of their tool of choice.” AtScale open-sourced its Semantic Modeling Language under an Apache licence on 10 September 2024. These systems change what a query means. They do not compute entailments.
Formal verification is the part of this field where anyone can check the result. A program either has a machine-checked proof or it does not.
Boolean satisfiability underlies most of it. SAT asks whether a Boolean formula can be made true, and it was the first problem shown NP-complete, which kept it out of engineering for twenty-five years. Conflict-driven clause learning changed that. When search hits a contradiction, the solver analyses the cause, records it as a new clause and jumps back to the decision that caused it. Sharad Malik and Lintao Zhang measured the gain in Communications of the ACM in August 2009: on hardware and software verification benchmarks, Grasp from 2000 was more than 500 times slower than RSAT with SatElite, the 2007 competition winner, and that figure is a lower bound because Grasp timed out on some benchmarks at 10,000 seconds. They also state that a million-variable instance is “considered within the reach of modern solvers.” A million-variable search tree has 2^1000000 leaves; a day of computation visits perhaps a billion nodes. The solver still returns an answer.
SMT solvers add theories on top of SAT: integers, bit-vectors, arrays, strings. Z3, by Leonardo de Moura and Nikolaj Bjørner, was a four-page TACAS 2008 tool paper; it won the 2015 ACM SIGPLAN Programming Languages Software Award and its authors received the 2019 Herbrand Award. cvc5 was described at TACAS 2022 by Haniel Barbosa, Clark Barrett, Cesare Tinelli and fourteen co-authors.
Model checking takes a finite model of a system and a property in temporal logic, then decides algorithmically whether the model satisfies the property, returning a concrete counterexample trace when it does not. Clarke, Emerson and Sifakis received the 2007 A.M. Turing Award for developing it into a verification technology widely adopted in the hardware and software industries. Abstract interpretation, from the Cousots in 1977, computes a sound over-approximation of what a program can do, so proving a property of the approximation proves it of the program.
A C compiler that random testing could not break. CompCert is a C compiler with a mechanically checked Coq proof that compiled code behaves as the source semantics specify. The strongest evidence is hostile. Xuejun Yang, Yang Chen, Eric Eide and John Regehr built the random C program generator Csmith and reported more than 325 previously unknown bugs across C compilers, including 79 in GCC and 202 in LLVM; twenty-five of the GCC bugs were classified P1, the maximum release-blocking priority. Their PLDI 2011 paper states: “The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task.” The CompCert bugs Csmith did find were outside the proof, in the unverified front end and in an under-specified PowerPC constraint. CompCert won the 2022 ACM Software System Award and is qualified for nuclear (IEC 60880) and avionics (DO-178C) use.
An operating system kernel with a functional correctness proof. Gerwin Klein and twelve colleagues published the seL4 verification at SOSP in October 2009. The kernel is 8,700 lines of C and 600 lines of assembler. The proof is 200,000 lines of Isabelle/HOL script and cost about 20 person-years, of which 11 were seL4-specific. What was proved is refinement: the C implementation always follows the abstract specification, so every Hoare-logic property of the abstract model holds of the code. This implies the kernel cannot crash and never dereferences a null or misaligned pointer. What was assumed matters equally, and the authors stated it: the C compiler, the hand-written assembly, the hardware, with roughly 1,200 lines of boot code excluded, and DMA assumed disabled or trusted. Later work shrank that set. Thomas Sewell, Magnus Myreen and Klein published translation validation at PLDI 2013 that checks gcc’s output against the C semantics, removing the compiler from the trusted set on supported architectures. A separate proof of information-flow security over 8,830 lines of C appeared at IEEE Security and Privacy in 2013. In DARPA’s HACMS programme a professional red team was given six weeks and access to the camera partition of Boeing’s Unmanned Little Bird helicopter, and could not break out of that partition in flight. seL4 now ships commercially: NIO mass-produces the ONVO L60 vehicle with an seL4-based operating system, and MEP’s SureVoice system is used by air traffic and maritime controllers.
Airbus flight control code. In November 2003 Astrée proved automatically that the primary flight control software of the Airbus A340 fly-by-wire system, 132,000 lines of C, contains no runtime errors. The analysis took one hour twenty minutes on a 2.8 GHz PC using about 300 MB of memory. Airbus France applied it operationally to the A380 electric flight control code by the end of 2004, before the maiden flight on 27 April 2005. The scope is specific: Astrée proves the absence of an enumerated class of errors, including division by zero, out-of-bounds indexing, erroneous pointer dereferencing, arithmetic overflow and data races. It is sound, so if no errors are signalled, absence of those errors has been proved. It does not prove the aircraft flies correctly.
Chips. Intel’s 1994 Pentium FDIV defect produced a wrong result once in roughly nine billion random operand pairs, and Intel’s 17 January 1995 earnings release records a one-time charge of $475 million. John Harrison, then at Intel, wrote that this “did at least considerably improve investment in formal verification.” As of Harrison’s April 2010 overview at the Second NASA Formal Methods Symposium, Intel’s portfolio spanned hardware verification with FEV and symbolic trajectory evaluation, protocol verification with model checking and SMT, and floating-point firmware verification with HOL Light, covering Marstein-style division and square root and table-driven transcendental functions such as log and sin. Harrison left Intel in 2020, so that source does not speak to current practice there. On the AMD side, David Russinoff’s ACL2 verification of the K5 division algorithm was published in Formal Aspects of Computing in 1998.
Windows device drivers. Microsoft’s SLAM verification engine drives Static Driver Verifier, shipped in the Windows Driver Kit. The EuroSys 2006 paper reports running it on 126 WDM drivers against more than 60 rules, with 75 to 80 percent of investigated reports confirmed as real bugs by the drivers’ own developers.
Railway signalling. The Paris Metro Line 14 driverless system, in service since October 1998, was built with the B method from over 110,000 lines of B models translated into 86,000 lines of Ada. ClearSy reports that no bugs were found after the proof completed, at functional validation, at integration, at on-site testing, or in operation since.
Cloud infrastructure. Chris Newcombe and five Amazon colleagues documented AWS’s use of TLA+ in September 2014, published in CACM in April 2015. Model checking found three bugs in DynamoDB’s replication and group-membership system; the shortest trace exhibiting one of them was 35 high-level steps long, and it had survived design reviews, code reviews and testing. AWS then industrialised solvers. Neha Rungta, director of applied science for AWS Identity, gave the invited CAV keynote “A Billion SMT Queries a Day” at CAV 2022, part of FLoC 2022 at the Technion in Haifa, held 31 July to 12 August 2022. The Zelkova service answers questions about IAM and S3 policies with a portfolio solver that “invokes multiple solvers in the backend, including Z3, CVC4, cvc5 and a custom automaton solver, and returns results from the solver that comes back first,” with solve times from a couple hundred milliseconds to tens of seconds. Callers include S3 Block Public Access, IAM Access Analyzer, Amazon VPC Network Access Analyzer and Amazon Inspector.
Over four years AWS then built AuthV2, a new authorization component written in Dafny, deployed to production in early 2024. Read the claim precisely. What was formally verified is that the Dafny implementation satisfies a specification the team reverse-engineered from the legacy Java system: behavioural equivalence to a hand-recovered specification, not correctness in any absolute sense. The deployed artifact is Java produced by a custom idiomatic compiler that was not itself verified; confidence in that step came from differential and shadow testing against 10^15 production samples, which exposed 7 specification mismatches. The two published performance accounts differ and should not be blended. Byron Cook’s AWS Security Blog post of 17 October 2024 says the component is “50% faster than its predecessor” and that IAM processes “over 1.2 billion requests per second.” The ICSE 2025 paper by Chakarov, Geldenhuys, Heck, Hicks, Huang, Jaloyan, Joshi, Leino, Mayer, McLaughlin, Rungta, Torlak and colleagues says it is “invoked 1 billion times per second” and delivered a “threefold performance improvement,” with average latency improved 69 percent and P99 improved 83 percent on four high-traffic services. Cook’s claim that AWS is the first and only cloud provider using automated reasoning at this scale is a marketing statement in a corporate blog post.
“Do people who take this drug have fewer heart attacks?” can be read off data. “Does this drug lower heart attack risk?” cannot. Closing that gap takes a formal model of the system plus a calculus for manipulating it.
Judea Pearl received the 2011 ACM A.M. Turing Award “for fundamental contributions to artificial intelligence through the development of a calculus for probabilistic and causal reasoning.” His 1986 paper on belief propagation gave a message-passing scheme for computing posterior probabilities by local updates. In 1998 McEliece, MacKay and Cheng showed in the IEEE Journal on Selected Areas in Communications that turbo decoding is an instance of that algorithm, and that it also yields iterative decoders for low-density parity-check codes. Turbo codes and low-density parity-check codes decode with it.
Pearl’s 1995 Biometrika paper introduced the do-operator. A structural causal model is a directed graph plus functional assignments. An intervention, written do(X = x), deletes the arrows into X and sets it. The do-calculus is three rules for rewriting expressions containing do() into expressions containing only observed distributions: insert or delete observations, exchange an action for an observation, insert or delete actions. Each rule fires only when a stated d-separation condition holds in a specific modified graph. The same paper gives the back-door criterion, which says which covariates license ordinary adjustment, and the front-door criterion, which recovers an effect through a mediator even when the confounder is unmeasured.
The completeness results matter more than the rules. In 2006 two groups proved the three rules complete: Yimin Huang and Marco Valtorta at UAI-06, pages 217 to 224, and Ilya Shpitser and Judea Pearl at AAAI-06, pages 1219 to 1226. (The UAI-06 Best Student Paper award was shared between the Huang-Valtorta paper and a separate Shpitser-Pearl UAI-06 paper on conditional interventional distributions.) The joint content: if a causal effect is identifiable from the graph and observational data, some finite sequence of the three rules produces a do-free formula for it, and if no such sequence exists, the effect is not identifiable by any method. Shpitser and Pearl extended this to counterfactual queries in the Journal of Machine Learning Research in 2008. Santtu Tikka and Juha Karvanen shipped the algorithm as the causaleffect R package in the Journal of Statistical Software in 2017, so anyone can run it on their own graph and get either a formula or a proof of non-identifiability.
Pearl set out the three-level hierarchy in Communications of the ACM in March 2019: association, P(y|x); intervention, P(y|do(x), z); counterfactual, P(y_x | x’, y’). He states the restriction plainly: “Interventional expressions cannot be inferred from passive observations alone, regardless of how big the data.” And on optimisation: “As long as our system optimizes some property of the observed data, however noble or sophisticated, while making no reference to the world outside the data, we are back to level-1 of the hierarchy.” Bareinboim, Correa, Ibeling and Icard formalised this as the Causal Hierarchy Theorem in 2022.
A parallel tradition runs through statistics and economics: Donald Rubin’s potential outcomes (1974), James Robins’s g-formula (1986), Angrist, Imbens and Rubin on instrumental variables (1996), Card and Krueger’s difference-in-differences minimum-wage study (1994). The 2021 economics Nobel went half to David Card and half jointly to Joshua Angrist and Guido Imbens “for their methodological contributions to the analysis of causal relationships.” Imbens compared the two traditions in the Journal of Economic Literature in 2020 and found them largely translatable, with graphs better at stating and checking assumptions and potential outcomes better at estimation under specific designs.
The applied record is where this lands. Hernán and colleagues re-analysed the Nurses’ Health Study in Epidemiology in 2008 by emulating the Women’s Health Initiative trial protocol, reconciling a decade-long contradiction about hormone therapy and coronary heart disease; Hernán and Robins formalised the method as target trial emulation in the American Journal of Epidemiology in 2016. Dagan and colleagues reported one of the first nationwide real-world effectiveness evaluations of the BNT162b2 vaccine in NEJM 384(15):1412-1423 on 15 April 2021: a matched observational cohort study of 596,618 vaccinated people and 596,618 matched controls in Israel’s Clalit Health Services, with effectiveness at seven or more days after the second dose of 92 percent for documented infection, 94 percent for symptomatic disease, 87 percent for hospitalisation and 92 percent for severe disease. Suchard and colleagues ran 4.9 million patients across nine databases in the Lancet in 2019, producing 22,000 calibrated hazard ratios and finding thiazide diuretics better than ACE inhibitors on acute myocardial infarction. Voight and colleagues used inherited genotype as an instrument in the Lancet in 2012 and showed that genetically raised HDL cholesterol does not lower myocardial infarction risk (odds ratio 0.93 per standard deviation), while genetically raised LDL does (odds ratio 2.13). Correlation had pointed the other way for decades.
Structure can also be learned, with stated assumptions and stated guarantees. The PC algorithm (Spirtes and Glymour, 1991) recovers sparse graphs by conditional independence testing; FCI (Spirtes, Meek and Richardson, 1995) handles latent confounders and selection bias; GES (Chickering, 2002) is proved consistent in the large-sample limit; LiNGAM (Shimizu, Hoyer, Hyvärinen and Kerminen, 2006) uses non-Gaussian noise to orient edges that independence tests leave undirected. Sachs and colleagues applied Bayesian network structure learning to flow-cytometry data from thousands of single immune cells in Science in 2005, recovered most known signalling connections, and confirmed novel predicted ones experimentally.
The expert systems of the 1970s handled uncertainty with hand-made numbers, and the field corrected itself with mathematics. Shortliffe and Buchanan introduced MYCIN’s certainty factors in Mathematical Biosciences in 1975. At the first Conference on Uncertainty in Artificial Intelligence in 1985, David Heckerman showed that the original definition of a certainty factor is inconsistent with the functions MYCIN used to combine them, and that the combining rules are defensible only under conditional independence of evidence and a tree-structured inference network, assumptions that “are rarely true in practical applications.”
Pathfinder shows what replaced them. Begun in 1983 by Heckerman, Bharat Nathwani, Eric Horvitz and Larry Fagan, it diagnosed lymph node disease. Heckerman built one version assuming conditional independence and one full Bayesian belief network. The network needed 74,854 probabilities; 61,118 were computed from others, leaving 13,736 for the expert to assess, and construction took about 35 hours. On 53 consecutive referral cases the network version matched the gold standard in 50 cases against 47 for the simpler version, and mean inferential loss fell from 340 micromorts to 16. In 1997 Nathwani and colleagues ran the harder test: nineteen pathologists read 30 slides, crossing over between routine and computer-assisted reading. Accuracy was 40 percent with Pathfinder and 32 percent without, P = 0.02.
Calibration is the modern version of the same discipline. A model is calibrated when the probability that it is correct, given that it reported confidence p, equals p for every p. Guo, Pleiss, Sun and Weinberger stated this formally in 2017 and measured it. Expected calibration error partitions predictions into equal-width confidence bins and averages the absolute gap between accuracy and mean confidence, weighted by bin population; they used 15 bins. Their headline comparison: on CIFAR-100 a 5-layer LeNet from 1998 had 44.9 percent error and 4.85 percent calibration error, while a 110-layer ResNet from 2016 had 30.6 percent error and 16.53 percent calibration error. The more accurate model was the less honest one. The correction is one parameter. Temperature scaling divides the logits by a single learned scalar fitted on a validation set, which cannot change the argmax and so cannot change accuracy; ResNet-110 went from 16.53 percent to 1.26 percent, and DenseNet-161 on ImageNet from 6.28 percent to 1.99 percent.
The grading mathematics predates machine learning. Glenn Brier published a scoring rule for probabilistic weather forecasts in Monthly Weather Review in January 1950. Gneiting and Raftery gave the general theory in JASA in March 2007: a scoring rule is proper when a forecaster maximises expected reward by quoting an honest belief, and strictly proper when honesty is the unique optimum. Weather services have worked under that discipline for seventy-five years.
Miscalibration is a property of particular systems, not a law. Minderer and colleagues found at NeurIPS 2021 that the most recent image models, particularly those not using convolutions, are among the best calibrated, and that architecture matters more than size. Kadavath and colleagues at Anthropic reported in 2022 that larger language models are well calibrated on multiple-choice and true-or-false questions when the format is right, with calibration degraded by reinforcement learning from human feedback and largely restored by a temperature adjustment.
The research path has dates. Maxwell Nye and colleagues published scratchpads for intermediate computation on 30 November 2021. Jason Wei, Xuezhi Wang, Dale Schuurmans, Denny Zhou and co-authors posted chain-of-thought prompting on 28 January 2022: eight worked examples in the prompt took a 540-billion-parameter model to state-of-the-art accuracy on GSM8K, a set of grade-school maths word problems. On 24 May 2022 Takeshi Kojima and co-authors showed the effect with no examples: prefixing “Let’s think step by step” moved MultiArith accuracy from 17.7 percent to 78.7 percent and GSM8K from 10.4 percent to 40.7 percent on text-davinci-002. Self-consistency, posted 21 March 2022, samples many reasoning paths and takes the most common answer, adding 17.9 points on GSM8K. That was the first clear result that spending compute at answer time buys accuracy.
The next step moved computation out of the model. PAL (Luyu Gao and colleagues, 18 November 2022) and Program of Thoughts (Wenhu Chen, Xueguang Ma, Xinyi Wang, William Cohen, 22 November 2022) have the model write a Python program and hand execution to an interpreter. PAL with Codex beat PaLM-540B with chain-of-thought by about 15 points on GSM8K; Program of Thoughts averaged about 12 points over chain-of-thought across eight datasets. The model interprets. A deterministic system computes.
Models were then connected to external systems. Retrieval-augmented generation (Patrick Lewis and colleagues, 22 May 2020) pairs a generator with a dense index over Wikipedia. ReAct (Shunyu Yao and colleagues, arXiv:2210.03629, 6 October 2022) interleaves reasoning traces with actions against an external API; its abstract reports outperforming imitation-learning and reinforcement-learning baselines by 34 and 10 absolute success-rate points on ALFWorld and WebShop, using one or two in-context examples. Toolformer (Timo Schick and colleagues, 9 February 2023) has the model teach itself which API to call and when. Tree of Thoughts (17 May 2023) searches over branching intermediate states with backtracking, taking GPT-4 from 4 percent to 74 percent on the Game of 24.
Supervision then moved from answers to steps. Hunter Lightman, Karl Cobbe, John Schulman and colleagues published “Let’s Verify Step by Step” on 31 May 2023, training a reward model to judge each step. Process supervision beat outcome supervision, and their best model solved 78 percent of a representative subset of the MATH test set. They released PRM800K, 800,000 step-level human labels.
A reasoning model is a model post-trained by reinforcement learning to produce long chains of thought before answering, whose accuracy rises with the length of that chain. OpenAI’s o1 System Card, posted 21 December 2024, describes the series as trained with large-scale reinforcement learning to reason using chain of thought. DeepSeek published a full recipe on 22 January 2025, later appearing in Nature 645:633-638: Group Relative Policy Optimization drops the critic network and estimates the baseline from a group of sampled answers, and the reward is rule-based, one component checking the final answer and one checking output format. DeepSeek-R1-Zero, trained by reinforcement learning alone with no supervised reasoning data, went from 15.6 percent to 71.0 percent pass@1 on AIME 2024, and to 86.7 percent with majority voting. Charlie Snell, Jaehoon Lee, Kelvin Xu and Aviral Kumar quantified the compute trade on 6 August 2024: on problems where a small model already has non-trivial success, optimally allocated test-time compute can beat a model 14 times larger.
Prompting alone stays brittle. Iman Mirzadeh and colleagues at Apple showed on 7 October 2024 that adding one irrelevant but plausible clause to a GSM8K problem drops accuracy by up to 65 percent across frontier models.
The results that survive that criticism share one architecture: a generator proposes and a formal system checks. AlphaGeometry (Trieu Trinh, Yuhuai Wu, Quoc Le, He He, Thang Luong, Nature 625(7995):476-482, 17 January 2024) pairs a language model trained on synthetic data with a symbolic deduction engine. On the paper’s IMO-AG-30 benchmark it solved 25 of 30 problems, against 10 for Wu’s method, which the abstract describes as approaching the performance of an average International Mathematical Olympiad gold medallist; it solved all IMO 2000 and 2015 geometry problems and produced human-readable proofs. AlphaGeometry2, February 2025, reached 84 percent across IMO geometry problems from 2000 to 2024, up from 54 percent.
AlphaProof works inside Lean, where proofs are machine-checked, and was trained with AlphaZero-style reinforcement learning on millions of auto-formalised problems. At IMO 2024, AlphaProof solved three non-geometry problems and AlphaGeometry 2 solved one, for 28 of 42 points, one point below the gold threshold; Timothy Gowers and Joseph Myers marked the work. The timing caveat is in DeepMind’s own announcement: minutes on one problem and up to three days on the others, against a human limit of two 4.5-hour sessions. The method was published in Nature 651:607-613 on 12 November 2025.
The same pattern produced results outside mathematics. AlphaTensor (Nature, 5 October 2022) found provably correct matrix multiplication algorithms by searching tensor decompositions. AlphaDev (Nature, 7 June 2023) found shorter sorting routines that were merged into the LLVM standard C++ library. FunSearch (Nature, 14 December 2023) paired a language model with an evaluator and found new large cap set constructions in extremal combinatorics. AlphaEvolve, announced 14 May 2025, found a way to multiply 4x4 complex matrices with 48 scalar multiplications, improving on Strassen’s 1969 result, and recovers on average 0.7 percent of Google’s worldwide compute. In each case the output carries the checker’s guarantee, and the generator’s confidence is irrelevant.
Contrast that with Gemini Deep Think at IMO 2025, which scored 35 of 42, solving five of six problems in natural language within the 4.5-hour limit, confirmed by IMO President Gregor Dolinar. Those proofs needed human graders, so the guarantee comes from the markers.
Calibration tells you whether stated confidence matches measured accuracy, on average. It is checked with reliability diagrams, expected calibration error and proper scoring rules, and corrected with methods as simple as temperature scaling.
Conformal prediction gives a per-prediction guarantee that does not depend on the model being good. Split conformal prediction takes about five lines of code. Hold out a calibration set of n labelled examples the model never saw. Define a score that is high when the model is wrong; for classification, one minus the softmax output of the true class. Compute the ceiling of (n+1)(1−α) divided by n as an empirical quantile of those scores. At test time, output every label whose score falls below that threshold. The guarantee, from Angelopoulos and Bates, is 1 − α ≤ P(Y_test ∈ C(X_test)) ≤ 1 − α + 1/(n+1) over n exchangeable calibration points. Read the fine print. The theorem as proved establishes the lower bound; the upper bound holds for continuous scores or with a tie-breaking randomisation that the paper notes is usually ignored in practice. The coverage is marginal, averaged over the draw of the calibration set and the test point, not conditional on any given input. And a bad model buys its coverage with enormous prediction sets. The method comes from Vladimir Vovk, Alexander Gammerman and Glenn Shafer, whose book appeared from Springer in 2005 with a second edition in 2022. Risk-controlling prediction sets (Bates, Angelopoulos, Lei, Malik and Jordan, Journal of the ACM, September 2021) extend it to arbitrary loss functions: a set predictor is (α, δ)-risk-controlling if, with probability at least 1 − δ, the expected loss is at most α. AstraZeneca researchers published on applying conformal prediction to compound property and safety models in 2017.
Verifiers check generated reasoning with a second system. Cobbe and colleagues trained verifiers on GSM8K in October 2021 by sampling many solutions and ranking them. Self-consistency takes a majority over independently sampled derivations. Process supervision scores each step. Using a model as a judge works with documented caveats: Zheng and colleagues reported over 80 percent agreement between GPT-4 judges and human preferences, alongside position bias, verbosity bias, self-enhancement bias and limited reasoning ability, all named by the method’s own authors. Formal checking of generated output now ships commercially: AWS Automated Reasoning checks in Amazon Bedrock Guardrails became generally available on 6 August 2025, with AWS claiming up to 99 percent verification accuracy against encoded rules.
Abstention is the option to stop. C. K. Chow analysed the error-versus-reject tradeoff in IEEE Transactions on Information Theory in 1970. Geifman and El-Yaniv’s 2017 selective classification method lets a user name a target error rate and abstain enough to hit it, guaranteeing 2 percent top-5 error on ImageNet with probability 99.9 percent at close to 60 percent coverage.
Deferral routes the case to a person. Madras, Pitassi and Zemel proposed learning to defer at NeurIPS 2018, training the model jointly with knowledge of the downstream human decision-maker rather than merely thresholding confidence. Mozannar and Sontag gave consistent surrogate losses at ICML 2020. Uncertainty is also decomposed: Kendall and Gal separated aleatoric uncertainty, noise in the observations that more data will not remove, from epistemic uncertainty, model ignorance that more data will. That distinction tells an operator whether collecting more data helps.
Regulators now require some of this by law. Article 14 of Regulation (EU) 2024/1689 requires high-risk AI systems to be designed so natural persons can effectively oversee them, and specifically requires that overseers remain aware of automation bias and be able to disregard, override or reverse an output, or stop the system in a safe state. For remote biometric identification under Annex III point 1(a), no action may be taken on an output without separate verification by at least two competent persons. Article 15 requires declared accuracy levels and metrics in the instructions for use. The Act entered into force on 1 August 2024, with prohibitions applying from 2 February 2025, general-purpose model rules from 2 August 2025, most remaining obligations from 2 August 2026, and Article 6(1) high-risk classification from 2 August 2027.
The US route is narrower and turns on reviewability. Section 3060(a) of the 21st Century Cures Act, enacted 13 December 2016, added section 520(o)(1)(E) to the Food, Drug and Cosmetic Act, excluding clinical decision support software from the device definition when it meets four criteria. The fourth requires the software to enable a health care professional to independently review the basis for its recommendations, so that they do not rely primarily on them. FDA’s current guidance, issued 6 January 2026 and re-issued 29 January 2026 under docket FDA-2017-D-6569, gives guideline-consistent order sets as a non-device example and image-derived radiation therapy planning as a device function. It defines automation bias as the propensity to over-rely on an automated suggestion, notes it produces both errors of commission and errors of omission, and states that urgency increases it. Explanations must be in plain language and avoid information overload. Software whose basis cannot be independently reviewed is a regulated medical device.
The deployment record for that regulated category is mixed. By 2024, 99.4 percent of US non-federal acute care hospitals had adopted a certified electronic health record, up from under 10 percent in 2008. Bates and colleagues found in JAMA in 1998 that computerised order entry cut nonintercepted serious medication errors by 55 percent, from 10.7 to 4.86 per 1,000 patient-days; Kucher and colleagues randomised 2,506 patients in 2005 and found deep-vein thrombosis or pulmonary embolism at 90 days in 4.9 percent of the alerted group against 8.2 percent of controls. Against that, Bright’s 2012 review of 148 randomised trials found consistent improvement in process measures and sparse evidence on clinical outcomes, cost and workload; clinicians override drug safety alerts between 49 and 96 percent of the time; and a 2012 review of order sets found eighteen studies and no randomised trials at all.
Searle. “Minds, brains, and programs” appeared in Behavioral and Brain Sciences 3(3):417-424 in 1980. Searle imagines himself in a room manipulating Chinese symbols by rule, producing answers indistinguishable from a native speaker’s, understanding nothing. His conclusion is that instantiating a program is never by itself a sufficient condition of intentionality. Two things are routinely misreported. He separates strong AI from weak AI and attacks only strong AI; he grants that brains are machines and that brains think. And he answered the standard replies in the original paper. To the Systems Reply, that the room as a whole understands, he answers that he can memorise the rulebook, internalise the entire system, and still not know what the Chinese word for hamburger means. To the Robot Reply, that sensors and effectors supply genuine semantics, he answers that sensor input arrives as more uninterpreted symbols.
Harnad. The symbol grounding problem, Physica D 42:335-346, 1990: how can the semantic interpretation of a formal symbol system be made intrinsic to the system rather than parasitic on the meanings in our heads? His illustration is learning Chinese as a first language from a Chinese-Chinese dictionary alone, passing endlessly from one meaningless string to another. Harnad proposed a solution rather than an impossibility verdict: ground elementary symbols bottom-up in iconic representations, which are analog transforms of sensory projections, and categorical representations, which are learned detectors of invariant features, with connectionism as the learning mechanism. The result is a hybrid nonsymbolic and symbolic architecture, which is broadly the route embodied and multimodal systems now take.
Dreyfus. “Alchemy and Artificial Intelligence” was a RAND memo in 1965; What Computers Can’t Do followed from Harper & Row in 1972, revised in 1979 and reissued as What Computers Still Can’t Do by MIT Press in 1992. Dreyfus named four assumptions behind symbolic AI: biological (the brain processes information in discrete on/off operations), psychological (the mind operates on bits by formal rules), epistemological (all knowledge can be formalised) and ontological (the world consists of independent facts representable by independent symbols). Drawing on Heidegger, he argued expert skill is largely non-propositional. His epistemological and ontological objections were correct about symbolic AI and about the failure of mid-1970s strong-AI predictions. His critique was aimed at the symbolic programme specifically; he explicitly welcomed connectionist and neural-network approaches as more consistent with his position, and the sub-symbolic methods that eventually made progress are broadly the kind he argued symbolic AI would need.
Bender and Koller. At ACL 2020, pages 5185-5198, they define form as any observable realisation of language and meaning as the relation between form and something external to language, then argue as a matter of principle that a system exposed only to form in training cannot learn meaning. The octopus test makes it concrete: a deep-sea octopus taps an undersea cable between two stranded English speakers, learns to predict the exchange, cuts the line and impersonates one party. It handles small talk. It fails when the other party is chased by a bear and asks how to build a weapon from sticks. The paper concedes the octopus produces fluent, coherent text and locates the failure at grounding. Bender, Gebru, McMillan-Major and Shmitchell extended this at FAccT 2021, pages 610-623, where “stochastic parrot” names a specific claim: the model stitches together sequences of observed form according to probabilistic information about how they combine, without reference to meaning.
Marcus and Davis supplied the empirical version, arguing in Rebooting AI (2019) that deep learning is data-greedy, opaque and brittle, and scoring GPT-3’s commonsense responses in MIT Technology Review in 2020 at roughly 45 percent clearly right, 45 percent clearly wrong and 10 percent borderline.
Chollet supplied the measurement objection in “On the Measure of Intelligence,” 5 November 2019: skill is heavily modulated by prior knowledge and experience, so unlimited priors or training data let an experimenter buy arbitrary skill in a way that masks a system’s own generalisation power. He defines intelligence as skill-acquisition efficiency and operationalises it in ARC-AGI. This objection applies to every benchmark cited in favour of machine reasoning too, and it is the strongest methodological criticism in the field. ARC-AGI-1 resisted five years of competition until o3 scored 75.7 percent and 87.5 percent on the Semi-Private Evaluation with 6 and 1,024 samples respectively, a 172-fold compute difference, reported by ARC Prize on 20 December 2024. ARC Prize has since restated the per-task costs as roughly $26 and $4,560 using o3-pro pricing; those figures are a later revision, not what was published on the day (page retrieved 2026-08-03). Chollet’s own words on the result: “I don’t think o3 is AGI yet. o3 still fails on some very easy tasks, indicating fundamental differences with human intelligence.” He also disclosed that OpenAI trained the tested model on 75 percent of the ARC-AGI public training set. On ARC-AGI-2, where every evaluation task has been solved by at least two humans in under two attempts, the best verified commercial model as of 5 December 2025 was Claude Opus 4.5 at 37.6 percent. The 85 percent Grand Prize target is unclaimed.
Unfaithful reasoning traces. Turpin, Michael, Perez and Bowman showed at NeurIPS 2023 that biasing an input shifts the answer without the explanation ever mentioning the bias, with accuracy falling as much as 36 percent across 13 BIG-Bench Hard tasks. Anthropic’s own April 2025 work found Claude 3.7 Sonnet mentioned a decisive hint 25 percent of the time and DeepSeek R1 39 percent, and that models trained to exploit a reward hack used it in over 99 percent of cases while admitting it in under 2 percent. A visible reasoning trace is not reliable evidence of the computation that produced the answer.
Contamination. Scale AI’s GSM1k study, a fresh 1,000-problem benchmark matched to GSM8k on solve rate, solution steps and answer magnitude, found accuracy drops of up to 8 percent and systematic overfitting in several model families, with a Spearman r-squared of 0.36 between a model’s likelihood of generating GSM8k examples and its performance gap. The authors nonetheless conclude that frontier models generalise to novel problems guaranteed not to be in training data.
The collapse claim, and where it stands. Apple’s “The Illusion of Thinking,” posted 7 June 2025, reported complete accuracy collapse on controllable puzzles past a complexity threshold, with reasoning effort declining on the hardest problems. Alex Lawsen’s comment, arXiv:2506.09250, identified defects. River Crossing instances with N ≥ 6 actors and boat capacity 3 were scored as failures although the Missionaries-Cannibals puzzle has no solution for N > 5 at that capacity. The grader could not distinguish truncated output from a reasoning failure. And asked for a generating function instead of an enumerated move list, Claude 3.7 Sonnet, Claude Opus 4, OpenAI o3 and Gemini 2.5 all produced correct recursive Tower of Hanoi implementations in under 5,000 tokens. The token-budget part of that comment was itself corrected between versions: at 10 tokens per move, version 2 computes a maximum of about 12 to 13 disks for a 64,000-token budget and states that “the reported collapse before N = 9 for most models occurs well before these theoretical limits,” so its revised argument is that the collapse reflects decisions about output length by models “poorly calibrated about their own context length capabilities.” A subsequent critical re-analysis by Iñaki Dellibarda Varela, Pablo Romero-Sorozabal, Eduardo Rocon and Manuel Cebrian (arXiv:2507.01231, 1 July 2025) re-ran the tasks under changed protocols and found the picture mixed: with incremental prompting removing the output-length constraint, Tower of Hanoi failures persist around 8 disks, while on solvable River Crossing configurations the models “effortlessly solve large instances involving over 100 agent pairs.” The authors characterise these systems as stochastic, reinforcement-tuned searchers in a poorly understood discrete state space. A similar correction hit the GSM-NoOp result: an audit found only 12.4 percent of the “irrelevant” distractors unambiguously irrelevant, and on the audited subset the drop was statistically indistinguishable from zero. That audit is a blog post and has not been peer-reviewed.
Two questions are being run together.
The metaphysical question is whether a system has phenomenal experience or intrinsic intentionality. Nobody has a test for it and no benchmark settles it. David Chalmers supplies the most rigorous version of the bridge: a physical system implements a computation when its causal structure mirrors the formal structure of the computation, with counterfactual-supporting transitions, so the organisationally invariant properties of the modelled system are replicated rather than merely depicted. Being a hurricane is not organisationally invariant, which is why a simulated hurricane is not wet. Whether mental properties are organisationally invariant is exactly where he and Searle disagree, and that disagreement is unresolved.
The engineering question is whether a procedure is sound, complete, calibrated and verifiable, and that question has measurable answers. When Heule, Kullmann and Marek settled the Boolean Pythagorean triples problem in 2016, showing that the integers 1 to 7,824 can be two-coloured with no monochromatic Pythagorean triple and that 1 to 7,825 cannot, the solver emitted a DRAT certificate of almost 200 terabytes, verified by an independent checker, with a 68-gigabyte compressed certificate published so anyone can re-check it. Lean’s Mathlib holds 283,802 machine-checked theorems, each verified down to a small logical kernel. The correctness of those results does not depend on anything having understood them.
Concede what should be conceded. Fluent output invites people to attribute understanding that has not been demonstrated. A reasoning trace is not proof of the computation behind it. Benchmarks can be bought with priors and data. ARC-AGI-2 is unsolved. Prompt-based reasoning is brittle under irrelevant detail. None of that touches the fact that a proof checked by Lean’s kernel is correct, that Astrée proved a class of runtime errors absent from 132,000 lines of flight control code, or that Csmith could not find a wrong-code error in CompCert’s verified region after six CPU-years of trying. Whether that counts as reasoning is a real question. Whether the results are correct is not.
Stop treating all AI as one thing. A description logic classifier, a SAT solver, a causal identification algorithm and a generative language model have different guarantees, different failure modes and different costs. A criticism of one is not a criticism of the others. The sentence “AI can’t reason” is unfalsifiable until someone names the system and the property.
Match the tool to the guarantee you need. Use a generative model when the task is interpretation, drafting, summarisation, translation between representations, or proposing candidates that something else will check. Use a deterministic, grounded, checkable system when a wrong answer is expensive and someone will have to defend the answer: policy evaluation, arithmetic, entitlement decisions, terminology classification, safety properties. The results that hold up in this material almost all pair the two, with a model proposing and a checker disposing. PAL moves arithmetic to an interpreter. AlphaProof emits Lean. AlphaTensor searches for decompositions that are correct by construction. In each case the guarantee comes from the checker.
Questions to ask a vendor.
Expect the failure to be organisational. T. Grandon Gill’s 1995 MIS Quarterly survey telephoned the owners of the 1987 catalogue of commercial expert systems. Most systems had fallen into disuse or been abandoned by 1992; about a third were still thriving; a predicted $4 billion market proved smaller by an order of magnitude. His central finding is that the short-lived systems mostly did not fail on technical or economic grounds. They died of lack of user acceptance, inability to retain developers, the handover from development to maintenance, and shifting organisational priorities. MYCIN outperformed five Stanford infectious disease faculty in a blinded 1979 JAMA evaluation, rated acceptable in 65 percent of ratings against a faculty average of 55.5 percent, and was never used to treat a patient. Kawamoto’s review found that the strongest predictor of a decision support system changing clinical practice was automatic delivery inside the clinician’s workflow, at an odds ratio of 112.1. Reasoning power was not the variable.