arXiv weekly literature review

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-13T01:09:51Z
Han Bao, Shinsaku Sakaue, Kazuki Watanabe
arXiv categories: math.OC, cs.AI, cs.LO

Safety verification of a Markov decision process (MDP) asks whether the probabilities of reaching several failure states jointly lie in a convex safe region under every scheduler. Watanabe and Unno (2026) prove safety by refining an outer approximation of the failure probabilities, where each query bounds a nonnegative weighted sum of the probabilities. Their rule selects weights by the largest Euclidean violation. We present a unified framework to measure violation in an explicitly chosen error unit: directions are scored by the support-function gap between the outer approximation and the safe region, normalized by the support function of the unit. We show that the maximal score, when positive, equals the smallest enlargement of the safe region in multiples of that unit that contains the outer approximation. The Euclidean unit recovers the earlier rule; two new rules are generated by the unit cube and the safe region itself. We experimentally evaluate how the choice of measurement rule affects the performance of safety verification for MDPs.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-13T10:33:58Z
S Akshay, Suguman Bansal, Gaurav Mahla
arXiv categories: cs.LO, cs.AI

{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with \emph{learning} an optimal policy against a formal specification in an unknown {\em Markov Decision Process (MDP)}. We take up the dual question. Given a policy already in hand, can one \emph{verify} that it is correct against a formal specification in an unknown MDP, using sampling access alone? Such a question arises naturally in safety-critical systems. We investigate it for the {\em almost-sure reachability property}, whose correctness is witnessed by a {\em ranking supermartingale (RSM)} certificate. Our first finding is negative. In the absence of any further information about the MDP, one can neither learn such a certificate nor verify a candidate one with probabilistic guarantees. On the positive side, we show that, under a mild restriction, a known lower bound $p_{\min}$ on nonzero transition probabilities, a correct certificate \emph{can} be learned with PAC-style guarantees. To the best of our knowledge, this is the first study of learning and verifying certificates for almost-sure reachability in unknown MDPs from sampling access alone. Finally, our experiments show that the $p_{\min}$-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-13T12:15:22Z
Yifan He, Munyque Mittelmann, Aniello Murano, Michael Thielscher
arXiv categories: cs.LO

This paper studies the complexity of model checking strategic abilities in multiagent systems under imperfect information, in particular systems represented succinctly. Such a representation can describe systems that are exponentially larger than their input and is particularly relevant to practical implementations of model checkers such as MCMAS. The logics we consider include epistemic strategy logic supporting partial binding $SLK_{P}$, and its syntactic fragments: epistemic strategy logic $SLK$ and variants of Alternating Time Temporal logics. We show that succinct model checking for $SLK_P$ and $SLK$ is $AEXP(poly)$-complete, while objective ATL and ATL$^{*}$ are $P^{NEXP}$-complete. The latter corrects a previous NEXP-completeness result for model checking succinct imperfect-information systems. Under subjective semantics, $P^{NEXP}$-completeness already holds for one-step Coalition Logic, and therefore also for ATL and ATL$^{*}$.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-15T06:58:18Z
Elli Anastasiadi, Kim Guldstrand Larsen, Martin Zimmermann
arXiv categories: cs.LO, cs.FL

Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows for arbitrary mixing of trace quantification and the use of fixed points for expressing temporal requirements, which makes it very expressive in comparison to other first-order hyperlogics. HyperRecHML has already been successfully applied in runtime verification, but the decidability of its model checking problem remains open. We answer this question positively by providing two main contributions. Firstly, a normalization procedure that allows to reduce arbitrary HyperRecHML formulas to a normal form with restricted nesting of trace quantification and fixed points. Secondly, we provide an automata-based model checking algorithm for formulas of this normal form. The complexity of our algorithm is comparable to similar ones for other hyperlogics, despite the extra expressive power.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-15T17:42:52Z
Omar Adalat, Edwin Hamel-De le Court, Francesco Belardinelli
arXiv categories: cs.LG, cs.LO, cs.MA

We study rational synthesis for stochastic multi-agent systems with unknown dynamics, where each agent is equipped with its own probabilistic temporal objective specified using Probabilistic Linear Temporal Logic on Finite Traces ($\mathsf{PLTL}_f}$). We impose solution concepts (e.g., Nash equilibrium, subgame-perfect equilibrium) as constraints on the joint strategy profile, using payoffs derived from each agent's probability of satisfying its temporal objective. In particular, we formulate per-agent rational synthesis as finding a strategy profile -- if one exists -- such that (i) the designated agent's probabilistic temporal constraint is satisfied, and (ii) the profile represents a stable solution under a chosen solution concept. We give conditional convergence guarantees for tabular Nash-Q learning, certify satisfaction with simultaneous finite-sample confidence bounds, and assess strategic stability with approximate best-response checking. Our approach operates in a stochastic \emph{Multi-Agent Reinforcement Learning} (MARL) environment, where model-free learning algorithms attempt to attain extremal satisfaction probabilities for temporal objectives automatically compiled into reward automata. Our approach is empirically validated using 8 general-sum concurrent stochastic games.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-15T23:45:21Z
Parv Kapoor, Teresa Fortes, Claudia Mamede, Rui Abreu, Jonathan Aldrich, Eunsuk Kang
arXiv categories: cs.LG, cs.LO

LLM safety evaluations via jailbreaking typically index on attack success rate (ASR): whether a generated response violates safeguards. However, ASR only evaluates sampled outputs and provides little information on the underlying generation process. Autoregressive language models define distributions over possible outputs, and a sampled refusal can coexist with substantial probability mass on harmful generation paths. We study this hidden structure through bounded continuation analysis (BCA), which models autoregressive generation as a stochastic process over token prefixes and computes the finite-horizon probability that generation reaches a harmful continuation. BCA constructs a bounded continuation tree, labels terminal continuations with a semantic harm evaluator, and estimates harmful reachability using exact probabilistic model checking. BCA complements ASR by measuring how much harmful behavior remains accessible beneath a sampled safe response. This makes it useful for distinguishing models that look identical under measured ASR values, and allocating red-team effort toward regions of the generation process with greater hidden risk. Across four instruction-tuned LLMs and 100 JailbreakBench behaviors, we show that BCA effectively quantifies hidden harmful behavior and provides a useful signal to guide red teaming.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-16T13:42:04Z
Mihir Vahanwala
arXiv categories: cs.FL, cs.LO

Toric words have recently gained attention as a means to model the behaviour of dynamical systems such as linear loops. This work is concerned with describing when the toric model is precise enough to decide whether the trace of a system is contained in an omega-regular language. Our contributions are threefold. (i) We use topological means to generalise a class of toric words by defining noise-robust dynamical systems and their sets of noisy traces. We prove that all noisy traces of a system are almost-periodic, and have the same set of recurrent factors. (ii) We apply the abstract techniques above to concrete sequences obtained as sign descriptions of real algebraic linear recurrence sequences (LRS), and show that the language-membership problem for sign descriptions of LRS with few dominant roots is decidable. (iii) We show that noisy traces of noise-robust dynamical systems are indistinguishable to a prefix-independent omega-regular language, and inclusion is decidable provided the common language of their recurrent factors is recursive. We incidentally obtain properties of prefix-independent omega-regular languages that may be of independent interest.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-16T17:54:38Z
Sai Sandeep Damera, Ryan Matheu, John S. Baras, Calin Belta
arXiv categories: eess.SY, cs.LO, cs.RO, cs.SY

A gradient-based solver that enforces a Signal Temporal Logic (STL) specification uses a smooth approximation of its quantitative semantics, the robustness. In safety-critical trajectory optimization, this approximation must have two properties. First, it must be sound, that is, nonnegative only on trajectories that satisfy the specification. Second, at each temporal operator, the weight of its gradient on the violating samples must stay bounded away from zero, however long the horizon. The approximations in use, including the log-sum-exp, its sound variant, and the generalized-mean robustness, do not have both. We introduce lower approximations of the minimum and the maximum whose gradients are sparsemax projections, and we prove that the robustness built from them has both. It lies below the exact robustness and is therefore sound, and its error has a bound that is independent of the number of samples and known before optimization. The gradient of each approximation is exactly zero on every sample beyond a data-dependent threshold, so the weight on violating samples a gap beyond the others has a positive lower bound at every horizon. On a planar unicycle and on a seven-joint manipulator beside a person in simulation, the log-sum-exp approximation is positive on a violating trajectory. As the horizon of the manipulator's task grows from 10 to 80 s, the gradient weight of the sound variant on the violating samples falls from 0.22 to 0.04, while that of sparsemax stays at 1. In a constrained trajectory optimization of the unicycle, the constraint on the log-sum-exp robustness returns a violating trajectory, whereas the constraint on the sparsemax robustness returns a trajectory that satisfies the specification with the required margin.

arXiv abstract · PDF

Probabilistic and Strategic Model Checking · primary corpus · published 2026-10-17T05:18:42Z
Shanxia Wang, Yuqiang Dou
arXiv categories: cs.LO, math.LO

For a fixed finite set $N$ of at least two agents, we investigate the lattice $L_N$ of coalition logics between minimal coalition logic (MCL) and classical coalition logic (CL), with extensions required to be structural. This lattice is order-dual to an interval in the subvariety lattice of Boolean coalition algebras. The eight basic extensions obtained by imposing seriality, independence of agents, and determinism form a Boolean cube under inclusion, but not a sublattice of $L_N$. Our main results concern coatoms and compact meets. First, finite critical coalition algebras, realized as complex algebras of finite general concurrent games, yield three infinite families of pairwise distinct coatoms containing seriality, distinguished by failures of independence, determinism, or both. An explicit splitting characterizes the unique coatom omitting seriality. Second, the meet of two basic extensions is compact if and only if the extensions are comparable. For incomparable pairs, no axiomatization of the meet can use formulas of uniformly bounded modal depth, even with infinitely many axioms. Consequently, $L_N$ and three natural principal intervals are non-coherent algebraic lattices. These results reveal lattice-theoretic phenomena beyond the inclusion order of the eight basic extensions.

arXiv abstract · PDF

SAT and SMT Solving · primary corpus · published 2026-10-13T11:39:45Z
Martin S. Fixman, Fredrik R{\o}mming, Sean B. Holden
arXiv categories: cs.LO, cs.AI

Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after a failed attempt. SATCoP addresses this by retaining grounded tableau clauses in an incremental SAT solver, allowing the prover to refute the problem once the accumulated ground clauses become propositionally unsatisfiable. We introduce SATResetCoP, which relies more directly on this persistent SAT state by not backtracking on unproductive tableaux and instead starting new ones to generate further ground clauses for the SAT solver. On TPTP, SATResetCoP improves over our leanCoP-style baseline by 54% and our SATCoP-style baseline by 18%. On the bushy MPTP2078 benchmark, it solves 616 problems, a 49% improvement over our leanCoP-style baseline and a 12% improvement over our SATCoP-style baseline. These results suggest that changing tableau guidance to accumulate useful ground clauses faster improves the performance of the prover.

arXiv abstract · PDF

SAT and SMT Solving · primary corpus · published 2026-10-15T17:16:55Z
L. Sunil Chandran, Rishikesh Gajjala, Suraj Kumar Sahoo, Aatman Supkar
arXiv categories: cs.CG, cs.DM, cs.DS, cs.LO, math.CO

We present compact SAT encodings and certifying exact solvers for boxicity and cubicity. The boxicity of a graph is the minimum dimension in which it is the intersection graph of axis-aligned boxes; cubicity is defined analogously using unit cubes. Grid-based formulations face a geometric discretization bottleneck, growing rapidly with the target dimension. We avoid this bottleneck by encoding the total order of interval endpoints in each coordinate. For an $n$-vertex graph and target dimension $d$, our boxicity encoding uses $O(n^2d)$ variables and $O(n^3d)$ clauses, both linear in $d$. Requiring the left- and right-endpoint orders to agree yields a cubicity encoding of the same asymptotic size. Satisfying models are decoded into independently checked geometric representations, while unsatisfiable instances used as lower-bound evidence carry mechanically verified DRAT certificates. In a controlled evaluation with 186 trials per encoding on standard and structured graph families, the order encoding solves 96.8% of trials, compared with 71.0% for the known grid formulation, and reduces mean PAR-2 time from 178.21 to 21.70 seconds. The pipeline also certifies exact values for several named graphs. We turn one such value into a reusable obstruction by proving that every Kneser graph $K(n,k)$ with $k\ge3$ and $n\ge2k+1$ contains an induced Desargues graph. The resulting lower bound, together with an explicit three-dimensional representation of $K(7,3)$, establishes $\operatorname{boxicity}(K(7,3))=3$. This disproves the conjecture of Caoduro and Sebo that $\operatorname{boxicity}(K(n,k))=n-k$ for all $k\ge3$ and $n\ge2k+1$.

arXiv abstract · PDF

SAT and SMT Solving · primary corpus · published 2026-10-16T17:08:03Z
Baiting Jiang
arXiv categories: cs.LO, cs.AI

Constrained Horn clause (CHC) solvers often struggle to discover deep counterexamples whose derivations may require extensive rule unfolding. Although large language models (LLMs) can propose long-range symbolic relations, prior work on formally checked LLM-assisted verification has mainly focused on generating inductive invariants and concrete traces. We exploit this broader capability through Derivation Power Under-approximations (DPUs). Each DPU is a solver-certified under-approximation of the relation induced by a multi-step CHC derivation. An LLM proposes each DPU with symbolic intermediate-state witnesses that enable SMT validation without introducing additional quantifiers. Validated DPUs can be composed and reused soundly. Building on this mechanism, our LLM-assisted framework HornCraft combines invariant generation for over-approximation with DPU generation for under-approximation in CHC solving. On 260 linear and nonlinear integer-arithmetic CHC-COMP benchmarks left unresolved by a 30-minute Spacer run, HornCraft returns certified verdicts for 228 instances. It certifies 42 instances as unsafe, compared with 22 when DPU construction and reuse are disabled.

arXiv abstract · PDF

SAT and SMT Solving · primary corpus · published 2026-10-17T01:47:55Z
Haoze Wu, Andr\'e Schidler, Armin Biere, Nina Narodytska
arXiv categories: cs.LO, cs.AI, math.LO

Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly coupled to particular strategies, making it inconvenient to define new strategies without changing solver internals. We present Tactix, a proof-producing sequential CDCL solver that incorporates a wide range of techniques in state-of-the-art solvers with a clean separation of proof rules from solving strategies. This separation enables a public interface through which users can invoke particular techniques, observe their effects, and program a wide range of solving strategies. The default strategy of Tactix is programmable over this interface and outperforms state-of-the-art solvers on benchmarks from the 2024--2026 SAT Competitions. We also use the interface to develop novel strategies tailored to challenging benchmarks from two application domains, which led to performance gains over strong baselines. We intend Tactix to serve as an infrastructure for designing and evaluating novel solving strategies. Finally, we also present a self-study of the AI-assisted development process behind Tactix.

arXiv abstract · PDF

SAT and SMT Solving · primary corpus · published 2026-10-18T11:35:13Z
Siyi Wu, Bican Xia
arXiv categories: cs.LO

Word equations with cyclic variable dependencies pose a challenge to SMT string solvers. In stabilization-based procedures, such dependencies can trigger repeated refinement of regular-language assignments without reaching stability. We present Z3-Noodler-C, an extension of Z3-Noodler, combining equality-aware stabilization with dedicated loop reasoning. We introduce equality predicates to retain relevant equations as single stability obligations, and extend stabilization with equality-aware substitution and adapted concatenation-eliminating refinement to expose cyclic dependencies as overlapping variable bindings. Dedicated loop reasoning rules then exploit the periodic structure of these bindings, avoiding certain infinite derivations. We evaluate Z3-Noodler-C against Z3-Noodler, cvc5 and OSTRICH2. On 64 systematically generated, syntactically simple instances involving cyclic dependencies and regular constraints, our solver solves all instances, compared with only 20 solved for the best baseline. On equation-oriented instances from SMT-LIB'25, Z3-Noodler-C achieves the highest coverage, solving 20 more instances than Z3-Noodler while maintaining competitive aggregate CPU time.

arXiv abstract · PDF

Constraint Satisfaction Complexity · primary corpus · published 2026-10-13T12:36:58Z
Manuel Bodirsky, Philipp A. Grzywaczyk
arXiv categories: cs.LO, math.LO

