# Agent G — Theory Specialist review (Phase 5), WP44

Scope: algorithms and data structures, computational complexity, programming languages, compilers, formal verification, software engineering (areas theory and software_pl of taxonomy/ontology.yaml). Date: 2026-11-03.

Inputs read: literature_synthesis/landmarks/theory_landmarks.csv (50 candidates) and software_pl_landmarks.csv (100 candidates) with their *_abstracts.jsonl; results/graph/category_counts_yearly.csv, category_flows_yearly.csv, category_cooccurrence_yearly.csv; results/bibliometrics/cagr_by_category.csv; results/econometrics/breaks.csv (rows cat_algorithms, cat_computational_complexity, cat_programming_languages, cat_compilers, cat_formal_verification, cat_software_engineering); manuscript/references.bib. No knowledge-graph extraction file exists for these areas (data/processed/graph/extraction/ is absent), so no extracted claim or method node was used. Evidence levels are stated per statement: metadata (title, venue, type, year, identifiers), abstract (the abstract recorded in OpenAlex), corpus statistic (a result file). No full text was read. Companion artefacts: claims.csv (G-01…G-24), contributions.csv (150 rows, one per candidate, with an audit verdict), open_problems.csv (G-P1…G-P10), verification_lookups_raw.txt (raw Crossref/DataCite/arXiv/OpenAlex responses), and the generated tables manuscript/tables/tab_theory_*.tex.

# 1. The candidate landmark set: an audit before a synthesis

The protocol selects landmarks as the works with the highest field-normalised 36-month citation score (NCS36) within each primary category, with a floor of fifteen per category, plus the 200 most cited works overall (literature_synthesis/select_landmarks.py). For the six categories reviewed here this produced 25 candidates each, 150 in total. Before any of them can be discussed as a landmark, the list has to be audited, because its composition is not what the selection rule intends (claim G-01; contributions.csv, column verdict):

Four mechanisms explain the composition, and each is a finding about the instrument rather than about the field.

Identifier collisions (claim G-02, machine-verified). Seven records carry OpenAlex identifiers that, resolved live on 2026-11-03, return a different and far more cited work. The record titled "Exploiting Generative AI to Scale up Intelligent Tutoring Systems" (DOI 10.4230/lipics.itp.2023.19, c36 = 72,130) resolves to Attention Is All You Need; its abstract in the corpus is that of MizAR 60 for Mizar 50 (ITP 2023), which is what the DOI actually denotes. The ECOOP 2025 paper on functionality-specific vulnerabilities (c36 = 15,245) resolves to the graph-convolutional-network preprint; the SEA 2024 paper on GNN branching for maximum independent set (c36 = 5,183) resolves to GraphSAGE; the WADS 2025 Kd-tree paper (c36 = 2,355) resolves to the variational-autoencoder preprint; the SAIA 2024 robustness framework resolves to the Madry et al. adversarial-training preprint; the ESEM 2026 record resolves to the Codex paper; the DX 2024 answer-set-programming paper resolves to an "Uncertainty-aware RSS" preprint. In every case the recorded c36 matches the citation count of the other work, so the citation windows attached to these records are not theirs. The mechanism (identifier merge or reuse between the 2026-10-14 snapshot and the live database) is inferred, not observed; the consequence is observed: the four most "cited" candidates of the software_pl area and the first candidate of the theory area owe their rank to another work's citations.

Generic-title chapters. Book chapters titled "Introduction to Algorithms" (2020, 2021, 2023), "Particle Swarm Optimization" (2019), "Introduction to Software Testing" (2021), "Introduction to Graph Theory" (2023) and Royce's 1970 paper in a 2021 anthology carry hundreds to thousands of citations in their 36-month window. A live lookup confirms the counts (the PSO chapter has 6,321 citations; the 2023 "Introduction to Algorithms" chapter 1,645). The plausible reading is that citations intended for the canonical work (the Cormen et al. textbook, the Kennedy–Eberhart PSO paper, Royce 1970) are attributed by the indexer to a same-titled chapter; this is an interpretation, recorded as such (claims.csv G-01 notes).

