arXiv weekly literature review

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T07:00:51Z
Saint Wesonga
arXiv categories: cs.CC, cs.LO

We formalize Hastad's PARITY lower bound in Lean using the switching lemma. For every fixed d >= 2, formulas and DAG circuits of computation depth at most d computing PARITY on n inputs require size exp(Omega_d(n^(1/(d-1)))) for all sufficiently large n. This matches the classical upper bound up to constants in the exponent and implies that PARITY is not in nonuniform AC0. We also construct a polynomial-size, logarithmic-depth bounded-fan-in formula family for PARITY, providing a witness to NC1 is not a subset of AC0 for the formalized models. The Lean source code is available at https://github.com/formalcs/circuit-complexity and is checked with Lean 4.33.1 and mathlib 4.33.1.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T08:17:46Z
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu, Oliver Soeser, Fernando Leal, Alvin Tang, Max Vistrup, Ralf Jung, Mario Carneiro, Joseph Tassarotti, Michael Sammler, Lars Birkedal
arXiv categories: cs.LO, cs.PL

The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-quality mechanization in Rocq. This mechanization uses a number of Rocq features in sophisticated ways, including a carefully constructed algebraic hierarchy for modeling separation logic resources, and a proof mode for embedded separation logic proofs, which combines custom Ltac with extensible typeclasses. The library has been developed for over a decade with dozens of contributors, with an emphasis on modularity and maintainability. We explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris. Using these features, we provide a novel implementation of the Iris proof mode with improved performance, simplify the handling of equivalences through quotient types, build a variant of Diaframe proof automation, and provide convenience features like automatic construction of Iris fixed points. Building on Lean lets us integrate with the extensive Mathlib library, allowing us to re-use results from this library for program verification tasks that have heavy mathematical dependencies, as we demonstrate with an application to probabilistic program verification.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T09:40:31Z
Sergei Stepanenko, Patrick Bahr, Rasmus Ejlers M{\o}gelberg
arXiv categories: cs.LO, cs.PL

Extending the recursion principles of a formal system is an enticing but dangerous endeavour with a well-documented history of leading to consistency bugs. Nakano's guarded recursion is an elegant, type-based approach to soundly extend type theory with a powerful recursion principle. This makes guarded recursion useful for many applications, from programming with infinite structures such as streams to reasoning about advanced programming language features using synthetic guarded domain theory. Sadly, guarded recursion is not directly supported by any major interactive theorem prover, which leaves users of guarded recursion with unmechanised pen-and-paper proofs or mechanisations that depend on unmaintained theorem provers. In this paper, we present an implementation of guarded recursion as an embedded language in Lean consisting of a simply-typed lambda calculus for definitions and a higher-order logic for reasoning. Using Lean's excellent support for metaprogramming, our language allows users to write guarded recursive definitions in an intuitive syntax and to prove properties about them using a dedicated proof mode. We give our language a presheaf model, which we use to prove the soundness of our language and to allow users to export guarded recursive definitions and their theorems into standard Lean developments. To demonstrate the usefulness of our language, we present several case studies for programming and reasoning with guarded recursion.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T11:30:33Z
Robin Cockett, Daniel Kiyoshi Hashimoto, Alexanna Little Berg, Priyaa Varshinee Srinivasan
arXiv categories: cs.PL, cs.DC, cs.LO

We introduce a novel functional-style concurrent programming language called Categorical Message Passing Language (CaMPL) which is designed using the mathematics of linear actegories. This mathematical underpinning gives CaMPL programs useful properties such as deadlock freedom, and additionally, livelock freedom for programs without general recursive processes. We explore CaMPL's type system through a series of code examples. The current proto-alpha version of the compiler and the abstract machine is implemented in Haskell. A reader is encouraged to experiment with writing CaMPL programs either using the online compiler https://campl-app.vercel.app/ or by installing CaMPL from https://campl-ucalgary.github.io -- our website has detailed instructions on how to run CaMPL code.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T13:51:52Z
Melanie Taprogge (CNRS, ENS Paris Saclay, DEDUCTEAM, LMF), Fr\'ed\'eric Blanqui (CNRS, ENS Paris Saclay, LMF, DEDUCTEAM), Alexander Steen
arXiv categories: cs.LO

We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to the EP calculus for higher-order logic and integrate it into the automated theorem prover Leo-III. The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse. The implementation uncovered several bugs in Leo-III.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T13:53:37Z
Fr\'ed\'eric Blanqui (CNRS, ENS Paris Saclay, LMF, DEDUCTEAM), Antoine Gontard (CNRS, ENS Paris Saclay, LMF, DEDUCTEAM)
arXiv categories: cs.LO

We report on our efforts to translate HOL-Light theorems on HOL-Light types/functions into Rocq theorems on Rocq types/functions. To this end, we developed in Rocq tactics to automate the proofs required for replacing a HOL-Light inductive type or recursive function definition by an equivalent but more idiomatic one in Rocq. We also explain how we replaced the definition of real numbers, as well as a number of mathematical notions like Rn spaces and the definition of limit, hence providing to Rocq users many definitions and theorems in logic and analysis that had not been formalized in Rocq before.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T13:55:11Z
Fr\'ed\'eric Blanqui (CNRS, ENS Paris Saclay, LMF, DEDUCTEAM), Rishikesh Vaishnav (CNRS, ENS Paris Saclay, LMF, DEDUCTEAM)
arXiv categories: cs.LO

The Lean proof assistant has a rich library of mathematical formalizations that are interesting to users of other proof assistants. To help with the translation of this library to other systems, we present a theory in the Dedukti logical framework in which one can encode Lean terms and types, and define a typability-preserving translation from some large subset of Lean to that Dedukti theory.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-21T21:26:43Z
Ramy Shahin
arXiv categories: cs.PL, cs.LO, cs.SE

Inductive types are ubiquitous building blocks in many programming and theorem proving languages. An inductive type is a closed set of constructors from which values of the type can be created. That set cannot be extended though once a type is defined. This limits extensibility, reuse, and modular separation of concerns when defining types and functions operating over their values. This limitation is manifested in the expression problem, where extending an expression language with new syntactic constructors without having to modify or re-compile existing ones is a challenge in almost all programming languages. This paper presents inductive type and function implementation composition algorithms based on meta-programming. In addition, a set of syntactic extensions to the Lean proof assistant implementing those algorithms are presented. This framework allows for modular reuse, composition, and extension of a subset of Lean type and function definitions. In addition, semantic subtyping relations between component and composite types are discussed both at the type theoretic and implementation levels. The framework is demonstrated on a case study, involving the composition of syntactic and semantic artifacts of three sublanguages into one language. The case study highlights both the features and limitations of the composition framework.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-22T01:50:31Z
Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro, Holger Thies
arXiv categories: cs.LO

