1# Agent G — Theory Specialist review (Phase 5), WP4423Scope: algorithms and data structures, computational complexity, programming languages, compilers, formal verification,4software engineering (areas `theory` and `software_pl` of `taxonomy/ontology.yaml`). Date: 2026-11-03.56Inputs read: `literature_synthesis/landmarks/theory_landmarks.csv` (50 candidates) and `software_pl_landmarks.csv`7(100 candidates) with their `*_abstracts.jsonl`; `results/graph/category_counts_yearly.csv`, `category_flows_yearly.csv`,8`category_cooccurrence_yearly.csv`; `results/bibliometrics/cagr_by_category.csv`; `results/econometrics/breaks.csv`9(rows `cat_algorithms`, `cat_computational_complexity`, `cat_programming_languages`, `cat_compilers`,10`cat_formal_verification`, `cat_software_engineering`); `manuscript/references.bib`. No knowledge-graph extraction file11exists for these areas (`data/processed/graph/extraction/` is absent), so no extracted claim or method node was used.12Evidence levels are stated per statement: *metadata* (title, venue, type, year, identifiers), *abstract* (the abstract13recorded in OpenAlex), *corpus statistic* (a result file). No full text was read. Companion artefacts:14`claims.csv` (G-01…G-24), `contributions.csv` (150 rows, one per candidate, with an audit verdict), `open_problems.csv`15(G-P1…G-P10), `verification_lookups_raw.txt` (raw Crossref/DataCite/arXiv/OpenAlex responses), and the generated tables16`manuscript/tables/tab_theory_*.tex`.1718## 1. The candidate landmark set: an audit before a synthesis1920The protocol selects landmarks as the works with the highest field-normalised 36-month citation score (NCS36) within21each primary category, with a floor of fifteen per category, plus the 200 most cited works overall22(`literature_synthesis/select_landmarks.py`). For the six categories reviewed here this produced 25 candidates each,23150 in total. Before any of them can be discussed as a landmark, the list has to be audited, because its composition is24not what the selection rule intends (claim G-01; `contributions.csv`, column `verdict`):2526| verdict | n | meaning |27|---|---|---|28| in_scope_research | 29 | a research contribution inside the category's definition |29| in_scope_survey | 8 | survey, handbook or competition report inside the category |30| misclassified | 33 | outside the category and outside the theory/software scope |31| dissertation | 27 | thesis (in scope), selected through the normalisation of small category×year cells |32| reprint_misdated | 24 | a classic re-deposited (repository, arXiv, anthology) under a recent record date |33| textbook | 22 | textbook, chapter or monograph |34| metaheuristic | 6 | metaphor-based metaheuristic optimiser (in scope, contested genre) |35| duplicate | 1 | second record of the Handbook of Satisfiability |3637Four mechanisms explain the composition, and each is a finding about the instrument rather than about the field.3839*Identifier collisions (claim G-02, machine-verified).* Seven records carry OpenAlex identifiers that, resolved live on402026-11-03, return a different and far more cited work. The record titled "Exploiting Generative AI to Scale up41Intelligent Tutoring Systems" (DOI 10.4230/lipics.itp.2023.19, `c36` = 72,130) resolves to *Attention Is All You Need*;42its abstract in the corpus is that of *MizAR 60 for Mizar 50* (ITP 2023), which is what the DOI actually denotes. The43ECOOP 2025 paper on functionality-specific vulnerabilities (`c36` = 15,245) resolves to the graph-convolutional-network44preprint; the SEA 2024 paper on GNN branching for maximum independent set (`c36` = 5,183) resolves to GraphSAGE; the WADS452025 Kd-tree paper (`c36` = 2,355) resolves to the variational-autoencoder preprint; the SAIA 2024 robustness framework46resolves to the Madry et al. adversarial-training preprint; the ESEM 2026 record resolves to the Codex paper; the DX472024 answer-set-programming paper resolves to an "Uncertainty-aware RSS" preprint. In every case the recorded `c36`48matches the citation count of the other work, so the citation windows attached to these records are not theirs. The49mechanism (identifier merge or reuse between the 2026-10-14 snapshot and the live database) is inferred, not observed;50the consequence is observed: the four most "cited" candidates of the software_pl area and the first candidate of the51theory area owe their rank to another work's citations.5253*Generic-title chapters.* Book chapters titled "Introduction to Algorithms" (2020, 2021, 2023), "Particle Swarm54Optimization" (2019), "Introduction to Software Testing" (2021), "Introduction to Graph Theory" (2023) and Royce's 197055paper in a 2021 anthology carry hundreds to thousands of citations in their 36-month window. A live lookup confirms the56counts (the PSO chapter has 6,321 citations; the 2023 "Introduction to Algorithms" chapter 1,645). The plausible reading57is that citations intended for the canonical work (the Cormen et al. textbook, the Kennedy–Eberhart PSO paper, Royce581970) are attributed by the indexer to a same-titled chapter; this is an interpretation, recorded as such (`claims.csv`59G-01 notes).6061*Re-deposited classics (24 records).* Dijkstra's 1959 note appears as a 2022 ACM Books chapter; Turing's 1936 paper as a622021 MIT Press chapter; the 1994 survey of decidability for Petri nets as a 2024 arXiv posting; Lynch and Tuttle's63introduction to I/O automata as a 2026 journal article; Cormode's 2003 thesis "Sequence distance embeddings" and the SODA642000 "Communication complexity of document exchange" as 2026 Warwick repository records; three UNSW theses of the L4/seL465verification lineage as 2022 records; the 2018 NeurIPS paper on online algorithms with predictions as a 2024 arXiv66posting. The year field of these records is the deposit year, so they enter the "post" period and inflate its apparent67landmark count (`\ThyLandTheoryDatedTwentysix` = 10 of 50 theory candidates are dated 2026).6869*Lexical misclassification (33 records).* The computational_complexity list contains fifteen works from psychology,70management, education and metrology (UTAUT adoption models, PLS-SEM studies of SMEs and students, "Complexity Theory and71the Social Sciences", fringe-projection profilometry), captured by the phrase "complexity" (claim G-03). The compilers72list contains ten works captured by "just-in-time" (adaptive interventions in mental health), "compiling" (a guide to73literature reviews), "polyhedral" (power-system dispatch) and generic education studies (claim G-20). The74programming_languages list includes a Nature paper on Calabi–Yau manifolds and a debris-flow hazard study. The75dissertation and misclassification problems interact: the NCS36 normalisation divides by the expected citations of a76category×year×type cell, and small cells of theses or of non-CS articles produce large normalised scores.7778What remains after the audit is a set of 29 research works and 8 surveys or reports, listed in79`tab_theory_landmarks_discussed.tex`. Sixteen of the 29 are post-period works. They are discussed below by category,80together with the verified references of the pre-2022 lineage from `references.bib` and the Part VII-a bibliography81(`manuscript/references_part07a.bib`, 65 entries, each resolved by a single live lookup). The major theoretical results of82the window are absent from the candidate list (claim G-14) and are brought in through verified records, not through the83corpus ranking.8485## 2. What the corpus statistics say about the six categories8687*Volume.* Multi-label counts grew in every category after 2022 (Table `tab_theory_counts`): the 2023→2025 compound88annual growth is 25.5% for software engineering, 22.7% for computational complexity, 22.4% for compilers, 14.2% for89algorithms, 13.1% for formal verification and 11.5% for programming languages, against 0.9%, 1.9%, −0.3%, 1.6%, −5.1%90and −2.4% over 2018→2022. The comparison with the corpus-wide multi-label growth (6.1% → 26.0%) shows that this is mostly91the corpus-wide acceleration (claim G-05), and the primary-label shares of all six categories fell between 2018 and 202592(algorithms 5.83% → 3.79%, software engineering 5.81% → 4.07%, formal verification 1.06% → 0.52%, programming languages930.88% → 0.47%, computational complexity 0.77% → 0.47%, compilers 0.15% → 0.09%; claim G-06). The theory and software94categories are growing in absolute terms and shrinking in relative terms. Two cautions: the post-period CAGR spans two95years and is exposed to indexing lag (Part IV, truncation section); and `results/bibliometrics/cagr_by_category.csv`96reports primary counts about three times smaller than `category_counts_yearly.csv` for these categories (algorithms972018: 9,716 against 29,148), so it predates the current classification and its CAGR values are not used here (claim98G-07; the generator `bibliometrics/04_diversity_cagr.py` reads the counts file, so re-running it resolves the issue).99100*Structural change.* The interrupted-time-series slope change at 2022-12 is positive and HAC-significant for all six101series (1.0% to 1.8% per month), but no series passes the placebo test at the 5% level: the placebo slope p-values are1020.062 (algorithms), 0.062 (computational complexity), 0.154 (software engineering), 0.215 (compilers), 0.246 (formal103verification) and 0.431 (programming languages). The 2022-12 slope change is therefore not distinguishable from104pseudo-events placed in the baseline (claim G-08). Level changes at 2022-12 are negative or null in five categories105(formal verification −10.9%, p = 0.029; computational complexity −6.8%, p < 0.001; algorithms −4.5%, p = 0.039) and106positive only in software engineering (+4.8%, p = 0.124), which is also the only category with a significant positive107level change at the GPT-4 date (0.102, p = 0.003; claim G-09). Bai–Perron dates a single break at 2023-04 for108algorithms, computational complexity and compilers, two breaks for programming languages (2022-04, 2024-06) and formal109verification (2022-02, 2024-07), and 2022-07 for software engineering. None of this supports a causal reading, and the110negative level changes are at least partly the seasonality of proceedings dates.111112*Composition.* Co-classification with the LLM category rose in every category between 2022 and 2025: software113engineering 4.0% → 21.2% of its works, programming languages 4.2% → 18.3%, compilers 3.1% → 14.9%, formal verification1140.7% → 7.9%, algorithms and computational complexity 1.3% → 5.3% (claim G-10; `tab_theory_llm_cooccurrence`). The115gradient runs from the applied, code-facing categories to the mathematical ones. Reference flows tell a more conservative116story: in the post period, software-engineering works direct 2.5% of their categorised references to LLM works,117computational complexity 1.8%, compilers 1.2%, programming languages 0.7%, formal verification 0.4% and algorithms 0.3%,118while self-citation shares are nearly unchanged (algorithms 65.1% → 65.0%, software engineering 64.6% → 62.4%, formal119verification 49.9% → 47.0%; claim G-11). Two flow changes deserve notice. Computational complexity's self-citation share120fell from 30.0% to 20.6% while its references to HCI doubled (3.0% → 6.7%); given the candidate list, this is more121plausibly the social-science contamination of the category than a change in theoretical research (claim G-12,122contested). Formal verification's inbound citations from computer vision doubled (6.7% → 13.8%), consistent with the123neural-network verification literature being cited by robustness work (claim G-13, contested; no paper-level breakdown).124125## 3. Algorithms and data structures126127*Established.* The window contains results that the field itself regards as landmarks and that the verified bibliography128records: maximum flow and minimum-cost flow in almost-linear time (Chen et al., FOCS 2022), negative-weight single-source129shortest paths in near-linear time (Bernstein, Nanongkai and Wulff-Nilsen, FOCS 2022; JACM and CACM republications1302025), the first directed SSSP algorithm below the sorting barrier (Duan et al., STOC 2025, best paper; JACM 2026), and131optimal bounds for open addressing without reordering (Farach-Colton, Krapivin and Kuszmaul, FOCS 2024), which overturned132a conjecture dating from the 1980s. None of them is in the candidate list (claim G-14). The corpus records the programme133of algorithms with predictions through a 2024 arXiv re-posting of the 2018 NeurIPS paper on ski rental and134non-clairvoyant scheduling (abstract: algorithms "oblivious to the performance of the predictor, improve with better135predictions, but do not degrade much if the predictions are poor"); the programme's canonical references are the JACM136competitive-caching paper and the CACM overview (claim G-22). The fine-grained-complexity programme that organised137baseline-period algorithms research (Part II) is represented by the ICM 2018 survey.138139*Contested.* Six of the 25 candidates are metaphor-based metaheuristics (Arithmetic Optimization Algorithm 2021, Aquila140Optimizer 2021, artificial lemming 2025, glider snake 2026, gray langurs 2026, starfish 2026), published in engineering141and AI-review journals and benchmarked on CEC function suites. Their abstracts promise balanced "exploration and142exploitation" and superiority over "13 state-of-the-art algorithms". The operational-research literature has argued since143Sörensen's "Metaheuristics—the metaphor exposed" that the genre re-describes known methods under new metaphors, a144position restated in the 2021 "call for action" and in the 2022 analysis of six such algorithms. The corpus shows the145genre's weight in the highly cited stratum of the category (claim G-04); it does not evaluate the algorithms. The two146post-period research candidates that survive the audit are modest: Kd-trees extended to Bregman divergences (WADS 2025,147with a C++ implementation) and GNN-selected branching inside branch-and-reduce for maximum independent set (SEA 2024);148both carry citation counts that belong to other works.149150*AI-discovered algorithms.* AlphaTensor (matrix multiplication, 2022), AlphaDev (sorting routines, 2023), FunSearch151(cap sets, 2023) and AlphaEvolve (2025, preprint) report improvements on specific instances; no independent replication152appears in the verified bibliography (claim G-23, contested). Whether these results change how algorithms are designed is153an open problem (G-P9), as is the diffusion of the 2022–2025 breakthroughs into practice (G-P6).154155## 4. Computational complexity156157The category is the least precise of the six (fifteen misclassified candidates). The two in-scope research candidates158are the STOC 2019 non-elementary lower bound for Petri-net reachability, whose abstract describes the problem as open159since the 1960s and the previous best lower bound as Lipton's 1976 exponential space, and a 2026 TCS paper on SAT in160spiking neural P systems (no abstract). The reachability story was completed in the baseline period: Czerwiński and161Orlikowski (FOCS 2021) and Leroux (FOCS 2021) established Ackermann-completeness, matching the Leroux–Schmitz upper bound162(claim G-15). In the window, the result the field regards as the main complexity-theoretic event is Williams's STOC 2025163simulation of time t in space O(√(t log t)) (JACM 2026), which improves the Hopcroft–Paul–Valiant bound after fifty164years; Kelley and Meka's strong bounds for 3-progressions (FOCS 2023) are the main additive-combinatorics result.165Neither appears in the candidate list; both are recorded through verified DOIs.166167The boundary with language models is where the category's post-2022 growth is most visible in the co-classification168statistics, yet the relevant works are mostly classified elsewhere: the proof that log-precision transformers lie in169uniform TC⁰ (TACL 2023) and the survey of formal-language results for transformers (TACL 2024) bound what a single forward170pass can compute and motivate chain-of-thought as a route to greater expressive power (claim G-21, speculative as to its171place in the corpus). Textbooks on Kolmogorov complexity (4th edition, 2019) and on parameterized complexity dominate the172rest of the list.173174## 5. Programming languages175176The baseline lineage (Part II) is Rust and its semantic foundation (RustBelt, 2017; the CACM account of safe systems177programming, 2021), the Lean 4 prover-as-language and mathlib, and the verified artefacts CompCert and seL4. The178candidate list records this lineage only through re-deposited theses of the L4/seL4 school (separation logic for virtual179memory, formal memory models for C systems code, the clustered multikernel), all dated 2022 by their deposit year. In the180window, Verus (SOSP 2024) extends the lineage with a Rust-based verification framework for systems code (claim G-24).181182The two post-period research candidates mark the entry of language models into the community's top venue (claim G-16):183LLift (OOPSLA 2024) combines static analysis with an LLM to find use-before-initialisation bugs in the Linux kernel, and184its abstract reports four previously unknown bugs acknowledged by the kernel community; WhiteFox (OOPSLA 2024) uses an185LLM that reads optimisation source code to generate test programs for compiler optimisations. Both report bugs found,186neither reports guarantees. The contrast with translation validation (Alive2, PLDI 2021, bounded) and with187Csmith-style differential testing (PLDI 2011) is the natural axis of comparison and an open problem (G-P4). ZEUS (NDSS1882018), which combines abstract interpretation and constrained Horn clauses to check smart contracts, is the baseline189representative of program analysis for a new target. Co-classification of programming-languages works with LLM reached19018.3% in 2025, the second highest of the six categories; references to LLM works are 0.7% of the category's references.191192## 6. Compilers193194The category is the smallest (0.09% of primary labels in 2025) and the most lexically contaminated after complexity. Its195in-scope candidates trace a coherent line. Baseline: MLIR (CGO 2021), the multi-level infrastructure that reduced the196cost of domain-specific compilers; Tiramisu (CGO 2019), a polyhedral compiler with an explicit scheduling language;197ExaStencils (2020), a layered DSL for multigrid solvers; and two surveys of machine learning in compiler optimisation198(Proc. IEEE 2018; CSUR 2018 on autotuning and phase ordering), which show that learned compiler heuristics are a199pre-2018 programme. Post-period: LLM4VV (FGCS 2024), an LLM-generated validation suite for OpenACC compilers, and LLM200Compiler (CC 2025), foundation models trained on 546 billion tokens of LLVM-IR and assembly, whose abstract reports 77%201of the optimising potential of an autotuning search for code size. The shift is from learning a heuristic inside a202compiler to pre-training a model on compiler artefacts; what it leaves open is correctness, which the compiler community203has historically handled by differential testing and translation validation. Co-classification with LLM reached 14.9%204in 2025; references to LLM works are 1.2%. The deep-learning compiler stack recorded in `references.bib` (TVM, Triton,205PyTorch 2) is the other post-2018 development and is reviewed in Part VI.206207## 7. Formal verification208209This is the category with the most in-scope research candidates (eight) and the clearest internal structure. Tools and210competitions: cvc5 (TACAS 2022), the SV-COMP 2024 report (76 tools, 30,300 C tasks), Marabou (CAV 2019), the Handbook of211Satisfiability (2nd ed., 2021). Neural-network verification: the 2018 symbolic-interval preprint, DeepPoly (POPL 2019),212Marabou, with Reluplex (CAV 2017) and VNN-COMP (2023 report) as the lineage; the doubling of formal verification's213inbound citations from computer vision is consistent with this literature (claim G-13). Smart contracts: VerX (S&P2142020), "the first automated verifier able to prove functional properties of Ethereum smart contracts" per its abstract.215Learned theorem proving: MizAR 60 for Mizar 50 (ITP 2023), which reports automatic proofs of about 60% of Mizar theorems216in the hammer setting and 75% with human-selected premises, through the E and Vampire provers with ENIGMA and Deepire217learning and an incremental loop over millions of ATP proofs (claim G-17). The LLM-based line (Baldur, 2023; LeanDojo and218DeepSeek-Prover, preprints; the 2024 position paper on formal mathematical reasoning) reports whole-proof generation on219Lean and Isabelle benchmarks whose figures are not comparable across systems and are exposed to training-set overlap220(open problem G-P5). Equality saturation (egg, POPL 2021; CACM research highlight 2026) and quantitative interface221automata (CSL 2026) are the theory-of-verification entries. The category's primary share halved (1.06% → 0.52%) while222its multi-label count grew, which suggests that works carrying both a verification and an AI or security label lose the223primary label to the larger category (open problem G-P10).224225## 8. Software engineering226227Software engineering is where the window's change is largest and best documented. Surveys: machine-learning testing228(TSE 2020, 144 papers) at the baseline, software testing with LLMs (TSE 2024, 102 studies) in the window; the latter's229abstract names test-case preparation and program repair as the most common uses. Program repair and testing with230pre-trained models (ICSE 2023) and universal fuzzing with LLMs (ICSE 2024) are the method entries from `references.bib`231and the Part VII-a bibliography; SWE-bench and SWE-agent define the agentic evaluation setting. Empirical: the232Management Science field experiments (Microsoft, Accenture, a Fortune 100 firm; 4,867 developers) report a 26.08%233increase in completed tasks (s.e. 10.3%) with larger gains for less experienced developers, while the 2025 METR234randomised trial preprint with experienced open-source developers reports slower completion. The two are not235contradictory once population and outcome are distinguished (enterprise task completion versus expert time per issue in236mature repositories), but the reconciliation is the specialist's reading of two abstracts (claim G-18, contested).237Security: Copilot's vulnerable suggestions (2022), the user study on insecure code with assistants (CCS 2023) and the238ICPEC 2025 CWE-classification study agree that high detection or completion rates coexist with poor fine-grained security239reasoning (claim G-19). Co-classification with LLM reached 21.2% of the category in 2025, the highest of the six, while240references to LLM works are 2.5%; whether the vocabulary shift is a method shift is open problem G-P2. The category241also contains the only positive 2022-12 level change and the only significant GPT-4-date level change (claim G-09).242243## 9. Synthesis244245Three conclusions follow, in decreasing order of evidential strength. First, the landmark instrument fails in these246areas, for identifiable and partly correctable reasons (identifier collisions, generic-title chapters, re-deposited247classics, lexical misclassification, thesis cells); the correction is a selection-stage problem (G-P1), not a synthesis248problem, and the specialist's audit table should accompany any use of the list. Second, the six categories grew in249absolute terms and declined in relative terms after 2022; their ITS slope changes are positive but not distinguishable250from baseline pseudo-events; their vocabulary moved toward language models in proportion to their distance from251mathematics (software engineering and programming languages most, algorithms and complexity least); and their citation252behaviour moved little. Third, the substantive developments of the window are of two kinds that the corpus treats very253differently: theoretical results (flow, shortest paths, hashing, time–space simulation, 3-progressions) that the254citation-normalised ranking does not see, and the entry of language models into verification, program analysis,255compiler testing and software engineering, which the co-classification statistics see clearly but whose guarantees,256comparability and productivity effects remain unresolved (G-P3, G-P4, G-P5).257