Re-deposited classics (24 records). Dijkstra's 1959 note appears as a 2022 ACM Books chapter; Turing's 1936 paper as a 2021 MIT Press chapter; the 1994 survey of decidability for Petri nets as a 2024 arXiv posting; Lynch and Tuttle's introduction to I/O automata as a 2026 journal article; Cormode's 2003 thesis "Sequence distance embeddings" and the SODA 2000 "Communication complexity of document exchange" as 2026 Warwick repository records; three UNSW theses of the L4/seL4 verification lineage as 2022 records; the 2018 NeurIPS paper on online algorithms with predictions as a 2024 arXiv posting. The year field of these records is the deposit year, so they enter the "post" period and inflate its apparent landmark count (\ThyLandTheoryDatedTwentysix = 10 of 50 theory candidates are dated 2026).

Lexical misclassification (33 records). The computational_complexity list contains fifteen works from psychology, management, education and metrology (UTAUT adoption models, PLS-SEM studies of SMEs and students, "Complexity Theory and the Social Sciences", fringe-projection profilometry), captured by the phrase "complexity" (claim G-03). The compilers list contains ten works captured by "just-in-time" (adaptive interventions in mental health), "compiling" (a guide to literature reviews), "polyhedral" (power-system dispatch) and generic education studies (claim G-20). The programming_languages list includes a Nature paper on Calabi–Yau manifolds and a debris-flow hazard study. The dissertation and misclassification problems interact: the NCS36 normalisation divides by the expected citations of a category×year×type cell, and small cells of theses or of non-CS articles produce large normalised scores.

What remains after the audit is a set of 29 research works and 8 surveys or reports, listed in tab_theory_landmarks_discussed.tex. Sixteen of the 29 are post-period works. They are discussed below by category, together with the verified references of the pre-2022 lineage from references.bib and the Part VII-a bibliography (manuscript/references_part07a.bib, 65 entries, each resolved by a single live lookup). The major theoretical results of the window are absent from the candidate list (claim G-14) and are brought in through verified records, not through the corpus ranking.

# 2. What the corpus statistics say about the six categories

Volume. Multi-label counts grew in every category after 2022 (Table tab_theory_counts): the 2023→2025 compound annual growth is 25.5% for software engineering, 22.7% for computational complexity, 22.4% for compilers, 14.2% for algorithms, 13.1% for formal verification and 11.5% for programming languages, against 0.9%, 1.9%, −0.3%, 1.6%, −5.1% and −2.4% over 2018→2022. The comparison with the corpus-wide multi-label growth (6.1% → 26.0%) shows that this is mostly the corpus-wide acceleration (claim G-05), and the primary-label shares of all six categories fell between 2018 and 2025 (algorithms 5.83% → 3.79%, software engineering 5.81% → 4.07%, formal verification 1.06% → 0.52%, programming languages 0.88% → 0.47%, computational complexity 0.77% → 0.47%, compilers 0.15% → 0.09%; claim G-06). The theory and software categories are growing in absolute terms and shrinking in relative terms. Two cautions: the post-period CAGR spans two years and is exposed to indexing lag (Part IV, truncation section); and results/bibliometrics/cagr_by_category.csv reports primary counts about three times smaller than category_counts_yearly.csv for these categories (algorithms 2018: 9,716 against 29,148), so it predates the current classification and its CAGR values are not used here (claim G-07; the generator bibliometrics/04_diversity_cagr.py reads the counts file, so re-running it resolves the issue).

Structural change. The interrupted-time-series slope change at 2022-12 is positive and HAC-significant for all six series (1.0% to 1.8% per month), but no series passes the placebo test at the 5% level: the placebo slope p-values are 0.062 (algorithms), 0.062 (computational complexity), 0.154 (software engineering), 0.215 (compilers), 0.246 (formal verification) and 0.431 (programming languages). The 2022-12 slope change is therefore not distinguishable from pseudo-events placed in the baseline (claim G-08). Level changes at 2022-12 are negative or null in five categories (formal verification −10.9%, p = 0.029; computational complexity −6.8%, p < 0.001; algorithms −4.5%, p = 0.039) and positive only in software engineering (+4.8%, p = 0.124), which is also the only category with a significant positive level change at the GPT-4 date (0.102, p = 0.003; claim G-09). Bai–Perron dates a single break at 2023-04 for algorithms, computational complexity and compilers, two breaks for programming languages (2022-04, 2024-06) and formal verification (2022-02, 2024-07), and 2022-07 for software engineering. None of this supports a causal reading, and the negative level changes are at least partly the seasonality of proceedings dates.