The safe operation of a humanoid robot critically relies on accurate estimation of its vertical orientation, or ``tilt''. This requires a variety of mathematical tools, including three-dimensional geometry and differential equations. To formally verify tilt estimation, we develop a library for stability analysis in the Rocq prover. We start by formalizing a theory of ordinary differential equations. We provide a formalization of the (local) Cauchy-Lipschitz (a.k.a. Picard-Lindelof) theorem for existence and uniqueness, taking advantage of the library support for quotients provided by the Mathematical Components library. We extend this formalization with a variant for global existence and continuous dependence on initial conditions. Building on these foundations, we develop a theory of Lyapunov stability that is compatible with an existing formalization of LaSalle's invariance principle. We also extend an existing library for the statics of robot manipulators to support dynamical systems. Finally, we apply these libraries to the verification of a state-of-the-art tilt estimation developed for a humanoid robot.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-22T03:48:28Z
Liangtao Dai, Yimin Gao, Melika Morsali, Mircea Stan
arXiv categories: cs.CR, cs.AR, cs.LO

Formal hardware information-flow verification (IFV) provides strong guarantees against secret-dependent timing and control behavior, but often scales poorly on realistic RTL. We identify two recurring proof barriers in self-composed IFV: implementation complexity, where proof-hard datapath logic dominates even though the property needs only a compact boundary relation, and relational inductive complexity, where the proof depends on cross-copy public-control facts that the backend prover does not infer efficiently. To address them, we introduce two semantic proof decomposition forms: functional simplification, which replaces a proof-hard RTL region with a validated over-approximate summary, and relational strengthening, which exposes and proves the cross-copy relations needed for induction. We further present SLED-IFV, a solver-validated LLM-guided flow that automates the selection of these forms and their concrete targets. Given a self-composed miter and an oracle-free decision sheet, the LLM proposes a decomposition, then materializes it into proof artifacts under controller checks. The controller compiles the checked artifacts into proof obligations, and the formal verification backend remains the sole authority for acceptance. Across nine nontrivial benchmarks constructed from real RTL, SLED-IFV achieves up to 603x solver-only speedup and converts two 12-hour timeouts into completed proofs. The closed-loop flow produces verifier-accepted decompositions for all cases.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-22T11:20:31Z
Gaston Besanson
arXiv categories: cs.SE, cs.AI, cs.LO

We call the object this paper derives and certifies a minimal sufficient governance context: given a finite reachable-state model, a deterministic declared verdict, and candidate observable attributes, we compute sufficient observation sets, distinguish attributes that are individually indispensable from contracts that are jointly sufficient, and select among sufficient contracts under a cardinality or declared-cost objective. An observation contract is a set of candidate attributes whose values determine the declared verdict on every reachable state; an authority contract is one selected under an objective and bound to a gate schema. We synthesize every inclusion-minimal sufficient contract where exhaustive enumeration is affordable, and a minimum-cardinality or minimum-cost contract by SAT/MaxSAT encoding otherwise, checking sufficiency directly. On a constructed code/cloud domain, the individually-indispensable core is not sufficient as an observation contract and two distinct reducts exist; a preregistered cost model separates them exactly. On a second, larger, constructed domain, the same pattern recurs, but that domain's cost model does not separate the alternatives: a fully explained cost tie, reported as found. We measure discernibility-family scaling where exhaustive enumeration is confirmed infeasible within a registered timeout, while SAT/MaxSAT synthesis solves in well under a second; MaxSAT showed no measured cardinality advantage over plain SAT. AuthorityBench compares four baselines across three domains; the declared-only baseline is not exactly sufficient on any. Every selected contract is checked for sufficiency, with a counterexample on failure and a check summary, not a portable certificate, on success -- the compiler-focused scope of a two-scope table; an independently specified end-to-end case study is registered follow-up work, not claimed here.

arXiv abstract · PDF

Formal Methods and Proof Assistants · primary corpus · published 2026-09-22T12:51:51Z
Can Cebeci, Nikolaj Bj{\o}rner, George Candea, Cl\'ement Pit-Claudel
arXiv categories: cs.LO

SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) in the context of program verification. We demonstrate that the generation (i.e., depth) accounting used to make quantifier instantiation practical and implemented in multiple state-of-the-art SMT solvers is non-confluent (i.e., prone to divergence), and that this leads to instability. We then address this deficiency and develop a new accounting method that is stable. The new method is justified using a sequence of refinements from an abstract, confluent solver model all the way to our implementation in Z3. Our empirical evaluation demonstrates that our implementation reduces outcome instability by 94% in the unstable core of the Mariposa benchmark without leading to performance regressions.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T02:11:41Z
Eiji Yamada
arXiv categories: cs.LO, cs.MA, math.LO

In dynamic epistemic logic, the four notions of success, self-refutation, true lies, and impossible lies have been discussed in the context of public announcements. In this paper, we introduce eventual and strong eventual versions of these notions, as well as their transfinite versions, which allow transfinite iteration of announcements. We also introduce the notions of always informativeness when true or false. For example, a formula is eventually self-refuting if, whenever initially true, it eventually becomes false at some finite stage under iterated announcements, and strong eventual self-refutation further requires the formula to remain false at all sufficiently late stages. There are two main results. The first result gives the relationship among strong eventual notions, eventual notions, and several other conditions including conditions on the limit of the truth values of the announced formula, the uniform bound condition, and the fixed-point views of the Moore sentence and the self-fulfilling sentence. The second result gives the relationship among finite and transfinite versions of the eventual and strong eventual notions and the fixed-point views.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T07:32:24Z
Gunnar Wilken
arXiv categories: math.LO

We uniformly generalize Goodstein's theorem (Goodstein 1944) and Cichon's independence proof (Cichon 1983) via the concept of maximality quotients.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T14:34:31Z
Justus Becker
arXiv categories: math.LO, cs.LO