We study definability in fixed-point logic with counting (FPC) for a class of constraint satisfaction problems (CSPs) that simultaneously generalises finite-domain CSPs and temporal CSPs. The templates for the CSPs are first-order expansions of the structure $([k] \times {\mathbb Q};<_1,\dots,<_k,\sim)$ where $<_i \, := \{((i,x),(i,x')) \mid x<x'\}$ and $\sim \, := \{((i,x),(i,x')) \mid i \in [k], x,x' \in {\mathbb Q}\}$, i.e., $k$ copies of $({\mathbb Q};<)$. Such a CSP is definable in FPC precisely when the template pp-constructs neither the ternary temporal relation $X$, which holds on three elements if the minimum is attained exactly twice, nor a nontrivial finite affine structure. Equivalently, the template has global polymorphisms that witness the tractability of the temporal CSPs on the copies, and that provide 3-4 weak near-unanimity operations on the set of copies of ${\mathbb Q}$. In this case, we prove that the CSP is even expressible in the less expressive logic FP$^*$, which is the restriction of FPC without counting terms (i.e., the extension of first-order logic by a fixed point operator and an ordered auxiliary number sort). Our algorithm samples finitely many values in each copy and then performs nested constraint-singleton consistency tests (which is a uniform polynomial-time algorithm for finite-domain CSPs). The correctness proof uses finite-domain CSP theory to combine consistency certificates by a single polymorphism term, fixing each variable to one copy without destroying the certificates needed for the temporal algorithm. We then use a known normal form for algebraic products to control the remaining interactions between different copies.

arXiv abstract · PDF

Constraint Satisfaction Complexity · primary corpus · published 2026-10-14T10:24:20Z
Manuel Bodirsky, David Bradley-Williams, Ehud Hrushovski, Christoph Spiess
arXiv categories: cs.LO, math.LO

We construct countable, stable, $\omega$-categorical structures with at most two binary relations whose CSPs exhibit three complexity regimes: NP-complete, decidable but not in NP, and undecidable. The templates arise from a controlled Hrushovski construction of stable $\omega$-categorical graphs $M_\alpha$ for suitable irrational parameters $\alpha>1$. Some of these graphs have NP-complete CSPs. Expanding the graphs $M_\alpha$ by the non-edge relation turns age membership into a restriction of the CSP. For every time-constructible bound $t$, there is such an expansion whose CSP is decidable but not in DTIME$(t)$. For an explicit parameter $\alpha$, the restriction to complete instances belongs to $\mathrm{coNP}$ and the full CSP belongs to $\Sigma_2^{\mathrm P}$. Separating the ages of the $M_\alpha$ using graphs with large girth and prescribed density yields $2^{\aleph_0}$ distinct CSPs of these expansions, all but countably many of which are undecidable.

arXiv abstract · PDF

Constraint Satisfaction Complexity · primary corpus · published 2026-10-14T10:26:21Z
Artur Je\.z, Jakub Michaliszyn, Piotr Witkowski
arXiv categories: cs.LO

We study finite satisfiability of two-variable first-order logic over structures equipped with an arbitrary finite number of independent successor relations of linear orders. The number of successor relations is part of the input, and the vocabulary may contain further unrestricted unary and binary relations. We prove decidability in deterministic doubly exponential space together with a triply exponential bound on the size of a smallest finite model. This settles the unrestricted finite case beyond two successors.

arXiv abstract · PDF

Constraint Satisfaction Complexity · primary corpus · published 2026-10-14T21:04:48Z
Bartosz Jan Bednarczyk, Daumantas Kojelis, Krzysztof Szyma\'nski
arXiv categories: cs.LO

We study the two-variable fragment FO^2 of first-order logic over two-dimensional structures. Formulae may employ two linear orders <=_1, <=_2, their successor relations S_1, S_2, and auxiliary predicates of any arity. Despite two decades of work, three cases of finite satisfiability in this setting were still open; we settle all three. First, finite satisfiability of FO^2 with one linear order and one successor relation, of the same or of a different order, is NExpTime-complete, even with arbitrary auxiliary predicates and constant symbols. This closes a gap left open by Manuel and Zeume (CSL 2013). As an application, a reduction based on swaps of adjacent elements shows that order-invariance and order-successor-invariance of FO^2 are coNExpTime-complete. This reproves the main result of Zeume and Harwath (LICS 2016) and settles their question on order-successor-invariance. Second, finite satisfiability of FO^2 with two linear orders is ExpSpace-hard, already without auxiliary non-unary predicates, matching the upper bound known since 2010. Our reduction combines Kieronski's encoding of alternating Turing machines with the classical fact that the pre-order and post-order traversals of a tree define its descendant relation. Third, with two linear orders and the successor of one of them, finite satisfiability is in ExpSpace even with arbitrary auxiliary predicates, improving the previous 2NExpTime bound and confirming a conjecture of Zeume and Harwath. Together with known results, our theorems show that in two dimensions, auxiliary (non-unary) predicates and constants come for free: with or without them, the complexities coincide. All our proofs are simple.

arXiv abstract · PDF

Constraint Satisfaction Complexity · primary corpus · published 2026-10-15T14:26:03Z
Lukas Pieper
arXiv categories: math.LO, cs.CC

We revisit the complexity classification of constraint satisfaction problems (CSPs) for first-order reducts of $(\mathbb{Z},<)$, established by Bodirsky, Martin, and Mottet in 2018. Following their approach, we give a self-contained proof of this classification, correcting several errors in the argument. We further show that, with the exception of cases arising from finite-domain CSPs, all tractable cases are solved by a well-known uniform algorithm, eliminating the need for the collection of ad-hoc algorithms used in the original paper. A central component of the proof allows the analysis to be restricted to first-order reducts of $(\mathbb{Z},<)$ that contain the successor relation. We substantially simplify this reduction and generalize the underlying construction. This generalization allows us to apply the same technique to first-order reducts of the triangular lattice graph and of infinite regular trees, yielding a complete complexity classification for these classes of structures, in particular a $\mathsf{P}$ versus $\mathsf{NP}$-complete dichotomy.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-12T13:52:21Z
Paolo Agliano, Mitar Nedeljkovic
arXiv categories: math.LO

In this paper we develop several aspects of the algebraic theory of Girard algebras, regarded as the equivalent algebraic semantics of multiplicative additive Linear Logic $\mathsf{MALL}$. The main structural results concern the bottom of the subvariety lattice of the variety of Girard algebras: varieties generated by simple Girard algebras generated by the constants correspond exactly to the atoms of the lattice. Moreover the lattice itself is atomic, i.e. every nontrivial subvariety contains an atom. These atoms can be represented uniformly by the maximal filters of the free algebra generated by the constants. Moreover every congruence of this free algebra is realized by a subvariety, and the resulting atom-support topology records the behavior of arbitrary joins: the atoms below a join of atoms are precisely the points in the closure of the corresponding subset of the spectrum. The concrete constructions show that the bottom of the lattice is already quite rich. Besides determining the integral and degenerate boundary cases and exhibiting finite modular and nonmodular atoms and chains of covers, we constructed infinite families of atoms whose topology reflects genuinely infinitary behavior; thus finite and infinite joins behave essentially differently at the bottom of the subvariety lattice. On the logical side, these results yield $2^{\aleph_0}$ Post-complete extensions of $\mathsf{MALL}$.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-12T16:21:33Z
Loic Cosyns
arXiv categories: math.LO, math.PR

A class of models which brings to the fore the inner logic of the calculus of probability instead of assigning probabilities to sentences is introduced and investigated.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-12T16:43:08Z
Khashayar Irani
arXiv categories: cs.LO

This concise manuscript investigates the nonlocal nature of natural deduction, particularly the possibility of introducing assumptions at intermediate stages of a derivation after those stages have already been passed. By examining the structural correspondence between natural deduction and sequent calculus, we demonstrate how the structural rule of left-weakening (LW) permits the enlargement of an antecedent after its corresponding succedent has been derived, without modifying the original inference. Through a number of symmetrical derivations, we establish the proof-theoretic relationship between the introduction of assumptions in natural deduction and antecedent expansion in sequent calculus. On this basis, we formulate the principle of Nonlocal Assumption Introduction (NAI), according to which assumptions may be introduced at any intermediate stage prior to the final conclusion, provided that the corresponding structural expansion is proof-theoretically valid. We further specify the conditions governing this operation, including the preservation of inferential validity, assumption dependencies, and the scope and discharge requirements of the resulting derivation.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-13T17:41:29Z
Tim S. Lyon (TU Dresden), Lukas Zenger (Peking University)
arXiv categories: cs.LO

We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central problems, which we call "cycle recognition" and "unraveling." Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call "saturation recurrence," which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-14T12:43:38Z
Fedor Pakhomov, Vlad Lazar
arXiv categories: math.LO

We introduce a novel extension of reflection calculus, $\mathsf{RC_{BI}}$, to analyze a family of extensions of $\mathsf{ACA}_0$ generated by uniform $\omega$-model and syntactic reflection principles, together with several other related operators. The union of these theories coincides with the theory of Bar Induction ($\mathsf{BI}$). We prove that $\mathsf{RC_{BI}}$ is arithmetically sound, and that it is sound and complete with respect to a natural class of Kripke models. Leveraging these modal semantics, we demonstrate that the class of theories denoted by $\nabla$-free closed formulas is a pre-wellordering with respect to $\Pi^1_1$-soundness and consistency strength. This allows us to establish an ordinal analysis for $\mathsf{BI}$ and its fragments, analogous to Beklemishev's analysis of $\mathsf{PA}$. The structural properties of $\mathsf{RC_{BI}}$ naturally give rise to a novel ordinal notation system for the Bachmann-Howard ordinal which differs substantially from existing representations.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-14T21:28:31Z
Sergio A. Celani, William Zuluaga
arXiv categories: math.LO, math.CT

Sequent algebras were introduced by D. Vakarelov \cite{VakarelovSequentALg} as a generalization of contact algebras, replacing the binary contact relation with a relation between finite sets of regions and regions. In this paper, we present sequent algebras as Boolean algebras endowed with a finitary closure operator satisfying four conditions. We study the irreducible closed sets of these operators, which coincide with Vakarelov's clans, and use them to develop a topological representation theory for sequent algebras. We introduce the categories of sequent algebras and sequent spaces and establish a dual equivalence between them, as well as a restricted dual equivalence for morphisms preserving the full Boolean structure. We also characterize sequent congruences in terms of positive filters and minimally decreasing closed subsets of the associated sequent spaces. Finally, we show that the category of sequent algebras with sequent homomorphisms is topological over the category of Boolean algebras, obtaining completeness and cocompleteness and a complete lattice structure on the sequent structures over each Boolean algebra.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-16T17:45:53Z
Victor Barroso-Nascimento, Arghya Chakrabarty, Elaine Pimentel
arXiv categories: cs.LO, math.LO

Base-extension semantics explains logical consequence via derivability in atomic systems. Extending this approach across logics requires careful control of structural principles and contexts. We present a modular sequent-based framework in which support is indexed by multisets of atomic resources and the semantic clauses for connectives are guided by their left introduction rules. The framework separates additive from multiplicative behaviour and makes explicit the contributions of structural rules and restrictions on sequents. We establish soundness and completeness for classical and intuitionistic propositional logic and for multiplicative-additive fragments of classical and intuitionistic linear logic. We then investigate axiomatic extensions of intuitionistic logic through Jankov logic. Two classes of atomic bases yield sound and complete semantics. Completeness is proven using two novel and modular methods using simulation bases, one of which is constructive. These results provide a common semantic treatment of several logical systems while identifying the additional conditions needed to extend the framework beyond structural variations.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-16T20:23:29Z
Nino Grandinetti, Abilio Rodrigues
arXiv categories: math.LO

This paper investigates the proof theory of the logic of evidence and truth LETFm, with the aim of obtaining a sequent calculus consisting only of logical rules, suitable for a simple bottom-up decision procedure. We begin with G1f, a sequent system containing structural rules, which makes explicit the main difficulties in obtaining a fully logical and decidable calculus for LETFm. We then introduce G3f, a G3-style system obtained from by applying Kleene's trick, which absorbs contraction into the logical rules by adding the principal formula of the rule to its premises.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-13T07:41:30Z
Jacek Karwowski, Frank Nielsen, Sam Staton
arXiv categories: cs.PL, cs.CG

We study the compositional, intensional information geometry of probabilistic programs. For a first-order probabilistic programming language with finite random variables, we construct a contravariant lax monoidal functor that, for a program of type $X \to Y$, pulls back a (degenerate) Riemannian metric on $Y$ to $X$. It specialises to the Fisher metric in the case of standard statistical models and to ordinary pullback in the case of deterministic programs. We further justify this construction in two ways. First, we show that this functor arises as a pullback of geometry from a universal space of programs over a type $Y$ with a fixed trace space. Second, we show that it is a special case of a more general pullback construction over weighted measures. Our compositional geometry depends on the presentation of the program, and we study how it relates to the (non-compositional) geometry of the realised measures by establishing a three-level inequality relating our score-velocity metric for the program, the program's corresponding output-conditioned metric, and the standard Wasserstein-Fisher-Rao metric of the realised family. Finally, we show how the theory can be extended to accommodate continuous random variables using diffeological quasi-Borel spaces. We also discuss several concrete directions for future work.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-13T16:43:05Z
Yuxu Chen
arXiv categories: math.GN, math.LO

We prove that every chain-continuous dcpo is continuous and that its way-below relation is the relational square of its chain-below relation, answering a question of Ern\'e. A subalgebra lattice obtained from a locally finite J\'onsson algebra shows that the chain-below relation itself need not interpolate. For approximation by Scott-closed sets, we give a finite-upper-bound characterization on lower-set lattices and characterize interpolation by an extension property for directed lower sets. This yields a countably based, completely distributive algebraic lattice on which chain and directed approximation coincide, whereas Scott-closed approximation fails to interpolate, answering questions of Ern\'e and of Ho and Zhao.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-14T15:31:09Z
Mingkun Xiao, Yixuan Sun
arXiv categories: cs.PL

System $F_{<:}^{\top}$ has decidable subtyping but lacks minimum types. We prove that typechecking is decidable for arbitrary explicitly annotated terms with unrestricted subsumption. The difficulty is that type abstraction uses a variable's declared bound to type its body, while quantified subtyping forgets that bound. We construct finite covers that preserve all required subtype comparisons across this change of context. These covers yield a compositional finite typing basis and a decision procedure. We then derive a backward checker that propagates acceptable targets without constructing the complete typing basis. Rectangularity of typing families gives a uniform elimination domain while retaining every result type, even when the canonical type is not least. Finite inverse families transport targets through type substitution. The same inverse specification recovers bound forgetting and yields finite type-avoidance families. Both typechecking procedures are total Rocq functions proved equivalent to the original typing judgment. For a separate symbolic word-RAM realization, we prove a quartic worst-case work bound. We measure family representation sizes and comparison storage in independent OCaml prototypes on synthetic checking judgments.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-15T02:39:37Z
Jason Z. S. Hu
arXiv categories: cs.PL, math.LO

In previous works on normalization by evaluation (NbE) with an untyped domain model, explicit substitutions are a major decision choice, which, in retrospect, is taken to simplify subsequent semantic proofs. This choice hence is taken for a purely technical reason. In addition, there is no obvious lemma to test the completeness of the definition or the laws for explicit substitutions. In this technical report, we investigate NbE in a typical setting, i.e. defining substitutions as operations. We show that this setting brings simplifications in proving syntactic properties and soundness of NbE, though complications are introduced in the completeness proof of NbE.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-16T06:58:21Z
Jean-Philippe Bernardy, Andreas Abel
arXiv categories: cs.PL

We study modalities in the linear lambda calculus, by interpreting them as endofunctors in monoidal closed categories. We support functors that do not distribute over products, including (co)monads. We also support arbitrary natural transformations as conversion between modalities. We provide a generic categorical semantics, which we then specialise to a sound and complete resource semantics. We use this resource semantics to derive normalisation by evaluation. Along the way, we describe several applications of such models. This work aims at providing a foundation for future programming languages with modalities. The paper is backed by a mechanisation in Agda.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-16T12:16:49Z
Shuwei Wang
arXiv categories: math.LO

We record some interesting technical caveats found when using universal formulae to formulate pcas -- namely, that there are different ways to extract a (partial) function from a definable collection of pairs, and these choices have an impact on formula complexity.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-18T07:48:17Z
Pavel Sokolov, Alexander Kuklev
arXiv categories: math.LO, cs.LO

We present a dependently typed pure type system that contains a circular axiom $s : s$ for a certain sort $s$ and is nonetheless strongly normalizing. Girard's paradox is avoided because our sorts are not closed under a $\Pi$-former: function types are placed in sorts according to their rank. Turns out that this system has a unique set of characteristics: it has similar normalization behaviour as STLC (so complexity of normalization is TOWER-complete) while at the same time allowing non-uniform representation of arbitrary elementary recursive functions; furthermore, it has a nontrivial set-theoretical model in ZF+GCH and allows to carry out nontrivial proof developments. Base normalization proof is surprisingly simple (modulo general metatheoretical properties of pure type systems) and has been fully formalized in vanilla Rocq (formerly Coq) without additional axioms.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-12T07:43:43Z
Jeremy Tan
arXiv categories: math.NT, cs.LO

We describe Redhill, a Lean formalisation of the major results in H\"olzl, Kleine and Stephan's "Improved Lower Bounds for Strong $n$-Conjectures" (arXiv:2409.13439). Design decisions regarding types and data structures are justified as enabling canonical versions of the paper's claims, and from there the most direct proofs of said claims. The formalisation process also uncovered many errors, omissions and optimisation opportunities in the informal proof, all of which are addressed in the final library. Although Redhill is meant to stand alone, a few lemmas were upstreamed to the primary Lean mathematics library mathlib. We discuss the tension between upstreaming and leaving lemmas in separate libraries. Unlike many other contemporary formalisation projects, Redhill was completed without any assistance from large language models (LLMs). We compare our work with LLM-assisted projects, in particular an extension of arXiv:2409.13439 to $n=4$, aiming to establish design and style guidelines that define good Lean formalisations.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-12T19:40:30Z
Tomas Ortega, Simon Park, Ayush Khaitan, Liam Fowl, Alex Kontorovich, Sanjeev Arora
arXiv categories: cs.AI, cs.LO

General-purpose coding agents use standard shell and file interactions, yet formal theorem-proving agents often rely on specialized, ad-hoc tooling. This makes it difficult to determine which components of theorem-proving agents provide benchmark gains: an improved base model, a specialized harness, a specific tool, or a combination of any of them. We introduce mini-Lean-agent, a deliberately minimal agent for Lean tasks whose only model-visible tool is bash. The model must use bash to inspect and edit the repository, search local libraries, invoke Lean, and manage its own intermediate work, while a separate trusted evaluator verifies the final artifact. We compare mini-Lean-agent against AxProverBase and Numina-Lean-Agent on the Putnam 2025 benchmark. Experiments with Gemini 3.8 Flash as the base model show that mini-Lean-agent solves 7/12 problems at \$2 per problem limit, compared with AxProverBase's 4/12. With Astra as the base model, mini-Lean-agent solves 12/12 problems at an average cost of \$1.28 per problem. This suggests that a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks. Our results motivate using mini-Lean-agent as a standard baseline when evaluating theorem-proving infrastructure.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-12T20:14:51Z
Martin Amster, One An, Holly Baker, Fernanda Graciolli, Simon Henniger, Nada Amin
arXiv categories: cs.CL, cs.AI, cs.PL

Formal verification proves that a program satisfies its specification, but says nothing about whether the specification captures what the author meant. As LLMs increasingly write both code and specifications, a gap between the author's natural-language requirement and the specification becomes a live risk. A machine-checked proof of a property narrower than the one requested is worthless but passes every check. Closing this gap is solving the spec formalization problem: given a natural-language requirement, produce a formal artifact whose meaning matches it. To measure the gap, we curate an end-to-end benchmark for spec formalization spanning four formal languages: Dafny contracts and Lean 4, Isabelle and Rocq theorem statements. Each of its 3,234 rows pairs a natural-language requirement with a formal artifact and a label established by execution, by proof, or by the benchmark it is drawn from. A third of the rows are meaning-preserving rewrites of the artifact that keep the faithful label, so a judge cannot score by detecting that a row was edited. We introduce claimcheck, a tool that detects incorrect formalizations: the formal artifact is translated back into plain English by a model that never sees the requirement, and a separate model, the judge, decides whether the informalization and the requirement express the same guarantee. On all four languages it gains 8.2 to 9.8 points of macro recall over a single call shown the requirement and the artifact, and 4.2 to 6.0 over that call handed the same list of meaning-preserving rewrites. Showing the judge the artifact as well costs 1.4 to 4.5 points. Across four judges that also see the artifact, the gain shrinks as the judge gets stronger, to within a point of the informed single call for the strongest.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-12T23:31:04Z
Piyush Jha, Cruise Song, Zhengyu Li, Yatharth Sejpal
arXiv categories: cs.LO, cs.AI

Financial Artificial Intelligence (AI) governance and model risk management (MRM) emphasize independent validation, transparency, and effective challenge of AI-generated computations. Text-to-SQL translates natural-language questions into Structured Query Language (SQL), but queries that agree on one database can still express different computations. We present VeriPIE, a neurosymbolic framework combining language-model generation with symbolic checks. It ensembles direct SQL generation with QuerySketch, a structured plan language checked by a backend implemented in Lean, a theorem prover and programming language. Plan diagnostics guide repair before SQL generation, while execution agreement and bounded searches for distinguishing databases inform candidate selection. These checks expose malformed plans and hidden disagreement without proving agreement with the user's intent. In single-run experiments on the complete Spider development set, VeriPIE achieves 72.05% test-suite accuracy (745/1,034), compared with DeepEye's 65.67% (679/1,034). Its two-query shortlist covers 78.43% (811 questions), compared with 74.66% for DIN-SQL (772) and 69.05% for DeepEye (714). On BIRD, VeriPIE reaches 68.90% execution accuracy and 73.73% two-query coverage. The central benefit is reviewable evidence about the generated computation: explicit plan checks, repair diagnostics, and concrete disagreements that support safer financial analysis.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-13T04:23:36Z
Rodney Lafuente-Mercado, Salman Rahman, Jingyan Shen, James Shiffer, Saadia Gabriel, Pavel Izmailov
arXiv categories: cs.LG, cs.AI, cs.LO

AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-14T16:43:10Z
Jiatong Li, Yatao Bian
arXiv categories: cs.CL, cs.CE, cs.PL

Chemical chain-of-thought can contain hallucinated structural and property claims. We thereby introduce MolLean, a process-verifiable language that grounds chemical reasoning in an explicit molecular state. A layered Lean-based kernel checks state transitions and assertions over molecular readouts, from primitive graph edits to compound transformations. Meanwhile, a typed witness protocol separates native structural checks from externally supplied measurements. We further introduce MolLean-MCP, a stateful tool interface that exposes these transitions, checks, and readouts during generation: the model receives feedback to decide its next action, and rejected actions leave the state unchanged. MolLean supports one-pass trace execution, whole-trace refinement, and interactive reasoning through MolLean-MCP. We evaluate these three modes with direct chain-of-thought on 8,800 matched examples across 12 tasks spanning molecular generation, editing, optimization, and reactions. With Qwen3.6-27B, whole-trace refinement outperforms direct chain-of-thought on all 12 tasks. MolLean-MCP complements whole-trace refinement with stepwise verification feedback, reaching better performance in reaction tasks. Together, these results highlight an executable foundation for chemical reasoning, in which explicit chemical commitments can be checked and revised rather than remaining solely in free-form explanations.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-14T17:54:48Z
Anna Mei, Michael R. Douglas
arXiv categories: cs.LO, cs.AI

We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-15T20:15:50Z
Madhuparna Das, Soumya Banerjee
arXiv categories: math.LO

In this article, we propose a benchmark to quantify the non-triviality and novelty of machine-generated mathematical proofs compared to existing literature. Our core methodology uses a probabilistic measure to evaluate the non-triviality of the underlying mathematical arguments in comparison to the current \texttt{MATHLIB} library. Finally, we apply this benchmark to the recent proof generated by Claude on the complex zeros of the Riemann zeta function to test for non-trivial steps.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-17T13:43:05Z
Ali Ansari, Farhana Ferdousi Liza
arXiv categories: cs.AI, cs.CL, cs.LO

Evaluating the reasoning of AI systems often relies on human-written reasoning chains as references, yet the logical support for their individual steps is rarely verified. Although prior neuro-symbolic approaches have formalized and checked reasoning, their reported evaluations do not systematically assess whether step conclusions in human-written reference derivations are entailed by their cited premise sets or investigate the sources of failures in those references. To address these limitations, we present a novel reference-centred assessment method for human-written derivations that combines entailment checking against cited premise sets, full-premise rechecking, and failure attribution to examine the reliability of these derivations and their formal representations. We evaluate it on P-FOLIO, using a large language model (LLM) to translate step conclusions into first-order logic (FOL) and the Z3 SMT solver to check entailment. Of 386 derivations examined, 202 (52.3%) meet all our checking criteria, meaning that every translated step is entailed by its stated support and the required target is established under the available FOL representations. Among 230 steps not entailed by their stated support, 191 become entailed when checked against the complete original premises, indicating that most initial failures reflect incomplete or mismatched support rather than unsupported claims. Manual analysis of the remaining 39 cases identifies 21 human reasoning errors, 11 FOL translation errors, and 7 dataset annotation errors. A separate manual audit of 50 randomly sampled steps that passed the entailment checks found 46 faithful FOL translations (92%). These findings suggest that disagreement with a human-written reasoning reference may originate in the reference or its formal representation rather than in the AI system being evaluated.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-18T04:58:11Z
Yi Yu, Yu-Hsuan Wu, Guang Lin, Yuhui Zhang, Yuxiang Peng
arXiv categories: cs.PL

Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but whole-statement logically equivalent pairs, while Mathesis LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either set as equivalent.

arXiv abstract · PDF

Lean and Autoformalization · primary corpus · published 2026-10-18T15:59:25Z
Safal Raman Aryal
arXiv categories: math.LO, cs.LO

I present a method for analyzing large collections of formally verified mathematical proofs (e.g. OpenAI's) grounded in some historical and philosophical musings on mathematics in the age of AI. Many of the quantities involved, such as the size of a proof term or the number of redundant steps, are already computed by work on improving automated provers, where they serve as targets. My aim is to turn them into measurements of proofs themselves: compared against a reference library and against each proof's own cut-free form, checked against theorems they must obey, and controlled for how the proofs were compiled. With these instruments, I measure how (much) machine-generated mathematics diverges from human mathematics, and find that AI-written formal proofs realize far less of the logical compression available to them than human mathematicians do (31% against 73% in mathlib, and 55% against 86% on proofs that call no automation). These figures are broadly in line with reports from those who build provers and proof-improvement tools that AI-written proofs are often longer than they need to be.

arXiv abstract · PDF

Program Verification · primary corpus · published 2026-10-12T05:43:56Z
Fatemeh Bahrami, Seyed-Hosein Attarzadeh-Niaki
arXiv categories: cs.AR, cs.AI, cs.LO, cs.SE

Embedded platforms increasingly host safety-related streaming functions next to less critical ones. Whether a safety architecture pattern, such as a doer/checker pair, protects a function depends on the cores that run its components. Their schedule must meet the throughput requirement, and mixing safety integrity levels (SILs) on one core raises development cost. This report presents SafeDSE, a design space exploration framework for synchronous dataflow applications. One declarative constraint model decides the pattern of each actor, the placement that the fault model requires, the static-order schedule, and the platform, and prices SIL promotion. Guards activate the chosen patterns in a fixed graph that holds all of them, and node potentials encode throughput. An independent verifier re-checks every solution, and a generator turns its checks into evidence of a safety argument in Goal Structuring Notation. On 9 benchmark instances under period bounds, no rule that fixes patterns before mapping was both always feasible and never more expensive under conservative pricing, while joint exploration was. In the generated arguments, 49 to 62% of the leaves cite verifier checks; the rest are claims a mapping cannot discharge. Optimality within the model was proven for all synthetic graphs with up to 16 actors. This extended version adds the full model, the verifier and generator in detail, the complete catalog and parameters, and a proof of the potential characterization. It also reports every experiment per instance, a mutation analysis of the verifier, and the negative results of the development.

arXiv abstract · PDF

Program Verification · primary corpus · published 2026-10-13T04:36:21Z
Yuanjie (Collin) Ren, Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi, Mingsheng Ying
arXiv categories: quant-ph, cs.PL

Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present QEDIA, a framework for verifying quantum programs with classical variables in Lean 4. At its foundation is an open library that formalizes the quantum Hoare logic QHL+ across all these levels and proves the logic sound for both partial and total correctness. We construct the library and the program proofs, under human supervision, using an LLM-based prover agent, whose general-purpose core we extend for quantum program verification. We illustrate QEDIA with verified programs including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Hamiltonian simulation.

arXiv abstract · PDF

Program Verification · primary corpus · published 2026-10-14T08:17:57Z
Seulkee Baek
arXiv categories: cs.PL, cs.LO

Much of Ethereum's most consequential code is immutable bytecode: old output of unverified compilers, and protocol logic run as contract code. We show that such bytecode can be verified as it is, without trusting what produced it, without simplifying the machine it runs on, and with no axioms beyond Lean's own. Blanc, a Lean 4 verification stack, reads fixed runtime bytes via kernel-checked certificates and states every theorem against Jaune, an executable semantics of the EVM and block processing that passes all 34,205 blockchain-test cases of Ethereum's fixture release v20.0.2 that involve only forks that have governed mainnet since May 2025. Eight artifacts, deployed from 2017 to 2026, come from seven compiler versions and an assembler. For the EIP-7002 contract, we prove that the end-of-block call to it, whose failure would invalidate the block, succeeds whatever its storage holds, and that each block's withdrawal requests are exactly the oldest pending submissions; mainnet met these theorems' starting premises when Prague began. For a Uniswap V2 pair, we prove that after any valid history whose hashed slots stay apart, from any checkpoint representing its Solidity model's state, the storage represents that model replayed over exactly the committed calls, a balanced liquidity ledger stays balanced, and, under a premise on token answers, geometric-mean reserves per share fall only through the protocol fee. Exact gas makes liveness provable: a tracked WETH9 holder without code can withdraw by a transaction whose gas has a closed form, matching all 3,748 comparable mainnet receipts of its shape in 30,000 blocks. On Curve pool bytes compiled with the lock bug exploited in 2023, Jaune executes such a reentrancy from deployment; for bytes from a fixed compiler, we prove the lock excludes it. AI agents wrote the proofs in fifteen days under one author's direction, atop an existing stack.

arXiv abstract · PDF

Program Verification · cs.SE candidate · published 2026-10-16T10:08:57Z
Rohith Kumar Shanmuganathan, Cedric Richter, Heike Wehrheim
arXiv categories: cs.SE

Formal verification of real-world projects requires substantial manual effort, from specifying correctness properties to constructing the infrastructure needed to check them. We envision verification agents that assist developers throughout this process. Among the many tasks involved, one stands out as both foundational and amenable to automation: proof-harness engineering. A proof harness defines an isolated verification environment for a program unit, such as a function or module, by providing symbolic inputs, initialization code, and models of its dependencies. Today, proof-harness engineering remains largely a manual task performed by verification engineers. To explore the potential of coding agents for this task, we propose an agentic proof-harness engineer that automatically constructs verifier-ready harnesses from a software project and a designated verification target. We combine the agent with formal soundness and precision guards to validate generated abstractions and guide their refinement. We evaluate the feasibility of our approach in an exploratory case study on curl and libuv, using three historical assertion violations already embedded in the source code as verification properties. Our results show that the agent successfully constructs proof harnesses that enable CBMC to detect all three violations. We further demonstrate the potential for reusing these harnesses with other verification tools.

arXiv abstract · PDF

Program Verification · primary corpus · published 2026-10-16T15:20:04Z
Abigail Pribisova, Yao Li, Cezar-Constantin Andrici, Catalin Hritcu, Kenji Maillard, Exequiel Rivas
arXiv categories: cs.PL

Monads of weakest precondition predicate transformers are the foundation of several verification frameworks for monadic programs. For specifying monadic computations with nondeterminism and nontermination, in addition to weakest preconditions, we introduce the first strongest postcondition monads covering all combinations of angelic or demonic nondeterminism and partial or total interpretations of nontermination. For extending these base strongest postcondition monads with side effects such as mutable state, monad transformers do not yield the expected monads, so we instead generalize the base monads to arrows and use arrow transformers. We give a taxonomy of weakest precondition and strongest postcondition monads, for the base monads and for their versions with state, and show that the known relationships between under- and over-approximate triples based on predicate transformers already hold at the level of the predicate transformers themselves. We use the predicate transformer monads to define under- and over-approximate triples and, where possible, Dijkstra monads. Finally, we relate these two specification styles.

arXiv abstract · PDF

Program Verification · primary corpus · published 2026-10-17T08:16:10Z
Archibald Browne, Eugene Lee, Cristopher Salvi
arXiv categories: cs.PL

Modern statistical model development begins with a high-level specification in an automatic differentiation framework such as PyTorch, JAX, or TensorFlow, which is then lowered to a target backend by a compiler or implemented manually by a research engineer. In this paper, we study whether frontier language models can correctly perform the latter task by generating GPU kernels from high-level benchmark specifications. We introduce a framework in which a language-model agent uses Velvet, a program verifier for imperative programs embedded in Lean, to prove semantic equivalence between a high-level specification and a generated CUDA kernel under an explicit set of assumptions. It also asks the LLM to prove thread safety and data race freedom of the generated kernel in VerCors, a deductive verifier for parallel code. Our main contribution to the formal verification of LLM- generated GPU kernels is showing that a combination of Lean automation and language-model-guided proof construction can verify a broad set of basic neural- network building blocks over floating-point values, allowing LLMs to implement semantically correct and safe kernels. In our framework, floating-point verifications never rely on compiled code and are always checked via the Lean kernel.

arXiv abstract · PDF

Compilation and Code Optimization · primary corpus · published 2026-10-13T09:44:28Z
Erc\"ument Kaya, Ekin Devim \c{S}ahinkaya, Minh Chung, Martin Schulz
arXiv categories: cs.PL

Quantum computing introduces specialized software stacks and programming interfaces that are often tightly coupled to specific ecosystems and hardware backends, limiting interoperability and software reuse. For HPCQC application developers, this complicates the integration of quantum accelerators into existing applications. Existing quantum frameworks also use ecosystem-specific circuit representations and compilation pipelines, hindering integration with established heterogeneous compiler infrastructures. We propose OpenMQPI, an MLIR-based OpenMP extension for quantum programming that leverages OpenMP's standardized target offloading infrastructure to integrate quantum resources into HPC applications. OpenMQPI introduces QPIR, a lightweight MLIR dialect for representing quantum circuits within OpenMP target regions, and a compiler pipeline that performs quantum-specific optimizations and lowers circuits to executables compatible with OpenMP offloading. At runtime, an MQSS plugin enables the generated executable to offload quantum circuits to quantum hardware through the OpenMP target offloading model. We evaluate OpenMQPI using the VQE, QFT, and Deutsch-Jozsa algorithms with 5, 10, 15, and 20 qubits, comparing execution times against Qiskit and CUDA Quantum. OpenMQPI achieves the lowest average VQE execution time across all tested qubit configurations. At 20 qubits, it requires 5.18 s, compared with 5.83 s for Qiskit and 7.39 s for CUDA Quantum. For QFT and Deutsch-Jozsa, OpenMQPI achieves execution times comparable to Qiskit and lower than those of CUDA Quantum.

arXiv abstract · PDF

Compilation and Code Optimization · primary corpus · published 2026-10-13T11:10:04Z
Alexander Stromberger, Christoph Hochrainer, Valentin W\"ustholz, Maria Christakis
arXiv categories: cs.SE, cs.PL

Smart contracts compiled to the Ethereum Virtual Machine (EVM) can manage high-value assets and are difficult to patch after deployment. Compiler miscompilations are therefore especially dangerous: compilation succeeds, but the generated bytecode does not preserve the semantics of the source program. Existing smart-contract compiler fuzzers either focus on robustness failures or rely on differential oracles that compare compiler configurations. We present Soliduzz, an approach for finding miscompilations in EVM smart-contract compilers using assertion-driven equivalence oracles. Soliduzz uses product programs to encode semantic equivalence as executable assertions. The key shift is to compile these self-checking programs and let off-the-shelf fuzzers and symbolic execution engines explore the resulting bytecode for assertion violations, without requiring compiler-specific support from the analyzer. Soliduzz instantiates this idea with two complementary families of metamorphic transformations. The first starts from equivalent expressions and lifts them into smart-contract code that deliberately exercises EVM-specific features such as storage, data locations, control flow, contract interactions, and inline assembly. The second generalizes Equivalence Modulo Inputs (EMI) from fixed concrete inputs to symbolic input spaces. Our symbolic EMI records coverage in the original computation and uses it to guard mutations in the transformed computation. Together, these transformations produce product programs that assert that paired computations yield the same outputs. We evaluate Soliduzz on three EVM smart-contract compilers (solc, solx, and vyper) using several analysis tools. Overall, Soliduzz exposes 29 bugs. Of these, 24 are compiler bugs: 6 miscompilations, 17 internal compiler errors, and 1 hang. The remaining 5 are bugs in the analysis tools.

arXiv abstract · PDF

Compilation and Code Optimization · primary corpus · published 2026-10-13T21:56:45Z
Casper L. Christensen, Kyle J. Ray, Dmitry Manning-Coe, Adam Shai, Paul Riechers
arXiv categories: cs.LG, cs.PL

When writing code, the same computation can be expressed in different programming languages and through different implementation strategies. We show that the activations of LLMs capture this shared structure in reusable and composable abstract representations when they generate code. These representations emerge in the middle layers, are reusable across programming languages, and afford the model an impressive amount of generalization ability when generating code under various interventions. Using activation steering, we show that function, programming language, and implementation strategy can be independently manipulated. The independent interventions on language and function can be flexibly composed to control code generation, even in cases when the prompt contains no information about language and function. We additionally find that finetuning on examples of arbitrarily defined functions in one programming language transfers to other languages, consistent with the models reusing abstract features of code generation that are shared across different examples. Finally, to study how such abstract representations come to be, we implement a minimal model of shared, reusable, and composable structure in a synthetic setting, and show that transformers trained on such data learn representations that reuse these parts flexibly across contexts.

arXiv abstract · PDF

Compilation and Code Optimization · cs.SE candidate · published 2026-10-15T18:22:13Z
Qinrun Dai, Ruitong Liu, Chien-Wei Huang, Guanhong Tao, Guannan Wei, Yueqi Chen
arXiv categories: cs.SE

Modernizing mature scientific software from Fortran to Python can improve accessibility and integration with modern computing tools, but manual rewriting is expensive. Large language models (LLMs) make translation more practical, yet generated code can pass regression tests while violating source-language semantics, and contextual corrections may not persist across subsequent translations. We present ForTress, which solidifies recurring LLM translation decisions into guarded executable rules for deterministic reuse and provides semantic assurance for a non-trivial subset of these rules. Its LLM-assisted auditing process expresses universally quantified preservation obligations over mechanized Fortran and Python semantics in Lean. Human experts review semantic fidelity and correspondence with production rules, and Lean's kernel checks proofs and refutations under explicit assumptions. These audit records expose the conditions either supporting correctness or identifying failure cases. We evaluate ForTress on 17 benchmarks from 15 scientific software spanning diverse domains. The translated programs achieve bitwise-identical with native Fortran on all evaluated tests under the recorded execution and initialization configurations. Against these software, ForTress accumulates 193 executable rules and 188 audit records, of which 121 have checked soundness proofs, including 31 established after counterexample-guided refinement. Cross-software reuse exceeds 90% for 14 of the 15 software. Even with additional assurance and determinism, the LLM usage cost is 44.2% lower than direct LLM translation.

arXiv abstract · PDF

Compilation and Code Optimization · primary corpus · published 2026-10-16T07:22:54Z
Zhiqiang Yuan, Chong Wang, Zhenhao Zhou, Junwei Liu, Xin Peng
arXiv categories: cs.AI, cs.PL

Rust is increasingly adopted as a memory-safe successor to C, and transpilers such as \crust{} can migrate entire C projects while preserving their behavior. Preserving behavior, however, does not guarantee preserving performance. We study this gap on 20 real-world C projects and their \crust{} translations. On the eight projects used for analysis, the translated Rust is more than 3\% slower than the original C on 12 of 19 operations, by up to 62.2\%. By comparing execution-cost profiles, optimized LLVM IR, and compiler optimization remarks across each C--Rust pair, we trace these slowdowns to nine recurring performance issues, spanning residual runtime work, missed compiler optimizations, and C-style source patterns, and derive an optimization direction for each. We then present \ourtool{}, an LLM-based approach that encodes these issues as reusable optimization rules to recover the performance of translated Rust. \ourtool{} profiles each project to locate hot functions and matches them against rule-specific patterns. The LLM then checks each rule's rewrite preconditions against the project context before rewriting, and a rewrite is kept only if it passes both functional and performance validation. On 41 operations from twelve held-out projects, \ourtool{} preserves C outputs on all tested workloads and speeds up 40 operations over the \crust{} translations, 18 of which end up faster than the original C. It outperforms the general-purpose coding agent \codex{} on 31 of the 37 operations where both preserve C outputs, and outperforms its own variant without rule guidance on 34 of the 41 operations.

arXiv abstract · PDF

Compilation and Code Optimization · primary corpus · published 2026-10-17T19:33:01Z
Wesley Lu, Runzhou Liu, Hongru Du, Xinyao Yi
arXiv categories: cs.AI, cs.PL, cs.SE

Existing evaluations of LLM-based code optimization primarily measure end-to-end speedup, obscuring whether a model actually performs the intended optimization. For compiled languages, this is especially problematic: observed gains may reflect transformations already recoverable by modern optimizing compilers rather than optimization behavior attributable to the model itself. We present PatternBench, a benchmark for studying compiler-transcendent optimization, i.e., performance improvements that remain after aggressive compiler optimization. PatternBench targets residual optimization opportunities across seven classes of transformations and pairs runtime evaluation with an AST-based optimization faithfulness analysis that verifies whether the intended optimization is realized in the generated program. Experiments with frontier, open-weight, and fine-tuned models show that runtime speedup alone provides an incomplete account of optimization capability. Optimization faithfulness is strongly associated with realized speedup, and fine-tuning improves both faithfulness and optimization effectiveness. These results suggest that evaluation of LLM-based code optimization should measure not only performance outcomes, but also whether the target transformation was successfully executed.

arXiv abstract · PDF

Compilation and Code Optimization · primary corpus · published 2026-10-18T04:46:51Z
Annabelle Sujun Tang, Rohan Mahapatra, Christopher Priebe, Hanyang Xu, Manya Ghobadi, Christopher Rossbach, Hadi Esmaeilzadeh
arXiv categories: cs.LG, cs.DC, cs.PL

As LLM adoption surges, scaling model serving requires unlocking stranded GPU capacity alongside deploying more GPUs. Speculative decoding brings two models into the serving process: a small draft model proposes tokens that a larger target model verifies. Yet compiling these models individually leaves their shared execution outside the compiler's optimization boundary. We introduce CONJUGATE COMPILATION, which reframes speculative decoding as a cross-model compilation problem and jointly optimizes the draft and target models within their shared execution rather than treating each in isolation. Our key insight is that cross-model compilation should be informed by the measured performance of the co-located shared execution it produces: an optimization that improves a kernel in isolation need not improve the models when they execute together. To expand cross-model opportunities, we devise operand layouts that interleave blocks from both models within common tiles, co-locating GEMM and non-GEMM work while preserving their mathematics. We realize CONJUGATE COMPILATION through a self-improving agentic search system in which an LLM edits cross-model optimization plans using the compiler and GPU execution as its environment. Each proposed plan is compiled and evaluated through its co-located shared execution, whose measured score, together with kernel-level verdicts and compiler feedback, informs subsequent proposals, while Monte Carlo tree search accumulates rewards to guide exploration. Across six single-GPU speculative-decoding configurations on NVIDIA B300 and RTX 5090 GPUs, CONJUGATE COMPILATION achieves a geometric-mean per-round speedup of 1.37x over conventional execution. Interleaved kernels raise this speedup to 1.45x, reaching 1.59x in the best case. CONJUGATE COMPILATION also improves GPU utilization on average by 1.46x on RTX 5090 and 1.50x on B300.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-12T14:34:48Z
Zhiqing Zhong, Mingyu Chen, Aoyang Fang, Yuzhong Zhang, Haoye Tian, Lionel Briand, Boxi Yu, Pinjia He
arXiv categories: cs.CL, cs.SE

As coding agents become more capable, tests remain the primary evidence for judging whether their code is correct. Yet passing available tests does not establish that an implementation satisfies its natural language specification. Reliable validation requires checks that faithfully capture the specification and scenarios that thoroughly exercise the code, but current benchmarks provide limited insight into whether agents can construct such evidence themselves. We introduce SpecGuardBench, a benchmark of 291 tasks from 13 real-world repositories, covering 8 types of verification logic such as functional postconditions and interaction protocols. Given a natural language specification, repository context, and a reference implementation, an agent constructs a validation harness comprising executable checks and test scenarios. The checks should reject implementations that violate the specification while accepting those that satisfy it, and the scenarios should thoroughly exercise the code. Across four proprietary and open-weight coding agents, none constructs a harness scored as faithful on the benchmark's implementations for more than 63% of the tasks. The bottleneck lies less in exploring test scenarios than in constructing checks that faithfully reflect the specification. Specifically, the agents show a clear tendency to write checks that mirror the reference implementation rather than the specification, and therefore reject implementations that the specification permits.

arXiv abstract · PDF

LLM Agents and Software Reliability · primary corpus · published 2026-10-12T16:13:31Z
Ashwani Anand, Ivi Chatzi, Ritam Raha, Anne-Kathrin Schmuck
arXiv categories: cs.CL, cs.LG, cs.LO

Tool-using LLM agents are increasingly used to automate workflows governed by procedural manuals, such as company rules for booking travel or procuring hardware. These manuals are written in natural language for humans and describe general requirements over such complex workflows. Ensuring compliance of LLM agents with these manuals is difficult, and state-of-the-art techniques use either LLM judges or manually written rules to forbid problematic tool-calls locally at runtime. This is insufficient because (i) only blocking tool calls keeps the agent clueless about how to make correct progress towards fulfilling its task, and (ii) can lead to overly conservative behavior of the agent, as tool calls might only be problematic in certain contexts. To overcome these challenges, we introduce MENTOR, which (i) additionally provides guidance for the agent to make procedural-compliant progress on the task, and (ii) ensures that this compliance is context-aware. We achieve these goals by building a novel history-dependent runtime shield that is obtained from the procedural manual via a multi-step autoformalization pipeline. At its core, MENTOR utilizes a game-based technique to ensure robustness against runtime uncertainty without over-resticting agents' behavior. This yields a formally assisted framework for procedural shielding of LLM agents that improves compliance well beyond existing methods. In particular, MENTOR lifts the compliance of shielded light-weight open-source LLMs above that of non-shielded proprietary models. Since a shield is synthesized once per manual and then serves every task, a MENTOR-shielded agent becomes a viable choice for repeatedly executed workflows, potentially reducing deployment costs when the offline construction cost is amortized over repeated tasks.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-13T17:12:59Z
Giovanni Pio Delvecchio, Stefano Fantazzini, Giacomo Frisoni, Gianluca Moro, Lorenzo Bacchiani, Mario Bravetti, Thomas Troels Hildebrandt
arXiv categories: cs.SE, cs.AI

Large language models increasingly generate Solidity smart contracts that, once deployed, can never be patched, making a single latent fault permanent and exploitable. Yet current evaluations mostly ask only whether generated code compiles. We introduce SolBehave, a benchmark for evaluating the correctness of model-generated contracts at scale, moving beyond ad hoc unit tests. Across 250 real, reproducible Ethereum contracts, we apply three complementary tests of behavioural fidelity: differential fuzzing, historical-transaction replay, and, as our core contribution, synthetic-transaction replay guided by a Dynamic Condition Response (DCR) graph that enumerates the space of legitimate function-call sequences. Differential fuzzing compares each generated function with the original on automatically generated inputs; historical replay compares the whole contract on the transactions it actually received on-chain; DCR-guided replay compares it on sequences of calls that follow its intended usage, including orderings that never occurred on-chain. We evaluate seven state-of-the-art open-weight models after one round of automated repair. Compilation success ranges from 26.4% to 92.7%, but under differential fuzzing only 31.4% of all generated function bodies that compile, pooled over models and samples, are equivalent to the original. Divergence at the contract level is the norm rather than the exception: for six of the seven models, between 13% and 31% of the generated contracts that compile diverge from the original under historical replay, and between 13% and 44% under DCR-guided replay; only Gemma-4-31B stays below 3% on both. Compilation is therefore a necessary condition for correctness and far from a sufficient one.

arXiv abstract · PDF

LLM Agents and Software Reliability · primary corpus · published 2026-10-14T02:02:03Z
Hang Lin
arXiv categories: cs.PL, cs.AI

We introduce FormCraft, a framework for representing acquired operations as first-class capabilities that can be recursively composed, directly invoked, and selectively retained in a persistent library through domain-specific verification. The framework separates capability well-formedness and public callability from later admission to persistent storage while preserving formation provenance and operational identity. We formalize recursive compositional closure over a uniform capability space and show that formed composites can be reused through the same public interface without re-forming their historical derivation. Experiments across continuous, discrete, propositional, and sequence domains demonstrate instance-independent reuse, independent checking, persistent acquisition, and reduced reuse-time search work under first-class exposure.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-15T05:42:04Z
Yifeng He, Yanjun Wang, Siwei Cui, Aritra Sengupta, Murali Krishna Ramanathan
arXiv categories: cs.SE, cs.AI

Software agents answer behavioral questions about code, such as whether a patch passes tests or which lines caused a failure. These tasks require repository-wide evidence, yet most scaffolds leave intermediate findings in free-form trajectories, making them hard to reuse and easy to disconnect from final answers. We present Agentic Interpretation (AgInt), a framework for harness-governed evidence construction. The model proposes typed records, while a deterministic harness admits, grades, and persists them, reports unresolved requirements, and licenses answers under task-specific rules. The resulting certificate gives the model persistent external state and leaves an auditable decision record. Formally, append-only certificate states form a grounding lattice ordered by record inclusion, where each admitted record extends the state by union. We evaluate AgInt with four models on SWE-bench-Live and DeepSWE for patch acceptance and Defects4J and GitBug-Java for fault localization. AgInt outperforms the plain agent and Agentic Code Reasoning on all reported patch-acceptance metrics and ranks responsible lines higher while inspecting fewer irrelevant lines in fault localization. For GLM-5, reject-class F1 rises from 0.256 to 0.543 on SWE-bench-Live, All@1 rises from 0.140 to 0.400 on Defects4J, and wasted inspected lines fall from 31.5 to 11.7 on GitBug-Java. A matched-template control separates the mechanism: the persistent scaffold drives most fault-localization gains, while the certificate body and gate govern patch-acceptance calibration. With execution licensed, AgInt produces harness-reproduced witnesses for 293 of 475 null-dereference candidates versus 253 for a matched shell agent, and 62 of 117 resource-leak candidates versus 58. Across reported efficiency measurements, it uses 35% fewer executions and reduces cost per candidate by 59%.

arXiv abstract · PDF

LLM Agents and Software Reliability · primary corpus · published 2026-10-15T15:24:46Z
Ali Mohammadi Shanghooshabad (JPMorgan Chase & Co.)
arXiv categories: cs.AI, cs.DB, cs.PL

Organizations increasingly encode operational procedures as multi-step agent skills, here called Agent Operating Procedures (AOPs), that must be traceable, auditable, reproducible, access-controlled, and bounded in time and cost, requirements that regulated sectors make mandatory. Yet AOPs are typically kept as coarse-grained files, in which steps bundle actions, copied procedures drift apart, any step may reach any tool, and refactoring goes unchecked. We present Functional Agent Operating Procedures (FAOP), a formal theory that brings database-grade discipline to AI agent workflows. FAOP recasts each workflow as a typed function over scoped state and subjects an entire library to four progressive normal forms: Decomposed (FNF-1) splits a workflow into atomic steps, Typed (FNF-2) makes its data flow explicit and type-checked, Factored (FNF-3) gives each shared procedure a single canonical definition so a change propagates instead of drifting, and Scoped (FNF-4) confines every step to least-privilege tool access. Once normalized, every atomic step is a separate entity with a declared contract and can be type-checked, scope-confined, bounded, tested, traced, and audited on its own. A FAOP algebra of provably sound equalities turns refactoring and parallelization into compiler rewrites; orthogonal extensions add verified termination (+V), optimization (+O), and time and cost bounds (+B); and an architectural-level classifier (0-3) determines whether a workflow needs AI at all. Together, these make integrity, isolation, typing, termination, cost, and optimization compile-time concerns across the whole library, not runtime hopes. We implement the theory in SkillBase, an AOP management system (what PostgreSQL is to data, SkillBase is to AOPs), together with a separate executor that enforces these guarantees at run time. A worked financial workflow illustrates the approach end to end.

arXiv abstract · PDF

LLM Agents and Software Reliability · primary corpus · published 2026-10-15T15:41:56Z
Asif Mohammed Saad, Ahsanul Ameen Sabit, Jonah Brandenburgh, Jiyuan Wang, Qian Zhang, Soneya Binta Hossain
arXiv categories: cs.SE, cs.PL

Quantum software relies on compilers, intermediate representations, and execution frameworks that transform programs before execution. Faults in these components can change the behavior of otherwise correct quantum programs. Yet quantum testing techniques are often evaluated using mutation-generated faults and curated bug benchmarks. We investigate how well the faults represented by these artifacts reflect those encountered in modern quantum software. We audit four quantum mutation-testing tools and three curated bug benchmarks, and collect 410 verified bugs from ten quantum software repositories over two years. We classify faults from all three sources into a common taxonomy of 56 bug families and compare their representation across mutation operators, curated benchmarks, and recent real-world bugs. The mutation tools support 20 bug families, and curated benchmarks add 15 more. Yet only 56 of the 410 real-world bugs (13.7%) belong to families represented by either source; the remaining 354 (86.3%) belong to families absent from both. The largest unrepresented families concern compiler transformations (66 bugs), type handling (53), and input validation (47). Unlike local gate or statement changes, these faults often depend on intermediate representations, compiler pipelines, input types, or dependency versions. Existing mutation operators primarily modify circuits and program constructs, whereas many real-world faults arise in the compilers, representations, and framework interfaces that process them. Addressing this gap requires looking beyond circuit-level faults toward testing semantic preservation across compiler transformations, correctness at representation boundaries, and interactions between software components. Our study provides empirical evidence to guide fault models and benchmarks that capture these mechanisms and preserve the contexts needed to reproduce them.

arXiv abstract · PDF

LLM Agents and Software Reliability · primary corpus · published 2026-10-16T07:12:35Z
Jinbao Chen, Zixiang Zhou, Yu Zhang, Yihong Wu
arXiv categories: cs.SE, cs.CR, cs.PL

Static Application Security Testing (SAST) reports flag operations whose safety depends on project-specific context, and maintainers must decide which reports describe real defects. Large language models (LLMs) can interpret this context, but adjudicating a report with them requires the decisive code, which often lies far from the reported line, and a decision basis that program analysis can check. We present VulnSAGE, an adjudication system for SAST reports that connects LLM reasoning to program structure in both directions. Its report-centered slicer recovers the dependencies of the reported operation together with the program structure that explains them, such as the caller object on which a helper acts. CLAIM, an intermediate representation for report judgments, records each model interpretation as a semantic fact that cites the program relations it assumes. Program analysis checks these premises, and the verdict follows from the facts whose premises hold. Both mechanisms share a program graph, which lets the model cite the code it reads and lets the checker query those citations. Statically supported true positives then guide proof-of-concept generation and runtime reproduction. Across 187 labeled reports from four corpora covering five vulnerability families, VulnSAGE rejects 89 of 97 false alarms and retains 85 of 90 real defects. Under a common PoC procedure, 25 of its positive verdicts reproduce at runtime, compared with three for the LLM-based adjudicator LLM4SA. Applied to 45,440 alerts raised by five SAST tools on the 200 most-starred C/C++ projects on GitHub, it reproduces 104 defects at runtime. Maintainers have confirmed 24 of the 26 defects they have responded to, including ten previously unknown defects, nine of which are already fixed.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-16T11:49:37Z
Aniruddha Chattopadhyay, Kanishka Halder, Partha Sarathi Roy
arXiv categories: cs.AI, cs.CL, cs.SE

Tool-augmented language-model agents rely on interface text: tool descriptions, argument schemas, and the candidate tool list shown at inference time. These interfaces often change after deployment even when the underlying tool semantics remain fixed, creating a practical reliability problem for function-calling systems. We study this failure mode as interface drift and evaluate whether a lightweight, training-free repair layer can recover robustness without retraining the base model. Our method, SchemaShield-Lite, combines schema validation, candidate-set retry for missing tool names, and one-shot constrained repair. On Qwen3.5-9B, it raises DICE-300 accuracy from 0.717 to 0.813 and BFCL-200 accuracy from 0.580 to 0.805, recovering 19/22 and 33/45 drift-induced failures with no observed repair harms. Naive retry does not explain the gains. Ablations show that candidate-set drift, especially distractor tools, accounts for most observed damage, while description and schema edits alone are less harmful. The results position validation-and-repair as a practical robustness layer for deployed LLM-agent tool use.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-16T23:50:11Z
Minbo Ma, Honglin Zhang, Bangtao Zhou, Chunguang Yu, Dasheng Ju, Yichen Shen, Fengli Xu, Yong Li
arXiv categories: cs.SE, cs.AI

Advances in reasoning, coding, and tool use enable LLM agents to solve operations research (OR) problems through iterative problem modeling, program construction, and verification. Yet passing self-authored verification does not ensure that the solutions satisfy task constraints and meet optimization quality. This gap can arise from correlated specification errors, where the generated program and its checks share omissions or misinterpretations of task requirements, alongside incomplete verification coverage and ineffective optimization strategies. We propose VERAS, a verification-guided adaptive search harness for reliable OR that uses verification evidence to prioritize feasibility repair, constraint-coverage review, and solution-quality improvement. VERAS combines task-specific solution checkers with a separate verification agent to examine candidate solutions against the task requirements. It uses verification feedback to guide feasibility repair, additional constraint checking, and objective improvement, while candidate acceptance criteria screen revisions for deterioration in output validity or constraint satisfaction. On ORAgentBench, VERAS achieves a 42.99% pass rate, exceeding the reported 35.51% of Codex using the same LLM. Across two industrial-scale OR problems, VERAS reduces inter-datacenter peak bandwidth by 10.34% relative to native Codex and lowers annualized distribution network planning costs by 6.28% compared with expert-designed solutions. Code and evidence are available at https://github.com/holimario/VERAS.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-17T08:14:37Z
Shihao Weng, Longtian Wang, Yang Feng, Mingfei Cheng, Jia Liu, Chao Shen, He Ye, Federica Sarro, Xiaofei Xie
arXiv categories: cs.SE, cs.AI, cs.CR

Software quality has long rested on specifications that state what code must do, and on testing and verification that check that the code does it. Agentic systems change this foundation: they replace parts of their logic, such as choosing the next tool, judging whether an action is allowed, or writing code to run, with calls to a large language model (LLM). The program still relies on what this logic must guarantee, but the model's behavior is not fixed by code, varies across runs, and can be steered by its input. The guarantee must therefore come from the program around each LLM call site, as a contract of pre-conditions, prompt constraints, and post-conditions. We present an empirical study of these contracts in 496 LLM call sites of 40 popular open-source agentic systems (13.4 MLOC, four languages). Using a multi-agent pipeline validated by 17,428 human judgments, we trace where every model output flows, derive an expected contract for each call site without access to its code, and compare it with the contract that the code implements. We find that 48% of LLM outputs reach control flow or execution, and 73% of these never reach a person. Programs enforce 78% of their constraints in code, but in the prompt, 67% of the constraints are only requested from the model. Although 82% of call sites are checked before and after the call, 63% of the expected constraints are unmet and only 5.3% of call sites satisfy their whole contract; ten recurring patterns explain 99% of the gaps. 38 mechanisms behind these gaps trigger at runtime, and a small code fix that enforces the expected constraint stops all 38. Our results show that the presence of checks says little about their adequacy, and we derive implications for agent developers, framework maintainers, and researchers.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-17T10:31:27Z
Hiroyasu Usami, Keisuke Hara, Ayato Tsuboi, Naohiko Matsuda
arXiv categories: cs.SE

Admission rules retain generated programs, whereas selection policies return one candidate per task. We audit how these decisions interact with execution contracts in two separately frozen, disjoint HumanEvalPlus cohorts, each comprising 32 tasks, four samples per task per profile and two served profiles. Under the inline execution contract, a structural-and-self-test screen admits 4-9 expanded-suite nonpasses per 80-107 admissions and excludes 14-43 suite passes per 128 planned attempts. A restricted module-supply condition adds 20 and 14 passing admissions for one profile in the respective cohorts, plus one follow-up nonpass, and reduces the excluded suite passes to 14-23. All fixed first-admitted outcomes and abstentions remain unchanged. In the original pool, the added passes enter already all-passing admitted pools; in the follow-up, four of 24 common sample orders lose one passed task. Selected-subset diagnostics separately address registration-sensitive completion and reference-relative assertion disagreement, accounting for input domains and comparator tolerances. In these high-pass pools, candidate retention and task-level return diverge and are reported separately. Results are conditional on the saved pools, contracts and pinned suites; downstream training effects are unmeasured.

arXiv abstract · PDF

LLM Agents and Software Reliability · cs.SE candidate · published 2026-10-17T14:21:29Z
Martim Monis, Martin Schwaighofer, Nuno Saavedra, Alexandra Mendes, Rene Mayrhofer, Jo\~ao F. Ferreira
arXiv categories: cs.SE

Implicit dependencies, uncontrolled network access, and other build-environment impurities create intransparent software supply chains. Identifying every dependency affecting a build is a difficult task. Functional package management addresses this through reproducible packaging, ensuring software relies exclusively on declared, hermetically isolated inputs. However, creating build recipes remains complex and time-consuming, posing a significant barrier to adoption for developers and maintainers. We present Vibenix, an open-source AI-powered agent that bridges this gap by automatically generating Nix packaging expressions. Vibenix uses a large language model (LLM) to iteratively refine recipes through a rule-guided build-repair feedback loop. On 466 packaging tasks from our new NixBench dataset, Vibenix produced buildable packages in 95.3% of cases using Claude Haiku 4.5, compared with 5.6% for a state-of-the-art LLM-based single-shot packaging tool. Manual validation of 100 packages revealed that 47% of the buildable packages were initially functionally correct; a post-build refinement process based on the evaluator-optimizer pattern increased functional correctness by 35 percentage points. On our new NixBench-Repair dataset of package maintenance tasks, Vibenix achieved an 87.6% success rate. These results demonstrate how unreliable LLMs can generate rigorously defined, complete, auditable dependency trees for real-world software, reducing maintainer burden while providing a trustworthy foundation for secure software distribution.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-12T04:36:33Z
Vera Koponen
arXiv categories: math.LO, cs.LO

A first-order theory $T$ has the {\em finite model property} if every first-order sentence that is implied by $T$ has a finite model. We give a characterization of when a complete $\omega$-categorical theory $T$ has the finite model property. The characterization makes it possible to transfer stability theoretic results in [29] to certain classes of finite structures. This approach also gives information concerning properties that a sequence of finite ``base structures'' of ever larger size must have in order for its random expansions to a larger vocabulary to have a chance to satisfy a convergence law for first-order logic.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-12T21:53:16Z
Jananan Arulseelan
arXiv categories: math.OA, math.LO

We examine various applications of logic to $\mathrm{AW}^*$-algebras, particularly the monotone completeness conjecture. We develop a model theory for $\mathrm{AW}^*$-algebras equipped with a faithful normalized quasitrace. Using this language, we provide a separable coding which allows us to reduce the finite case of the monotone completeness conjecture to monotone sequential completeness of $\mathrm{II}_1$ $\mathrm{AW}^*$-factors. Combining an explicit recursive axiomatization with the completeness theorem for continuous logic, we show that this case of the conjecture, and Kaplansky's problem whether every $\mathrm{AW}^*$-factor of type $\mathrm{II}_1$ is a von Neumann algebra, are each equivalent in ZFC to a $\Pi^0_2$ sentence of arithmetic, so that their answers are the same in every $\omega$-model of ZFC. We also consider real $\mathrm{AW}^*$-algebras. Here the Baer-$*$-ring notion of an abelian projection must be distinguished from commutativity; following the real-operator-algebra terminology we call the former semi-abelian. Handelman's matrix theorem implies that a real $\mathrm{AW}^*$-algebra with no nonzero central semi-abelian projection has $\mathrm{AW}^*$ complexification. We answer a number of other open problems in real $\mathrm{AW}^*$-algebras.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-13T15:15:30Z
Aaron Anderson, Henry Towsner
arXiv categories: math.CO, math.LO, math.ST, stat.TH

We characterize several properties of higher-arity function classes, specifically finite $\VC_k$-dimension, slicewise finite $\VC$-dimension, and finite slicewise Littlestone dimension, in terms of generalizations of Rademacher complexity. These characterizations sets up simple new proofs of several results on finite $\VC_k$-dimension and slicewise finite $\VC$-dimension. These include the preservation of finite $\VC_k$-dimension under taking expectations and uniform law of large numbers statements for both properties. All of these results apply naturally to real-valued function classes as well as boolean-valued classes. We also prove a new adversarial uniform law of large numbers for classes with finite slicewise Littlestone dimension.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-13T17:18:15Z
Zhengqing He, Martin Hils
arXiv categories: math.LO

We continue the study of beautiful pairs of henselian valued fields, initiated in joint work of the second author with Cubides Kovacsics and Ye. As our main result, we show that separably closed non-trivially valued fields of arbitrary imperfection degree admit beautiful pairs which are elementary pairs satisfying certain natural axioms. They satisfy beauty transfer, i.e., saturated models of their theory are again beautiful. The same holds for beautiful pairs associated to natural subclasses of all definable types, most notably for all definable types orthogonal to the value group and for all bounded definable types. This yields strict pro-definability of the space of the definable types from any of these classes, in the theory SCVF of separably closed non-trivially valued fields. We also show a separable analog of a classical result of Keisler's, namely that the first order theory of an infinite separable extension $L/K$ of fields - considered in the pairs language and where the large field $L$ is separably closed, is determined by the theory of the small field $K$ together with the imperfection degree of $L$ over $K$.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-14T07:11:17Z
Jinhe Ye
arXiv categories: math.AG, math.LO

Let $k_0$ be a field of characteristic $0$, and let $C/k_0$ be a smooth geometrically integral curve of positive genus with $C(k_0)=\varnothing$. We prove that the regular inverse Galois problem is solvable over every field existentially closed in the class of $k_0$-fields avoiding $C$, including the curve-excluding fields of Johnson and the author. To this end, we show that for every finite group $G$, there is a parameter variety over $\mathbb Q$ whose function field admits a regular realization of $G$ without adding points to $C$. Finally, we establish $\mathrm{RIGP}$ over the variety-excluding fields of Szachniewicz and the author, when the excluded variety is a locally closed subvariety of an abelian variety.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-14T18:11:13Z
Alf Onshuus, Mariana Vicaria
arXiv categories: math.LO

In this paper we study Keisler measures in models of ACVF. We give analogue definitions for a Keisler measure to be orthogonal to the value group and stably dominated using unique extensions, in the spirit of invariant types. Our first theorem shows that a global $M$-invariant Keisler measure is generically stable if and only if it is orthogonal to the value group if and only if it is stably dominated. This theorem is later applied to prove that for a projective variety $X$ defined over a spherically complete model $M$ of ACVF whose value group is $\mathbb R$, there is a one-to-one correspondance between the generically stable measures centered on $X$ and the Radon measures on its Berkovich analyfication of $X$. Such theorem is a measure-theoretic extension of the celebrated work of Hrushovski-Loeser, which establishes a correspondence between generically stable types with the points of the Berkovich analyfication $X^{an}$ of a projective variety$X$. As an application, normalized Chambert-Loir measures associated with semipositive continuous metrics naturally give rise examples of generically stable Keisler measures.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-15T11:42:27Z
Armin Rainer
arXiv categories: math.CA, math.FA, math.LO, math.NT

For functions $f : [0,1] \to [0,1]$ in quasianalytic Denjoy-Carleman classes $\mathcal C_M$, we establish explicit bounds for the number of intersection points of the graph $\Gamma(f)$ with algebraic curves of degree at most $d$. The bounds are given in terms of the Bang degree determined by the weight sequence $M$, the degree $d$, and the norming constant of $\Gamma(f)$ with respect to the space of real bivariate polynomials of degree at most $d$. We give instances, where the bounds are at most polynomial in $d$ and, consequently, the graph $\Gamma(f)$ contains few rational points: the number of rational points of height at most $H$ is bounded by a polynomial in $\log H$.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-15T11:55:39Z
Gareth John Boxall, Charlotte Kestner, Tsinjo Rakotonarivo
arXiv categories: math.LO

We prove the definable $(p,q)$-conjecture for NIP formulas in arbitrary first-order theories. We also prove a refinement and apply it to dense pairs.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-15T14:44:39Z
Connor Watson
arXiv categories: math.LO

Hanson introduced the class of theories with bounded $k$-splitting, a higher-arity notion of stability, and proved an indiscernible extraction result for those theories assuming the existence of a $k$-ineffable cardinal. In this article, we show that the conclusion of Hanson's theorem is equivalent to the weaker assertion that there exists a weakly compact cardinal, as well as prove additional indiscernible extraction results for these theories in ZFC. Finally, we show that Hanson's construction of total bounded ultraimaginary Morley sequences in theories with bounded $k$-splitting follows from ZFC.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-15T16:54:41Z
Eduardo Due\~{n}ez, Jos\'{e} Iovino
arXiv categories: math.LO, quant-ph

The paradigm of a simple unstable theory in the sense of Shelah is the theory of the random graph, the Fra\"iss\'e limit of the finite graphs. Quantum error correction has a paradigm of its own, and we show that it is the counterpart of the random graph: the Pauli group on countably many qubits, taken modulo phases and with commutation as its relation, is the Fra\"iss\'e limit of the finite alternating spaces over the two-element field, and its form computes the syndromes of stabilizer codes. Seen through this correspondence, simplicity theory turns out to be a theory of error correction. Clifford encoding circuits implement the homogeneity of the Pauli group, forking recognizes the logical errors, and the independence theorem of Kim and Pillay is the gluing of syndromes. The two paradigms look alike as first-order structures, and they part company only when observables enter. Each defines a bipartite observable, and we prove that, once preparations are mixed, both acquire the tree property of the second kind in real-valued logic. They reach it by different roads, however, and we show that the probes decide which. The probes of the Pauli observable are the Pauli channels; for them the indicator of each syndrome sector is the difference of the responses of two uniform mixtures, and actual mixtures already witness the tree. The probes of the Rado observable see only marginals; conditions given by actual mixtures remain compatible on disjoint blocks, and the tree must be sought among idealized preparations.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-15T17:51:18Z
Wei Li, Thomas Scanlon
arXiv categories: math.LO, math.RA

We analyze the behavior of systems of algebraic differential equations when considered as systems of difference-differential equations, with special emphasis on systems which define minimal sets relative to the theory $\operatorname{DCF}$ of differentially closed fields of characteristic zero with $m$ distinguished commuting derivations. We show that if $p$ is a minimal type relative to $\operatorname{DCF}$ defined by a system of algebraic partial differential equations and inequations and the forking geometry on $p$ is trivial (also called ``disintegrated''), then $p$ remains minimal when regarded as a partial type relative to the theory $\operatorname{DCFA}$ of difference-differentially closed fields of characteristic zero with $m$ commuting derivations in the sense that every completion has $\operatorname{SU}$-rank one. We illustrate this theorem by describing in detail the possible difference-differential equations consistent with differential equations of the form $y' = y^3 + a_2 y^2 + a_1 y + a_0$ where $a_0$, $a_1$, and $a_2$ are differential constants.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-16T10:48:42Z
Mark Kamsma, Giacomo Tendas
arXiv categories: math.LO, math.CT

The framework of enriched logic extends positive logic (also known as coherent logic) from sets to structures internal to a symmetric monoidal closed category $\mathcal{V}$. This framework was developed by Rosick\'y and the second-named author. The main novelty of this logic is that the arities of the function and relation symbols are now objects in $\mathcal{V}$. We prove the compactness theorem for this enriched logic. That is, a set of $\mathcal{V}$-enriched sequents has a model (internal to $\mathcal{V}$) if every finite subset has a model. To achieve this, we define ultraproducts of enriched structures and prove enriched versions of {\L}os' theorem. We then develop some model-theoretic applications. We start with an enriched version of the model-theoretic method of diagrams, establishing a correspondence between homomorphisms whose domain is some enriched structure $A$ and models of the set $\operatorname{Diag}(A)$ of all enriched atomic formulas with parameters from $A$ that are true in $A$. Combining this with our compactness theorem, we prove amalgamation results, laying the foundations for enriched syntactic types (in the model-theoretic sense). We finish the paper with a collection of examples of $\mathcal{V}$ that our results apply to. Besides recovering the classical case when $\mathcal{V} = \mathbf{Set}$, these include many presheaf toposes, categories of monoid acts, the category of abelian groups and related additive categories, categories of (small) enriched categories, and the categories of posets and pseudometric spaces.

arXiv abstract · PDF

Model Theory · primary corpus · published 2026-10-17T13:31:34Z
Milo\v{s} S. Kurili\'{c}
arXiv categories: math.LO

We show that regarding the model-theoretic properties of distributive lattices isomorphic to finite products of linear orders there is a significant symmetry: if ${\mathbb X}_i$, $i<n$ are linear orders of size $>1$, ${\mathcal T}:=\mathop{\rm Th}\nolimits (\prod _{i<n}{\mathbb X} _i)$ and ${\mathcal T}_i:=\mathop{\rm Th}\nolimits ({\mathbb X}_i)$, for $i<n$, then ${\mathcal T}$ is finitely axiomatizable (resp. atomic, small) iff ${\mathcal T}_i$, $i<n$, are finitely axiomatizable (resp. atomic, small); the countable atomic (resp. countably saturated) model of ${\mathcal T}$, if it exists, is the product of countable atomic (resp. countably saturated) models of ${\mathcal T}_i$; further, we describe all models of ${\mathcal T}$: ${\mathbb Y} \models {\mathcal T}$ iff ${\mathbb Y}\cong \prod _{i<n}{\mathbb Y}_i$, where ${\mathbb Y} _i \models {\mathcal T}_i$, for $i<n$, and show that ${\mathbb E} \preccurlyeq \prod _{i<n}{\mathbb X}_i$ iff ${\mathbb E} = \prod _{i<n}{\mathbb E}_i$, where ${\mathbb E}_i \preccurlyeq {\mathbb X}_i$, for $i<n$. ($I({\mathcal T},\omega)\in \{ 1,{\mathfrak{c}}\}$ was proved in a previous paper.) In addition, for each $n\in {\mathbb N}$ the class ${\mathcal C}_n$ of distributive lattices isomorphic to a direct product of $n$ linear orders of size $>1$ is first order definable.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-12T09:28:36Z
Lorenzo Luperi Baglini, Boris \v{S}obot
arXiv categories: math.LO, math.CO

Recently, two exponentiations of ultrafilters have been introduced in [7]. We rephrase them in nonstandard terms, and use the nonstandard formulations to characterize some of their properties. We also study their relations with divisibility by introducing factor-picking functions and highly exponential ultrafilters.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-12T12:19:57Z
Antonio Avil\'es, Maur\'icio Rossetto
arXiv categories: math.LO, math.FA

Assuming that $\mathcal{P}(\omega)$ is tightly $\sigma$-filtered, we prove that $C(\omega^*)$ fails the ball fixed point property. This axiom holds under the continuum hypothesis and in the $\aleph_2$-Cohen model. The proof shows that the Stone space of the countable--cocountable algebra $\operatorname{Cc}(\omega_1)$ is a continuous retract of $\omega^*$ and uses the equivalence between tight $\sigma$-filteredness of $\operatorname{Cc}(\omega_1)$ and of $\mathcal{P}(\omega)$. We also prove that the quotient of a tightly $\sigma$-filtered Boolean algebra $B$ with the countable separation property by an $\aleph_1$-generated $P$-ideal is a Boolean retract of $B$.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-13T01:17:46Z
Gunter Fuchs, Hiroshi Sakai
arXiv categories: math.LO

We investigate the relationships between fragments of SRP and diagonal reflection principles. It turns out that the subcomplete fragment of SRP, augmented with CH, implies that the nonstationary ideal on $\omega_1$ is not saturated, but that Larson's diagonal reflection principle $OSR_{\omega_2}$ holds. In contrast, it was known that the full principle SRP implies the saturation of the nonstationary ideal on $\omega_1$, but it does not imply $OSR_{\omega_2}$. We find several instances of this phenomenon: pairing (variations of) the subcomplete fragment of SRP with stronger failures of the nonstationary ideal on $\omega_1$ to be saturated allows us to conclude more instances of diagonal reflection principles, while boosting (the corresponding variations of) the full principle SRP with strong forms of the saturation of the nonstationary ideal allows us to produce models where these principles still hold, yet weaker versions of diagonal reflection fail.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-13T19:29:03Z
Gabriel Goldberg, Grigor Sargsyan
arXiv categories: math.LO

Assuming $\mathrm{AD}^+ + V = L(P(\mathbb{R}))$, we show that the Ultrapower Axiom holds in $\mathrm{HOD}_s$ for every $\omega$-sequence of ordinals $s$. We use this result to analyze the structure of Nairian models, showing that they contain many measurable cardinals. As an application, we establish the consistency of the existence of infinitely many consecutive measurable cardinals with ZF, starting with a Woodin limit of Woodin cardinals. This solves a question of Henle, Mathias, and Woodin. From the same large cardinal hypothesis, adapting a forcing technique of Adkisson and Ben-Neria, we produce a model of ZF in which every uncountable cardinal is singular. Gitik's original construction requires a proper class of strongly compact cardinals.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-13T23:02:18Z
Ali Enayat
arXiv categories: math.LO

We examine the metamathematical significance of the Levy scheme $\Lambda$, which asserts, for each natural number $n$, the existence of an $n$-Mahlo cardinal $\kappa$ such that $V_\kappa\prec_{\Sigma_n}V$. Several initially unrelated constructions single out $\mathsf{ZFC}+\Lambda$: comparisons with the model theory of arithmetic and finite set theory; class theories in which the class of ordinals has the tree property; set theories with a proper class of indiscernibles; and interpretations of ordinary set theory in Cantorian parts of models of the extension \mathsf{NFUA} of Quine--Jensen set theory $\mathsf{NFU}$. Taken together, the results surveyed here provide a precise sense in which $\mathsf{ZFC}+\Lambda$ is an inevitable extension of $\mathsf{ZFC}$ if one attempts to generalize certain metamathematical results about the microcosm of hereditarily finite sets to the entire macrocosm of sets.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-16T09:52:40Z
Santiago Jockwich, Giorgio Venturi, Pedro Yago
arXiv categories: math.LO

There is a growing literature on arbitrary objects as other types of mathematical objects, besides particular mathematical objects. In this paper we study arbitrary sets in the context of ZFC set theory. An arbitrary object is one that is determined by a state space across which it varies and by its instantiations. We compare two semantic strategies. First, we analyse the possibility of modeling arbitrary sets using direct powers of a ZFC structure. This yields a natural setting, but one where Extensionality and, crucially, the full Separation scheme fail. Second, we consider structures composed of arbitrary sets using a direct power construction evaluated in a Boolean-valued semantics. Within this setting, we develop the cumulative hierarchy of arbitrary sets, arbitrary ordinals, cardinals, and filtrations of the structure of arbitrary sets. The final section develops a combinatorial interpretation in terms of independent assignments across a fixed state space. Its connection with the iterative conception is then discussed.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-17T08:59:52Z
Asaf Karagila
arXiv categories: math.LO

We show that Vop\v{e}nka's Principle is stable under symmetric extensions. Recently, de Groot and Woloszyn [1] proved this fact. We found the proof of this theorem unnecessarily complicated. In this short note we prove the same statement. We direct the reader to [3] for an exposition on symmetric extensions.

arXiv abstract · PDF

Set Theory and Large Cardinals · primary corpus · published 2026-10-18T08:21:02Z
Fengju Zhang
arXiv categories: math.LO

Bagaria and Goldberg asked if $\kappa$ being tightly $C^{(n)}$-compact implies $\kappa\in C^{(n+1)}$ for natural numbers $n\ge 1$? Usuba gave a negative answer for $n=1$. In this paper we give a negative answer for $n=2$.

arXiv abstract · PDF

Descriptive Set Theory · primary corpus · published 2026-10-12T09:26:24Z
Jacques Duparc (UNIL), Olivier Finkel (IMJ-PRG (UMR\_7586)), Dominique Lecomte (IMJ-PRG (UMR\_7586))
arXiv categories: cs.LO, cs.FL, cs.GT, math.GN, math.LO

Fix a finite alphabet $\Sigma$ having at least two letters, and natural numbers $n,k\geq 1$. We denote by $D_n(\mathbf{\Pi}^0_k)$ the class of differences of $n$ subsets of the Cantor space $\Sigma^\omega$ in $\mathbf{\Pi}^0_k$, and by $\checked{D}_n(\mathbf{\Pi}^0_k)$ the class of complements of sets in $D_n(\mathbf{\Pi}^0_k)$. We prove, for any natural numbers $n,k\geq 1$, the existence of a finite alphabet $\Sigma$ having at least two letters and a finitary language $U_{n,k}$ over $\Sigma$ accepted by a one-counter automaton such that the $\omega$-power $$U_{n,k}^\infty:=\{ w_0w_1\cdots\in\Sigma^\omega\mid\forall i\in\omega ~~w_i\in U_{n,k}\}$$ is $D_{2n-1}(\mathbf{\Pi}^0_k)$-complete. We also prove a conditional result for the dual classes $\checked{D}\_{2n}(\mathbf{\Pi}^0\_k)$: under the assumption that there exists a finitary language $V_{n,3}$ accepted by a one-counter automaton, such that its $\omega$-power $V_{n,3}^\infty$ is $\checked{D}_{2n}(\mathbf{\Pi}^0_3)$-complete, there would also exist, for any integer $k>3$, a finitary language $V_{n,k}$ accepted by a one-counter automaton, such that its $\omega$-power $V_{n,k}^\infty$ is $\checked{D}_{2n}(\mathbf{\Pi}^0_k)$-complete. Finally we add another conditionnal result about Wadge degrees of rational $\mathbf{\Delta}^0_2$ omega powers, which completes the recent results of [FGL26].

arXiv abstract · PDF

Descriptive Set Theory · primary corpus · published 2026-10-12T22:15:43Z
Vera Fischer, Yurii Khomskii, Yipu Li, Julia Millhouse
arXiv categories: math.LO

T\"ornquist (arXiv:1310.3250) proved that if there exists a $\boldsymbol{\Sigma}^1_2$ maximal almost disjoint (MAD) family, then there exists a $\boldsymbol{\Pi}^1_1$ MAD family. Since then, several other "complexity reduction" proofs have been found for other combinatorial objects, such as maximal independent families or ultrafilters. All of these proofs have relied on $\boldsymbol{\Pi}^1_1$-uniformization, so they did not easily lift to higher projective levels. In this paper, we introduce a principle weaker than Uniformization which we call "Functional Projection", and show that this principle is sufficient for most complexity reduction proofs. On the other hand, we prove that in $L[U]$, the canonical inner model for a measurable cardinal, Functional Projection holds for $\boldsymbol{\Pi}^1_2$ relations. As an immediate corollary, we obtain that in $L[U]$ there are $\boldsymbol{\Pi}^1_2$ witnesses for many combinatorial families.

arXiv abstract · PDF

Descriptive Set Theory · primary corpus · published 2026-10-13T13:47:09Z
Hyoyoon Lee
arXiv categories: math.CO, math.LO

Finite convexly ordered binary branching $C$-relations have been viewed as a notable exception to the broad applicability of the partite construction in structural Ramsey theory. The absence of a proof of their Ramsey property by the partite construction was noted by Bodirsky in his 2015 survey and pointed out again by Hubi\v{c}ka and Kone\v{c}n\'y in their 2026 survey. We overcome this limitation by giving proofs based on the partite construction of the known Ramsey properties of the class $\mathcal{CT}$ of finite convexly ordered treeable meet semilattices and of the classes of finite convexly ordered $C$-relations with arbitrary branching and with binary branching. Our proofs do not rely on Milliken's tree theorem. The key is to expand $\mathcal{CT}$ by level predicates and a predecessor function so that the locally finite subclass method applies. We then transfer the resulting Ramsey witnesses to the corresponding reduct classes and to the classes of convexly ordered $C$-relations.

arXiv abstract · PDF

Descriptive Set Theory · primary corpus · published 2026-10-15T17:57:39Z
Asger Tornquist
arXiv categories: math.LO, math.MG

We construct a complete, second countable metric space with uncountable Scott rank. This answers a well-known question posed by Fokina, Friedman, K{\"o}rwien and Nies, and shows that the known upper bound $\omega_1$ on the rank, proved by Doucha, is sharp. Further, a Baire category based variant of the rank of metric spaces is developed, and this is used to give new proofs of the known rank bounds based only on standard methods of descriptive set theory.

arXiv abstract · PDF

Descriptive Set Theory · primary corpus · published 2026-10-18T23:32:17Z
B. Miller
arXiv categories: math.LO, math.CO

We give classical proofs of the generalizations of the $\mathbb{G}_0$ dichotomy to $\kappa$-Souslin digraphs and uniformly analytic sequences of digraphs indexed by $\kappa^{\mathbb{N}}$.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-10-12T02:01:06Z
Bj{\o}rn Kjos-Hanssen
arXiv categories: math.LO

We show that if an automorphism $\pi$ of the truth-table degrees is induced by a Baire measurable function $F\colon 2^{\omega}\to 2^{\omega}$, or merely induced on some comeager set by a continuous function, then $\pi$ is the identity. The same results hold for the weak truth-table degrees. The argument is an adaptation to truth-table reducibility of OpenAI's recent proof that the Turing degrees are rigid.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-10-14T17:56:19Z
Zhi-Wei Sun
arXiv categories: math.NT, math.LO

Recently, Hilbert's Tenth Problem over the field $\mathbb Q$ of rational numbers was solved negatively by OpenAI based on a five-contact height estimate and a pole-parity construction. In this paper, we prove further that there is no algorithm to decide for any polynomial $P(x_1,\ldots,x_{86})$ with integer coefficients whether the equation $P(x_1,\ldots,x_{86})=0$ has solutions with $x_1,\ldots,x_{86}\in\mathbb Q$.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-10-15T16:00:54Z
Jason Bell
arXiv categories: math.DS, math.LO, math.NT

Given a variety $X$ with a self-map $\phi$ and subvarieties $Y$ and $Z$ of $X$, we consider the set of $n$ for which $\phi^n(Y)$ intersects $Z$ nontrivially. Extending a beautiful construction of Lee and Nam, we show this gives rise to an undecidable problem for a fixed ambient variety $X$ and morphism $\phi$. We further use this construction to give a counterexample to a conjecture of the author, Satriano, and Sierra.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-10-17T03:38:07Z
Joey Lakerdas-Gayle
arXiv categories: math.LO

We introduce the definition of a weakly $X$-uniformly $Y$-computably categorical structure, relativizing a definition of Kudinov (1996), and show that this relativized notion is closely related to the 2-dimensional complexity of the pairs of partial functions $(f,g)$ with the property that the composition $g\circ f$ simulates convergent $\emptyset'$-oracle computations. We develop a general theory for computing via composition and use it to prove results about the surprisingly complex weakly uniform categoricity spectrum of the structure $(\omega,S)$ where $S(n)=n+1$. Namely, that $(\omega,S)$ is w.$X$.u.$Y$.c.c. for some $X\not\geq_T\emptyset'$ and $Y<_T\emptyset'$, but $(\omega,S)$ is not w.$X$.u.$Y$.c.c. for any $X<_T\emptyset'$ and $Y\not\geq_T\emptyset'$. We also construct a computably categorical structure that is not w.$\emptyset'$.u.c.c., but is w.$X$.u.c.c. for a set $X$ that is $\leq_T$-incomparable with $\emptyset'$.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-10-17T23:55:11Z
Joel David Hamkins, Atticus Stonestrom
arXiv categories: math.LO

Every computable preorder relation on the natural numbers is the order of consistency strength for the membership assertions "$n\in A$" in some computably enumerable set $A$. Moreover, for every computably enumerable list of theories $T_0,T_1,T_2,\ldots$, each extending PA, there is a computably enumerable set $A$ such that each $T_n$ is equiconsistent over PA with the membership assertion $n\in A$. And similarly for both results when using instead the nonmembership assertions $n\notin A$.

arXiv abstract · PDF

Computability and Undecidability · primary corpus · published 2026-10-18T03:13:36Z
Naoya Kato
arXiv categories: math.LO

We prove over $\mathrm{PA}^{-}$ that the restricted Euclidean division principle $\mathrm{pa17}^{-}$, which asserts division only for co-prime pairs, is equivalent to the full principle $\mathrm{pa17}$. The proof uses a transformation that preserves the quotient in division with remainder to reduce an arbitrary division problem to one for a co-prime pair. This answers Visser's Open Question 8.29 and shows that the restricted principle has the same strength as full Euclidean division over $\mathrm{PA}^{-}$.

arXiv abstract · PDF

Triangulated and Derived Categories · primary corpus · published 2026-10-12T10:25:56Z
Zheng Xin
arXiv categories: math.CT, math.RA, math.RT

We develop a support theory for wide subcategories of essentially small Krull--Schmidt \(n\)-abelian categories. We construct spectra associated with families of wide subcategories and establish the corresponding support and radical theories. In particular, we characterize prime wide subcategories as the completely meet-irreducible elements of the lattice of wide subcategories and prove that every wide subcategory is recovered from the prime wide subcategories containing it. We further show that any classifying support datum is recovered, together with its object supports, from the canonical prime spectrum. Finally, we provide a \(2\)-abelian example admitting no classifying support datum.

arXiv abstract · PDF

Triangulated and Derived Categories · primary corpus · published 2026-10-14T15:52:31Z
Simion Breaz, Cristian Rafiliu
arXiv categories: math.CT

We establish a Kaplansky-Walker type lemma for idempotent complete additive categories with direct sums. It will be used in compactly generated triangulated categories to provide a version of Kaplansky's theorem on projective modules and an isomorphism-refinement result for direct sums of countable objects.

arXiv abstract · PDF

Triangulated and Derived Categories · primary corpus · published 2026-10-15T08:43:05Z
Yajun Ma, Peiru Yang
arXiv categories: math.RT, math.CT, math.RA

Let k be a commutative noetherian hereditary ring and let Q be a small, Hom-finite, locally bounded k-linear category admitting a Serre functor and satisfying the strong retraction property, with nilpotent pseudo-radical. For every k-algebra A, we construct a recollement of the Q-shaped homo?topy category KQ(A Inj) of objectwise injective Q-shaped modules by its full subcategory Kac Q (A Inj) of exact objects and the Q-shaped derived category DQ(A). The construction uses complete hereditary cotorsion pairs and does not require A to be noetherian. If A is left noetherian, both KQ(A Inj) and Kac Q (A Inj) are compactly generated by special preenvelopes of finitely generat?ed stalk modules. We identify (Kac Q (A Inj))c with the idempotent completion of (KQ(A Inj))c/LI ((DQ(A))c ), where LI is the fully faithful left adjoint of the localization. This paper builds on and generalizes works of Krause and Liu

arXiv abstract · PDF

Triangulated and Derived Categories · primary corpus · published 2026-10-15T16:24:30Z
Pat Lank
arXiv categories: math.AG, math.AC, math.CT, math.RT

We study whether weak approximability glues along recollements of triangulated categories that are compactly generated by a single object. This is applied to derived categories of complexes with quasi-coherent cohomology and prescribed support for quasi-compact quasi-separated algebraic spaces.

arXiv abstract · PDF

Triangulated and Derived Categories · primary corpus · published 2026-10-18T11:40:36Z
Chencheng Zhang
arXiv categories: math.CT, math.AT

Over every nonzero commutative ring $R$, we construct a nontopological triangulated category over $R$, whose finitely generated thick subcategories are alegbraic, while the scalar action of $R$ is faithful.

arXiv abstract · PDF

Triangulated and Derived Categories · primary corpus · published 2026-10-18T14:43:46Z
Hideto Asashiba
arXiv categories: math.RT, math.CT, math.RA

Let $B$ be a piecewise hereditary algebra of affine type over an algebraically closed field. In this paper we give a derived and stable equivalence classification of twisted multifold extensions of $B$. The types $\widetilde D$ and $\widetilde E$ are already covered by the classification for tree type. We therefore consider the remaining types $\widetilde{A}_{p,q}$. We show that the $n$th power of the Nakayama functor on the full subcategory of a transjective component determines the twist, including its action on morphisms, up to conjugacy in the derived Picard group of a hereditary algebra. Together with the hereditary derived type and the folding number, this gives a complete invariant for derived equivalence, and also for stable triangle equivalence. We then compute these conjugacy classes in the unbalanced, balanced, bypass, and Kronecker cases, keeping the finite rotation data. Finally, by the normalization theorem of Asashiba--Kimura--Nakashima--Yoshiwaki, we obtain the same classification for generalized multifold extensions with nonzero integer jump.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-12T19:09:43Z
Keima Akasaka
arXiv categories: math.CT, math-ph, math.AT, math.MP

We identify the $(\infty,1)$-category presented by the dagger Bergner, dagger Joyal, and dagger Rezk models of Parts I and II with that of univalent flagged dagger $(\infty,1)$-categories. We first construct a realization--nerve adjunction between reversal simplicial anima and Hermitian flags. We prove that its nerve restricts to an equivalence between flagged dagger $(\infty,1)$-categories and dagger Segal anima, under which univalence corresponds to unitary completeness. We then construct the adjunctions for univalentization and Hermitian completion and identify univalentization with unitary completion.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-14T16:20:06Z
Zhen Lin Low
arXiv categories: math.AT, math.CT

The category of all topological spaces and homotopy classes of maps is cartesian closed. In fact, the $(\infty, 1)$-category of all topological spaces and continuous maps, localised at homotopy equivalences, is cartesian closed. We model the exponential object using a topological space whose points are continuous maps equipped with putative neighbourhood filters. In general, this topological space will not even be $T_1$-separated, but the evaluation map induces a natural weak homotopy equivalence witnessing the universal property.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-15T18:00:17Z
Wern Juin Gabriel Ong, Gabriel Ribeiro
arXiv categories: math.CT, math.AG, math.AT, math.NT

We prove that certain categories of Bousfield localizations are presentable and give explicit regular cardinals $\kappa$ for which they are $\kappa$-presentable. As an application, we show that the category of analytic rings in the sense of Clausen and Scholze is $(2^{\aleph_0})^+$-presentable.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-16T16:33:54Z
Pedro Brunialti
arXiv categories: math.AT, math-ph, math.CT, math.MP

We construct a strict involution, that is, a strict $\mathbb{Z}/2$-action, on the $(\infty,n)$-category $\mathbf{Bord}_n(H_n)$ of bordisms with $H_n$-structure, where $H_n$ is the symmetry type of a TQFT, using the complete $n$-fold Segal space model. Using this involution, we develop an appropriate definition of reflection TQFTs in this setting and show that they correspond to certain homotopy fixed point spaces. Finally, we apply the machinery to the example of super algebras, where, depending on the symmetry type, the homotopy fixed point data corresponds to either a stellar structure or a real structure on the algebra that the reflection theory assigns to the point.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-17T05:34:26Z
Lorenzo Riva
arXiv categories: math.CT, math.AT

Motivated by the desire to turn the cobordism hypothesis (a statement about the universal property of some $n$-category of bordisms) into a $1$-categorical statement, we prove that all $n$-categories can be modeled by \emph{$n$-cospan contexts}: these are $1$-categories equipped with a collection of iterated cospans that satisfy a composition property in terms of pushouts. In particular, we construct an adjunction from $\mathsf{Cat}_n$ to the category of $n$-cospan contexts which simultaneously generalizes the $n$-fold span construction of Haugseng and the twisted arrow category construction (when $n = 1$).

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-18T08:01:11Z
Li He
arXiv categories: math.AT, math.CT

We refine the proper descent of Postnikov completed sheaves on locally compact Hausdorff spaces to the dualizable world.

arXiv abstract · PDF

Semi-Abelian and Algebraic Categories · primary corpus · published 2026-10-12T06:14:50Z
Sergei O. Ivanov, Georgii Kadantsev
arXiv categories: math.GR, math.CT

We give negative answers to two questions of Farjoun about localizations of groups. For every odd prime $p$, we construct a finite $p$-group $G$, an infinite non-nilpotent group $H$, and a local embedding $f\colon G\hookrightarrow H$. The associated localization satisfies $L_f(G)\cong H$, showing that localizations need not preserve nilpotence and that the localization map $G\to L(G)$ need not be surjective when $G$ is a finite $p$-group.

arXiv abstract · PDF

Semi-Abelian and Algebraic Categories · primary corpus · published 2026-10-12T20:52:37Z
Marino Gran, James R. A. Gray
arXiv categories: math.CT, math.GR, math.RA

We characterize the central extensions, in the sense of the categorical theory of central extensions of Janelidze and Kelly, relative to the Birkhoff subcategory of $n$-nilpotent objects of a semi-abelian and algebraically coherent category. An extension $f \colon A \to B$ with kernel $K$ turns out to be central precisely when the iterated Huq commutator $[A,[A,\dots,[A,K]\dots]]$, with $n$ occurrences of $A$, vanishes. For $n=2$ this condition reads $[A,[K,A]] = 0$, that is, $[K,A]$ is a central subobject of $A$. In the special case of groups this description was obtained by Everaert and the first author. The present proof is categorical, and applies in particular to Lie algebras, to crossed modules, to cocommutative Hopf algebras over a field, and to any category of interest.

arXiv abstract · PDF

Semi-Abelian and Algebraic Categories · primary corpus · published 2026-10-13T00:42:29Z
Li Guo, Yunzhou Xie, Yi Zhang
arXiv categories: math.CT, math.CO, math.QA

A tensor product is known for commutative Rota--Baxter algebras through a universal construction, but its underlying algebra need not be the ordinary tensor product $A\otimes B$ and can be substantially larger. We show that, after passing to augmented Rota--Baxter algebras, the ordinary tensor product itself carries a natural Rota--Baxter operator which makes the category monoidal with the usual associator and unit constraints. The resulting structure is intrinsically nonsymmetric: over a field of characteristic zero, this operator and its flip-conjugated counterpart are the only possibilities among linear combinations of five natural terms, while over any field the full category admits no braiding. Its comonoid objects are precisely Rota--Baxter cocycle bialgebras. Moreover, the free Rota--Baxter adjunction yields a bimonad and free cocycle bialgebras on ordinary bialgebras, with compatible Hopf structures for connected filtered inputs, in both the associative and commutative settings.

arXiv abstract · PDF

Semi-Abelian and Algebraic Categories · primary corpus · published 2026-10-13T12:48:47Z
Manuel Mancini
arXiv categories: math.CT, math.RA

This article surveys the main results on the representability of internal actions in varieties of non-associative algebras over a field. We begin by recalling the general framework of internal actions and split extensions in semi-abelian categories, before specialising to Orzech categories of interest and varieties of non-associative algebras. We discuss action representability, weak action representability, and action accessibility, with emphasis on the relationship between the latter two notions. We then describe the constructions of the universal strict general actor in Orzech categories of interest and the external weak actor in action accessible, operadic varieties of non-associative algebras over a field, as well as their role in the study of weak action representability. We also give a tensor-domain formulation of partial algebras and adapt the construction of the external weak actor to this setting. These notions are illustrated by examples arising from associative, Lie, Leibniz, Jacobi-Jordan, anti-commutative anti-associative, alternative, and $2$-nilpotent algebras. We conclude with a summary of the known results and some open questions for future research.

arXiv abstract · PDF

Semi-Abelian and Algebraic Categories · primary corpus · published 2026-10-17T14:31:53Z
Maxime Culot, Tomas Everaert
arXiv categories: math.CT

Let $\mathcal{C}$ be a semi-abelian category, $\mathcal{D}$ a Birkhoff subcategory of $\mathcal{C}$, and $I$ the associated reflector. For $C\in \mathcal{C}$, we establish an isomorphism between $\mathrm{H}_1(\mathrm{N}(I(\check{C}(f,C))))$ (where $\mathrm{N}$ is the Moore normalization functor and $\check{C}(f,C)$ is a Cech resolution associated to $C$) and $\mathrm{H}_1(\mathrm{N}(I(\mathbb{G}(C))))$ (where $\mathbb{G}(C)$ is the canonical $\mathbb{G}$-simplicial resolution of $C$ for $\mathbb{G}$ the comonad derived from an adjunction $F\colon \mathcal{X}\to \mathcal{C}\dashv U\colon \mathcal{C}\to \mathcal{X}$ satisfying classical conditions introduced by Quillen). The former corresponds to the Hopf formula for the second homology object associated to $I$, while the latter represents the first \v Cech derived functor of $I$. Specifically, we show that both can be expressed by a single unified formula. Furthermore, we can also prove that, under certain assumptions, the first \v Cech derived functor of $I$ is naturally isomorphic to the first non-additive derived functor of $I$ (in the sense of Culot--Renaud--Van~der~Linden).

arXiv abstract · PDF

Tensor Categories and Quantum Invariants · primary corpus · published 2026-10-13T03:19:51Z
Kevin Coulembier, Edmund Heng
arXiv categories: math.RT, math.CT, math.QA

By equipping the category $\mathcal{M}$ of modules over a finite dimensional algebra with the action of a finite tensor category $\mathcal{C}$, we introduce a subcategory $\mathcal{PM}$ satisfying numerous remarkable properties: it is generating and cogenerating, functorially finite, closed under Auslander--Reiten translations (i.e. precluster tilting), and it computes the finitistic dimension. Through a functor category perspective, $\mathcal{PM}$ is identified with the $\mathcal{C}$-module functors that are projective, and we also prove a $\mathcal{C}$-equivariant version of the Auslander(--Solberg) correspondence. As examples, we show that $\mathcal{PM}$ contains only finitely many indecomposable modules for some tensor product algebras. For some family of 1-Iwanaga--Gorenstein algebras introduced by Geiss--Leclerc--Schr\"oer, we show that $\mathcal{PM}$ is exactly the subcategory of $\tau$-locally free modules.

arXiv abstract · PDF

Tensor Categories and Quantum Invariants · primary corpus · published 2026-10-13T05:54:43Z
Mohamad Maassarani
arXiv categories: math.QA, math.CT, math.GR, math.RT

We give two types of examples where two non isomorphic finite quandles have isomorphic enveloping groups. This implies that two non-isomorphic finite quandles can share isomorphic representation categories (as additive and tensor categories simultaneously).

arXiv abstract · PDF

Tensor Categories and Quantum Invariants · primary corpus · published 2026-10-14T00:55:29Z
Rhea Palak Bakshi, Mitchell Jubeir, Quinn T. Kolt
arXiv categories: math.GT, math.CT, math.QA

We calculate the chromatic spherical invariant $\mathscr{K}_{\mathrm{Rep}(H)}(L(p,q))$ of lens spaces $L(p, q)$ for arbitrary finite-dimensional unibalanced, unimodular Hopf algebras $H$. In the case of the index-2 Nichols Hopf algebra $\mathcal{K}_2$ and $q=1$, we find that the invariant of $L(p, 1)$ depends only on the parity of $p$ for $p\geq 1$. We also describe the duals $\mathcal{S_I}(M)^*$ of the admissible skein modules of handlebodies $M=H_g$ and of $M=L(p, q)$ for arbitrary tensor ideals $\mathcal{I}$ of a ribbon tensor category. In particular, $\mathcal{S_I}(L(p, q))^*$ corresponds with cyclic traces on $\mathcal{I}$ satisfying a property reminiscent of the modified trace condition.

arXiv abstract · PDF

Tensor Categories and Quantum Invariants · primary corpus · published 2026-10-16T09:30:02Z
No\'e Delorme, Simon Perdrix
arXiv categories: quant-ph, cs.LO

Control is a fundamental concept in quantum and reversible computational models. It enables the conditional application of a transformation to a system, depending on the state of another system. We introduce a general framework for diagrammatic reasoning featuring control as a constructor. To this end, we provide an elementary axiomatization of control functors, extending the standard formalism of PROPs to controlled PROPs. As an application, we show that controlled PROPs facilitate diagrammatic reasoning for quantum circuits. In particular, they admit a simple and complete axiomatization involving at most three qubits, whereas in the standard PROP setting, completeness necessarily requires axioms involving arbitrarily many qubits.

arXiv abstract · PDF

Tensor Categories and Quantum Invariants · primary corpus · published 2026-10-18T09:53:16Z
Jaehyeok Lee, Jae-Suk Park
arXiv categories: math.CT, math.AG, math.RT

We develop a theory on duality between groups and the categories of their representations, by providing an abstract characterization of such categories. The theory has two parallel formulations, each presenting a duality analogous to one of the two that were originally proposed by Grothendieck: the one between profinite groups and the abstract categories of their continuous representations on finite sets, and the other between affine group schemes over a field and the abstract categories of their finite-dimensional linear representations. In the present theory, groups and their representations are internal to a symmetric monoidal base category, with no finiteness condition imposed. The role of a fiber functor is played by a fiber point, an abstraction of the forgetful functor with its chosen adjoint. Over each base, a group determines the category of its representations equipped with the canonical fiber point, and a pointed abstract category determines the group that represents the presheaf of automorphisms of its chosen fiber point. These constructions yield mutually quasi-inverse equivalences of $(2,1)$-categories. By introducing change of base, we gather the dualities over individual bases into a single duality in each formulation. For a pointed abstract category, fiber points of the category are in perfect correspondence with torsors under the group associated to the chosen point. As an illustration of the theory, we reformulate the Galois theory of covering spaces for nonempty, path-connected, locally path-connected, semilocally simply connected spaces.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-12T00:52:14Z
\'Edouard Bonnet, Yeonsu Chang
arXiv categories: cs.DS, cs.DM, cs.LO, math.CO

A hereditary graph class has strongly edge-sublinear separators if, for some constant $0 \leqslant b < 1$, every graph in the class with $m$ edges admits a balanced separator of size $\mathcal O(m^b)$. We show that Max Weight Independent Set (MWIS) admits a deterministic quasipolynomial-time approximation scheme (QPTAS) on every such class. In particular, this applies to graphs excluding any fixed graph as an induced minor, by a separator theorem of Korhonen and Lokshtanov [SODA 2024]. Our theorem generalizes the QPTASes for axis-parallel rectangles [Adamaszek and Wiese, FOCS 2013] and polygons [Adamaszek, Har-Peled, and Wiese, JACM 2019], or equivalently for packing connected subgraphs of a planar graph [Pilipczuk, van Leeuwen, and Wiese, Algorithmica 2020]. It also generalizes the QPTAS for MWIS on hereditary classes with strongly sublinear separators measured in vertices [Dvo\v{r}\'ak, EJC 2018; Dvo\v{r}\'ak and Lahiri, ESA 2021], as well as the QPTASes for graphs excluding particular induced minors [Chudnovsky et al., arXiv 2025; Bonnet et al., SWAT 2026; Czy\.zewska et al., arXiv 2026].

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-12T08:25:46Z
Georg Struth, Krzysztof Ziemia\'nski
arXiv categories: cs.FL, math.CT

Using the formalism of presheaf automata, we introduce new classes of automata for modelling concurrency that extend higher-dimensional automata and symmetric higher-dimensional automata. We study their languages and characterise these languages in terms of posetal cospans.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-12T09:17:17Z
Juan Antonio Vega Coso
arXiv categories: math.PR, math.CT, math.RA

Spectral duality structures (SDS) explain why a distinguished family of initial distributions makes the absorption probabilities of resetting processes insensitive to the resetting mechanism. Here we study their axioms. We prove that the six defining conditions are mutually independent and determine what each one contributes. The key tool is a structure theorem valid for an arbitrary permutation and an arbitrary positive weight: every insensitive distribution is supported on a union of cycles balanced at a common level, and the level of a cycle is fixed by the geometric mean of the weight on it. From it, positivity selects the admissible root, the constant orbit product is equivalent to the existence of an insensitive distribution of full support, and the involution is equivalent to the response rank being equal to the number of free weight parameters. Without the duality relation, insensitivity of a single distribution is cheap and generically isolated; duality turns it into structural neutrality of the separatrix. The full-rank condition splits into two layers: a weaker condition is equivalent to maximal response rank, while full rank also excludes insensitivity at any other level. We then show that a single SDS is internally rigid: compatible semigroup structures force a constant weight, compatible abelian group structures obey a precise arithmetic condition, congruences form a simple lattice, and the automorphism group is computed explicitly. Finally, the axioms do not determine the orientation of the response; in the two-site case we give the exact condition under which the geometric and analytic sign criteria agree.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-12T13:34:05Z
Nikolaos Galatos, Simon Santschi
arXiv categories: math.LO, math.RA

We show that every proper variety of distributive $\ell$-pregroups is periodic; as a result, the subvariety lattice of the variety of distributive $\ell$-pregroups decomposes into a disjoint union of bounded intervals each consisting of all properly $n$-periodic varieties, for different $n \in \mathbb{Z}^+$. On the way, we study non-periodic (one-generated) subalgebras of $\mathbf{F}(\mathbb{Z})$ and show that they either contain a non-periodic idempotent or they contain idempotents of arbitrary big periodicity. The same results holds for non-periodic one-generated subalgebras of $\mathbf{F}(\mathbf{J} \overrightarrow{\times} \mathbb{Z})$, where $\mathbf{J}$ is a chain, generated by a composite element and the resulting idempotents can be taken to be local in the associated wreath product.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-12T15:44:17Z
Daumantas Kojelis, Carsten Lutz
arXiv categories: cs.LG, cs.LO

A landmark result states that the expressive power of graph neural networks (GNNs) is bounded from above by the 1-dimensional Weisfeiler-Leman (1-WL) test. We ask whether a constant-depth GNN can match the expressive power of 1-WL while using only rational weights. We prove that this is the case when Schanuel's conjecture, a famous open problem from transcendental number theory, is taken to be true. Our GNN construction works even with integer weights, and more generally with a broad range of rational weights. As the activation function, it may use logistic sigmoid, hyperbolic tangent, or related functions. It is uniform across all graph sizes. We also prove a partial converse: if a GNN with exponentiation, hyperbolic sine or hyperbolic cosine as activation matches the expressive power of the 1-WL test in a slightly more expressive setting where graphs may contain certain auxiliary vertices, then this implies Schanuel's conjecture restricted to the numbers that arise in computations of the GNN. We also conduct experiments showing that the constructed GNNs indeed match the 1-WL test.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-12T20:49:31Z
Ilyas Khan
arXiv categories: math.CT

We investigate Eduard Hanslicks formalist aesthetics through the prism of Category Theory

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-13T13:12:39Z
Heshun Fan
arXiv categories: math.CO, cs.LO

We construct trees with perfect matchings and independence sequences that fail log-concavity near the independence number $\alpha$. For every integer $k\geq1$, one family fails at $\alpha-k$ and has a witness of order $O(k^2\log(k+2))$. For every integer $t\geq2$, a single tree has simultaneous failures at $\alpha-1,\alpha-3,\ldots,\alpha-(2t-1)$, with a witness of order $O(t^3)$. All these trees satisfy $\alpha=N/2$, where $N$ is the number of vertices, and contradict Conjecture 4.2 of Ramos and Sun. A sufficient condition uses a fixed tree and the numbers of attached leaves. For fixed $k$ or $t$, explicit bounds give geometric decay of $a_j^2/(a_{j-1}a_{j+1})$ at these indices as the trees grow; $a_j$ counts independent $j$-sets. The proofs count independent sets by empty matching pairs. The Lean proof assistant checks formal proofs of the parameterized results and their quantitative bounds; exact 90- and 180-vertex examples illustrate the constructions.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-14T19:07:44Z
Marcel Friedrichs, Addie Jordon, Juri Kol\v{c}\'{a}k, Daniel Merkle
arXiv categories: cs.LO, cs.DM, q-bio.MN

Graph transformations model changing systems, with applications in software, biology and chemistry, among others. We introduce MolFoundry, a graph transformation framework, and present a workflow for observable analysis that tracks the dynamics of local patterns through rule composition. Analysing rule compositions avoids the need to enumerate a potentially infinite state space. Building on rule-algebraic stochastic rewriting, MolFoundry's kernel composes rules with nested application conditions, including missing-edge constraints. Given rules, rates and query patterns, the algorithms iteratively identify auxiliary pattern counts and search for closure. Using exact counting identities supplied by graph-family backends, successful searches yield closed ordinary differential equations for average counts or, with justified individual jumps, finite event models describing joint changes and rates. We evaluate conditional composition and automated discovery of auxiliary observables against published calculations and independent rule application. Applications to aldol addition, copolymerization and chlorination show how the framework yields quantitative predictions directly from molecular graph rules.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-14T19:56:20Z
Julius Monsen, Jakob Suchan, Mehul Bhatt
arXiv categories: cs.AI, cs.LO

We present a general declarative framework for anticipatory reasoning about interactive motion in complex dynamic environments. Our focus is on (explainable) anticipatory space-time mental model formation at a semantic level to heuristically guide low-level motion computation. Our method is hybrid, modular and elaboration tolerant integrating: 1) An ASP model characterising the dynamics of interactive motion trajectories; 2) Semantically-guided prediction for deriving `branching trajectory futures'; and 3) An energy-based {optimisation} model to evaluate, rank and filter anticipations. We evaluate with the Argoverse 2 benchmark, where each anticipated trajectory carries an explicit, inspectable event-level hypothesis, unlike end-to-end stochastic prediction.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-14T20:05:26Z
Gabriel Bauza-Llompart, Raquel Fernandez-Peralta, Marc Munar
arXiv categories: cs.LO

The completion problem for continuous and Archimedean triangular norms (t-norms for short) consists in describing all the operators that take predefined values on a given subset of the unit square, and it reveals how much of a t-norm is determined by partial information. In this paper, we focus on the case where this subset is a parametric curve. We first formulate the problem in terms of the functional equation satisfied by an additive generator, and we then restrict our attention to curves of the form $(x,p(x))$ with $p$ continuous and increasing, which include the classical diagonal and horizontal section cases. We determine when the known values are compatible with a continuous and Archimedean t-norm, and we show that every completion is obtained by choosing the additive generator on a subinterval and reconstructing it elsewhere from the values on the curve. This description is recursive in general and becomes a closed formula under additional conditions, recovering the two classical results as particular cases. The completions are not unique, and we give examples with infinitely many t-norms sharing the same section along a curve. Finally, we combine our results with the reconstruction of a t-norm from its values above a level curve, which determines exactly the additive generator on that subinterval, so that the two pieces of information are complementary and together determine a unique completion.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-16T16:28:49Z
Savitha Sam Abraham, Marjan Alirezaie, Hossein Rahnama
arXiv categories: cs.AI, cs.CL, cs.LO

Text-to-Image (T2I) generative models have made significant progress in producing high-fidelity images from natural-language prompts. Alongside this progress, numerous benchmarks have been developed to evaluate capabilities such as attribute binding, numeracy, spatial reasoning, and commonsense reasoning. In this work, we propose a new perspective on T2I evaluation by casting it as a constraint-satisfaction problem. We introduce a logical framework that formally specifies the benchmark domain, including objects, attributes, and relations, alongside the constraints that generated images must satisfy. We evaluated four state-of-the-art T2I models across 9 classes of constraints ranging from a single-object-attribute to multi-object relationships constraints involving logical operators ($\forall, \exists, count, \rightarrow$). Our results reveal a substantial gap between single-object and complex conditional multi-object relationship constraint classes, with the best-performing model achieving 98% accuracy on the former and just 53% on the latter. We assess compositional generalisation, finding that the best-performing model`s accuracy drops from 84% on single-constraint prompts to 20% when satisfying multiple constraints simultaneously. Identifying unsatisfiable constraints is also challenging, with the best model correctly recognizing only 23% of such prompts. Building on this framework, we introduce \textbf{LogicVal}, an evaluation methodology that combines neural visual detection with logical reasoning to assess constraint satisfaction in generated images. On CLEVR, LogicVal achieves ROC-AUC scores ranging from 0.88 to 0.98, indicating strong alignment with human judgments. These findings underscore the value of logic-based evaluation for characterizing T2I model capabilities and limitations.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-18T17:53:10Z
Apostolos Syropoulos, Basil Papadopoulos, Binod Kumar Sharma
arXiv categories: cs.LO

Graphs, which are made up of points connected by lines, are used to represent relationships between objects. They are useful for solving problems in computer science, logistics, biology, and other fields, including social networks and the internet. Neutrosophic graphs are graphs whose points and lines are characterized by membership, indeterminacy, and non-membership degrees. In the simplest case, only lines are characterized by these degrees. The process by which we transform one graph to another is called graph rewriting. It has been shown that graph rewriting can be described mathematically by pushouts, which are category-theoretic structures. It has also been shown that fuzzy graphs have this property, and here we prove that neutrosophic graph rewriting can be described by pushouts in a certain category. By providing a fuzzy version of category theory, it is possible to define fuzzy categorical structures and thus to define neutrosophic graph rewriting in a more suitable manner. Since graph rewriting is actually a model of computation, neutrosophic graphs are a neutrosophic model of computation. A hypergraph is a generalization of a conventional graph. It allows a single "hyperline" to connect many points, which is different from regular graph lines that only connect two points. Neutrosophic hypergraphs can be used to reformulate Wolfram's models, which are supposed to be a mathematical model of reality.

arXiv abstract · PDF