Composition. Co-classification with the LLM category rose in every category between 2022 and 2025: software engineering 4.0% → 21.2% of its works, programming languages 4.2% → 18.3%, compilers 3.1% → 14.9%, formal verification 0.7% → 7.9%, algorithms and computational complexity 1.3% → 5.3% (claim G-10; tab_theory_llm_cooccurrence). The gradient runs from the applied, code-facing categories to the mathematical ones. Reference flows tell a more conservative story: in the post period, software-engineering works direct 2.5% of their categorised references to LLM works, computational complexity 1.8%, compilers 1.2%, programming languages 0.7%, formal verification 0.4% and algorithms 0.3%, while self-citation shares are nearly unchanged (algorithms 65.1% → 65.0%, software engineering 64.6% → 62.4%, formal verification 49.9% → 47.0%; claim G-11). Two flow changes deserve notice. Computational complexity's self-citation share fell from 30.0% to 20.6% while its references to HCI doubled (3.0% → 6.7%); given the candidate list, this is more plausibly the social-science contamination of the category than a change in theoretical research (claim G-12, contested). Formal verification's inbound citations from computer vision doubled (6.7% → 13.8%), consistent with the neural-network verification literature being cited by robustness work (claim G-13, contested; no paper-level breakdown).

# 3. Algorithms and data structures

Established. The window contains results that the field itself regards as landmarks and that the verified bibliography records: maximum flow and minimum-cost flow in almost-linear time (Chen et al., FOCS 2022), negative-weight single-source shortest paths in near-linear time (Bernstein, Nanongkai and Wulff-Nilsen, FOCS 2022; JACM and CACM republications 2025), the first directed SSSP algorithm below the sorting barrier (Duan et al., STOC 2025, best paper; JACM 2026), and optimal bounds for open addressing without reordering (Farach-Colton, Krapivin and Kuszmaul, FOCS 2024), which overturned a conjecture dating from the 1980s. None of them is in the candidate list (claim G-14). The corpus records the programme of algorithms with predictions through a 2024 arXiv re-posting of the 2018 NeurIPS paper on ski rental and non-clairvoyant scheduling (abstract: algorithms "oblivious to the performance of the predictor, improve with better predictions, but do not degrade much if the predictions are poor"); the programme's canonical references are the JACM competitive-caching paper and the CACM overview (claim G-22). The fine-grained-complexity programme that organised baseline-period algorithms research (Part II) is represented by the ICM 2018 survey.

Contested. Six of the 25 candidates are metaphor-based metaheuristics (Arithmetic Optimization Algorithm 2021, Aquila Optimizer 2021, artificial lemming 2025, glider snake 2026, gray langurs 2026, starfish 2026), published in engineering and AI-review journals and benchmarked on CEC function suites. Their abstracts promise balanced "exploration and exploitation" and superiority over "13 state-of-the-art algorithms". The operational-research literature has argued since Sörensen's "Metaheuristics—the metaphor exposed" that the genre re-describes known methods under new metaphors, a position restated in the 2021 "call for action" and in the 2022 analysis of six such algorithms. The corpus shows the genre's weight in the highly cited stratum of the category (claim G-04); it does not evaluate the algorithms. The two post-period research candidates that survive the audit are modest: Kd-trees extended to Bregman divergences (WADS 2025, with a C++ implementation) and GNN-selected branching inside branch-and-reduce for maximum independent set (SEA 2024); both carry citation counts that belong to other works.

AI-discovered algorithms. AlphaTensor (matrix multiplication, 2022), AlphaDev (sorting routines, 2023), FunSearch (cap sets, 2023) and AlphaEvolve (2025, preprint) report improvements on specific instances; no independent replication appears in the verified bibliography (claim G-23, contested). Whether these results change how algorithms are designed is an open problem (G-P9), as is the diffusion of the 2022–2025 breakthroughs into practice (G-P6).

# 4. Computational complexity