A key motivation for Heyting's intuitionistic logic was to gain a formal notion of Brouwer's idea of mathematics as a "construction of the mind". One might thus argue that Heyting's Calculus should also correspond to a notion of provability. Inspired by this idea, G\"odel formalised this connection via an embedding into a modal calculus, which is now known as the modal logic S4. While in his original publication, he only proved soundness for the embedding from intuitionistic propositional logic into S4, the converse was proved fifteen years later by McKinsey and Tarski. Although, it was later discovered that G\"odel also had obtained a proof of the faithfulness of his embedding in unpublished notes in 1941. Rasioa and Sikorski later extended G\"odel's embedding to first-order intuitionistic logic. In 1954, Maehara independently obtained the same results using proof-theoretic methods, even extending the embedding to one from intuitionistic first-order logic into intuitionistic first-order modal logic. This document presents a faithful English translation of Maehara's 1954 paper.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T15:55:47Z
Mojtaba Mojtahedi, Fedor Pakhomov, Giovanni Sold\`a
arXiv categories: math.LO

G\"odel-L\"ob provability logic $\GL$ is a propositional modal system that on one hand enjoys completeness with respect to conversely well-founded Kripke frames and on the other hand captures all modal principles about $\PA$-provability that are provable in $\PA$ itself. In the present paper we carry out an initial investigation into the question of what the infinitary counterpart of $\GL$ is. We develop a non-well-founded deep inference proof system $\dgla$ for the modal language with at most countably infinite conjunctions and disjunctions. We show that the calculus is sound and complete for well-founded transitive Kripke frames. Using Kripke-Platek set theory we develop an interpretation of the infinitary modal language in terms of infinitary provability over admissible sets. Then we show that a natural Hilber-style variant of infinitary $\GL$ is sound for this interpretation. We leave open, however, the question if $\dgla$ proves any additional theorems in comparison with the Hilbert-style calculus. Nevertheless, under certain conditions we do show that the infinitary provability logic arising from certain admissible sets lies between the set of theorems of the Hilbert-style calculus and the non-well-founded deep inference system.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T17:07:47Z
Ruiting Jiang
arXiv categories: math.LO

We study the finite spectra of the syllogistic logic with cardinality comparisons $S^\dagger(card)$. Since the language does not contain conjunction at the sentence level, we consider the spectrum of a theory $\Gamma$, namely the set of positive integers $n$ for which $\Gamma$ is satisfiable in an $n$-element model. We give a complete classification of these spectra: besides the empty set, every $S^\dagger(card)$-spectrum is either an eventual tail of the positive integers or an eventual tail of the positive even integers. We then consider the extension of $S^\dagger(card)$ by Boolean connectives at the sentence level and show that the collection of its spectra forms the topology generated by the spectra of the original language.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T17:18:22Z
Marianna Girlando, Roman Kuznets, Sonia Marin, Lutz Stra{\ss}burger
arXiv categories: cs.LO

In this paper, we show that the two intuitionistic modal logics IS4 and IK4 are decidable. We provide a constructive decision procedure, that, given a formula, produces either a proof showing the formula to be valid or a finite countermodel falsifying the formula, thus also proving the finite model property for both logics. The main ingredient of our strategy is the introduction of (possibly unsound) loop rules, which encode repeating behaviour in proof search. This paper fixes a previous mistake in our LICS'23 contribution.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-21T17:39:51Z
Filipe Marinho Rocha, In\^es Dutra, V\'itor Santos Costa, Lu\'is Paulo Reis
arXiv categories: cs.LG, cs.AI, cs.LO

A model generalizes outside its training distribution only when it computes a representation structurally equivalent to the generating mechanism, not an approximation fitted to it. Such equivalence is necessary for exactness in and out of distribution, and extrapolation is governed by this exactness at inference, whatever its realization. Tensor Logic shows this: a zero-temperature contraction is equivalent to discrete logic, deducing in place with no artefact extracted, its tensors Boolean, its embeddings orthonormal, only its arithmetic continuous. Lacking infinite recursion it reaches Datalog, not Prolog, and though exact over closed domains it needs external memory to bind a novel entity. The criterion needs neither a discrete representation nor an extracted expression, and constrains inference, not training: an exact marginal in $[0,1]$ passes, a Neural Network thresholded to a hard label does not. Logic Tensor Networks fail it, while differentiable ILP and Tensor Logic at $T=0$ pass. Piecewise-affine extrapolation divergence and an inability to bind novel entities are two faces of a shortfall in exact representability. For hybrid architectures, a propagation rule follows: the output inherits the bounds of every fitted estimator on its path, explaining which axes fail in equivariant models and the ARC-AGI induction/transduction split. Only an exact hypothesis class certifies what the training data leave underdetermined: on a law-derived partition it finds the $56.3\%$ of distant queries that are answerable, which ensembles meet with false confidence and distance metrics rank backwards. Common inductive biases, from symmetries to memory, reach exactness only because humans inject them, an argument for inducing exact representations rather than fitting surrogates whose residuals, even at the arithmetic floor in training, diverge outside the data and compound under composition.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-22T01:43:45Z
Florian Lengyel
arXiv categories: math.LO, cs.LO

Montagna (1989) and Di Paola--Montagna (1991) claim that the algebraic systems $S'$ and $S'_T$, respectively, are categories. We show that the proposed composition is not independent of the choice of representatives. For every consistent recursively enumerable extension $T$ of Peano arithmetic ($\mathrm{PA}$), we exhibit two program indices that are pointwise provably equal in $T$ but yield inequivalent composites when each is run after the same program. Montagna's $S'$ is the case $T=\mathrm{PA}$. The failure already occurs for partial maps from $\omega$ to itself. Weak totality and the proposed range assignment also depend on the choice of representatives. More generally, for consistent $T\supseteq\mathrm{PA}$, pointwise provable equality is a composition congruence exactly when $T$ proves every true $\Pi^0_1$ sentence, in which case it is extensional equality. This completeness condition fails for every consistent recursively enumerable $T\supseteq\mathrm{PA}$ by G\"odel's second incompleteness theorem. For every extension $T\supseteq\mathrm{PA}$, the least composition congruence containing pointwise provable equality is extensional equality if $T$ is $\Sigma^0_1$-sound and the universal relation otherwise.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-22T12:45:55Z
Robbe Van den Eede
arXiv categories: cs.LO, math.LO

Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID, for mathematical induction, and LKID{\omega} and CLKID{\omega} , for infinite descent. LKID{\omega} is an infinitary system, in which proofs are infinite trees, and CLKID{\omega} a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone definitions, while inductive definitions are generally non-monotone. The logic FO(ID) extends classical first-order logic with non-monotone inductive definitions. In earlier work, we provided a formalization of the principle of mathematical induction for non-monotone definitions by extending LKID to a sequent calculus SCFO(ID) for FO(ID). In this paper, we provide a formalization of the principle of infinite descent for non-monotone definitions by extending LKID{\omega} and CLKID{\omega} to sequent calculi SCFO(ID)-inf resp. SCFO(ID)-cyc for FO(ID). Furthermore, we extend several proof-theoretic results for LKID{\omega} and CLKID{\omega} to SCFO(ID)-inf and SCFO(ID)-cyc regarding soundness, completeness, cut-elimination and the relation with SCFO(ID).

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-22T15:11:40Z
Khashayar Irani
arXiv categories: cs.LO

In this paper, we argue that acceptance and rejection are classical speech acts that express two opposite polar positions toward propositional content and can be systematically represented within a classically outlined bilateral formal model. Acceptance occupies the positive pole, represented by positive A, whereas rejection occupies the negative pole, represented by minus A. Their classical relationship is mediated by negation because acceptance of A corresponds to rejection of negation A, while rejection of A corresponds to acceptance of negation A, represented by positive A iff minus negation A and minus A iff positive negation A. Coherency and incoherency are introduced as supplementary notions to clarify this relationship and its connection with reflexivity. A further result of the manuscript is the methodical distinction between rejection and negation namely, rejection expresses negative polarity toward A, whereas negation operates upon propositional content.

arXiv abstract · PDF

Logic and Proof Theory · primary corpus · published 2026-09-22T17:55:06Z
Yuya Uezato
arXiv categories: cs.LO, cs.CC

Three-variable first-order logic (FO3) and the calculus of relations (CoR) define the same binary queries, an equivalence going back to Tarski in the 1940s. While the classical translation $\text{FO3} \Rightarrow \text{CoR}$ is exponential, we prove that this blow-up is unavoidable, resolving a long-standing open question. We construct positive formulas $\varphi$ with a single quantifier whose equivalent terms require size $2^{\Omega(|\varphi|)}$, even over finite structures and circuit representations with subterm sharing. Our proof uses a preservation argument over a single finite structure. This approach applies beyond our primary question, establishing the lower bound even for size-specific circuits and bounded-error randomized circuits, and yielding an analogous exponential gap for the matrix query language MATLANG.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-21T05:41:33Z
Gal Binyamini, Yuval Salant
arXiv categories: math.CA, math.LO, math.MG

We establish the full version of a conjecture of Guth and Zahl, giving a lower bound for the volume of a semialgebraic set that has a large intersection with a collection of $\delta$-separated $\delta$-tubes. Our proof uses o-minimal methods to simplify the proof of Katz and Rogers, who proved the conjecture up to a small factor. We also establish that the constants depend polynomially on the complexity of the semialgebraic set, and more generally in the #o-minimal setting.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-21T09:32:26Z
Olga Kharlampovich, Rizos Sklinos
arXiv categories: math.LO, math.GR

We prove that the first-order theory of nonabelian free groups does not admit a model companion.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-21T16:10:08Z
Benedict Eastaugh
arXiv categories: math.HO, math.LO

Reverse mathematics is a branch of mathematical logic dedicated to determining the minimal set existence principles necessary and sufficient to derive ordinary mathematical theorems about concrete structures like the real line. Since the mid-1970s, reverse mathematics has developed a systematic classification of the strength of theorems in areas of mathematics ranging from real and complex analysis to infinitary combinatorics. This essay will place reverse mathematics in its historical and philosophical context, and reveal its relevance to central issues in the philosophy of mathematics, from the foundational programmes of Hilbert and Brouwer to contemporary debates about realism, determinacy, and applicability of mathematics. In doing so, it will discuss the role of computability theory in measuring the strength of set existence principles, as well as related questions about idealisation when these principles are applied in the physical sciences and in philosophy.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-21T18:33:45Z
Jonathan Osinski
arXiv categories: math.LO

We characterise exacting, rank-Berkeley, Berkeley, and club Berkeley cardinals by compactness properties of logics and, equivalently, by compactness properties of certain topological spaces. This raises the strength known to be obtainable by statements about compactness into the realm of choiceless large cardinal axioms, the strongest known statements in terms of consistency strength. Moreover, it shows that compactness assumptions can directly violate the axiom of choice and the axiom $V=\text{HOD}$.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-21T22:00:31Z
Martina Conte, Matteo Vannacci
arXiv categories: math.GR, math.LO

We study the (Haar) measure of verbal sets in profinite groups, and especially in free profinite groups. Relating the measure of a verbal set with the width of the corresponding word, we find verbal sets of positive measure different from one. We prove a sufficient condition for the measure of a verbal set to be zero in a free profinite group of finite rank, from which we deduce that certain existentially definable sets in free profinite groups of finite rank can only have measure zero or one. Finally, we compute the measure of definable sets in torsion-free finitely generated abelian groups.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-21T23:53:29Z
Chencheng Zhang
arXiv categories: math.RA, math.LO

Assuming the nonexistence of uncountable measurable cardinals, we construct an $\mathbb F_2$-algebra and a covering class of right modules which is not closed under colimits of countable chains. This gives a counterexample to Enochs' conjecture under $V=L$.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-22T12:21:08Z
Rapha\"el Faure, Alain Finkel, Gaspard Fougea, Lina Ye
arXiv categories: cs.LO, cs.FL

Well-structured transition systems (WSTS) provide a classical framework for the verification of infinite-state systems, but their probabilistic extensions lack a unified treatment of quantitative coverability: path-enumeration algorithms assume a finite branching degree, while alternative approximation schemes defer some computations, such as probabilities over a bounded horizon, to the model at hand. We introduce probabilistic well-structured transition systems (pWSTS), Markov chains over countable state sets whose underlying transition systems are WSTS, with no a priori assumption on the branching degree. This class encompasses any WSTS equipped with a Markov kernel, such as probabilistic vector addition systems (pVAS) and probabilistic lossy channel systems (pLCS). For an effective subclass, we solve the approximate quantitative coverability problem over bounded horizons, and over infinite horizons under decisiveness, requiring no probabilistic information beyond individual transition probabilities. We then identify a general source of decisiveness: every stochastically monotone pWSTS is decisive with respect to every upward-closed set. We finally instantiate the framework on multi-type Galton--Watson processes, a classical model of population dynamics whose offspring distributions may have infinite support. Under mild assumptions on the reproduction laws, these processes are effective pWSTS, and they are stochastically monotone, hence decisive. Approximate quantitative coverability is therefore computable for them over both horizons, with a proof that uses none of the traditional tools: neither generating functions nor any case distinction between regimes.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-22T12:28:41Z
Martino Lupini
arXiv categories: math.OA, math.FA, math.LO

We solve Dixmier's 1967 problem about spectra of simple $C^*$-algebras. A function between spectra is called Borel-definable when it is induced by a Borel map between standard Borel spaces of unitary representations. Let $\Gamma=\mathrm{SL}_3(\mathbb{Z})$, let $K$ be its completion with respect to the congruence kernels modulo $2^n$, let $A$ be the canonical anticommutation relations (CAR) algebra, and let $B=C(K)\rtimes_r\Gamma$ be the reduced crossed product. The algebras $A$ and $B$ are simple, separable, unital, exact, and antiliminary; $A$ is nuclear, whereas $B$ is nonnuclear. There is no Borel-definable injection from the spectrum of $B$ to the spectrum of $A$. In fact, there is a probability measure on the pure-state space of $B$ such that every Borel lift of a Borel-definable function from the spectrum of $B$ to the spectrum of $A$ takes values in a single unitary-equivalence class almost everywhere. Answering a question of Simon Thomas, we also prove that, for every countable amenable group $H$, there is no Borel-definable injection from the unitary dual of the free group $F_\infty $ on infinitely many generators to the unitary dual of $H$. There is a fixed probability measure on a family of infinite-dimensional irreducible representations of $F_\infty$ such that every Borel lift of a Borel-definable function takes values in a single unitary-equivalence class almost everywhere. We also show that, in contrast, the spectra of any two separable nuclear non-type-I $C^*$-algebras admit a Borel-definable bijection.

arXiv abstract · PDF

Mathematical Foundations · primary corpus · published 2026-09-22T14:40:20Z
Edgar Valenzuela
arXiv categories: math.LO

We will use consistency properties to characterize strongly compact cardinals, first showing an adequate Model Existence Theorem for larger fragments.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-09-21T02:59:53Z
Masaki Fukuda, Tommy Shu
arXiv categories: math.CT

In this paper, we investigate the relation between the category of 3-crossed modules and the category of Gray-type 4-groups. The notion of a 3-crossed module was first introduced by Arvasi \textit{et al.}, motivated by the question of what kind of algebraic structure completely encodes a homotopy 4-type. On the other hand, from the point of view that higher groups are equivalent to algebraic realizations of higher categories -- as exemplified by the relationship between 2-crossed modules and Gray 3-groups established by Sarikaya--Ulualan -- it had not been clear how the 3-crossed modules of Arvasi \textit{et al.} relate to any higher category. In our previous paper, we proposed a new definition of a 3-crossed module and observed that it admits a natural interpretation in terms of higher categories. In this paper, we make this interpretation precise: we introduce a 4-category, which reduces to a semistrict braided monoidal 2-category when restricted to a single object and a single 1-morphism, and prove that the category of our 3-crossed modules is equivalent to the category of Gray 4-groups, defined as single-object versions of this 4-category in which all morphisms are invertible. We therefore expect that these structures can correctly capture the topological nature of surface knots and higher-dimensional manifolds.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-09-21T09:27:45Z
Xabier Garc\'ia-Mart\'inez, James R. A. Gray, Michael A. Hoefnagel, Tim Van der Linden, Corentin Vienne
arXiv categories: math.CT

In previous work, we analysed a number of categorical properties, of interest in the context of Janelidze-M\'arki-Tholen semi-abelian categories, for the variety $\mathsf{HSLat}$ of Heyting semilattices. In this paper, we focus on the subvariety $\mathsf{ELHSLat}$ of equationally linear Heyting semilattices. Our main objective is to show that, unlike $\mathsf{HSLat}$, this category is algebraically coherent. We furthermore prove that it is neither locally algebraically cartesian closed nor cosmash associative.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-09-21T11:13:07Z
Sigiswald Barbier, L\'eo Schelstraete
arXiv categories: math.RT, math.CT, math.QA

We introduce an analogue of Gr\"obner bases, or equivalently, Bergman's diamond lemma, for linear (super)monoidal categories. It gives a systematic way to study monoidal ideals and to prove basis theorems. The central notion is that of a monoidal Gr\"obner system and is based on higher linear rewriting theory. We then apply the theory to categories of affine Brauer type: linear (super)monoidal categories that have the same hom-basis as the affine Brauer category, but possibly distinct composition and tensor product. Our main result is a criterion for a category to be of affine Brauer type, reducing the question to an explicit list of local computations, which we partially implement in the computer algebra system FORM. This gives new combinatorial proofs of the basis theorems for the affine Brauer category, the nil-Brauer category and the affine VW supercategory, and yields new examples. In particular, we construct the odd nil-Brauer category, a conjectural supercategorification of the split $\imath$quantum group of rank one, and the quantized affine VW supercategory, whose non-affine part is the quantized periplectic Brauer category and which we expect to satisfy a higher quantum Schur--Weyl duality. Finally, we classify the categories of affine Brauer type admitting a sufficiently simple presentation.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-09-21T16:29:35Z
Terry Gannon, Andrew Schopieray, Harshit Yadav
arXiv categories: math.QA, hep-th, math.CT, math.OA

For every odd $N$, we construct a Haagerup-Izumi (HI) category for $\mathbb Z/N$, using Barnes double-sine functions. Equivariantization gives near-group categories of type $((\mathbb Z/N)^2,N^2)$ for every odd $N$. We classify connected separable algebras up to Morita equivalence in such HI categories and describe their dual categories. These duals are often HI for noncyclic groups with nontrivial pointed associators. We prove the Evans-Gannon conjecture that the modular data of the center is always a smashed sum involving a finite metric group of order $N^2+4$ and recover this group and its quadratic form directly from the data of the HI category. We also give the HI equations and reconstruction in arbitrary characteristic and prove a Frobenius symmetry in characteristic two. Using this, we obtain the complete list of (untwisted, subfactor type) HI categories over $\mathbb{C}$ for odd $N\le 43$. Other applications include finding three pairwise non-Morita-equivalent $\mathbb Z/15$ categories whose centers have the same modular data. We show that the center of a $\mathbb Z/5$ HI category cannot be defined (i.e., admits no split ribbon form) over a cyclotomic field, disproving a conjecture of Davidovich-Hagge-Wang.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-09-22T14:31:19Z
Yifan Jin
arXiv categories: math.AT, math.CT, math.KT

We develop the chromatic theory of dualizable stable categories, with chromatic purity for continuous $K$-theory at its center. We generalize the chromatic purity theorem for algebraic $K$-theory to continuous $K$-theory of dualizable stable categories and reformulate it as the purity of $H$-unital rings. Using categorical completion theory, we construct chromatic fracture squares and obtain a refinement of chromatic purity: for every dualizable stable category $\mathcal{C}$, the $T(n)\oplus T(n-1)$-completion map induces an equivalence $$ K_{T(n)}^{\mathrm{cont}}(\mathcal{C})\xrightarrow{\simeq}K_{T(n)}^{\mathrm{cont}}(\mathrm{Nuc}_{T(n)\oplus T(n-1)}(\mathcal{C})). $$ We also establish chromatic descent for continuous $K$-theory of dualizable homotopy fixed points and prove a categorical nuclear refinement of descent. This framework allows us to lift redshift bounds, Tate vanishing, and blueshift from spectra to dualizable stable categories. We show that the $T(n)$-completion of a rigid symmetric monoidal stable category is equivalent to the dualizable limit of module categories over a tower of type $n$ generalized Moore spectra. As applications, we prove that both nuclear solid and nuclear gaseous module categories satisfy chromatic redshift.

arXiv abstract · PDF

Software Engineering and AI Agents · primary corpus · published 2026-09-21T00:00:09Z
Simon Henniger, Stephen Chong, Nada Amin
arXiv categories: cs.PL, cs.AI, cs.SE

Programmers write formal specifications, and LLMs implement them, proving that each implementation matches its spec. Taken to its extreme, this makes specification languages the new programming languages. We argue that an unambiguity constraint is key: in addition to proving that its implementation satisfies the specification, the LLM must also prove that any other implementation satisfying it must produce the same outputs on the same inputs, i.e. that the relation formed by the constraints is deterministic. This leaves the LLM no leeway on program semantics: as with a conventional compiler, the generated code never needs to be read and can be regenerated from the spec at any time. Under this constraint and with a powerful LLM, the difference between a specification language and a programming language becomes essentially meaningless, and the LLM essentially becomes a part of the compiler toolchain. The arrangement doubles as a strong form of AI control: an untrusted model writes the code, yet its work is tightly checked by a verifier. To demonstrate that our LLM-in-the-compiler paradigm is feasible when supported by our unambiguity constraint, we present Djinnlang, a high-level specification language built for this future. A Djinnlang program consists only of specifications --- the programmer never writes executable code. In place of a traditional compiler, a symbolic translator lowers each spec to Dafny stubs and proof obligations, and a driver harness orchestrates an LLM that fills in implementations and proofs, all checked by the Dafny verifier. We evaluate our language and implementation on multiple examples and we show that it is self-hosting: an LLM can implement the Djinnlang translator from its specification and the reimplementation can verify itself.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-21T07:52:28Z
Furqan Nasir, Arif Shah, Iftikhar Alam
arXiv categories: cs.SE, quant-ph

Test oracles for quantum transpilers typically judge correctness by comparing compiled output against a reference: a statevector, a sampled distribution, or a unitary compared modulo global phase. A companion empirical study measures how often that choice fails. Roughly 28% of merged Qiskit transpiler bug-fixes (95% Wilson CI 19-40%) repair a fault that corrupts layout metadata, global phase, or run-to-run reproducibility while output stays correct: invisible to a black-box output-equivalence oracle by construction. This paper closes that gap with a fault-class-matched, layout-aware, width-tiered oracle family: a layout/permutation contract checker and a contract-level metamorphic relation (MR-1) for the metadata channel, a global-phase tracker for the phase channel, and a determinism runner for reproducibility. Verified from source on nine real, merged Qiskit transpiler regressions (three per channel), the output-equivalence oracle is blind throughout and the matched mechanism fires on every case. A 675-configuration sweep of the contract/metadata invariant finds no false positive. Synthetic mutant families confirm reliability at scale: 1.00 sensitivity and specificity across 36 mutants apiece for the contract/metadata and global-phase channels, and 1.00 sensitivity (95% CI 0.44-1.00) for reproducibility on the three circuits where the mutation is constructible. The contract checker costs two to six orders of magnitude less than a plain output check, the global-phase tracker is comparably cheap within its exact tier, and only the metamorphic relation carries a bounded cost. Ported natively to pytket/tket, the global-phase mechanism transfers cleanly, an identical 1.00/1.00 result with phases recovered to double-precision accuracy, evidence against a Qiskit-specific artifact.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-21T09:37:19Z
Bilal Al-Ahmad, M. Harshvardhan, Khaled El-Fakih, Anas AlSobeh
arXiv categories: cs.SE

Context: Large language models (LLMs) can generate unit tests quickly, but high structural coverage does not establish that those tests execute reliably or detect faults. Existing evidence often treats coverage as the principal outcome and rarely compares prompt strategies and models through mutation testing at class level. Objective: This study examines how prompt strategy and model choice shape the executability, structural coverage, fault-detection effectiveness, and structural quality of LLM-generated Python test suites relative to human-written suites. Method: We evaluate multiple prompt strategies across a diverse set of current LLM configurations on the ClassEval benchmark. The evaluation combines execution outcomes, line and branch coverage, Cosmic Ray mutation scores, and structural quality indicators. Primary analyses treat successful execution as a prerequisite; paired comparisons use only classes shared by the relevant executable subsets. Results: Structural coverage is consistently near its ceiling and offers little discrimination among configurations. Executability varies substantially. The proposed prompt performs strongly for mutation score, but no prompt dominates across models. Model choice explains more variation than prompt choice, and their interaction shows that prompt effectiveness depends on the selected model. Human and LLM suites are evaluated on unequal executable subsets, so their relative mutation scores do not establish superiority. Conclusion: Reliable assessment of LLM-generated tests should treat executability as a gate and combine coverage with mutation testing and structural quality indicators. In practice, model selection should precede prompt tuning.

arXiv abstract · PDF

Software Engineering and AI Agents · primary corpus · published 2026-09-21T14:11:12Z
Ianna Osborne, Maxym Naumchyk, Tai Sakuma, Andres Rios-Tascon, Peter Elmer
arXiv categories: cs.DC, cs.PL

The High-Luminosity LHC (HL-LHC) will demand order-of-magnitude gains in analysis throughput, and increasingly those gains must come from GPUs that are not made by a single vendor. Leadership-class systems such as El Capitan, Frontier and LUMI are built on AMD accelerators, yet the Scikit-HEP analysis stack---and Awkward Array in particular---has grown up CUDA-first. We report on $rawkward$, a Rust-backed kernel engine that adds a ROCm/HIP backend for Awkward Array's nested, jagged, variable-length data structures. Our central finding is that a naive source-level port of CUDA kernels to HIP loses $5$--$10\times$ in performance on irregular kernels, because AMD's $64$-lane wavefronts, higher register pressure and more expensive divergence behave fundamentally differently from NVIDIA's $32$-thread warps. We show that a small, reusable set of optimization patterns---loop flattening, $128$-bit vectorized loads, splitting fused kernels, and profile-guided launch configuration---recovers CUDA-class performance without changing the public API. A Rust macro-and-match dispatch layer keeps a single, backend-agnostic call site while emitting vendor-specific kernel strategies, and the type system enforces buffer-size and lifetime correctness at compile time. On a two-socket AMD Instinct MI210 node we measure GPU speedups from $1.03\times$ (bandwidth-bound $sum$) up to $12.5\times$ ($count$) over $128$ EPYC~7763 CPU cores, and the Rust CPU kernels match or beat on aggregate the incumbent C++ kernels (geometric-mean runtime ratio $0.37\times$ across twelve kernels). We argue that these patterns constitute a practical recipe for performance-portable, vendor-agnostic HEP analysis kernels.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-21T17:23:28Z
Mahmoud Ayyad, Zehao Wang, Jiho Shin, Ying Zou, Bram Adams
arXiv categories: cs.SE

Autonomous software engineering agents (SWE-agents) automate coding tasks. Each agent update may require re-running the full benchmark to detect regressions and improvements, at a cost of hundreds of millions of LLM tokens per run, which makes evaluation a bottleneck. One solution is to evaluate only a subset of benchmark instances. Yet, simple approaches, such as random sampling or stratified random sampling based on past pass/fail outcomes, risk producing high variance and unrepresentative subsets. We turn to agent trajectories, the step-by-step record of the actions an agent took. We propose a trajectory-aware subset selection approach that replaces random sampling with deterministic selection based on trajectory embeddings. We first group test set instances by their test outcome in a recent full test run to preserve the historical pass/fail rate, then select the subset using the trajectory's embedding space. We evaluate 76 subset selection configurations, including random sampling, embedding-based selection, clustering-based selection, and hybrid shortlist-then-subsample strategies, across three regression scenarios: same-configuration reruns, model and configuration changes, and agent framework changes. Our best trajectory-aware method is the one selecting benchmark instances closest to the centroid of each outcome group in the embedding space. It achieves the lowest estimation error among all methods we evaluate. For instance, when evaluating a given agent version on a selected subset of 5% or 10% of the test instances, our approach reduces the average estimation error by 3--11% and the worst-case error by 4--11% relative to the typical draw and 38--46% relative to the 95th-percentile draw of the strongest baseline. Our results show that a 10% trajectory-aware subset keeps the median estimation error below 5% while cutting token cost by roughly 90%.

arXiv abstract · PDF

Software Engineering and AI Agents · primary corpus · published 2026-09-21T19:27:47Z
Hepziba Susan, Shivaranjani G. R., Malik Imran, Muhammad Rashid, Sumathi Gokulanathan, Zain Ul Abideen
arXiv categories: cs.AR, cs.PL

Large language models (LLMs) can generate register-transfer-level (RTL) code from natural-language specifications, but compilation alone does not establish structural completeness, functional correctness, or implementation efficiency. This paper presents a framework for evaluating LLM-generated RTL beyond compilation, which we named GRADE-RTL. Using fixed prompts and validation settings, GRADE-RTL applies five checks, such as Port Signature, Compilation, Elaboration, Module Completeness, and Functional Equivalence against trusted reference RTL. With the help of compact metrics, we identify where candidates fail and distinguish end-to-end success from eligibility for downstream synthesis. We evaluate nine general-purpose and RTL-specialized LLMs on ten edge-relevant intellectual property designs under a budget of three generation attempts with failure-directed feedback. End-to-end success ranges from 0% to 70% across the evaluated models, with failures extending beyond compilation to hierarchy resolution, incomplete logic, and behavioral mismatch. FPGA implementation and 65 nm ASIC synthesis results further show that functionally equivalent RTL can differ substantially in resource use, timing, area, and power. A PID-controller place-and-route case study illustrates the physical-design consequences of different RTL implementations. GRADE-RTL provides a practical basis for comparing LLM-generated hardware descriptions by separating structural validity, behavioral correctness, and implementation quality.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-21T20:38:50Z
Haocheng Xia, Eugene Wu, Yongjoo Park
arXiv categories: cs.CL, cs.AI, cs.SE

Parallel coding agents can produce patches that work alone but fail when merged. This happens when one agent changes an interface or rule that another agent still relies on. We study these failures with stale, a benchmark for semantic coordination. Our evaluation runs the same tests on each patch alone and on their combination, counting only failures introduced by combining the patches. We use three tiers: synthetic tasks with controlled interface changes, pairs of merged pull requests, and constructed tasks that use real Django helpers. Among 834 runs on 417 mined Django pairs, only one showed interference after correcting the grading procedure. On constructed tasks using 12 Django helpers, interference occurred in 97% of runs. A message describing the completed concurrent change recovered 82% of runs. Reviewed pull requests may contain few unresolved parallel changes, even when agents fail on controlled tasks using real code. The constructed failure rates do not estimate how often these problems occur in practice.

arXiv abstract · PDF

Software Engineering and AI Agents · primary corpus · published 2026-09-21T21:19:46Z
Yifeng He, Jiachen Liu
arXiv categories: cs.PL, cs.AI

As autonomous AI agents take on every stage of scientific inquiry, research output is expanding far beyond human review capacity. Yet scientific communication still relies on natural-language prose: an informal medium prone to ambiguity, hidden assumptions, and untracked limitations that machines cannot reliably audit. We introduce Lara, a machine-checkable language and protocol for checking and revising support for research claims. By turning research arguments into executable artifacts, Lara provides an epistemic kernel for autonomous science: it enables automated validation pipelines for research agents, lets declared bridges connect arguments across papers into an auditable network, and allows both humans and machines to recheck the standing of an encoded claim in milliseconds. In a Lara program, authors explicitly declare their claims, supporting evidence and assumptions, and known objections or limitations. A lightweight, deterministic checker adjudicates these interactions, assigning each claim a reproducible status: "justified", "defeated", "contested", or "gap", which marks a claim whose support is incomplete and locates the unanswered question. Case studies cover empirical review, a philosophical debate without measurements, and the loss of support when an assumed axiom is withdrawn. We establish the metatheory of claim checking and cross-context argument transport, and mechanize the semantic guarantees in Lean 4 (roughly 117,000 lines), leaving three arguments on paper. The audited public metatheory is "sorry"-free and uses only Lean's three standard axioms; some executable examples additionally trust native evaluation.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-22T00:18:39Z
Jo\~ao Medeiros, Denini Silva, Breno Miranda
arXiv categories: cs.SE

Flaky tests produce non-deterministic outcomes without code change, eroding CI confidence and delaying deliveries. While vocabulary-based machine learning prediction has proven effective for Java and JavaScript, no study has evaluated it for Swift, a language whose testing style is dominated by UI and asynchronous code. We collect 91 flaky and 22,349 stable tests from 15 open-source Swift projects via re-execution and commit-history mining, then train five classifiers (Random Forest, Decision Tree, Naive Bayes, SVM, KNN) on TF-IDF unigram+bigram features under stratified 5-fold cross-validation. Random Forest achieves the best performance (Precision = 0.92, F1 = 0.86, AUC = 0.95) and substantially outperforms trivial baselines, among them a vocabulary-threshold rule applied to the most informative tokens, confirming a genuine discriminative signal (MCC = 0.75 vs. 0.08 for the best baseline). Information-gain analysis reveals two complementary signal types. Flakiness markers appear predominantly in unstable tests and comprise concurrency primitives (async, await), expectation-based synchronisation (expectation, fulfill), error propagation (throws), and explicit timing dependence (timeout, wait, now). Stability markers, chiefly the assertion vocabulary of plainly synchronous tests (xctassertequal), count as evidence against flakiness. Error analysis shows that the model fails when flakiness is hidden in shared infrastructure outside the test body or when async constructs are used in a deterministic context, exposing the intrinsic limit of lexical prediction. These results extend vocabulary-based flakiness detection to the Swift ecosystem and characterise both its effectiveness and its boundaries.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-22T00:32:46Z
Mahya Samdaliri, Zhihao Yao, Kasthuri Jayarajah
arXiv categories: cs.SE, cs.CR

WebGPU is a low-level graphics and compute API that exposes modern GPU functionality to web applications. While the official WebGPU Conformance Test Suite (CTS) focuses on well-formed usage under the WebGPU specification, it is not designed to stress implementations with semantic edge cases or adversarial inputs. General-purpose fuzzers, in contrast, struggle with WebGPU because of its complex graphics stack and multi-process architecture. We introduce LANTERN, a specification-guided dynamic conformance testing framework that mutates CTS tests using constraints extracted from the WebGPU specification. LANTERN extracts explicit syntactic API rules from WebIDL definitions and recovers semantic constraints, such as command ordering and object lifetimes, from natural-language specification text. Selected rules guide AST-located textual transformations that generate both valid and intentionally invalid CTS variants. We execute the resulting tests at scale on AddressSanitizer-instrumented Chromium to discover bugs. Our evaluation discovers three reproducible bugs, including a heap corruption, in Chromium versions current at the time of study. These results demonstrate that syntactically seeded, semantics-aware mutation of conformance tests provides a way to uncover browser bugs during WebGPU testing.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-22T00:48:48Z
Gabriela Leal, Denini Silva, Leopoldo Teixeira
arXiv categories: cs.SE

Flaky tests pass or fail non-deterministically on unchanged code, eroding trust in test suites and inflating the cost of every failure. Shaker detects them by injecting resource contention (CPU, memory, and I/O stress) to amplify non-determinism caused by concurrent execution, and was reported to detect 95% of the flaky tests in a Java and Android benchmark against 37.5% for plain re-execution (ReRun). We present the first empirical evaluation of Shaker for Python. Drawing non-order-dependent flaky tests from the ground-truth dataset of Gruber et al., we compare Shaker against a budget-matched ReRun baseline in a paired design, giving both techniques the same number of test executions: Each of 137 tests is run 100 times under each. As configured for Java and Android, Shaker provides no statistically significant detection advantage over plain re-execution (37.2% vs. 35.8%; McNemar exact p = 0.84). Two findings explain why. First, fewer than half of the ground-truth flaky tests reproduce as flaky at all on independent hardware under either technique, and most of the tests that fail to reproduce never diverge once across 100 runs. Second, the tests that do reproduce are dominated by flakiness from network interactions and randomness rather than the concurrency Shaker targets. Beyond the tool, this exposes a broader hazard for the field: reusing a flaky-test ground truth across execution environments silently converts genuine flaky tests into apparent true negatives, deflating any tool's measured recall.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-22T02:51:23Z
Wen-ling Huang, Jan Peleska
arXiv categories: cs.FL, cs.SE

Symbolic finite state machines (SFSMs) describe input/output behaviour using guards and output assignments with possibly infinite data domains. We study deterministic and completely specified SFSMs whose guards and output assignments depend only on the current input. We define finite representative input sets that contain witnesses for relevant guard overlaps and separating witnesses for output assignments that differ on those overlaps. Our main theorem shows that language equivalence of the finite instantiations implies language equivalence over the full input domain. This result transfers complete testing methods for deterministic finite state machines (DFSMs) to SFSMs, provided finite sets of admissible guards and output assignments and an upper bound on the number of distinguishable reachable states are known. Under these assumptions, a DFSM learner with complete testing can learn a finite instantiation, which is then lifted to an equivalent SFSM. We establish a bound on the size of representative input sets and give an SMT construction whose correctness and termination hold under stated solver assumptions.

arXiv abstract · PDF

Software Engineering and AI Agents · cs.SE candidate · published 2026-09-22T09:16:13Z
Liheng Fan, Jialun Yin, Yuzhi Chen
arXiv categories: cs.SE

Dependency-update pull requests are frequent and mostly routine, but a small subset requires non-trivial compatibility repair. Recent repository-level coding agents make such repair increasingly plausible, yet invoking them on every dependency update wastes model calls, CI time, repository context, and review attention. We frame this as a pre-agent routing problem: deciding which dependency-update pull requests should be escalated before downstream diagnosis or repair attempts. We introduce DepFixRouter, a lightweight router that ranks dependency updates by historical compatibility-repair likelihood using creation-time textual and metadata signals. On 497 labeled GitHub dependency-update candidates, only 72 require substantive repair. A creation-time-safe LinearSVC using only PR titles and bot/dependency flags reaches 0.488 repair F1 and captures 51.4% of repairs within the top 20% routed pull requests, improving calls per captured repair from 6.90 under route-all or random policies to 2.68. Retrospective full-history signals improve top-20% recall to 65.3%, revealing substantial hindsight leakage in pull-request histories rather than deployment-time routing utility. In a 60-case diagnosis-agent pilot, router-gated diagnosis reduces actual LLM calls by 66.7% and tokens by 66.1%, suggesting budgetaware escalation while measuring diagnosis rather than patch generation. DepFixRouter can serve as a lightweight escalation layer between routine dependency-update automation and expensive repository-level agents, enabling budget-aware maintenance without relying on retrospective repair evidence for deployment-time routing.

arXiv abstract · PDF