spb/wp44_uqo

1% part07a_theory.tex — Part VII (theory half): algorithms and data structures, computational complexity, programming2% languages, compilers, formal verification, software engineering. Agent G (Theory Specialist), 2026-11-03.3% The director merges this file with part07b_security.tex into Part VII. Every corpus number is a macro of4% tables/numbers.tex (prefix \Thy..., appended by tables/make_numbers.py, Agent G block) or appears in a generated table5% (tables/make_tables.py, tables_part07a). Sources: results/graph/category_counts_yearly.csv, category_flows_yearly.csv,6% category_cooccurrence_yearly.csv; results/econometrics/breaks.csv; literature_synthesis/landmarks/{theory,software_pl}_*;7% literature_synthesis/agent_G/{claims,contributions,open_problems}.csv and review.md. Bibliography: references.bib and8% references_part07a.bib (65 entries, each resolved by one live lookup; references_verification_part07a.csv).910\section{Scope, evidence and reading rules for the theory half}11\label{sec:thy-scope}1213This half of Part~VII reviews six categories of the taxonomy: algorithms and data structures, computational14complexity, programming languages, compilers, formal verification and software engineering (the areas15\emph{theory} and \emph{software\_pl} of the ontology, Section~\ref{sec:p2-ontology}). It has two objects. The16first is the research itself: what the baseline period established in these categories, what the window added,17and where the additions are contested. The second is the instrument: the corpus statistics for the six18categories and, above all, the automatically selected landmark candidates, which in these areas turn out to19measure the bibliographic record more than the research it records. The two objects cannot be separated,20because the landmark list is the protocol's channel from corpus to synthesis, and in the theory and software21areas that channel is obstructed in ways that are themselves findings.2223Three reading rules apply. First, no full text was read. Every statement about a work rests on its metadata24(title, venue, type, year, identifiers) or on the abstract recorded in OpenAlex, and the text says which; where25an abstract is the source, the phrase ``the abstract reports'' is used deliberately. Second, works available26only as arXiv postings are preprints and are described as such, whatever their later fate. Third, the27structural-change statistics are read as the protocol prescribes (Section~\ref{sec:m-structural}): the November282022 boundary is a reference date, the placebo distribution is the test, and nothing below attributes a change29to any single event. The categories are small relative to the AI categories of Part~V (their combined primary30share in 2025 is under ten per cent of the corpus), so the statistics are those of minorities inside a31corpus whose growth is set elsewhere.3233The section proceeds from the instrument to the field. Section~\ref{sec:thy-landmarks} audits the landmark34candidates; Section~\ref{sec:thy-statistics} reports the six categories' volume, structural-change and35composition statistics; Sections~\ref{sec:thy-algorithms} to~\ref{sec:thy-se} review the categories; and36Section~\ref{sec:thy-synthesis} draws the conclusions that Part~X and Part~XI inherit.3738\section{The landmark candidates: an audit}39\label{sec:thy-landmarks}4041The protocol selects landmarks as the works with the highest field-normalised 36-month citation score42(NCS36, Section~\ref{sec:m-citations}) within each primary category, with a floor of fifteen per category, plus43the 200 most cited works overall; for 2025--2026 works the 12-month window replaces the 36-month one44(Section~\ref{sec:data-core}). The theory area contributed \ThyLandTheoryN{} candidates and the software area45\ThyLandSoftwarePlN{}, twenty-five per category, of the \SelectionLandmarks{} landmarks of the whole corpus.46Before any of the \ThyAuditN{} can be called a landmark, the list has to be audited, and the audit is the first47result of this section (Table~\ref{tab:theory_landmark_audit}). Each candidate received one of eight verdicts48from its metadata and, where available, its abstract: an in-scope research contribution49(\ThyAuditVerdictInScopeResearch{} candidates), an in-scope survey or report (\ThyAuditVerdictInScopeSurvey{}),50a misclassified work outside the category and outside the theory and software scope51(\ThyAuditVerdictMisclassified{}), a thesis (\ThyAuditVerdictDissertation{}), a classic re-deposited under a52recent record date (\ThyAuditVerdictReprintMisdated{}), a textbook or chapter (\ThyAuditVerdictTextbook{}), a53metaphor-based metaheuristic (\ThyAuditVerdictMetaheuristic{}) or a duplicate record54(\ThyAuditVerdictDuplicate{}). Fewer than one candidate in five is a research contribution inside its55category, and only \ThyAuditInScopeResearchPost{} of those are post-period works. Four mechanisms account56for the rest.5758\input{tables/tab_theory_landmark_audit}5960\paragraph{Identifier collisions.}61\ThyAuditIdCollision{} candidates carry OpenAlex identifiers that, resolved against the live database on623~November 2026, return a different work. The record titled ``Exploiting Generative AI to Scale up Intelligent63Tutoring Systems'', with the DOI of an ITP~2023 paper, resolves to \emph{Attention Is All You Need}; the abstract64stored for it in the corpus is that of \emph{MizAR~60 for Mizar~50}, which is what the DOI denotes65\citep{jakubuv2023mizar}; its 36-month citation count in the corpus is that of the Transformer paper, which is66why it ranks first in the whole software area. The ECOOP~2025 paper on functionality-specific67vulnerabilities \citep{chen2025apiss} resolves to the graph-convolutional-network preprint; the SEA~202468paper on learned branching for maximum independent set \citep{langedal2024mis} to GraphSAGE; the WADS~202569Kd-tree paper \citep{pham2025kdtree} to the variational-autoencoder preprint; the SAIA~2024 robustness70framework \citep{awadid2025robust} to the adversarial-training preprint of Madry and co-authors; an71ESEM~2026 record \citep{naqvi2026bigger} to the Codex paper; and a DX~2024 answer-set-programming paper72\citep{klampfl2024asp} to an unrelated preprint. In every case the recorded citation window matches the other73work's count.\footnote{Raw responses in \texttt{literature\_synthesis/agent\_G/verification\_lookups\_raw.txt}.74The mechanism (identifier merging or reuse between the snapshot of 14~October 2026 and the live database) is75inferred; the consequence, that the citation windows of these records belong to other works, is observed.} The76four top-ranked candidates of the software area and the top-ranked candidate of the theory area owe their rank77to citations that are not theirs. The same check should be run on the other areas' lists before Part~IX uses78them.7980\paragraph{Generic-title chapters.}81Chapters titled ``Introduction to Algorithms'' (2020, 2021, 2023), ``Particle Swarm Optimization'' (2019),82``Introduction to Software Testing'' (2021), ``Introduction to Graph Theory'' (2023), and Royce's 1970 paper on83managing large software developments reprinted in a 2021 anthology, carry hundreds to thousands of citations in84their windows, and live lookups confirm the counts. The plausible reading, offered as an interpretation, is85that citations intended for the canonical work are attributed to a same-titled chapter by the indexer's86reference matching. Whatever the mechanism, a chapter of a 2023 undergraduate textbook is not a landmark of872023 research.8889\paragraph{Re-deposited classics.}90\ThyAuditVerdictReprintMisdated{} records are works whose record date is the date of a deposit, reprint or91re-posting rather than of the work. Dijkstra's 1959 note on two problems in connexion with graphs appears as a922022 ACM Books chapter; Turing's 1936 paper as a 2021 MIT Press chapter; the 1994 survey of decidability for93Petri nets as a 2024 arXiv posting; Lynch and Tuttle's introduction to input/output automata as a 2026 journal94article \citep{lynch2026ioautomata}; the \emph{egg} equality-saturation paper \citep{willsey2021egg} as a 202695research highlight \citep{willsey2026eggcacm}; doctoral theses of the early 2000s as 2026 repository records;96three theses of the L4/seL4 verification school as 2022 records; and the 2018 conference paper on online97algorithms with machine-learned predictions as a 2024 arXiv posting. Because the year field is the deposit year,98these records enter the post period: \ThyLandTheoryDatedTwentysix{} of the \ThyLandTheoryN{} theory candidates99and \ThyLandSoftwarePlDatedTwentysix{} of the \ThyLandSoftwarePlN{} software candidates are dated 2026, a year100of which the corpus holds ten months.101102\paragraph{Lexical misclassification and small cells.}103\ThyAuditVerdictMisclassified{} candidates are outside the theory and software scope altogether. The104computational-complexity list contains \ThyAuditComputationalComplexityMisclassified{} such works of its105\ThyAuditComputationalComplexityN{}: technology-acceptance models of mobile learning, PLS-SEM studies of106small enterprises and of students' well-being, a Routledge volume on complexity theory in the social sciences,107a review of fringe-projection profilometry, captured by the word ``complexity''. The compilers list contains108\ThyAuditCompilersMisclassified{}, captured by ``just-in-time'' (adaptive interventions in mental health),109``compiling'' (a guide to literature reviews) and ``polyhedral'' (power-system dispatch). The110programming-languages list includes a Nature paper on Calabi--Yau manifolds in black-hole scattering. The111classifier's per-category precision, estimated on the validation sample (Section~\ref{sec:m-validation}), is112the right place to quantify this; what the landmark list shows is the interaction between imprecision and113normalisation. NCS36 divides a work's citations by the expectation for its category, year and type114(Section~\ref{sec:m-citations}); cells of theses or of non-computing articles are small and lightly cited, so a115thesis with a handful of citations, or a social-science article with a hundred, obtains a normalised score that116no STOC paper of the same year can match. \ThyAuditVerdictDissertation{} of the \ThyAuditN{} candidates are117theses.118119What survives is a set of \ThyAuditVerdictInScopeResearch{} research works and \ThyAuditVerdictInScopeSurvey{}120surveys or reports, listed in Table~\ref{tab:theory_landmarks_discussed}. They are reviewed below with the121pre-2022 lineage of Part~II and with the window's results that the ranking does not see: the major theoretical122results of 2022--2025 are absent from the candidate list and enter this review through verified bibliographic123records, not through the corpus ranking. Open problem~G-P1 of Part~X states the correction: type filters,124live re-resolution of identifiers and venue priors at the selection stage, evaluated against a125specialist-labelled sample.126127\input{tables/tab_theory_landmarks_discussed}128129\section{Volume, structural change and composition}130\label{sec:thy-statistics}131132\subsection{Growth in absolute terms, decline in relative terms}133134Table~\ref{tab:theory_counts} gives the yearly counts of works carrying each category (multi-label) and of135works whose primary category it is; Table~\ref{tab:theory_summary} summarises growth and structural change.136The multi-label counts grew in every category after 2022. Between 2023 and 2025 the compound annual growth was137\ThyCagrMultilabelSoftwareEngineeringPostPct\% for software engineering,138\ThyCagrMultilabelComputationalComplexityPostPct\% for computational complexity,139\ThyCagrMultilabelCompilersPostPct\% for compilers, \ThyCagrMultilabelAlgorithmsPostPct\% for algorithms,140\ThyCagrMultilabelFormalVerificationPostPct\% for formal verification and141\ThyCagrMultilabelProgrammingLanguagesPostPct\% for programming languages, against142\ThyCagrMultilabelSoftwareEngineeringBaselinePct\%, \ThyCagrMultilabelComputationalComplexityBaselinePct\%,143\ThyCagrMultilabelCompilersBaselinePct\%, \ThyCagrMultilabelAlgorithmsBaselinePct\%,144\ThyCagrMultilabelFormalVerificationBaselinePct\% and \ThyCagrMultilabelProgrammingLanguagesBaselinePct\%145between 2018 and 2022. The acceleration is real but not specific: the corpus-wide multi-label growth rose from146\ThyCagrMultilabelTotalBaselinePct\% to \ThyCagrMultilabelTotalPostPct\% over the same periods, so the six147categories accelerated with the corpus rather than within it. Measured by primary-label share, every category148lost ground between 2018 and 2025: algorithms from \ThySharePrimaryAlgorithmsTwoZeroOneEightPct\% to149\ThySharePrimaryAlgorithmsTwoZeroTwoFivePct\%, software engineering from150\ThySharePrimarySoftwareEngineeringTwoZeroOneEightPct\% to \ThySharePrimarySoftwareEngineeringTwoZeroTwoFivePct\%,151formal verification from \ThySharePrimaryFormalVerificationTwoZeroOneEightPct\% to152\ThySharePrimaryFormalVerificationTwoZeroTwoFivePct\%, programming languages from153\ThySharePrimaryProgrammingLanguagesTwoZeroOneEightPct\% to \ThySharePrimaryProgrammingLanguagesTwoZeroTwoFivePct\%,154computational complexity from \ThySharePrimaryComputationalComplexityTwoZeroOneEightPct\% to155\ThySharePrimaryComputationalComplexityTwoZeroTwoFivePct\% and compilers from156\ThySharePrimaryCompilersTwoZeroOneEightPct\% to \ThySharePrimaryCompilersTwoZeroTwoFivePct\%. The theory and157software categories are growing and shrinking at once: more works, a smaller fraction of a corpus whose growth158is set by the AI categories of Part~V.159160\input{tables/tab_theory_counts}161162Two cautions attach to these numbers. The post-period growth rate spans two years and is exposed to the163indexing lag of the most recent year (Section~\ref{sec:m-truncation}); the primary-label counts for 2025 are164the last complete ones. And the file \texttt{results/bibliometrics/cagr\_by\_category.csv}, from which165Table~\ref{tab:cagr} is generated, reports primary counts for these categories about three times smaller than166those of the graph counts file (algorithms in 2018: \ThyCagrfileAlgorithmsNTwoZeroOneEight{} against167\ThyCountAlgorithmsTwoZeroOneEightPrimary{}), so it predates the current classification; its growth rates are168not used here, and the discrepancy is recorded for the reproducibility audit.\footnote{The generator169\texttt{bibliometrics/04\_diversity\_cagr.py} reads \texttt{category\_counts\_yearly.csv}; re-running it on the170current counts resolves the discrepancy. Until then, Table~\ref{tab:cagr} and Table~\ref{tab:theory_summary}171disagree for these six rows.}172173\subsection{Structural change at the reference date}174175The interrupted-time-series slope change at December 2022 is positive for all six primary-label series and176significant with HAC standard errors (Section~\ref{sec:m-its}): \ThyBreakAlgorithmsChatgptSlopePct\% per month177for algorithms, \ThyBreakComputationalComplexityChatgptSlopePct\% for computational complexity,178\ThyBreakProgrammingLanguagesChatgptSlopePct\% for programming languages,179\ThyBreakCompilersChatgptSlopePct\% for compilers, \ThyBreakFormalVerificationChatgptSlopePct\% for formal180verification and \ThyBreakSoftwareEngineeringChatgptSlopePct\% for software engineering. The placebo test181(Section~\ref{sec:m-placebo}) does not confirm any of them at the five per cent level: the share of182baseline-period pseudo-events whose slope statistic exceeds the observed one is183\ThyBreakAlgorithmsPlaceboSlopeP{} for algorithms, \ThyBreakComputationalComplexityPlaceboSlopeP{} for184computational complexity, \ThyBreakSoftwareEngineeringPlaceboSlopeP{} for software engineering,185\ThyBreakCompilersPlaceboSlopeP{} for compilers, \ThyBreakFormalVerificationPlaceboSlopeP{} for formal186verification and \ThyBreakProgrammingLanguagesPlaceboSlopeP{} for programming languages. The two theory187categories are closest to the threshold; none crosses it. A slope change that pseudo-events of the baseline188reproduce at these rates is a feature of series that were already accelerating, not of the reference date.189190\input{tables/tab_theory_summary}191192The level changes point the other way in five categories. At December 2022 the level fell by193\ThyBreakFormalVerificationChatgptLevelPct\% for formal verification ($p = \ThyBreakFormalVerificationChatgptLevelP$),194\ThyBreakComputationalComplexityChatgptLevelPct\% for computational complexity195($p = \ThyBreakComputationalComplexityChatgptLevelP$), \ThyBreakAlgorithmsChatgptLevelPct\% for algorithms196($p = \ThyBreakAlgorithmsChatgptLevelP$), \ThyBreakProgrammingLanguagesChatgptLevelPct\% for programming197languages and \ThyBreakCompilersChatgptLevelPct\% for compilers (both not significant); only software198engineering shows a positive level change (\ThyBreakSoftwareEngineeringChatgptLevelPct\%,199$p = \ThyBreakSoftwareEngineeringChatgptLevelP$), and it is also the only category with a significant positive200level change at the GPT-4 date (\ThyBreakSoftwareEngineeringGptFourLevel{},201$p = \ThyBreakSoftwareEngineeringGptFourLevelP$; Section~\ref{sec:m-altdates}). The negative level changes202are at least partly the seasonality of proceedings dates in categories dominated by conferences, and the203alternative-date estimates for the o1 date (\ThyBreakComputationalComplexityOOneLevel{} for computational204complexity, $p = \ThyBreakComputationalComplexityOOneLevelP$) show how sensitive a level estimate is to where205the window is cut. The Bai--Perron procedure (Section~\ref{sec:m-bp}) dates a single break at206\ThyBreakAlgorithmsBpBreaksBic{} for algorithms, computational complexity and compilers, two breaks for207programming languages (\ThyBreakProgrammingLanguagesBpBreaksBic{}) and formal verification208(\ThyBreakFormalVerificationBpBreaksBic{}), and one at \ThyBreakSoftwareEngineeringBpBreaksBic{} for software209engineering: the data-driven dates fall in spring 2023 for the three categories with a single break, which is210after the reference date and before the GPT-4 release had been indexed, and they say nothing about cause.211212\subsection{Vocabulary moves, citations do not}213214Composition is where the window is visible. Table~\ref{tab:theory_llm_cooccurrence} reports, for each215category and year, the number of works that the multi-label classifier also assigns to the LLM category and216their share of the category. Between 2022 and 2025 that share rose from217\ThyCoocSoftwareEngineeringLlmTwoZeroTwoTwoPct\% to \ThyCoocSoftwareEngineeringLlmTwoZeroTwoFivePct\% in218software engineering, from \ThyCoocProgrammingLanguagesLlmTwoZeroTwoTwoPct\% to219\ThyCoocProgrammingLanguagesLlmTwoZeroTwoFivePct\% in programming languages, from220\ThyCoocCompilersLlmTwoZeroTwoTwoPct\% to \ThyCoocCompilersLlmTwoZeroTwoFivePct\% in compilers, from221\ThyCoocFormalVerificationLlmTwoZeroTwoTwoPct\% to \ThyCoocFormalVerificationLlmTwoZeroTwoFivePct\% in formal222verification, and from \ThyCoocAlgorithmsLlmTwoZeroTwoTwoPct\% to \ThyCoocAlgorithmsLlmTwoZeroTwoFivePct\% in223both algorithms and computational complexity. The gradient runs from the code-facing categories to the224mathematical ones, and it is a gradient of vocabulary: co-classification is a lexical and topical signal225(Section~\ref{sec:m-classification}), not a measure of method adoption.226227\input{tables/tab_theory_llm_cooccurrence}228229Citation flows are more conservative. In the post period, software-engineering works direct230\ThyFlowSoftwareEngineeringToLlmPostPct\% of their categorised references to works of the LLM category,231computational complexity \ThyFlowComputationalComplexityToLlmPostPct\%, compilers232\ThyFlowCompilersToLlmPostPct\%, programming languages \ThyFlowProgrammingLanguagesToLlmPostPct\%, formal233verification \ThyFlowFormalVerificationToLlmPostPct\% and algorithms \ThyFlowAlgorithmsToLlmPostPct\%; the234within-category shares barely moved (algorithms \ThyFlowAlgorithmsToAlgorithmsBaselinePct\% to235\ThyFlowAlgorithmsToAlgorithmsPostPct\%, software engineering236\ThyFlowSoftwareEngineeringToSoftwareEngineeringBaselinePct\% to237\ThyFlowSoftwareEngineeringToSoftwareEngineeringPostPct\%, formal verification238\ThyFlowFormalVerificationToFormalVerificationBaselinePct\% to239\ThyFlowFormalVerificationToFormalVerificationPostPct\%).\footnote{Flows are aggregated from240\texttt{results/graph/category\_flows\_yearly.csv} over citing years 2018--2022 (baseline) and 2023--2026241(post) and are shares of the references that fall inside the categorised corpus (Section~\ref{sec:m-citgraph}).242The LLM category is young, which depresses its share of cited works mechanically; the comparison with the243co-classification shares is therefore indicative, not a test.} Two flow changes deserve notice. The244self-citation share of computational complexity fell from245\ThyFlowComputationalComplexityToComputationalComplexityBaselinePct\% to246\ThyFlowComputationalComplexityToComputationalComplexityPostPct\% while its references to human--computer247interaction rose from \ThyFlowComputationalComplexityToHciBaselinePct\% to248\ThyFlowComputationalComplexityToHciPostPct\%; given the candidate list of249Section~\ref{sec:thy-landmarks}, this is more plausibly the category's contamination by social-science works250than a change in theoretical research, and it is recorded as a contested reading. Inbound citations to formal251verification from computer vision doubled, from \ThyInflowFormalVerificationFromComputerVisionBaselinePct\% to252\ThyInflowFormalVerificationFromComputerVisionPostPct\% of the category's inbound references, which is253consistent with the neural-network verification literature reviewed in Section~\ref{sec:thy-fv} being cited by254robustness work; no paper-level breakdown tests this.255256\section{Algorithms and data structures}257\label{sec:thy-algorithms}258259\subsection{What the window established}260261The category's largest results are not in the candidate list, and the first task of the review is to say what262they are, from verified records. Maximum flow and minimum-cost flow were brought to almost-linear time263\citep{chen2022maxflow}, closing a line of work that had run through interior-point methods and dynamic graph264data structures for a decade. Single-source shortest paths with negative weights were brought to near-linear265time by a combinatorial algorithm \citep{bernstein2022negative}, a result republished in the \emph{Journal of266the ACM} and \emph{Communications of the ACM} in 2025. The sorting barrier for directed single-source shortest267paths, the $\Omega(m + n \log n)$ cost that Dijkstra's algorithm with a priority queue cannot avoid, was268broken by a deterministic $O(m \log^{2/3} n)$ algorithm \citep{duan2025sorting}, the best paper of STOC~2025.269In data structures, the open-addressing bounds conjectured by Yao in 1985 were shown to be beatable: without270reordering, a greedy scheme achieves expected amortised probe complexity $O(\log^2 \delta^{-1})$ at load271$1 - \delta$, against the conjectured $\Theta(\delta^{-1})$ \citep{farachcolton2024openaddressing}. These272four results, from 2022 to 2025, are what a specialist would list first for the window; none has the citation273profile that the ranking rewards, because theoretical results are cited by a small community over long274horizons, and the 36-month window and the field normalisation are both calibrated on the behaviour of275applied categories.276277What the corpus does record is the programme of \emph{algorithms with predictions}, which the baseline period278established and the window continued. The candidate list carries it through a 2024 arXiv re-posting of the 2018279conference paper on ski rental and non-clairvoyant scheduling with machine-learned predictions, whose280abstract describes algorithms that are ``oblivious to the performance of the predictor, improve with better281predictions, but do not degrade much if the predictions are poor''; the programme's canonical references are282the journal version of competitive caching with learned advice \citep{lykouris2021caching} and the overview in283\emph{Communications of the ACM} \citep{mitzenmacher2022predictions}. The formal object is a pair of284guarantees, consistency (the competitive ratio when the prediction is exact) and robustness (the ratio under285arbitrary error), with a trade-off between them; it is the point at which online algorithms and machine286learning meet without either giving up its guarantees, and it is the one place in the category where the287``learning'' vocabulary of the window names a theory rather than a tool. The fine-grained complexity programme288that organised algorithms research at the baseline (Section~\ref{sec:p2-theory}) is represented in the289bibliography by the ICM survey \citep{vassilevskawilliams2019finegrained} and by the parameterized-algorithms290monograph \citep{cygan2015parameterized}.291292\subsection{What the candidate list contains}293294Of the \ThyAuditAlgorithmsN{} algorithms candidates, \ThyAuditAlgorithmsInScopeResearch{} are research295contributions and none is misclassified; the rest are textbook chapters, re-deposited classics, theses and296metaheuristics. The two post-period research candidates are modest and both carry citation counts that belong297to other works: the WADS~2025 paper extends Kd-trees to Bregman divergences, shows that the triangle inequality298is not needed for correct pruning, and reports two orders of magnitude over linear search for299Kullback--Leibler nearest-neighbour queries in up to a hundred dimensions \citep{pham2025kdtree}; the SEA~2024300paper replaces the highest-degree branching rule of branch-and-reduce for maximum independent set with a graph301neural network \citep{langedal2024mis}. Both abstracts describe engineering contributions with experimental302evaluation, which is what algorithm engineering is; neither is the kind of result that defines the window.303304The other research genre in the list is the metaphor-based metaheuristic: the Arithmetic Optimization Algorithm305\citep{abualigah2021aoa} and the Aquila Optimizer \citep{abualigah2021aquila} in 2021, and the artificial306lemming, glider snake, gray langur and starfish optimisers in 2025--2026, published in engineering and307AI-review journals and evaluated on CEC benchmark functions and constrained design problems. The abstracts share308a template, a natural metaphor mathematically modelled into exploration and exploitation phases and309``outperforming or matching'' a dozen earlier metaheuristics. The operational-research literature has argued310since \citet{sorensen2013metaphor} that the genre re-describes existing methods under new names and that its311benchmarks do not discriminate; the position was restated in a ``call for action'' \citep{aranha2021metaphor}312and substantiated for six widely cited algorithms, shown to be equivalent to or special cases of earlier313methods \citep{camachovillalon2022exposing}. The corpus does not adjudicate this dispute; what it shows is314the genre's weight in the highly cited stratum of the algorithms category, where six of twenty-five candidates315belong to it and where the post-2022 research articles with the highest normalised scores are of this kind.316Whether the genre grows faster than the rest of the category and absorbs a growing share of its citations is an317open problem of Part~X (G-P7), answerable with a keyword-defined subseries.318319\subsection{Algorithms discovered by learning systems}320321Three Nature papers and one preprint report algorithms found by reinforcement learning or program search:322faster matrix-multiplication tensor decompositions for small sizes \citep{fawzi2022alphatensor}, shorter323sorting networks for short sequences, merged into a standard library \citep{mankowitz2023alphadev}, new324constructions for the cap-set problem and bin packing from evolved programs \citep{romeraparedes2024funsearch},325and, as a 2025 preprint, a coding agent that reports improvements on a collection of open mathematical and326algorithmic problems \citep{novikov2025alphaevolve}. All four are reports by the developers; the improvements327are on specific instances; and no independent reproduction or extension by the theory community appears in the328verified bibliography. The question these works pose to the category, whether search over programs changes how329algorithms are designed or only how constants are tuned, is one the corpus cannot answer at this granularity;330it is stated as open problem G-P9. The honest position is that the window's algorithmic breakthroughs were331obtained by people, and that the learned-discovery results are promising, contested in scope, and awaiting332replication.333334\section{Computational complexity}335\label{sec:thy-complexity}336337The category's statistics are the least trustworthy of the six: \ThyAuditComputationalComplexityMisclassified{}338of its \ThyAuditComputationalComplexityN{} candidates are outside computing, and the flow and co-occurrence339changes of Section~\ref{sec:thy-statistics} are to that extent artefacts. The two in-scope research candidates340are a STOC~2019 paper and a 2026 \emph{Theoretical Computer Science} article on SAT in spiking neural P systems341(no abstract). The STOC paper is a genuine landmark of the baseline: its abstract describes the reachability342problem for Petri nets as open since the 1960s, with Lipton's 1976 exponential-space lower bound unimproved, and343establishes a non-elementary lower bound \citep{czerwinski2019petri}. The story was completed within the344baseline period, when reachability in vector addition systems was shown Ackermann-complete345\citep{czerwinski2021ackermann,leroux2021notprimitive}, matching the upper bound of Leroux and Schmitz; the346window inherits a closed problem whose closure the corpus ranks below a technology-acceptance survey.347348The window's own contribution to complexity theory that a specialist would name first is the simulation of349time $t$ in space $O(\sqrt{t \log t})$ \citep{williams2025sqrtspace}, which improves the Hopcroft--Paul--Valiant350simulation of 1975 after fifty years and implies, through a known argument, that there are problems solvable351in linear space that need nearly quadratic time on multitape machines; the paper is a STOC~2025 result352republished in the \emph{Journal of the ACM} in 2026. In additive combinatorics, the strong bounds for353three-term arithmetic progressions \citep{kelley2023threeap} brought the Roth-type exponent to a form conjectured354since Behrend. Neither appears in the candidate list; both enter through verified records, and the general355point is the one made for algorithms: results of this kind are cited slowly and by few, and a 36-month356field-normalised window does not see them.357358The boundary with language models is where the category's co-classification share grew, yet the relevant359works are mostly classified elsewhere. The proof that transformers with logarithmic precision lie in uniform360$\mathrm{TC}^0$ \citep{merrill2023parallelism}, and the survey of what formal languages transformers can361express \citep{strobl2024survey}, bound what a single forward pass can compute and make the case that362chain-of-thought computation is where additional expressive power must come from; they are, in the verified363bibliography, the window's main contribution of complexity theory to the study of the models that dominate364Part~V. Whether such works are classified under computational complexity or under natural language processing365is an empirical question about the taxonomy (open problem G-P8). The remainder of the candidate list is366teaching material, including the fourth edition of the Kolmogorov-complexity monograph \citep{li2019kolmogorov}367and undergraduate chapters on complexity and on parameterized complexity, and re-deposited classics, including368Turing's 1936 paper and Wolfram's cellular-automata chapters.369370\section{Programming languages}371\label{sec:thy-pl}372373The baseline lineage was set out in Section~\ref{sec:p2-pl}: Rust and its semantic foundation374\citep{matsakis2014rust,jung2017rustbelt,jung2021saferust}, Lean~4 as a prover that is also a programming375language \citep{demoura2021lean4} with its mathematical library \citep{mathlib2020}, and the verified376artefacts CompCert \citep{leroy2009compcert} and seL4 \citep{klein2009sel4} that showed production software377can be proved correct. The candidate list records this lineage only obliquely, through three theses of the378L4/seL4 school re-deposited in 2022 (separation logic for programs in virtual memory, formal memory models for379C systems code, a verified multiprocessor kernel design), which the ranking places in the post period. In the380window the lineage continued with Verus \citep{lattuada2024verus}, a verification framework for Rust programs381presented at SOSP~2024, which treats the ownership discipline of the language as the foundation for382specification and proof rather than as an obstacle to them; the content of Verus is known here from its verified383title and venue only.384385Of the \ThyAuditProgrammingLanguagesN{} candidates, \ThyAuditProgrammingLanguagesInScopeResearch{} are386research contributions. Two of them mark the entry of language models into the community's top venue in3872024. LLift \citep{li2024llift} combines static analysis with an LLM to find use-before-initialisation bugs in388the Linux kernel; its abstract reports post-constraint guidance of the path analysis, procedures for handling389``the unpredictable nature of LLMs'', and four previously unknown bugs acknowledged by the kernel community.390WhiteFox \citep{yang2024whitefox} is described by its abstract as the first white-box compiler fuzzer that uses391an LLM reading the source code of optimisations to generate test programs that exercise them, against392black- and grey-box fuzzing that lacks that information and symbolic execution that does not scale to a393compiler. Both papers report bugs found; neither reports a guarantee, and the abstracts do not claim one. The394natural comparison is with the two instruments that the compiler community built for correctness before the395window, Csmith's random differential testing, which found hundreds of bugs in production C compilers396\citep{yang2011csmith}, and Alive2's bounded translation validation of LLVM optimisations397\citep{lopes2021alive2}; whether LLM-generated tests can be combined with validation of that kind, so that the398share of reported bugs that are confirmed can be measured per optimisation pass, is open problem G-P4. The399third research candidate, ZEUS \citep{kalra2018zeus}, is the baseline representative of program analysis for a400new target: abstract interpretation and constrained Horn clauses applied to smart contracts, with an abstract401reporting that about 95\% of 22,400 contracts analysed were vulnerable. The universal fuzzer of402\citet{xia2024fuzz4all} and the LLM-based bug-reproduction study of \citet{kang2023fewshottesters} are the403software-engineering counterparts of the same move.404405The category's vocabulary moved more than any except software engineering's: co-classification with the LLM406category reached \ThyCoocProgrammingLanguagesLlmTwoZeroTwoFivePct\% in 2025. Its references to LLM works are407\ThyFlowProgrammingLanguagesToLlmPostPct\%, and its structural ties are unchanged, with408\ThyFlowProgrammingLanguagesToFormalVerificationPostPct\% of its references going to formal verification and409\ThyFlowProgrammingLanguagesToSoftwareEngineeringPostPct\% to software engineering in the post period, against410\ThyFlowProgrammingLanguagesToFormalVerificationBaselinePct\% and411\ThyFlowProgrammingLanguagesToSoftwareEngineeringBaselinePct\% at the baseline. Programming languages is, in412the citation graph, the hinge between verification and engineering, and the window did not move the hinge.413414\section{Compilers}415\label{sec:thy-compilers}416417Compilers is the smallest of the six categories, \ThySharePrimaryCompilersTwoZeroTwoFivePct\% of primary labels418in 2025, and the most lexically contaminated after complexity. Its in-scope candidates nevertheless trace a419coherent line. At the baseline, MLIR \citep{lattner2021mlir} is the infrastructure whose abstract promises to420reduce ``the cost of building domain specific compilers'' and to connect existing ones; Tiramisu421\citep{baghdadi2019tiramisu} is a polyhedral compiler whose scheduling language separates algorithm, loop422transformation, data layout and communication so that one algorithm can target multicores, GPUs and423distributed machines; ExaStencils is a four-layer domain-specific language for multigrid solvers. Two surveys424establish that learned compiler heuristics are a programme older than the window: the \emph{Proceedings of the425IEEE} survey of machine learning in compiler optimisation \citep{wang2018mlcompiler} and the \emph{Computing426Surveys} review of autotuning, optimisation selection and phase ordering \citep{ashouri2018autotuning}, which427dates the first attempts to the mid-1990s. Three MIT and Delaware theses on learned optimisation selection and428on sparse tensor-algebra compilation complete the baseline picture.429430The post-period candidates show the programme's change of scale. LLM4VV \citep{munley2024llm4vv} uses language431models to generate a validation test suite for directive-based parallel programming compilers (metadata only;432no abstract). LLM Compiler \citep{cummins2025llmcompiler} is a suite of foundation models built on Code Llama433and trained, per its abstract, on 546 billion tokens of LLVM intermediate representation and assembly, then434instruction-tuned to predict and emulate compiler behaviour; fine-tuned versions reach 77\% of the optimising435potential of an autotuning search for code size and disassemble x86-64 and ARM assembly back to LLVM-IR. The436preprint that preceded it \citep{cummins2023llmcompiler} framed the task as predicting optimisation-pass437sequences. The shift is from learning a heuristic inside a compiler, with features chosen by compiler writers,438to pre-training a model on the compiler's own artefacts; what the shift leaves open is the question that439compiler research has always had to answer last, correctness, which the field handled through differential440testing \citep{yang2011csmith} and translation validation \citep{lopes2021alive2} rather than through model441evaluation. Co-classification with the LLM category reached \ThyCoocCompilersLlmTwoZeroTwoFivePct\% in 2025;442references to LLM works are \ThyFlowCompilersToLlmPostPct\%, and the category's citations continue to go443first to computer architecture (\ThyFlowCompilersToComputerArchitecturePostPct\% of references in the post444period) and to itself. The deep-learning compiler stack recorded in the main bibliography, TVM, Triton and445PyTorch~2 \citep{chen2018tvm,tillet2019triton,ansel2024pytorch2}, and the image-processing DSL that preceded446it \citep{ragankelley2013halide}, belong to Part~VI and are only noted here as the other post-2018 development447of the category.448449\section{Formal verification}450\label{sec:thy-fv}451452Formal verification has the most in-scope research candidates of the six453(\ThyAuditFormalVerificationInScopeResearch{} of \ThyAuditFormalVerificationN{}) and the clearest internal454structure, which the review follows: solvers and competitions, neural-network verification, verification of new455targets, learned theorem proving, and the theory of verification.456457\paragraph{Solvers and competitions.}458cvc5 \citep{barbosa2022cvc5} is the system description of the SMT solver that succeeded CVC4, evaluated on all459SMT-LIB benchmarks against CVC4 and Z3; the Handbook of Satisfiability in its second edition460\citep{biere2021handbook} is the reference work, present twice in the candidate list under two records. The461SV-COMP~2024 report \citep{beyer2024svcomp} describes the largest edition of the software-verification462competition to that date, 76 tools from 34 teams on 30,300 verification tasks for C programs, with a second463track for witness validation and a new witness format. Competitions of this kind are the category's benchmark464culture, and they are a point of contrast with the benchmark culture of Part~V: the tasks are fixed programs465with fixed specifications, a tool's result is a proof or a counterexample that a validator checks, and the466score is not self-reported.467468\paragraph{Neural-network verification.}469The baseline built a sub-field: Reluplex \citep{katz2017reluplex} extended the simplex method to ReLU470constraints; the 2018 symbolic-interval preprint in the candidate list argued, per its abstract, that existing471analyses ``struggle to scale beyond very small networks'' and proposed interval propagation that does;472DeepPoly \citep{singh2019deeppoly} introduced an abstract domain of floating-point polyhedra with intervals and473transformers for ReLU, sigmoid, tanh and maxpool, and reported the first proofs of robustness to rotations474with interpolation; Marabou \citep{katz2019marabou} packaged SMT-based verification as a framework accepting475TensorFlow models. The VNN-COMP report \citep{brix2023vnncomp} summarises the first three years of the476competition that organised the sub-field. The doubling of formal verification's inbound citations from477computer vision in the post period (Section~\ref{sec:thy-statistics}) is consistent with this literature being478cited by robustness work, and the sub-field is the main channel through which the category meets the479machine-learning categories; whether it has guarantees that survive the scale of the models of Part~V is not a480question these abstracts address.481482\paragraph{New targets.}483VerX \citep{permenev2020verx} is described by its abstract as the first automated verifier of functional484properties of Ethereum smart contracts, combining reduction of temporal properties to reachability, a symbolic485execution engine for the Ethereum virtual machine, and delayed predicate abstraction, evaluated on 83486properties of 12 projects. The answer-set-programming monitor for automated driving \citep{klampfl2024asp}487and the theses on parametric and multi-objective Markov models represent runtime and probabilistic488verification; the Warwick thesis on model checking quantum protocols, re-deposited with a 2026 date, is a489baseline work of the previous decade.490491\paragraph{Learned theorem proving.}492The abstract attached in the corpus to the ITP~2023 paper, under a wrong title (Section~\ref{sec:thy-landmarks}),493is the clearest statement in the candidate set of what machine learning has done for automated reasoning:494MizAR \citep{jakubuv2023mizar} proves about 60\% of the theorems of the Mizar Mathematical Library in the hammer495setting and 75\% when given the premises of the human proofs, through the E and Vampire provers with the ENIGMA496and Deepire learned guidance and an incremental loop that grows a corpus of millions of proofs while training497stronger systems on it. This is the saturation-prover line. The language-model line is represented by Baldur498\citep{first2023baldur}, which generates and repairs whole Isabelle proofs; by LeanDojo499\citep{yang2023leandojo} and DeepSeek-Prover \citep{xin2024deepseekprover}, both preprints, which report500retrieval-augmented and synthetic-data-trained provers on Lean benchmarks; and by the position paper on formal501mathematical reasoning as a frontier \citep{yang2024formalmath}, also a preprint. The figures these works502report are on different benchmarks, under different compute budgets, with the possibility of overlap between503training corpora and test theorems that the abstracts do not exclude; a benchmark of theorems posted after the504training cut-off, with proof checking rather than self-reported success, is the direction stated as open505problem G-P5. The machine-learned mathematics of Part~V, olympiad geometry \citep{trinh2024alphageometry} and506program search \citep{romeraparedes2024funsearch}, is adjacent but distinct: it produces objects that a human or507a checker then verifies, where the works above produce the proofs.508509\paragraph{Theory of verification.}510Equality saturation as implemented in \emph{egg} \citep{willsey2021egg}, whose abstract describes e-graph511rewriting that ``only adds information'' and extraction by a user-supplied cost function, is a baseline result512republished as a research highlight in 2026; the quantitative interface automata of the CSL~2026 paper on reward513interfaces, whose abstract introduces multi-valued correctness requirements and best-effort satisfaction into514interface theories, is the one post-period research candidate of this kind.515516The category's primary share halved between 2018 and 2025 while its multi-label count grew by eleven per cent517(Table~\ref{tab:theory_counts}). The arithmetic of the argmax assignment (Section~\ref{sec:m-score}) suggests518why: a work that carries a verification label and an AI or security label loses the primary label to the519larger category when the scores are close, so the primary series understates a category whose work is520increasingly done in combination. Measuring the share of works whose primary label switched, by co-assigned521category and year, is open problem G-P10.522523\section{Software engineering}524\label{sec:thy-se}525526Software engineering is where the window's change is largest, best documented, and most contested. Its527baseline was not AI-free (Section~\ref{sec:p2-pl}): the Codex models \citep{chen2021codex}, the528code-generation benchmarks \citep{austin2021mbpp}, the systematic evaluation of code models529\citep{xu2022codelms} and the first productivity assessment of neural code completion530\citep{ziegler2022copilot} precede the reference date, and the survey of machine-learning testing531\citep{zhang2022mltesting}, 144 papers on testing properties, components and workflows of learned systems,532shows the category already organised around learned software as an object of test. The window's surveys533reverse the direction of the relation. The survey of software testing with large language models534\citep{wang2024llmtesting} analyses 102 studies and reports, per its abstract, that test-case preparation and535program repair are the most common uses; the two systematic reviews of language models for software536engineering \citep{fan2023llm4se,hou2024llm4se} and the code-generation survey \citep{jiang2024codegensurvey}537map the same territory. Method papers from the main bibliography and the Part~VII-a bibliography give the538texture: program repair in the era of pre-trained models \citep{xia2023apr}, bug reproduction from reports539\citep{kang2023fewshottesters}, universal fuzzing \citep{xia2024fuzz4all}, and the agentic setting defined by540SWE-bench \citep{jimenez2024swebench} and SWE-agent \citep{yang2024sweagent}, both preprints, in which a model541is asked to resolve a GitHub issue end to end. Among the candidates, APISS \citep{chen2025apiss} retrieves542functionality-equivalent APIs through LLM embeddings to migrate proof-of-concept exploits, and a 2026 paper543proposes a multi-scale temporal model for just-in-time defect prediction; both are method contributions judged544from their abstracts.545546\paragraph{Productivity: two findings that need reconciling.}547The most cited post-period empirical candidate reports three randomised field experiments at Microsoft,548Accenture and an unnamed Fortune~100 company, run by the firms in the course of business, in which a random549subset of 4,867 developers received an AI coding assistant; the pooled estimate is a 26.08\% increase in550completed tasks with a standard error of 10.3\%, each experiment being ``noisy'' on its own, and less551experienced developers adopting more and gaining more \citep{cui2026genaiwork}. The earlier controlled552experiment on a single task reported a larger speed-up \citep{peng2023copilot}, and the field studies of553generative AI at work outside software \citep{brynjolfsson2023genaiwork,noy2023productivity,dellacqua2023jagged}554report the same pattern of larger gains for less experienced workers. Against these stands a 2025 randomised555trial preprint in which experienced open-source developers working on repositories they maintain took longer556to complete issues with AI tools than without \citep{becker2025metr}. The two findings are not contradictory557once population and outcome are distinguished: enterprise developers completing assigned tasks versus expert558maintainers resolving issues in mature codebases they know well, and tasks completed versus time per issue.559But the reconciliation is a reading of two abstracts, the second of a preprint, and the design that would560settle it, a preregistered multi-site trial stratified by experience and repository maturity with time-to-merge561and defect rate as joint outcomes, has not been run (open problem G-P3). The user studies of how programmers562interact with code-generating models \citep{barke2023groundedcopilot,vaithilingam2022expectation,liang2024usability}563supply the mechanism, acceleration mode against exploration mode, that any such trial would need to measure.564565\paragraph{Security of generated code.}566The security evaluations agree with one another. Copilot's suggestions were found vulnerable at a substantial567rate in 2022 \citep{pearce2022asleep}; the CCS~2023 user study found that participants with an AI assistant568wrote less secure code and believed it more secure \citep{perry2023insecure}; and the ICPEC~2025 study in the569candidate list, evaluating three open models on a filtered Big-Vul subset with eight CWE categories, reports570``a sharp contrast between high detection rates and markedly poor classification accuracy''571\citep{gasparlopes2025vuln}. High detection or completion paired with poor fine-grained security reasoning is572the consistent pattern across three designs, and it is the category's clearest negative result about the573models.574575\paragraph{The statistics.}576Software engineering has the highest co-classification with the LLM category of the six577(\ThyCoocSoftwareEngineeringLlmTwoZeroTwoFivePct\% of its works in 2025, from578\ThyCoocSoftwareEngineeringLlmTwoZeroTwoTwoPct\% in 2022), the largest post-period growth579(\ThyCagrMultilabelSoftwareEngineeringPostPct\% per year), the only positive level change at the reference580date and the only significant positive level change at the GPT-4 date (Section~\ref{sec:thy-statistics}).581Its references to LLM works are \ThyFlowSoftwareEngineeringToLlmPostPct\% in the post period, from582\ThyFlowSoftwareEngineeringToLlmBaselinePct\%, and inbound citations from the LLM category are583\ThyInflowSoftwareEngineeringFromLlmPostPct\% of its inbound references. Whether a vocabulary shift of this584size is a method shift, that is, whether the works co-classified with LLM cite LLM method papers at a higher585rate than the category's baseline, can be tested on the knowledge graph of Part~III once method nodes are586extracted for the high-priority set; it is open problem G-P2. The research-software case of the Astropy587project \citep[in the candidate list;][]{collberg2016repeatability} and the reproducibility literature of588Part~IX are the other side of the same category, and the only part of it where the window changed nothing589visible.590591\section{Synthesis}592\label{sec:thy-synthesis}593594Three conclusions follow, in decreasing order of evidential strength.595596The first is about the instrument. In the theory and software areas the automatically selected landmark597candidates do not identify landmarks: \ThyAuditVerdictInScopeResearch{} of \ThyAuditN{} are in-scope research598works, \ThyAuditIdCollision{} carry citation windows that belong to other works, and the rest are chapters with599generic titles, re-deposited classics, theses in small normalisation cells and lexical misclassifications. The600defects are identifiable and partly correctable at the selection stage, and the audit table601(Table~\ref{tab:theory_landmark_audit}) should accompany any use of the list; the major theoretical results of602the window, almost-linear flow, near-linear negative-weight shortest paths, the directed sorting barrier,603optimal open addressing, square-root-space simulation and the 3-progression bounds, are invisible to a60436-month field-normalised ranking and were brought into this review through verified records. The same605blindness will affect any bibliometric answer to RQ3 and RQ7 for these categories.606607The second is about the statistics. The six categories grew in absolute terms and declined in relative terms608after 2022; their slope changes at the reference date are positive but not distinguishable from pseudo-events609in the baseline; their vocabulary moved toward language models in proportion to their distance from610mathematics; and their citation behaviour moved little. For RQ2 the answer is that none of the six is among611the categories with structural change that survives the placebo test, and for RQ5 that the relationship with612the foundation-model categories changed in what these works say far more than in what they cite.613614The third is about the research. The substantive developments of the window are of two kinds that the corpus615treats very differently. Theoretical results were obtained by people, at the rate and in the venues of the616previous decade, and are cited accordingly. The entry of language models into verification, program analysis,617compiler testing and software engineering is visible in the co-classification statistics and in the abstracts618of the in-scope candidates, and it is where the open problems lie: guarantees for learned program analysis and619compiler testing (G-P4), comparability of learned provers (G-P5), the productivity effect on experienced620developers (G-P3), and the distinction between a vocabulary and a method (G-P2). What this half of Part~VII621can say with confidence is which of these questions the corpus can answer with its present instruments, and622which it cannot.623