The category is the least precise of the six (fifteen misclassified candidates). The two in-scope research candidates are the STOC 2019 non-elementary lower bound for Petri-net reachability, whose abstract describes the problem as open since the 1960s and the previous best lower bound as Lipton's 1976 exponential space, and a 2026 TCS paper on SAT in spiking neural P systems (no abstract). The reachability story was completed in the baseline period: Czerwiński and Orlikowski (FOCS 2021) and Leroux (FOCS 2021) established Ackermann-completeness, matching the Leroux–Schmitz upper bound (claim G-15). In the window, the result the field regards as the main complexity-theoretic event is Williams's STOC 2025 simulation of time t in space O(√(t log t)) (JACM 2026), which improves the Hopcroft–Paul–Valiant bound after fifty years; Kelley and Meka's strong bounds for 3-progressions (FOCS 2023) are the main additive-combinatorics result. Neither appears in the candidate list; both are recorded through verified DOIs.

The boundary with language models is where the category's post-2022 growth is most visible in the co-classification statistics, yet the relevant works are mostly classified elsewhere: the proof that log-precision transformers lie in uniform TC⁰ (TACL 2023) and the survey of formal-language results for transformers (TACL 2024) bound what a single forward pass can compute and motivate chain-of-thought as a route to greater expressive power (claim G-21, speculative as to its place in the corpus). Textbooks on Kolmogorov complexity (4th edition, 2019) and on parameterized complexity dominate the rest of the list.

# 5. Programming languages

The baseline lineage (Part II) is Rust and its semantic foundation (RustBelt, 2017; the CACM account of safe systems programming, 2021), the Lean 4 prover-as-language and mathlib, and the verified artefacts CompCert and seL4. The candidate list records this lineage only through re-deposited theses of the L4/seL4 school (separation logic for virtual memory, formal memory models for C systems code, the clustered multikernel), all dated 2022 by their deposit year. In the window, Verus (SOSP 2024) extends the lineage with a Rust-based verification framework for systems code (claim G-24).

The two post-period research candidates mark the entry of language models into the community's top venue (claim G-16): LLift (OOPSLA 2024) combines static analysis with an LLM to find use-before-initialisation bugs in the Linux kernel, and its abstract reports four previously unknown bugs acknowledged by the kernel community; WhiteFox (OOPSLA 2024) uses an LLM that reads optimisation source code to generate test programs for compiler optimisations. Both report bugs found, neither reports guarantees. The contrast with translation validation (Alive2, PLDI 2021, bounded) and with Csmith-style differential testing (PLDI 2011) is the natural axis of comparison and an open problem (G-P4). ZEUS (NDSS 2018), which combines abstract interpretation and constrained Horn clauses to check smart contracts, is the baseline representative of program analysis for a new target. Co-classification of programming-languages works with LLM reached 18.3% in 2025, the second highest of the six categories; references to LLM works are 0.7% of the category's references.

# 6. Compilers

The category is the smallest (0.09% of primary labels in 2025) and the most lexically contaminated after complexity. Its in-scope candidates trace a coherent line. Baseline: MLIR (CGO 2021), the multi-level infrastructure that reduced the cost of domain-specific compilers; Tiramisu (CGO 2019), a polyhedral compiler with an explicit scheduling language; ExaStencils (2020), a layered DSL for multigrid solvers; and two surveys of machine learning in compiler optimisation (Proc. IEEE 2018; CSUR 2018 on autotuning and phase ordering), which show that learned compiler heuristics are a pre-2018 programme. Post-period: LLM4VV (FGCS 2024), an LLM-generated validation suite for OpenACC compilers, and LLM Compiler (CC 2025), foundation models trained on 546 billion tokens of LLVM-IR and assembly, whose abstract reports 77% of the optimising potential of an autotuning search for code size. The shift is from learning a heuristic inside a compiler to pre-training a model on compiler artefacts; what it leaves open is correctness, which the compiler community has historically handled by differential testing and translation validation. Co-classification with LLM reached 14.9% in 2025; references to LLM works are 1.2%. The deep-learning compiler stack recorded in references.bib (TVM, Triton, PyTorch 2) is the other post-2018 development and is reviewed in Part VI.

# 7. Formal verification

This is the category with the most in-scope research candidates (eight) and the clearest internal structure. Tools and competitions: cvc5 (TACAS 2022), the SV-COMP 2024 report (76 tools, 30,300 C tasks), Marabou (CAV 2019), the Handbook of Satisfiability (2nd ed., 2021). Neural-network verification: the 2018 symbolic-interval preprint, DeepPoly (POPL 2019), Marabou, with Reluplex (CAV 2017) and VNN-COMP (2023 report) as the lineage; the doubling of formal verification's inbound citations from computer vision is consistent with this literature (claim G-13). Smart contracts: VerX (S&P 2020), "the first automated verifier able to prove functional properties of Ethereum smart contracts" per its abstract. Learned theorem proving: MizAR 60 for Mizar 50 (ITP 2023), which reports automatic proofs of about 60% of Mizar theorems in the hammer setting and 75% with human-selected premises, through the E and Vampire provers with ENIGMA and Deepire learning and an incremental loop over millions of ATP proofs (claim G-17). The LLM-based line (Baldur, 2023; LeanDojo and DeepSeek-Prover, preprints; the 2024 position paper on formal mathematical reasoning) reports whole-proof generation on Lean and Isabelle benchmarks whose figures are not comparable across systems and are exposed to training-set overlap (open problem G-P5). Equality saturation (egg, POPL 2021; CACM research highlight 2026) and quantitative interface automata (CSL 2026) are the theory-of-verification entries. The category's primary share halved (1.06% → 0.52%) while its multi-label count grew, which suggests that works carrying both a verification and an AI or security label lose the primary label to the larger category (open problem G-P10).

# 8. Software engineering

Software engineering is where the window's change is largest and best documented. Surveys: machine-learning testing (TSE 2020, 144 papers) at the baseline, software testing with LLMs (TSE 2024, 102 studies) in the window; the latter's abstract names test-case preparation and program repair as the most common uses. Program repair and testing with pre-trained models (ICSE 2023) and universal fuzzing with LLMs (ICSE 2024) are the method entries from references.bib and the Part VII-a bibliography; SWE-bench and SWE-agent define the agentic evaluation setting. Empirical: the Management Science field experiments (Microsoft, Accenture, a Fortune 100 firm; 4,867 developers) report a 26.08% increase in completed tasks (s.e. 10.3%) with larger gains for less experienced developers, while the 2025 METR randomised trial preprint with experienced open-source developers reports slower completion. The two are not contradictory once population and outcome are distinguished (enterprise task completion versus expert time per issue in mature repositories), but the reconciliation is the specialist's reading of two abstracts (claim G-18, contested). Security: Copilot's vulnerable suggestions (2022), the user study on insecure code with assistants (CCS 2023) and the ICPEC 2025 CWE-classification study agree that high detection or completion rates coexist with poor fine-grained security reasoning (claim G-19). Co-classification with LLM reached 21.2% of the category in 2025, the highest of the six, while references to LLM works are 2.5%; whether the vocabulary shift is a method shift is open problem G-P2. The category also contains the only positive 2022-12 level change and the only significant GPT-4-date level change (claim G-09).

# 9. Synthesis

Three conclusions follow, in decreasing order of evidential strength. First, the landmark instrument fails in these areas, for identifiable and partly correctable reasons (identifier collisions, generic-title chapters, re-deposited classics, lexical misclassification, thesis cells); the correction is a selection-stage problem (G-P1), not a synthesis problem, and the specialist's audit table should accompany any use of the list. Second, the six categories grew in absolute terms and declined in relative terms after 2022; their ITS slope changes are positive but not distinguishable from baseline pseudo-events; their vocabulary moved toward language models in proportion to their distance from mathematics (software engineering and programming languages most, algorithms and complexity least); and their citation behaviour moved little. Third, the substantive developments of the window are of two kinds that the corpus treats very differently: theoretical results (flow, shortest paths, hashing, time–space simulation, 3-progressions) that the citation-normalised ranking does not see, and the entry of language models into verification, program analysis, compiler testing and software engineering, which the co-classification statistics see clearly but whose guarantees, comparability and productivity effects remain unresolved (G-P3, G-P4, G-P5).