arXiv weekly literature review

Formal theorem proving · primary corpus · published 2026-09-28T07:17:43Z
Sareh Nabi, Roland Vogl, Marzieh Nabi
arXiv categories: cs.AI, cs.LG, cs.LO

Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries such as Mathlib encode 285,000+ verified theorems with syntactic dependencies, but the semantic layer mathematicians rely on for discovery (analogies, generalizations, cross-domain bridges) remains implicit. We introduce MathAgent, which builds this layer as a knowledge graph, MathKG, and uses it to augment LLM theorem provers. MathKG connects 364 Mathlib theorems and definitions by 9,434 typed semantic edges inferred via LLM-based relation extraction anchored to verified Mathlib declarations. We run a controlled ablation across four augmentation modes (no context, knowledge-graph context, Mathlib retrieval, both) and five models: Qwen3-8B/32B, their Lean-specialized derivatives Goedel-Prover-V2-8B/32B, and Claude Sonnet 4.6, on miniF2F, plus PutnamBench and MathOlympiadBench for Sonnet. Three findings emerge. (i) Specialization dominates augmentation: Lean fine-tuning adds 33-38 percentage points of solve rate in every mode, and a specialized 8B model beats a $4\times$ larger general one by 29-35 points, while no augmentation mode improves solve rate by more than 3 points. (ii) Augmentation is capability-conditioned: knowledge-graph context helps small models but hurts large ones, with the specialized model gaining more relative to its general base at every scale. (iii) Yet the augmentation modes solve different problems: an oracle selecting the best mode per problem solves 6% to 58% more than the unaugmented prover, a complementarity effect that strengthens on harder problems (32% more on PutnamBench). These results motivate adaptive strategies that select augmentation by model capability and problem. Code, data, and artifacts are available at https://github.com/sarehnabi/mathagent

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:56:55Z
Zuzana Hanikov\'a (Institute of Computer Science of the Czech Academy of Sciences), \v{S}t\v{e}p\'an Holub (Faculty of Mathematics, Physics, Charles University, Prague)
arXiv categories: cs.LO

The axiomatization of the theory of hereditarily finite sets in first-order classical logic is systematically explored and formalized in Isabelle/HOL. The formalization uses a hierarchy of locales, each corresponding to a fragment of the theory given by a particular collection of axioms. An inductive definition of first-order definable predicates is introduced and used to formalize axiom schemata. Special attention is paid to several equivalent axioms of finiteness, as well as to several equivalent ways of expressing regularity. The work also formalizes several facts about the independence of an axiom from a system of axioms by defining appropriate models.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:57:13Z
Janis Kr\"oger (Carl von Ossietzky Universit\"at Oldenburg), Paul Kr\"oger (Carl von Ossietzky Universit\"at Oldenburg), Martin Fr\"anzle (Carl von Ossietzky Universit\"at Oldenburg)
arXiv categories: cs.GT, cs.LO

Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge due to the conflict between system availability and update execution. In this paper, we present a bounded SMT encoding for synthesizing fixed global-time update schedules for timed-games with linear update automata and a fixed number of update transitions. We model the interaction between the system and the update as a two-player timed game. Our key contribution is the synthesis of global time points that define a fixed update schedule which guarantees safe and complete deployment of the update independently of the autonomous system behavior. To this end, we reduce the scheduling problem to a reachability and safety objective and encode it as a quantified SMT problem. We demonstrate it on an example system of a trajectory planner for autonomous driving, showing that the synthesized schedule ensures safe deployment under all admissible executions.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:57:31Z
G\'abor Kusper (Eszterh\'azy K\'aroly Chatolic University)
arXiv categories: cs.LO

A resolvable network is a directed-graph representation of SAT: every SAT instance can be translated into an RN, and every RN has an associated CNF formula. Each reach represents one clause. In a mixed reach, the head and tail are disjoint sets of variables containing the variables occurring negatively and positively in the clause, respectively; the distinguished symbols Source and Sink represent a missing negative- or positive-literal side. RN-Solver is a proof-of-concept SAT solver based on this representation. Its all-positive clauses are represented by white reaches, and its token distributions are the inclusion-minimal hitting sets of the current white tails, generated by monotone CNF-DNF dualization. RN-Solver learns new white reaches by private-pivot resolution, a structured resolution sequence that uses old white reaches as pivot witnesses. In the original algorithm, every candidate white reach generated by such a chain was followed by a global subsumption test against the current network. Profiling showed that this subsumption test can dominate the runtime on random 3-SAT instances. We show that this check is unnecessary when the mixed reach used for learning is falsified by the current token distribution, meaning that the distribution makes all variables in the head true and all variables in the tail false. The key invariant is simple: the resulting white tail is disjoint from the triggering token distribution, while the same distribution intersects every old white tail. Hence no old white reach can subsume the generated reach. This structural observation allows us to construct a simpler, snapshot-based, subsumption-free variant of RN-Solver, where each main-loop iteration uses a fixed set of old reaches and installs newly generated white reaches only at the end of the iteration. We prove soundness of the revised algorithm. Empirical evaluation confirms the elimination of the targeted checks: within an 8 second budget, snapshot/full-DNF solves 963 of 1,000 uf20-91 instances, compared with 724 for the original control flow. A separate 100-instance comparison identifies exact incremental DNF as the most effective of the three tested configurations.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:57:48Z
Ioana Sila\c{s} (West University of Timi\c{s}oara), Adrian Cr\u{a}ciun (West University of Timi\c{s}oara)
arXiv categories: cs.LO, cs.DC

In distributed systems, model checking is usually used at design time for specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is commonly used in this way as a specification language, together with the TLC model checker. In this paper, we present a monitoring tool that, at its core, utilizes TLA+ specifications in a different way. The tool utilizes a TLA+ trace-checking specification to detect violations in behavior inferred from Kubernetes audit logs. Our primary use case focuses on multitenancy violations; however, the pipeline is not limited to that setting. Specifically, it demonstrates how formal reasoning can be incorporated into live Kubernetes environments to improve monitoring and correctness checking.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:58:06Z
Ariadna Br\u{a}nici-Faraon (Alexandru Ioan Cuza University of Iasi), \c{S}tefan Ciob\^ac\u{a} (Alexandru Ioan Cuza University of Iasi), Diana-Elena Gratie (Alexandru Ioan Cuza University of Iasi)
arXiv categories: cs.LO, cs.PL, cs.SC

We present a formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representations for rational numbers, linear expressions, inequalities, equalities, divisibility constraints, and systems of constraints, together with their semantic interpretation through valuations. We fully specify and verify the implementation in Dafny. We describe the lessons learned and how the formalization process led to new insights into the algorithm.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:58:23Z
\c{S}tefan Ciob\^ac\b{a} (Alexandru Ioan Cuza University of Ia\c{s}i, Romania), Diana-Elena Gratie (Alexandru Ioan Cuza University of Ia\c{s}i, Romania), Drago\c{s}-Irinel Rotariu (Alexandru Ioan Cuza University of Ia\c{s}i, Romania)
arXiv categories: cs.LO, cs.FL, cs.PL

We describe the formalization in Dafny of two computational models, Turing Machines and the Lambda Calculus. We present several application of the formalizations: machine proofs of termination for Turing machines, Dafny proofs for Church encodings, and a mechanized proof of the Church-Rosser theorem.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:58:59Z
David Nowak (Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France), Vlad Rusu (Inria, Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France)
arXiv categories: cs.LO

We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we avoid complications occurring in earlier works, such as artificially including silent steps to comply with Rocq's productivity checker, treating monad laws as weak bisimulations, and coinductive bisimulation reasoning. We define an inductive program equivalence relation as the congruence closure of a base relation on primitive effects with respect to action sequencing and least upper bounds. This enables reasoning about possibly non-terminating programs by reducing their equivalences to equivalences of their terminating approximations, which are then proved by induction. This relation is proved correct: provided the base relation is correct, equivalent computations have equal denotations in any monad that faithfully implements the effects. We illustrate the framework by showing the equivalence of two programs encoding the Syracuse sequence, whose termination is an open mathematical conjecture.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:59:16Z
Isabela Dr\v{a}mnesc (West University of Timi\c{s}oara, Romania), Tudor Jebelean (RISC, Johannes Kepler University, Austria, ICAM, West University of Timi\c{s}oara, Romania), Sorin Stratulat (Universit\'e de Lorraine, CNRS, LORIA, France)
arXiv categories: cs.LO

This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more complex but more efficient tail recursion, together with its formal implementation and certification in Theorema and Rocq (formerly Coq). We identify some general principles of algorithm transformation, and we develop the necessary background theory and proof methods. As a significant distinctive aspect, the approach in Theorema uses multisets, which simplifies the whole process and makes it more intuitive. The certification process reveals significant differences between the Theorema and Rocq approaches, about which we provide a comparative analysis with respect to algorithm definition, proof development, and proof effort. This analysis offers insights into how algorithm design influences the complexity and structure of formal proofs and demonstrates how non-trivial algorithms can be effectively verified across different formal frameworks.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T10:59:51Z
\'Ad\'am Kurucz (ELTE E\"otv\"os Lor\', University), P\'eter Bereczky (ELTE E\"otv\"os Lor\', University), D\'aniel Horp\'acsi (ELTE E\"otv\"os Lor\', University)
arXiv categories: cs.LO

This paper investigates model composition—often referred to as "gluing"—within the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T11:00:10Z
Hora\c{t}iu Cheval (University of Bucharest)
arXiv categories: cs.LO

We present work in progress towards an intuitionistic version of Applicative Matching Logic. We introduce a semantics based on complete Heyting algebras, and propose a proof system which we prove to be sound relative to this semantics.

arXiv abstract · PDF

Formal theorem proving · primary corpus · published 2026-09-28T11:25:34Z
Franco Barbanera (DMI - University of Catania, Italy)
arXiv categories: cs.LO

The Participants-as-Interfaces (PaI) methodology for system composition proposes that system participants can be regarded as interfaces. For each system in a given collection, one participant is designated to serve as its interface. When the systems are composed, these interface participants are replaced with gateways that communicate with one another by forwarding messages. We generalise the approach to partial gateways, where gateways can forward only a chosen set of messages. As for the standard PaI approach, we exploit such extended version for systems of communicating finite state machines (CFSMs). This extension is fully detailed for the binary case, and can be scaled up to the multicomposition case. We prove that many relevant communication properties (deadlock-freeness, reception-error-freeness, etc.) are preserved by PaI composition via partial gateways in case also the connection policy (i.e. the system representing the way we wish gateways interact with each other) enjoys the same properties. Such a proof turns out to be just a corollary of a property preservation result for a restricted and partial composition method, dubbed fusion-composition. Fusion-composition hence turns out to be at the heart of the PaI composition approach.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-28T11:25:52Z
Hern\'an Melgratti (ICC - Universidad de Buenos Aires - Conicet, Argentina), Claudio Antares Mezzina (Dipartimento di Informatica, Universit\`a di Bari Aldo Moro, Italy), G. Michele Pinna (Dipartimento di Matematica e Informatica, Universit\`a di Cagliari, Italy)
arXiv categories: cs.LO, cs.FL, cs.PL

Asynchronous communication is a fundamental feature of modern distributed systems, where messages are emitted without requiring immediate synchronization with receivers. In process calculi, this behaviour is typically modelled by separating message emission from message consumption. At the same time, reversible computation has emerged as an important paradigm for analysing concurrent systems, enabling computations to be undone while preserving causal dependencies between actions. While reversible semantics have been extensively studied for synchronous process calculi such as CCS, their integration with asynchronous communication remains largely unexplored. In this paper we investigate the interaction between asynchrony and reversibility in the setting of CCS. We first introduce CCSa, an asynchronous variant of CCS in which output actions generate explicit message entities that can later be consumed by matching input actions. We then define rCCSa, a reversible extension of CCSa obtained by adapting the framework of Phillips and Ulidowski. In rCCSa, prefixes and messages are annotated with unique keys that record message emission and consumption events, allowing computations to be reversed while preserving causal dependencies. We show that the resulting reversible semantics satisfies causal consistency, ensuring that computations can be reversed exactly up to causal equivalence. The proof relies on the axiomatic framework for reversible computation proposed by Lanese et al.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-28T11:26:09Z
Alexandre Zua Caldeira
arXiv categories: cs.PL, cs.LO

We prove that the state space of every well-formed session type, quotiented by strongly connected components, forms a bounded lattice; n-ary parallel composition yields product lattices. Two consequences follow: duality preserves the lattice up to isomorphism, and Gay-Hole width subtyping corresponds to lattice embedding for non-recursive types. We validate this on 108 benchmark protocols across networking, databases, distributed systems, AI, and fault tolerance: all form lattices, 93 distributive, 15 non-distributive. Mechanised in Lean 4 with two independently developed tool implementations.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-28T14:59:07Z
Riccardo Porcedda
arXiv categories: cs.AI, cs.LO, cs.SY, eess.SY

The appearance of Jev marked the era of System One Models, foundation models that return structured decisions with probability distributions rather than text. Aside from low cost and great speed, Jev's central promise is that these probabilities are calibrated: such claim is not backed by any public test and available external benchmarks evaluate confidence calibration, not whether every returned option probability has the right numerical meaning. To tackle this issue, we introduce Sys1Cal-v1, a dataset of True/False questions about a proposition $A$ for which the exact probability $P(A)$ is known by construction. Each item is queried through the three Jev primitives - Noul, Choice and Score - and evaluated by total variation distance from the ground-truth distribution, which can be used to estimate a soft accuracy of System One Models. We showcase the utility of Sys1Cal-v1 as a benchmark dataset by evaluating Jev and SemIf, an open-source Choice-style baseline. In this work, however, we focus even more deeply on Jev, by studying the calibration of its Score and Choice answers. In particular, we discover a peculiar behaviour that can be explained by assuming that Jev suppresses a third truth value, going beyond True and False. In other words, in \texttt{Choice} answers, $P(A)$ and $P(\neg A)$ are presented as if $P(A)+P(\neg A)=1$, while a term $P(U)\neq0$ is missing in the sum. Recovering $P(U)$ leads to an improvement of median soft accuracy in \texttt{Choice} answers from $0.771$ to $0.978$, suggesting that, even in binary decisions, Jev wants to answer with a third option:``I don't know''.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-28T17:37:37Z
Ugo Dal Lago, Zeinab Galal
arXiv categories: cs.LO, cs.PL, math.CT

Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-28T18:20:12Z
Jingyu Ke, Jingyang Li, Guoqiang Li
arXiv categories: cs.PL, cs.LO, cs.SE

Equivalence checking is essential for validating compiler transformations of hybrid quantum programs, which combine quantum operations, measurements, and classical control. Measurement-dependent control limits unitary reasoning, while dependencies between classical outcomes and quantum operations can enlarge intermediate symbolic states. We present Irene, an equivalence-checking framework for bounded hybrid quantum programs based on structure-preserving symbolic reduction. The framework progressively simplifies equivalence obligations through three levels of reasoning. At the gate level, algebraic identities simplify unitary regions. At the hybrid path-sum (HPS) level, reduced symbolic execution states are represented as typed graphs, whose isomorphism certifies equivalence. Remaining obligations are handled by density kernels that characterize transformations of input density operators into observable outputs, allowing comparison even when internal measurement histories differ. Residual coefficient differences are encoded as SMT queries. A common set of symbolic reductions supports HPS and density-kernel reasoning by preserving factored Boolean and arithmetic expressions, eliminating reducible dependencies before expanding residual sums. We evaluate Irene against five equivalence checkers on 1,982 program pairs from seven benchmark suites. Irene solves 1,584 pairs (79.92%), compared with 57.52% for MQT QCEC, the baseline with the highest aggregate coverage, with a mean end-to-end time of 3.93 seconds per solved pair. Applied as an equivalence-checking oracle, Irene also identifies 15 previously unknown bugs in quantum compilers, including Qiskit, Cirq, and PennyLane.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-28T21:09:57Z
Christoph Benzm\"uller
arXiv categories: cs.LO, cs.AI, math.LO

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzm\"uller and Scott's Notes on G\"odel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nominals and satisfaction operators of hybrid logic, and a proof using one proves a theorem of the embedding that need not be one of the modal logic. That the framework affords this is not new, and whether a result is one of the modal logic can be settled in two ways: by replaying it in an explicit proof calculus, done by hand for chosen theorems, or by analysing the proofs the embedding itself produces, done here mechanically, for every result at once. Every statement the Notes prove has a proof inside the object language: 294 written out by hand and machine-checked, none using a nominal. The proofs the Notes themselves give instantiate no nominal either; what the detector flags there are terms a prover substituted. The three questions the Notes leave open are settled too, without nominals, but the conjunction axiom has to be emended: generalised in the Notes to G\"odel's "any number of summands", it covers the conjunction of no properties, and of one; the empty one alone settles all three, and the two together yield what a separate axiom of G\"odel's is for. This article restricts the conjunction axiom to at least two different conjuncts, the reading G\"odel's footnote suggests, and the questions are settled again, by proofs that turn on the argument rather than a degenerate instance. The restriction holds of the object language only: with a nominal the axioms make the accessibility relation the identity and the readings coincide. Every theorem is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, certified by the build.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-29T03:16:30Z
Eric Allen
arXiv categories: cs.PL, cs.LO

Programs that compute with physical quantities often need to convert between units of measurement, and as the Mars Climate Orbiter showed, these conversions can be a rich source of errors. Meanwhile, typed unit calculi, our most rigorous formalisms for checking physical units in a program, have excluded unit conversions. Through this exclusion, they have established a powerful property: well-typed programs are invariant under rescaling (no program can depend on how big a meter is). But losing the ability to convert between units is a significant cost. In contrast, practical languages provide conversion but no invariance theorem. We present $\Lambda_S$, a typed lambda calculus with conversion, quantification over units and dimensions, and vectors and linear maps with per-component units, and we determine exactly how much invariance survives conversion. For terms without unit constants we prove two abstraction theorems: (i) a convert-free term is invariant under every rescaling; (ii) a term with conversions is invariant under every rescaling that scales all units of one dimension by the same factor. The condition in (ii) cannot be weakened: under any other rescaling, some conversion of a nonzero value is not invariant. For first-order programs, a verified decision procedure returns one of three verdicts: it certifies that no error in the declared conversion factors can change the program's answer, names the accumulated ratio through which such an error would scale it, or declines. A verified checker decides whether unit declarations are consistent and determine every conversion factor, and extracts each factor exactly. We also prove adequacy, erasure, and the $n$-variable Pi theorem of dimensional analysis with conversion. Every theorem is mechanized in Lean 4, and the evaluator compiles to a native binary.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-29T04:06:07Z
Shuangping Li, Peng Zhang
arXiv categories: cs.LG, cs.LO

We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit. Introduced by Kleinberg and Mullainathan at NeurIPS 2024, language generation in the limit studies a theoretical question motivated by LLMs: how to generate valid new strings from observed examples. This young and rapidly evolving field offers a natural testbed for studying large-scale formalization. GenLimitLib contains formal developments for 30 papers. It extracts shared definitions and reusable proof components while preserving paper-specific assumptions and statements, and records relationships across papers. In this way, GenLimitLib provides a concrete and structured view of the literature. We show through mathematical case studies and LLM experiments how our library can support both human mathematical research and AI-assisted research. Our Library: https://github.com/pengzhang91/generation-in-the-limit-lib.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-29T12:09:06Z
Steffen van Bergerem, Martin Grohe, Charlotte Lenz, Nicole Schweikardt
arXiv categories: cs.LO, math.LO

We prove a rank-preserving version of Gaifman's Theorem. Compared to earlier rank-preserving locality theorems (in particular, [Grohe, Kreutzer, Siebertz, JACM 2017]), our theorem is much simpler and yields formulas in exactly the same normal form as Gaifman's original theorem. Furthermore, it holds not only for first-order logic, but also for first-order logic with modulo-counting quantifiers and, more generally, for the first-order logic on weighted structures ngFOW+ that is introduced in this article. As an application of our theorem, we give a simplified proof of the algorithmic meta-theorem of [Grohe, Kreutzer, Siebertz, JACM 2017] stating that first-order properties of nowhere dense structures can be decided in almost-linear time. Our locality theorem for the weight logic ngFOW+ can be seen as an essential step toward such a meta-theorem for this logic.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-29T13:00:14Z
Clara Lerouvillois, Francesca Poggiolesi
arXiv categories: cs.LO

This paper proposes a calculus for Dynamic Epistemic Logic (DEL) based on dynamic hypersequents, a new framework for capturing the dynamics of epistemic models in a purely structural and natural way. We enrich dynamic hypersequents with agent indices and an event store, yielding a uniform representation of epistemic events. The resulting calculus enjoys a set of logical rules that are provably invertible. Moreover, all structural rules, including the contraction rules, as well as the cut-rule, are shown to be admissible. Finally, the calculus constitutes, to the best of our knowledge, the only proof-theoretic calculus for DEL that is both grounded in a classical S5 framework and inherently dynamic.

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-29T14:50:20Z
Corentin Reuther (University of Namur, Belgium), Jean-Marie Jacquet (University of Namur, Belgium)
arXiv categories: cs.LO, cs.PL

Although significant research has focused on the theory and implementation of data-based coordination languages, the critical aspect of their automated verification using model-checking techniques remains underexplored, which is essential for ensuring reliability and correctness in distributed systems. Existing tools, such as Anemone, provide a solid foundation for reachability-based verification of Bach programs. While they effectively analyze properties expressed in terms of state attainability, extending support to more expressive temporal specifications-such as liveness properties or invariants over shared space contents-remains an open opportunity. Such extensions are important to capture comprehensive system behaviors, for instance, ensuring that "a request is always matched by a response" or that "no message is silently lost". Addressing this limitation, we propose an automated translation from Bach to mCRL2, which explicitly represents the shared space, thereby enabling the use of mCRL2's mu-calculus model checker to verify complex properties beyond simple reachability. Complementing this translation, we introduce a systematic method to analyze the shared space in mCRL2 concerning data reachability, by directly expressing properties over the shared space's contents in the mu-calculus, thus providing a clearer framework for verification. This approach enables a novel verification process that combines action-based properties with state-based properties over the shared space contents, a largely unexplored area in current coordination-language verification approaches, offering a new dimension of analysis

arXiv abstract · PDF

Concurrency and semantics · primary corpus · published 2026-09-29T14:50:33Z
Moussa Labbadi, Rupak Majumdar, V.R. Sathiyanarayana, Sadegh Soudjani
arXiv categories: cs.LO, cs.PF, cs.PL

Discrete-event simulation is a standard technique for modelling and analysing the performance of computer systems, networks, and services. Although simulation tools are widely used, reasoning about the correctness and performance guarantees of the models they implement remains largely ad hoc: simulation outputs are interpreted statistically, but there is no logical foundation for deductive reasoning about their behaviour. We present a core imperative calculus that captures the essential constructs common to discrete-event simulators: asynchronous execution, continuous and discrete sampling from distributions, and time-based event scheduling through a global event queue. On top of this calculus, we develop a proof system for reasoning about almost-sure reachability and expected reaching time properties. Our main result is a sound and complete proof rule for these properties. Our framework generalizes deductive reasoning for discrete-time probabilistic programs to the setting of performance models, in which continuous time and continuous probability distributions are central. We have implemented the proof rules in a tool embedded in Lean. We demonstrate the applicability of our proof rule by deriving proofs of almost-sure reachability and expected reaching time for a number of case studies, including client-server examples that go beyond analytic solutions from queueing theory as well as convergence behaviours in network routing protocols. Establishing the soundness and completeness of our proof rules requires significantly more complex arguments than in the discrete-time setting. This is due to the fundamentally discontinuous nature of the operational semantics and the measure-theoretic challenges of continuous time and probability distributions.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-29T14:56:03Z
Simon Fl\"ugel, Till Mossakowski
arXiv categories: cs.LG, cs.LO

While attaining remarkable results for many applications, Deep Learning models are notoriously difficult to explain. This work introduces HyDI, a hybrid ensemble architecture for hierarchical multi-label classification. It combines a Deep Learning (DL) model with rule-based classifiers generated by Inductive Logic Programming (ILP). For leaf classes of the label hierarchy, the rule-based classifiers replace the DL model, leading to more transparent classification results. HyDI is applied to the Chemical Entities of Biological Interest (ChEBI) ontology, providing ILP-generated rules for 314 classes. For these classes, HyDI can generate global explanations as well as local explanations that combine visual and text-based descriptions.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-29T15:27:09Z
Hugo Paquet, Glynn Winskel
arXiv categories: cs.LO, math.CT

Concurrent games and strategies based on event structures are an established and expressive model of interactive computation. In this paper we revisit the problem of equipping this model with symmetry. Symmetry is essential for many applications, but it is also a source of mathematical complexity, not least because strategies with symmetry can be compared up to several distinct notions of equivalence. Our first contribution is a complete characterization of two classes of strategies for which composition admits an identity. For these two classes the identity laws hold, respectively, up to a "weak" and a "strong" notion of equivalence. The main result is that the weak class of strategies corresponds precisely to those inducing Street fibrations over the game. We also show how the established "thin" approach to symmetry also fits in this general framework. A second contribution is a formal connection between games and setoid-valued profunctors. This follows a long tradition of relating games and relational models, but here additionally includes a very general model of symmetries. Our characterization of strategies as Street fibrations makes the connection to profunctors significantly easier to establish.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-29T19:13:28Z
Adrian de Wynter
arXiv categories: cs.LO, cs.AI, cs.CL

We introduce Type-6 logic, a variant of dynamic epistemic logic augmented with two operators (uncertainty and recurrence), designed to model the inferential dynamics of contemporary large language model (LLM) chain-of-thought (CoT) reasoning. Type-6 accounts for common LLM reasoning pathologies such as unlicensed revision, enthymemes, loopbacks, and unverifiable/incorrect claims. We propose a verifier based on Type-6 logic that builds a graph out the trace, and checks it against Type-6's axioms and inference rules. We evaluate our framework on LLM-generated CoTs four splits spanning formal and informal reasoning. Our verifier detects structurally unsound reasoning steps that surface-level heuristics miss, and allows for easy visualisation of the model's reasoning process. In our corpus, our verifier shows that derived contradiction is the most common hard-fail category in CoT, and that only about 3\% of the propositions of a trace have impact on the final derivation. Ablation studies show that other verification methods (LLMs-as-judges, other neurosymbolic approaches, etc.) cannot be considered interchangeable: for example, agreement between LLMs-as-judges and LINC is $\kappa \approx 0.034$, and this persists within a method across underlying models. Type-6, however, is the most agreed-with method amongst the ones we tested. We prove our verifier runs on average-case linear time; and release our logic specification and artefacts.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-29T19:27:09Z
Aidan Healy, Bartek Klin
arXiv categories: math.LO, cs.CC, cs.LO

We determine the decidability of Karp's NP-complete problems on structures which are first-order definable over the theory of equality, also known as orbit-finite sets with atoms or nominal sets.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-29T20:21:25Z
Volkan Da\u{g}l{\i}, Zerrin Da\u{g}l{\i}, Da\u{g}han Da\u{g}l{\i}
arXiv categories: cs.LO, cs.SC

We present gap-lean4-port (Release v0.2.0), a machine-checked formalization of foundational algorithms in computational discrete algebra and permutation group theory within the Lean 4 interactive theorem prover and Mathlib4. While modern proof assistants feature extensive abstract algebraic hierarchies, constructive and operational permutation group algorithms, such as Charles Sims' 1970 Schreier-Sims algorithm, transversal tree lookups, and backtrack ordered partition refinement, have remained largely unformalized in dependent type theory. Here, we formalize the operational algorithmic core of the Groups, Algorithms, Programming (GAP) system library across four foundational modules, proving 35 machine-checked theorems with zero unproven conjectures (sorry) and zero custom axioms under standard Lean 4 foundations (propext, Classical.choice, Quot.sound). We machine-check: (1) Schreier-Sims stabilizer chain hierarchies (StabLevel, StabChain) and the invariance of incremental transversal tree extensions (extendSchreierPoint_invariant); (2) single-level and multi-level Schreier sifting reductions (siftOneLevel, siftFull), proving that full sifting strictly fixes all base points (siftFull_fixes_all_basePoints); (3) constructive soundness and completeness of Base and Strong Generating Set (BSGS) membership testing (membershipTestKnownBase_iff_mem); (4) backtrack ordered partition cell refinement (splitCellByPred), proving mutual cell disjointness, union conservation, and exact cardinality preservation; (5) cyclotomic extension rings Z/nZ(eps_m) and machine-check GAP's exact size theorem |Z/nZ(eps_m)| = n^m; and (6) executable Bezout inverses via Extended Euclidean GCD (Nat.gcdA) over residue rings Z/nZ. The entire codebase compiles deterministically under 'lake build RequestProject' and is openly available at https://github.com/pCwOrM/gap-lean4-port.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T05:18:02Z
Nandakumar Edamana, Piyush P Kurur, Unnikrishnan Cheramangalath
arXiv categories: cs.LO

We give a new multiplication algorithm for tristate numbers improving upon the state-of-the-art implementation from the Linux kernel in terms of precision and formal proofs. Our algorithm is significantly more precise as shown by experimental evaluation (at the peak, giving better results in 95.59% cases compared to the previous work for 31-bit samples). Importantly, we achieve this additional precision with performance comparable to the previous algorithm, as demonstrated by benchmarks. Finally, we formalize and prove the soundness of the algorithm in the Rocq proof assistant, adding to the trust in the resulting implementation. Our algorithm is now part of the upstream Linux kernel. Our soundness proof in Rocq for the new multiplication algorithm works for all bit widths, while the SAT/SMT-based machine-checked proof accompanying the previous algorithm was restricted to 8 bits. We also provide Rocq proofs for the soundness and optimality of the newly added tnum union operation and the existing tnum addition algorithm from the Linux kernel. Our optimality proof for tnum addition presents a simpler and straightforward lemma compared to prior work.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T05:27:26Z
Yuqing Zhai, Xiaohong Chen, Lingming Zhang, Sriram Vishwanath, Grigore Rosu
arXiv categories: cs.SE, cs.AI, cs.LO, cs.PL

Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K framework with a kit of procedures for constructing specifications, repairing proofs, and auditing their adequacy. A human-guided development campaign on HumanEval, a benchmark of 164 Python programming tasks, achieves a 164/164 success rate with the semantics and the kit, measured by final AI audit Pass verdicts after two targeted repairs. To examine whether auditing detects problems that successful proofs leave unresolved, we construct 12 author-reviewed pairs of clean and defective packages. Every package passes its K proofs, and completed audits identify all defects and accept all clean packages. We then use KleverBench to test specification and proof construction for 31 programs with changed operator meanings. Comparisons with complete acceptance rules and equally long generic advice yield mixed results across two model and budget settings, motivating further work on selecting useful guidance within resource limits. Human-reviewed Optimism proofs establish expected pause reverts for six operations within declared input bounds under London semantics with unbounded gas. We report progress, difficulties, and lessons toward agents that deliver programs with checkable correctness arguments.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T12:09:44Z
Han Xiao
arXiv categories: cs.LO, math.LO

We prove that $\mathsf{Cheq}$ is not finitely axiomatizable, resolving a longstanding open problem in intermediate and modal logics. We further prove that the undecidability of Medvedev logic implies the undecidability of $\mathsf{Cheq}$.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T13:58:46Z
Adrian Wurm
arXiv categories: cs.LO, cs.CC, cs.CR, cs.LG

Certifying a deployed neural network raises decision problems that the verification literature has not classified: whether the model carries a backdoor planted in its training data, whether a fault in its stored parameters can drive it into an unsafe state, whether its output leaks a private part of its input. We formalise eight such problems and classify what we can. The organising observation is a logical one. The function computed by a piecewise linear network, together with all its node values, is definable by a quantifier-free formula of real addition of size linear in the network, so a property of the network is a quantifier-alternation sentence, which Sontag's 1985 theorem places in the polynomial hierarchy at the level of its prefix. Membership results are thus corollaries, and the argument makes plain what they need: that the quantified objects are inputs rather than the network's own parameters. Non-interference, monotonicity and counterfactual fairness have exactly the complexity of network equivalence and of interval verification, all co-NP- complete over ReLU. Detection of backdoor triggers from a quantised alphabet is Sigma_2^P-complete, one level above robustness certification, so it does not reduce to polynomially many robustness queries unless the hierarchy collapses. Inversion resistance is co-NP-complete for every l_p metric, p a fixed positive integer. Quantifying over parameters instead of inputs - the fault model of bit-flip attacks, radiation upsets and analog accelerators - makes verification exists-R-complete already for networks of identity nodes, for which every previously studied problem is in P, and it stays so when each parameter is confined to a box of inverse-polynomial width; the corresponding safety question is forall-R-complete for ReLU.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T16:14:11Z
Fernando Lucatelli Nunes
arXiv categories: cs.PL, cs.LO, math.CT

This version contains the introduction and conclusion of my PhD thesis, "Freely Generated Categorical Structures and Automatic Differentiation", together with its English and Dutch summaries. The full thesis consists of an introductory chapter, six joint research papers, and a concluding chapter, developed during my PhD studies at Utrecht University under the supervision of Gabriele Keller and Matthijs V\'ak\'ar. The research papers are available separately and are not reproduced here. The introduction presents the scope of the thesis, explains the contributions of the six papers and their connections, and introduces the categorical foundations of our approach. The guiding idea is that programming languages, viewed as freely generated categorical structures, provide a principled setting for constructing structure-preserving program transformations and proving their correctness. Automatic differentiation supplies the central application: we study forward- and reverse-mode differentiation for expressive typed languages, including higher-order functions, recursive types, iteration and partiality. The semantic requirements of these transformations also motivate independent mathematical results on free distributive and extensive categories, cartesian closedness, and Grothendieck constructions. The conclusion brings these contributions together, discusses their limitations, and outlines further directions. Throughout, the thesis develops a dialogue between theory and practice: categorical semantics guides the construction of reliable and practically useful program transformations, while the demands of computation lead to new categorical structures and results.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T20:04:32Z
Thorsten Engesser, Agata Ciabattoni
arXiv categories: cs.AI, cs.LO

Making decisions despite conflicting norms and incomplete or unreliable information is a fundamental challenge for autonomous systems. We introduce a simple doxastic deontic logic for this setting: a classically reducible fragment of Chellas' Minimal Deontic Logic, extended with explicit conditional norms and combined with multi-agent KD45, so that norms can depend on agents' beliefs about both facts and norms. On this logic we define the Doxastic Norm Compliance Optimization Problem, where an agent chooses a decision minimizing weighted norm violations. We distinguish subjective optimization (relative to the agent's beliefs) from objective optimization (relative to the actual facts). We give conditions under which (i) the two coincide and (ii) optimal decision-making can be reduced to weighted partial MaxSAT in polynomial time.

arXiv abstract · PDF

Logical methods · primary corpus · published 2026-09-30T23:49:42Z
Shuo Pang
arXiv categories: cs.CC, cs.LO

For every constant-width CNF, we show that linear degree in polynomial calculus (PC) implies exponential size in resolution over constant-degree polynomials, over the same prime field. Applications include exponential lower bounds for CNFs in $\operatorname{Res}(\operatorname{PC}_r/\mathbb{F}_p)$ and hence in $\operatorname{Res}(\oplus_p)$, separations between different moduli, improved lower bounds for $\operatorname{Res}(k)$ up to $k=\varepsilon\log n$, proof-search consequences, and an implication of super-polynomial $AC^0[p]$-Frege bounds from very strong PC degree lower bounds. The proof uses the common-multiplier idea isolated from Braun [arXiv:2609.23015] to construct a Razborov--Smolensky approximation that preserves inferences, without introducing extension variables. The approximation errors are measured by ranks of the multiplication maps induced by the error-witness polynomials, modulo bounded-degree PC consequences.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T00:22:13Z
Arun Govindankutty
arXiv categories: quant-ph, cs.ET, cs.LO

Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates superposition tracking from basis-state behavior, enabling SMT-based verification of fixed-size error-detection and entanglement circuits built from H, X, and C-NOT gates. This paper extends the framework in five directions. First, we generalise correctness properties to parametrised repetition and concatenated phase-flip codes with up to 101 logical elements. Second, we verify syndrome extraction for CSS codes specified by arbitrary parity-check matrices, including the Steane, [[15,7,3]] Hamming, [[15,1,3]] Reed-Muller, and rotated surface codes with distances up to 101. We consider arbitrary error patterns, detection up to a specified weight, and recovery using a classical decoder, with counterexamples beyond each code's correction or detection capability. Third, we characterize the {H,X,C-NOT} fragment for which the abstraction faithfully represents Hilbert-space semantics. We prove soundness, demonstrate necessity with counterexamples, validate the characterisation against state-vector simulation, and prove the six lemmas from the original work. Fourth, a mutation study using 13 operators identifies equivalent mutants and detects all 622 non-equivalent mutants within the evaluated fault model. Fifth, a direct Z3 implementation verifies GHZ circuits with up to 262,144 qubits across three topologies on a 16GB laptop. Random H+C-NOT networks show verification cost rises sharply with depth when outputs depend on many inputs. The approach does not target general stabilizer circuits, Y-type stabilizers, fault-tolerant protocols, or physical noise; we identify extensions needed to address these cases.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T01:00:35Z
Naing Oo Lwin
arXiv categories: cs.SE, cs.AI, cs.LO

Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification. The framework combines isolated workspaces, Lean tools, and fresh review with statement comparison, axiom audits, and independent proof checking where supported. Verification evidence and reviewer decisions are bound to the same candidate artifact, making acceptance traceable. We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track. On the 100-task VeriSoftBench subset, integration with FORALLLEAN-AGENT raises benchmark-rule success from 93 to 100 for GPT-5.6 Sol at low effort while reducing cost from $69 to $62. The PutnamBench evaluation accepts all 672 problems at an average of $4.72 each. These results show that agent harness design can improve correctness and efficiency while providing evidence beyond aggregate solve counts.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T03:29:09Z
Junyi Liu, Tianchi Ren, Fei Guan, Xu Jiang, Zhe Jiang, Wang Yi, Nan Guan
arXiv categories: cs.LO, cs.AI

Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa. This work presents ProsaBuddy, an LLM?based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints. It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof. We evaluate ProsaBuddy on a mini benchmark drawn from real-time scheduling literature. Experiment results show that ProsaBuddy significantly outper?forms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T07:39:46Z
Tom Verhoeff
arXiv categories: math.CO, cs.DM, cs.LO

In 1965, D. H. Lehmer conjectured that the permutations of every multiset admit an imperfect Hamiltonian traversal by adjacent swaps: a walk in the neighbor-swap graph that visits every word, with some words visited twice in order to reach a neighbor and return. The question is posed as an unsolved research problem in Knuth's Art of Computer Programming. Verhoeff (2017) chose the stutter words, in which every domino is a double, as the words to be reached this way, and reformulated the conjecture as the Hamiltonicity of the graph $N(S)$ on the non-stutter words, with two exceptional families --- binary signatures with an odd multiplicity, and the permutations of $(2k,1,1)$ --- that admit a Hamiltonian path but no cycle. This article proves the reformulated conjecture, and with it Lehmer's conjecture. The key structure is a partition of the words into hypercubes: the swaps inside dominoes turn each class of words with the same domino contents into a hypercube, and the stutters are exactly the $0$-dimensional classes. When every multiplicity is even, Hamiltonian cycles of the hypercubes are glued along a spanning tree, with no finite check. The case of exactly one odd multiplicity reduces to the all-even case and to a theorem of Stachowiak (1992), the one inherited Hamiltonicity input, which also settles two or more odd multiplicities. The only finite ingredients are two explicit cycles, of 28 and 84 words. Every construction is implemented in Python and checked against brute-force graphs, and the proof is formalized in Lean 4 over Mathlib.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T08:52:29Z
Aldo Gangemi, Rita T. Sousa, Luigi Asprino, Giorgia Lodi, Andrea G. Nuzzolese, Valentina Presutti, Johannes Gysen, Diana F. Sousa, Luigi Spagnolo
arXiv categories: cs.AI, cs.LO

This paper presents the European Crisis Management Ontology (ECMO), a modular OWL-based ontology intended as a cross-sectoral reference for disaster risk reduction and response. ECMO is designed to be organised as a network of ontological modules. Among the modules, ECMO-CORE captures fundamental crisis management concepts such as hazard, event, exposure, impact, and response measure and uses ontology design patterns and the OWL2 punning technique to resolve ambiguities between hazard types and event manifestations. In addition, domain-specific modules are defined as in the case of the public health module aligned with SNOMED CT and ICD-11. To demonstrate the resource's utility, we used ECMO to represent the data of the Epidemic Intelligence from Open Sources system of the Joint Research Centre to generate an end-to-end pipeline that populates an ECMO-compliant knowledge graph from unstructured epidemiological news. Initial results demonstrate that ECMO provides the formal guardrails necessary for consistent and unified knowledge representation and integration. The ontology is publicly available at https://doi.org/10.5281/zenodo.20070268 and is released under the Creative Commons Attribution 4.0 International (CC BY 4.0) license.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T12:48:54Z
Yuzhou Wang, Emile Anand, Ijay Narang
arXiv categories: cs.CV, cs.AI, cs.LG, cs.LO

Reliable visual reasoning requires composing multiple visual observations and returning consistent answers to logically equivalent questions. We introduce Hob-VL, a benchmark for visually grounded Boolean reasoning. Hob-VL comprises two tasks: (1) evaluating whether a Boolean rule holds in an image, and (2) identifying the (unique) object satisfying a Boolean description. Hob-VL contains 6,000 human-verified balanced Yes/No questions, each defined by a Boolean combination of ten visual statements, across 1,000 generated scenes and 46 diverse labeled photographs, along with 1,000 object-identification questions over the same photographs. Our question families are deliberately constructed to challenge reasoning through misleading local cues and nested logical operations, and include symbolic and structured natural-language presentations. Across eight model configurations with thinking disabled or minimized, Boolean accuracy ranges from 48.52% to 50.57%, while the identification accuracy reaches at most 43.0%. A thinking-enabled GLM configuration achieves uneven gains while retaining substantial errors and inconsistencies. Hob-VL exposes these failures through executable reference answers and matched evaluations.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T14:32:10Z
Lu-Chin Chang, Suguman Bansal
arXiv categories: cs.AI, cs.LG, cs.LO

Reinforcement learning (RL) for reachability specifications is fundamental to sequential decision-making. Prior work establishes asymptotic convergence to optimal policies, but only through model-based methods that must explicitly estimate the transition probabilities of the underlying Markov Decision Process (MDP). We present Quasar, the first model-free algorithm with asymptotic guarantees for reachability on the fragment of MDPs free of non-terminal maximal end components (MECs), a building block to which every MDP reduces by the standard MEC quotient. Our algorithm follows the classical Q-learning approach, using temporal-difference updates to converge to an optimal policy without ever learning the transition probabilities. The resulting learner reduces the memory footprint from the O(|S|^2|A|) that model-based methods require to O(|S||A|). On the standardized Quantitative Verification Benchmark Set, our algorithm converges to the optimal policy with orders of magnitude fewer samples than the previous model-based state-of-the-art. Together these results are a concrete step toward the practical deployment of reachability learning and, with it, of specification-guided RL.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T15:12:20Z
Thomas Perez, Titouan Carette
arXiv categories: quant-ph, cs.LO

Local fermionic mode (LFM) based quantum computation has pure state spaces that are isomorphic, via the Jordan-Wigner representation, to qubit state spaces, but its compositional structure is subtly different. Indeed, the algebraic formalism specifying how to embed fermionic systems underlies a notion of parallel composition, for which, in general, the usual interchange law of monoidal categories fails. We give a categorical account of this phenomenon. Starting from the CAR-algebraic semantics of fermionic gate application, we show that LFM processes form a symmetric premonoidal category whose centre is precisely the even, parity-preserving subcategory. The same processes can alternatively be organized with the ordinary tensor product and a fermionic presymmetry that is natural exactly on even maps. To reason diagrammatically in this latter presentation, we introduce pronaps, a relaxation of the notion of prop, in which permutations are not-necessarily-natural, and use them to organize a hierarchy of fragments of the fermionic ZW calculus relevant to the study of fermionic circuits on physically motivated gate-sets. We then extend scalable diagrammatic notation to pronaps. In this setting, syntactic sugars inspired by SZX and GSA are defined, with the specificity that matrix arrows encode minors and determinants, while graph triangles encode pfaffians of principal submatrices. These constructions yield elegant normal forms and completeness proofs for our presentations of the EoW, FoW, EW, and FW fragments. In particular, the FW presentation gives a new normal form for the matchgate fragment, distinct from the rWGS-X normal form of the planar-W (pW) presentation of the same category. The resulting framework connects fermionic circuit semantics, diagrammatic rewriting with scalable notations, and the algebra of determinants and pfaffians.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-01T21:22:18Z
Jo\~{a}o Ara\'{u}jo, Jan H\r{u}la, Mikol\'{a}\v{s} Janota, Edmond W. H. Lee, Bartosz Naskr\k{e}cki
arXiv categories: cs.LO, math.GR

We introduce SemiBase, a project that computes and formally certifies finite identity bases for small semigroups. Deciding finite basability is undecidable for finite algebras and remains open for finite semigroups. The task requires a proof that a candidate basis is complete, or a proof that none exists, rather than a single first-order validity query. LLM-guided agents search for these proofs; a referee agent rebuilds them from source, and the Lean kernel checks the resulting corpus in a final audit. Humans choose targets and approve final outcomes. We certify every semigroup of order at most 6: all 1309 semigroups of order at most 5 and all 15973 of order 6, including proofs that the four known nonfinitely based semigroups have no finite basis. The bases for order 6 define 505 distinct varieties, whose inclusion order Vampire determines except for four pairs. The resulting catalogue is a machine-checked account of results scattered across the literature and a tested foundation for order 7.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-02T02:04:34Z
Toshiaki Koike-Akino
arXiv categories: cs.LG, cs.ET, cs.LO

Can programmable radio propagation serve as computational depth rather than only as a communication channel or one-shot analog transform? We introduce the Radio Alternating Operator Ansatz (RAOA), a recurrent computing architecture that alternates an energy-derived problem update with a mixing update over a persistent latent state. Recomputing the problem field after each mix makes repeated passes compositional even when the same learned controls are reused across depth. We evaluate this idea through exact discrete optimization, constrained programmable-propagation simulation, and pretrained-model adaptation. On discrete objectives, repeated execution can improve solution quality without increasing the learned-control count, and the same formulation handles higher-order interactions directly. A passive phase-only free-space model further shows that the required operators can be approximated by programmable propagation while retaining useful downstream behavior despite realization error. When inserted as a zero-initialized residual adapter, RAOA adapts pretrained language models with WikiText performance close to a matched shallow MLP across three model families, while reasoning-task transfer remains model-dependent. Together, these results connect alternating-operator computation, programmable radio propagation, and neural adaptation within one recurrent framework. The RF realization evidence is simulation-based rather than a hardware demonstration.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-02T05:02:06Z
Naing Oo Lwin
arXiv categories: cs.SE, cs.LO, cs.PL

Keeping a Python program and its formal guarantees aligned is a continuing maintenance problem. Specifications must describe the implementation that actually runs, and updates must preserve the behavior on which existing callers depend. VeriPy brings these obligations into a common workflow for annotated Python components. Developers and agents express contracts, invariants, and proof hooks as Python comments, then refine checked auxiliary lemmas using source-located diagnostics. Direct encoders produce Dafny or Lean artifacts while retaining admitted executable bodies and explicit models of their dependencies. A relational product checks whether an updated component still admits old inputs and preserves returned values and modeled exceptions. The resulting workflow connects source-level proof development with functional verification and backward compatibility, recording the assumptions under which each guarantee applies. The code is available at https://github.com/astrio-labs/veripy.

arXiv abstract · PDF

Verification systems · primary corpus · published 2026-10-02T08:06:51Z
Nao Hirokawa, Teppei Saito, Teppei Tanaka, Wataru Yachi
arXiv categories: cs.LO

We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity assignment and reification, to overcome difficulties in handling partial and variable application.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-02T08:38:22Z
Clemens Bombach, Rajmadan Lakshmanan, Marco Ragni
arXiv categories: cs.LO, cs.AI, q-bio.NC

Understanding how humans reason -- and how reasoning responses vary across tasks and individuals -- remains a core challenge for modeling and explanation in cognitive science. We investigate the stability of response patterns within reasoners and whether variation in these patterns can be used to predict learning effects. We introduce a formal, geometry-based method to quantify distances between individual reasoning patterns and their internal variability, grounded in heuristic theories. The proposed framework is tested against experimental data via generalized linear mixed-effects models and clustering, where we find that our proposed variation measure interacts with correctness to predict performance gains. Moreover, we find that reasoning patterns are stable over time within the same reasoner. The method is general enough to be applied to other reasoning domains.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-02T14:16:56Z
Johannes Weiser, Zafer Esen, Philipp R\"ummer
arXiv categories: cs.LO, cs.PL

Constrained Horn clauses (CHCs) are a fragment of first-order logic widely used as an intermediate language for verification. We study constrained resolution as a calculus for reasoning about the satisfiability of sets of CHCs. Constrained resolution forms a simple alternative to model checking algorithms such as CEGAR and IC3 and is here shown to exhibit complementary features. We show that, when CHCs encode programs, forward symbolic execution corresponds to positive unit hyper-resolution, and backward symbolic execution to SLD resolution, which are special cases of constrained resolution. We formalize forward and backward reasoning for linear and non-linear CHCs and transition systems, prove refutational completeness under fair strategies, and develop subsumption criteria for pruning redundant derivations. We moreover show that backward resolution with subsumption generalizes $k$-induction to non-linear CHCs, and that forward constrained resolution is related to the problem of constructing proofs in incorrectness logic. Lastly, we provide an experimental evaluation in the Eldarica CHC solver on benchmarks from CHC-COMP.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-02T16:33:02Z
Arnar \'A. Kristj\'ansson
arXiv categories: math.CO, cs.DM, cs.LO

We refute the Strong Roberson Conjecture, which asserts that adding any graph outside a class closed under minors and disjoint unions strictly increases the distinguishing power of homomorphism counts from that class. More precisely, we construct connected graphs $H$ for which counts from graphs excluding $H$ as a minor determine the number of homomorphisms from $H$ to any target graph. We also refute the analogous conjecture with immersions in place of minors. We give explicit infinite families of excluded graphs, including cubic bipartite graphs that yield counterexamples for both relations. The proof introduces a method for deriving exact homomorphism count dependence from modular equivalences. We obtain these equivalences for infinitely many primes using prime-order automorphisms of graphs that exclude their orbit quotients as minors or immersions.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-02T19:56:10Z
Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi
arXiv categories: cs.LO, cs.AI, cs.SE

VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that proof generation is the bottleneck for frontier models: given the specification and the code, the best model produces an accepted Verus proof for 13.95% of the problems on the first attempt. We report on solving the same proof-generation task with Rust-Prover, a verifier for Rust backed by Lean 4. The Verus specification and the Rust code are restated and translated into Lean, each specification becomes a theorem, and agents prove the theorems with Lean's kernel as the final check. All 1325 theorems of all 1007 problems were proved. 1259 of them were proved in one run of under 32 hours on Claude Opus 5.5, at a median of 3.2 minutes and $1.17 per proof, and 70% of them on the first iteration. The restated specifications were checked against the benchmark's test suites, and reviewed where no suite applies. None was wrong or weakened. The translated Lean programs were run on 21,413 of the benchmark's test cases and produced the same output as the Rust programs on every one. Across four Claude and four GPT models at five reasoning-effort settings, every current frontier model proves nearly all of a ten-theorem sample at every setting, and more effort raises the cost without raising the number of proofs. The cheapest Claude setting, Sonnet 5.5 at low effort, proves all of the 50 hardest theorems. We also rerun the benchmark's own Verus protocol with Claude Opus 5.5 on the 50 problems with the longest reference proofs. Opus 5.5 alone fails to prove one of them.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-03T02:37:12Z
Guilherme V. Toledo, Yoni Zohar
arXiv categories: cs.LO

Shininess is one of the main theory combination methods in Satisfiability Modulo Theories. We present two infinite families of generalizations of it: one involving a property between gentleness and shininess, which helps us see gentleness itself as a variation of shininess; and another having no further computability requirements on the weaker theory, in addition dropping the need for smoothness. We prove these methods sharp, and compare them with existing methods.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-03T04:03:19Z
Ruoran Xu
arXiv categories: cs.LO

Formal theorem proving increasingly combines learned semantic guidance with verified symbolic execution. The quality of the symbolic search substrate therefore determines how much useful mathematical structure can be accumulated, reused, and exposed under a finite inference budget. We introduce ViaLean, a Lean4 prover that organizes symbolic reasoning as bounded exploration of a persistent proof-state graph. Its search preserves coverage across complementary reasoning modes, merges semantically equivalent goals, retains verified intermediate structure, and observes short symbolic futures before committing to a transition. On the complete miniF2F test split, the model-free configuration solves 122/244 problems (50.0% pass@1). Historical and recent symbolic reference points range from Lean's earlier tidy search to modern grind and SMT-backed verification, showing that proof-space organization remains a substantial source of capability. The same persistent state also provides a natural interface for neural--symbolic agents: neural reasoning can operate over verified regions and intermediate objects while Lean continuously expands and validates the local proof space.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-03T13:20:23Z
Marianna Girlando, Fabrizio Montesi
arXiv categories: cs.LO

Modal logic comprises a broad family of logics to reason about relational structures. The literature presents many such logics, displaying diverse operators, semantics, and applications. This plurality is reflected in a zoo of mechanised modal logics, which often duplicate syntax, semantics, metatheory, and reasoning infrastructure. We present a library-grade formalisation of modal logic in Lean, developed as part of CSLib (the Lean Computer Science Library) and designed around two complementary forms of reuse: vertical reuse, whereby specialised logics inherit from common abstractions, and horizontal reuse, whereby modal logic becomes a reasoning tool for independently formalised domains. Our development provides a generic framework for polyadic modal languages, reusable metatheory and proof automation, and derived interfaces for specialised modal logics. We exemplify our infrastructure by deriving basic modal logic, basic temporal logic, and Hennessy-Milner Logic; the latter subsumes and extends CSLib's previous implementation while reducing its logic-specific code by 67%. We further apply the same modal infrastructure to reasoning about mathematics (radicals of ideals), theory of programming languages (the type safety strategy for the simply typed $\lambda$-calculus), and concurrency theory (reasoning about processes in the Calculus of Communicating Systems). Our experience suggests that reuse, automation, and integration with the strong Lean ecosystem should be treated as first-class design concerns when formalising theories for shared libraries.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-03T15:09:25Z
Yoshiki Nakamura, Yuya Uezato
arXiv categories: cs.DB, cs.CC, cs.LO

We study the fine-grained complexity of evaluating Boolean bounded-variable first-order queries over sparse relational structures. For every fixed $k \ge 2$, every relational signature, and every fragment between $k$-variable primitive positive ($\mathrm{PP}^{k}$) and first-order ($\mathrm{FO}^{k}$) logic, we prove, assuming the Sparse MAX-$3$-SAT hypothesis, a dichotomy theorem for evaluation in $O(m^{k-\varepsilon})$ time, where $m$ is the number of tuples in the input structure. The only tractable cases fall into three families: (1) three-variable fragments, (2) two-variable fragments, and (3) fragments over unary signatures. On the hard side, for every fixed $k \ge 4$ and every $\varepsilon > 0$, there is a fixed sentence $\varphi_\varepsilon$ in $\mathrm{PP}^{k}$ over a single binary relation symbol, depending on $\varepsilon$ but not on the input structure, whose evaluation cannot be performed in $O(m^{k-\varepsilon})$ time. For the tractable cases, we show that the evaluation problem can be solved in $2^{O(|\varphi|)} \cdot m^{k-\varepsilon}$ time for some $\varepsilon > 0$. Moreover, every tractable fragment reduces, with a $2^{O(|\varphi|)}$ blowup in formula size under DAG representations, to one of the following query languages: (1) Tarski's calculus of relations, (2) a new Boolean modal logic for sparse model checking, and (3) one-variable counting logic.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-03T20:25:04Z
Benjamin Icard, Gauvain Bourgne, Jeanne Bonnaventure, Jean-Gabriel Ganascia
arXiv categories: cs.AI, cs.LO, cs.MA

In life-or-death situations, a benevolent lie may appear more moral than telling the truth. Yet such lies can backfire, producing unintended and sometimes fatal consequences. This tension, famously disputed by Kant and Constant in 1797, applies not only to lying but to assertive speech acts in general, raising the question of which utterance should be chosen when moral stakes are high. We present a logical framework for the ethical evaluation of speech-act utterances based on agents' beliefs. Implemented in Answer Set Programming (ASP), the framework assesses utterances under deontologism, consequentialism, and principialism, and is illustrated on Sartre's The Wall (1939), a reworking of that controversy in which lying leads alternately to rescue and to death. Our setting is general by design: as two variants show, accommodating a new moral situation amounts to adjusting parameters, not rules.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-04T12:51:44Z
Chuangjie Xu
arXiv categories: cs.LO

We revisit the Gentzen-style monadic translation of G\"odel's System T. The translation is parametrized by a nucleus, a monad-like structure that need not satisfy the monad laws. A fundamental theorem of logical relations provides a uniform correctness argument for its instances. By choosing suitable nuclei, we obtain majorants, moduli of pointwise and uniform continuity, internal dialogue trees, and functionals of general bar recursion, all represented by terms of T. The internal dialogue-tree application gives a simpler construction, with correctness established directly using Church-encoded terms. We also extend the translation and its fundamental theorem to sums and finite lists. Finally, we develop the Kuroda-style translation and its continuity instance, comparing the moduli obtained with those of the Gentzen-style translation.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-04T14:34:24Z
Nikolas M\"ahlmann, Patrice {Ossona de Mendez}, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, {Dimitrios M.} Thilikos, Alexandre Vigny
arXiv categories: cs.LO, cs.DM, math.LO

We introduce \emph{sub-connectivity logic}, denoted by $\textsf{FOscon}$, an extension of first-order logic for graphs with a specified set $Z$ of admissible edges. Its additional atom $\textsf{scon}(x,y;\bar z)$ asserts that $x$ and $y$ are connected by a path using only edges of $Z$ and avoiding the vertices in $\bar z$. Our main structural result states that, for every weakly sparse graph class $\mathscr C$, the class of all expansions of graphs in $\mathscr C$ by rooted spanning forest orders has bounded twin-width if and only if $\mathscr C$ excludes a fixed minor. When $\mathscr C$ excludes a fixed minor, we can also compute an additional linear order that preserves bounded twin-width in polynomial time. We translate $\textsf{FOscon}$ into first-order logic over an expansion by a depth-first spanning forest order of the admissible-edge graph. Combining this translation with our structural result, we obtain a model checking algorithm for $\textsf{FOscon}$ with running time $f(|\phi|,h(G))\cdot |G|^c$, where $f$ is computable, $c$ is an absolute constant, and $h(G)$ is the Hadwiger number of $G$. The translation and model-checking algorithm extend to binary relational structures, with the Hadwiger number measured on the Gaifman graph. For a graph class $\mathscr C$ let $\mathscr C_Z:=\{(G,Z):G\in\mathscr C,\ Z\subseteq E(G)\}$. We show that for every weakly sparse graph class $\mathscr C$, the class $\mathscr C_Z$ is monadically dependent for $\textsf{FOscon}$ if and only if $\mathscr C$ excludes a fixed minor. For monotone classes that admit efficient minor encodings, a corresponding hardness result makes this frontier computationally tight. We give applications to combinatorial reconfiguration and solution discovery problems, and study a guarded extension of $\textsf{FOscon}$ motivated by database queries.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-04T15:56:51Z
Jinwook Kim (for the Oraclizer Core Team)
arXiv categories: cs.CR, cs.LO

GKR soundness bounds false output claims about arithmetic circuits, but an application also needs assurance that its circuit encodes the intended state transition. We machine-check this connection for sparse-Merkle membership, non-membership, and update in Isabelle/HOL. A compiler model relates circuit acceptance to transition validity in both directions. A reusable protocol model assembles layer reduction, wiring-predicate extensions, and imported sumcheck soundness into a bound on an explicit chain event. Their composition transfers semantic invalidity to that bound, with the witness fixed before the challenge experiment. Concrete interpretations and premise activations expose vacuous assumption sets that a clean build alone would miss. A further development constructs the exact degree-four KoalaBear extension, lifts the base-field circuit objects, and establishes the assembly bound with denominator $p^4$ under its stated challenge assumptions. An executable Rust prover accompanies the model. Creusot/Why3 contracts provide a partial implementation connection, and a conditional theorem relates successful verifier traces to the model event under an undischarged value-correspondence premise. Neither the transcript's online challenge distribution nor a multi-round Fiat--Shamir reduction is established. The contribution is the composition, within one proof assistant, of compiler correctness with a GKR assembly model, together with an explicit account of the remaining implementation and cryptographic obligations.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-04T16:48:12Z
Prithwish Jana, Viet Bach Hoang, Logan Luna, Viresh Pati, Akash Singirikonda, Cy Xie, Lisa Carbone, Wuyang Chen, Walter Moreira, Joe Stubbs, Sriram Vishwanath, Vijay Ganesh
arXiv categories: cs.LO, cs.AI, cs.LG

Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.

arXiv abstract · PDF

Automated verification · primary corpus · published 2026-10-04T22:13:46Z
Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang, Beyazit Yalcinkaya, Sanjit A. Seshia
arXiv categories: cs.LO, cs.AI, cs.RO, cs.SE, cs.SY, eess.SY

In safety-critical domains such as autonomous driving, systems must be evaluated across a large number of environment conditions, often represented as composite scenarios built from primitive scenarios. Existing statistical model checking (SMC) approaches analyze each composite scenario independently, requiring many expensive simulations and resulting in substantial redundant computation when scenarios share common structure. This work introduces a scenario-based compositional SMC framework for safety and co-safety specifications, enabling efficient analysis of composite scenarios. Our approach decomposes scenarios into primitives and specifications into sub-specifications, verifies each primitive independently, and composes the resulting statistical estimates using importance sampling and kernel density estimation. Our empirical evaluation shows that the proposed framework can accurately answer verification queries for previously unseen composite scenarios while reducing simulation cost through parallelization and trace reuse.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-28T00:50:30Z
Piyush Jha, Aishik Ghosh, Vijay Ganesh
arXiv categories: cs.AI, cs.PL, cs.SE

The upgrade and rewriting of large scientific codebases has traditionally been a major challenge. While evolutionary search with large language models (LLMs) can port and accelerate legacy code, repair feedback in prompts alone does not prevent subsequent candidates from repeating the same errors. We introduce Certificate-Driven Evolutionary Search (CDES), which extends evolutionary search with enforceable restrictions derived from failed candidates, recorded as certificates of assumptions, checker evidence, and justified restrictions. Its control logic enforces these restrictions through rejection, backtracking, and targeted repair while preserving compatible edits. We apply CDES to CPU-to-GPU translation of two particle-simulation functions from the Geant4 toolkit, evaluated with a harness that goes beyond unit tests to combine formal checks, numerical comparisons, physics checks, and GPU safety tests. Generated implementations achieve 13.78x and 23.54x function-level speedups over CPU code, including data conversion and transfers; for one function, GPU throughput exceeds an expert implementation by 14.9%, reaching 16.1% when complementary components are combined. In an ablation over execution settings, certificate feedback increases the fraction of candidates passing required correctness checks from 55% to 90%.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-28T01:30:28Z
Luke Dramko, Claire Le Goues, Edward Schwartz
arXiv categories: cs.PL, cs.CR, cs.SE

Neural decompilers are machine learning models which perform the process of decompilation, lifting code from a lower-level language to a higher one. Neural decompilers offer substantial utility relative to traditional deterministic decompilers because they can probabilistically recover information discarded during lowering, like variable names, types, and control flow structuring. However, they can also make mistakes, producing code that is not equivalent to the original, making it difficult to trust their output. In this work, we introduce Faultless, a program equivalence technique for performing translation validation on neural decompilers. Faultless compares code produced by a deterministic decompiler, which has stronger correctness properties, with that of a neural decompiler. Faultless is also useful for model evaluation, a highly related task, in which the neural decompilers' prediction is compared with a reference solution. Neural decompilation introduces significant challenges to the task of program equivalence which existing techniques are not equipped to handle, including limited extrafunctional context and systematic semantic inconsistencies in decompiled code. Faultless takes a static symbolic execution-based approach with an execution model and memory model designed to handle these challenges.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-28T08:55:53Z
Christian Kissig, Jay Richards, Mark Batty
arXiv categories: cs.PL

Lock-free synchronisation algorithms are often implemented with fallible operations, such as compare-and-swap (CAS), wrapped in unbounded retry loops. Verifying such algorithms requires considering arbitrarily many failing iterations, yielding large state spaces, compounded by the interleavings of concurrent threads. Prior work discarded failing iterations, arguing that they leave no trace in the post-loop state. Compilers and hardware reorder instructions, and load-store reorderings may cross the boundaries of failing iterations, introducing subtle concurrency bugs. We demonstrate one such bug, making use-after-free possible in a previously verified variant of Read-Copy-Update - a synchronisation primitive widely adopted in the Linux Kernel - and we provide and verify a fix. We find that practical retries in lock-free algorithms adhere to a common pattern. We introduce episodic loops, a semantic characterisation of unbounded retry loops which is syntactically recognisable in many practical cases, and synchronisation points, operations that bound both instruction reordering and state space within episodic loops. We show that SMRD - a symbolic event structure semantics for C11 programs which allows for load-store reordering - admits a finite representation in programs where unbounded loops are episodic. We further introduce a finitary operational semantics that allows safety properties to be verified in finitely many steps. For the use-after-free bug we demonstrate, verification takes a single pass over the program, linear in the program size. We provide a reference implementation of SMRD reproducing the bug and verifying the fix, and mechanise the operational semantics together with the minimal bug and its fix in Isabelle/HOL.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-28T10:58:41Z
Andrada-Livia Antoneac (Alexandru Ioan Cuza University of Ia\c{s}i, Bitdefender), Dorel Lucanu (Alexandru Ioan Cuza University of Ia\c{s}i), Drago\c{s} Teodor Gavrilu\c{t} (Alexandru Ioan Cuza University of Ia\c{s}i, Bitdefender)
arXiv categories: cs.AI, cs.PL, cs.SE

LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for verification—it becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-28T15:34:59Z
Paul Kronlund-Drouault
arXiv categories: cs.PL, cs.AI, cs.CL

Constrained decoding can enforce regular or context-free output formats, but many program-generation failures are semantic: scope, typing, and declaration effects depend on context. We present semantic grammar specifications, a declarative formalism that attaches such constraints to a context-free surface and executes them during Earley descent. Our implementation enforces \emph{safe pruning}: it rejects only prefixes whose semantic contradictions cannot be repaired by any continuation. A separate, grammar-dependent, \emph{dead-end freedom} property guarantees the existence of a realizable witness for each remaining branch. We give simple sufficient conditions based on surface productivity, type coverage, and left-to-right constraint flow. Our finite-lambda, core ML, and C-like fragments satisfy them, while the STLC instance used in our experiments does not: plain STLC can violate type coverage, and we show how restricting its type universe recovers it. A tokenizer-lifting lemma carries character-level witnesses to token sequences under an explicit vocabulary-coverage hypothesis. We validate the implementation differentially against production compilers (\texttt{ocamlc}, \texttt{cc}). Across every prefix of 65 compiler-valid programs we observe zero false prunes. The semantic oracle localizes 25/30 invalid programs mid-stream, against 0/30 for a syntax-only oracle, and agrees on 42/42 recursion probes. A twelve-model generation study, including a matched semantic-versus-syntactic ablation for nine models, finds nonnegative observed semantic-minus-syntactic point estimates for every model-language pair, with maxima of $+15.2$ points on STLC task correctness and $+14.3$ points on ML validity.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-28T23:26:12Z
Ishan K Singavarapu, Manish Bhatt
arXiv categories: cs.PL, cs.CR

Verifying large C codebases requires translating them into formally checkable semantics, but most autoformalization work reports a single aggregate success rate that conflates two different failure modes: code the translator declined to handle and code the translator translated incorrectly. We present a deterministic code-property-graph (CPG)-based exporter that translates C source into a small Lean~4 core semantics under a three-tier correctness discipline: hole-free, call-closed, and dynamic-hole-risk, that keeps these modes distinct. Applied to a re-export of the SQLite source tree (8{,}602 functions, over 1.5~million AST nodes), the exporter translates 5{,}222 functions (60.7\%) hole-free, of which only 2{,}134 (24.8\%) are call-closed, a $2.4\times$ gap a single rate would hide. Both figures are reported in a full per-construct trust ledger rather than a single score. Our main contribution is methodological: a protocol for separating constructs that are fundamentally unresolvable by whole-program static analysis (such as public API boundaries) from constructs that only look that way. For example, we retracted our own ``impossible'' classification of function-pointer/vtable dispatch after tracing a concrete counterexample in the target codebase. Separately, a search for ``more holes closed'' surfaced a latent silent-wrong-answer bug: a translation that succeeded with an incorrect result rather than declining, a failure mode we argue is more dangerous than any hole, and one a hole-count-only evaluation would never surface.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-29T10:43:39Z
Yuan Li, Hanyun Jiang, Guowei Tian, Chengpeng Wang, Peisen Yao
arXiv categories: cs.PL, cs.AI

Datalog underpins reasoning tasks such as program analysis, but its programs are hard to write. Existing synthesizers automate this task but require users to state their intent as input-output examples. Large language models (LLMs) suggest a more natural route, text-to-Datalog synthesis from a natural-language question, yet how well they do so has not been systematically evaluated. We present DatalogBench, a benchmark of 136 text-to-Datalog synthesis tasks curated from existing Datalog-based artifacts. Synthesized programs are graded by execution on held-out inputs against an oracle validated by mutation analysis. Across six LLMs and four prompting configurations, exact match peaks at 68.4%, and relation descriptions or an input-output example have only modest, model-dependent effects. Under direct prompting, most failures occur at compile time, typically because a model invents auxiliary predicates that it never declares or types consistently. Two coding agents reach up to 83.8% and eliminate nearly all such failures, leaving mostly semantic errors concentrated in recursive tasks. DatalogBench thus identifies recursive reasoning and decomposition as open challenges for current LLMs and agents, and offers a reliable, execution-grounded measure of both.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-29T19:31:43Z
Baichuan Li, Jayanaka Dantanarayana, Savini Kashmira, Lingjia Tang, Jason Mars
arXiv categories: cs.DB, cs.PL

Dependent database accesses can serialize application--database round trips on a request's critical path. Planning across traversal steps requires knowing both which relationships a computation may follow and how discovered objects become subsequent execution contexts. We identify a programming-model contract that exposes this information through inspectable access paths and explicit traversal continuation. We demonstrate this contract in Object-Spatial Programming (OSP), where walkers traverse a typed object graph and execute node-type-specific code. We introduce the Temporal Trace Graph (TTG), a bounded, request-specific graph of candidate objects and traversal-derived transitions. At walker spawn, the TTG Builder composes statically extracted access and continuation rules over the live graph from the request's starting node. An asynchronous prefetcher loads planned objects while the walker executes. We implement TTG in Jac/PostgreSQL and evaluate four applications covering linear, multi-hop, recursive, and value-dependent traversals. TTG improves end-to-end latency in three applications, achieving up to 2.99x speedup over the stock runtime. Comparisons with manually staged prefetching characterize the benefits and costs of automatic cross-step planning. The evaluation also shows that planning overhead can exceed avoided demand latency and that value-dependent control can introduce bounded overfetch.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-29T20:22:13Z
Barak A. Pearlmutter, Jeffrey Mark Siskind
arXiv categories: math.NA, cs.NA, cs.PL

We present a novel algorithm for calculating the preimage of an affine space through a product ${J}={J}_{T-1}\cdots{J}_0$ of matrices ${J}_t$ of special form: finding the largest input space $\mathbf{X}$ such that $\mathbf{x}\in\mathbf{X}$ implies ${J}\mathbf{x}\in \mathbf{Y}$, where $\mathbf{Y}$ is a given output affine space. These special matrices arise in AD, where the Jacobians $J$ describing the linearized computation have precisely this structure: the product of a series of linearized primitive numeric operations. This allows us to use the new algorithm to formulate Null-A mode preimage AD, which finds the affine preimage through the Jacobian or Jacobian transpose of a numeric computation. This is a generalization of the inverse AD problem of solving ${J}\acute{\mathbf{x}}^{\ast}=\acute{\mathbf{y}}^{\ast}$ or ${{J}}^{T}\grave{\mathbf{y}}^{\ast}=\grave{\mathbf{x}}^{\ast}$. The key is to represent affine spaces in a fashion which lends itself to efficient preimage calculation, in a compositional and quasi-local fashion, through a succession of matrices ${J}_t$. Unlike previous methods, Null-A preimage mode AD allows the ${J}_t$ matrices to be non-square, corresponding to a computer program whose number of active variables swells and shrinks during the computation. When ${J}$ is square and the initial affine space is a single point, this finds the conventional inverse. But in the more general case, having the entire affine space provides freedom which can be leveraged in a problem-specific manner. We apply the method to small problems on-CPU where the $J_t$ are linearized scalar unary or binary numeric functions; and to larger problems on-GPU where the $J_t$ are linearized aggregate array operations like convolution and attention.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-30T04:58:09Z
Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, Danyang Zhuo
arXiv categories: cs.DC, cs.PL

LLM inference systems may vary batch composition, prompt chunking, prefill/decode execution, and KV-cache reuse, eviction, or recomputation. These optimizations should not affect system outputs. Production systems, including vLLM's batch-invariant mode and SGLang's deterministic mode, target this goal but lack a formal system-level specification. We formalize deterministic LLM inference: under a fixed model and deployment configuration, requests with the same prompt and initial sampler state produce bitwise-identical logits at corresponding output positions across executions. Our tests find that these production modes produce different logits under some execution variations. To address this limitation, we present Vosti, an inference engine designed and verified against this specification. Vosti chooses kernels independently of runtime engine state and ties cached KV values to their logical token prefixes. Its proof decomposes at the engine/GPU kernel boundary: a Verus inductive proof establishes that scheduling and the paged, prefix-sharing KV-cache preserve output logits, while a Triton analyzer proves bitwise-equal selected kernel outputs across batches, query lengths, and paged KV-cache layouts. Vosti produces bitwise-identical logits across every tested execution variation and achieves performance comparable to vLLM's batch-invariant mode on decode-heavy workloads, while providing a stronger, formally verified determinism guarantee.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-30T16:44:34Z
Haokun Li, Zhongyi Wang, Guanyan Li, Xiao Yi, Shengchao Qin, Jianwei Yin, Mingshuai Chen
arXiv categories: cs.PL, cs.SE

Large language models (LLMs) have shown promise in automating interactive theorem proving, yet verification of real-world C codebases requires more than discharging individual proof goals. The task involves jointly constructing expressive function specifications and their proofs, and ensuring that library interfaces compose along intended call sequences even without a designated client. This paper presents CCV, an LLM-assisted framework for building machine-checked assurance cases: structured, auditable artifacts supporting the claim that a C codebase meets its intended requirements. To model intended cross-interface use in open libraries, CCV constructs an interface protocol that exposes permitted call sequences and resource assumptions for review, with a conditional safety guarantee under verified contracts and caller obligations. CCV coordinates two complementary phases: (i) requirement-guided analysis and bottom-up construction of candidate specifications and protocols; and (ii) modular proof construction with feedback that revises the specifications and proofs. Implemented using VST in Rocq, CCV verifies memory safety and leak freedom for all 299 function definitions across six C benchmarks, including industrial cryptographic components, with less than one person-day of reported human effort per benchmark. The guarantees depend on disclosed contracts and assumptions; human review supplies the conformance judgments connecting the formal artifacts to the intended requirements.

arXiv abstract · PDF

Programming languages · primary corpus · published 2026-09-30T18:16:21Z
Chengxi Yang, Tej Chajed, Thomas Reps
arXiv categories: cs.PL, cs.DB

Modern incremental computation theories like DBSP have enabled efficient incrementalization of general recursive computations. To do so, they require a runtime Fixpoint Detection (FPD) mechanism to detect whether an iterative computation has reached the fixpoint and thus should terminate. However, we show that the commonly suggested "FirstZero" strategy is unsound even in naturally arising cases, and that exact FPD is impossible for arbitrary DBSP circuits with expressive primitive nodes. This issue reveals a fundamental gap between the mathematical specification and implementations of such theories. To fill this gap, using DBSP as a core calculus, we develop a formal theory of convergence detection. Within this theory, we define internal convergence (IntConv) as a declarative criterion corresponding to the internal-state-stability strategy used by practical implementations, and prove that IntConv is a sufficient condition for external convergence. We then define the state fixpoint (StFP) predicate and a sound and complete StFP detector. Combining the StFP detector with fixed-input and zero-output checks yields a sound and complete IntConv detector. Moreover, for a large class of useful circuits (programs) including Datalog queries, nested while queries, and their incrementally optimized versions, we show that IntConv is not only sound but also complete (meaning any convergence in the theory implies the convergence in our criterion). As a result, our theory provides semantic guarantees for convergence detection on all these circuits. Our results are formally verified in Lean, with the formalization available at https://github.com/Arcadia-Y/fixing-the-fixpoint/.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-01T07:10:43Z
Tarik Rosin, Marcel Ullrich, Sebastian Hack
arXiv categories: cs.PL

Equality saturation is a promising technique for program optimization which sidesteps the phase ordering problem. However, current e-graph implementations grow exponentially large, even for simple examples. Many practical applications involve associative and commutative (AC) operators. We present an extension of relational e-matching that handles AC operators natively by storing terms as multisets. Preliminary results show that equality saturation modulo AC uses asymptotically less memory in certain cases.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-01T07:42:47Z
Michael Schifferer, Marcel Ullrich, Sebastian Hack
arXiv categories: cs.PL

Equality Saturation (EqSat) is a powerful technique for program optimization, systematically exploring the search space of candidate programs to overcome the phase ordering problem. However, the feasibility and performance of EqSat rely heavily on the specific rewrite rules used to derive equivalent programs. These rule sets are typically handcrafted, requiring extensive domain expertise and carrying the risk of missing valuable transformations. In this work, we evaluate Knuth-Bendix Completion (KBC) as a method for automatically generating and augmenting rewrite rules for EqSat. Our experiments show faster optimization as well as reaching better terms with previously missed optimizations.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-01T18:55:52Z
Samuel Kushnir, Kavya Sreedhar, Yeshwanth Reddy Pogula, Amir Yazdanbakhsh, Narges Shahidi, Ming Liu, Varun Gohil, Ravi Iyer, Parthasarathy Ranganathan, Christina Delimitrou, Suvinay Subramanian
arXiv categories: cs.PL, cs.AI

Co-designing ML models and the accelerators that run them is an unusual reasoning task: architects must draw confident, high-stakes conclusions about systems that do not yet exist, and the pace of both model evolution and hardware cadence means the analysis burden grows every quarter. The evidence behind each decision--hundreds of gigabytes of fresh simulation sweeps over novel design points--is by construction absent from any LLM's pretraining corpus, and there is no external literature to retrieve; naive "chat-with-your-data" approaches hallucinate exactly where correctness matters most. We present Coco (Copilot for Codesign), an agentic platform deployed with TPU architects that accelerates the co-design lifecycle of setting up experiments, sweeping simulators, and deriving insights. Coco is built as four layers: (i) a datastore that automatically registers every simulation sweep into a normalized relational schema, so agents ground every number in a SQL query rather than scraping heterogeneous files; (ii) a library of tools with typed APIs that agents compose without human orchestration; (iii) agents that encode recurring analysis workflows--most notably iso-execution analysis, which compares systems at matched execution configurations, including swept-but-dominated points off the Pareto frontier; and (iv) a platform UX whose navigation state doubles as agent context. We report early deployment experience toward a reduction in time-to-simulation and time-to-insight, and argue that co-design is a distinct agentic domain: its data must be retrieved rather than memorized, its workflows are recurring but context-dependent, and expert adoption hinges on UX that balances IDE-style control with interactive exploration.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-01T20:04:14Z
Nickil Maveli, Antonio Vergari, Shay B. Cohen
arXiv categories: cs.LG, cs.AI, cs.CL, cs.PL

Large language models (LLMs) have demonstrated strong performance in code generation, where success depends on both recalling relevant algorithmic knowledge and reasoning about how to apply it. However, existing LLM pipelines are opaque, with no explicit separation between these two components. We argue that for well-known algorithms whose canonical implementations are widely accessible in pretraining corpora, code generation is better measured as \textit{parametric code retrieval}: reproducing a named algorithm from internalised knowledge rather than synthesizing a novel one. We introduce AlgoREval, a benchmark of 599 problems spanning classical 77 algorithms across 14 domains, 7 programming languages, and 4 graph-input representations to evaluate this capability in isolation, and assess 15 models (7B--34B parameters) in a zero-shot setting. We find substantial variation in retrieval accuracy across languages and input representations, even for widely documented algorithms and show that prompt augmentation with retrieved code snippets or structured algorithmic hints improve accuracy on complex algorithms, while SFT achieves broader language gains and GRPO achieves larger per-language gains on specific languages. Together, our results establish parametric code retrieval as a distinct, measurable capability and caution against deploying AI-generated algorithmic code without systematic validation.\footnote{Code and dataset are available at https://github.com/Nickil21/AlgoREval

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-01T20:17:48Z
Nishant Kheterpal, Matthew Keenan, Cyrus Omar, Jean-Baptiste Jeannin
arXiv categories: cs.PL

This paper describes a mathematics interface intended for both educational applications and exploratory mathematics. Both learners and mathematics practitioners often use pen and paper or a whiteboard to perform equational reasoning, manipulate expressions, or construct proofs. These workflows lead to a variety of problems: transcription errors, tedious writing and notation, and/or unclear standards for proof justification. We extend the Hazel Prover, an equational-reasoning interface in the Hazel live programming environment, to add capabilities for exploratory mathematics, with varying levels of verbosity and automation aimed at both students and expert users. Students require more deliberate practice when learning mathematical concepts and correspondingly more verbose justifications, while experts may benefit from significant mathematical automation. With this in mind, our interface supports multiple levels of mathematical automation and simplification, grounded in a rewrite search architecture. For expert users, motivated by a gap in the accessibility of formal methods, we support proof export to the Rocq theorem prover, extending this rewrite search to proof tactics. This paper closes with several case studies covering elementary- to college-level mathematics.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-02T00:29:29Z
Byeongjee Kang, Jan Hoffmann, Limin Jia, Brandon Lucia, Feras A. Saad
arXiv categories: cs.PL

Intermittent computing enables batteryless embedded devices to operate in harsh environment, but frequent power failures interrupt program execution and require careful management of state across power cycles. The core challenge is to guarantee both memory consistency and forward progress while minimizing the energy overhead of checkpointing. Recent compile-time approaches identify regions that fit in the energy buffer. At runtime, the device waits and recharges between the regions. However, they still rely on greedy or path-local heuristics that commit to local decisions and can miss globally lower-overhead boundary placements. To address this limitation, we present Bao, a system that jointly finds optimal energy-aware region formation and memory allocation decisions with formal correctness guarantees, by formulating it as a mixed-integer linear program. We prove that any feasible solution guarantees energy safety and implement our approach in LLVM. Our evaluation on 13 benchmarks across 3 capacitor sizes shows that Bao outperforms existing baselines, achieving 10% faster execution and 52% fewer region boundary hits on average compared to the best baseline.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-02T12:44:26Z
Dominik Magiera, Lukas R\"ohrig, Frank J\"akel
arXiv categories: cs.PL, cs.AI

We present WAMpy, a Python framework optimized for synthesizing Prolog programs. Unlike general-purpose Prolog systems, WAMpy targets workloads that repeatedly generate and evaluate small candidate programs. WAMpy compiles Prolog clauses into NumPy array-based WAM instructions and supports partial recompilation of hypotheses against fixed background knowledge. Performance-critical routines are accelerated using Numba just-in-time (JIT) compilation. In a benchmark of repeated compilation-and-evaluation workloads, WAMpy improves end-to-end performance compared with SWI-Prolog accessed from Python using Janus.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-02T16:46:22Z
Luca Parigi, Giuseppe Tagliavini
arXiv categories: cs.PL, cs.DC

The increasing diversity of parallel hardware challenges existing compilation flows. While OpenMP provides a portable abstraction for shared-memory parallelism, existing compilers tightly couple the frontend semantics with fixed lowering strategies. This design limits performance portability across different runtimes and architectures. In this paper, we present a modular approach to parallel code generation based on the Multi-Level Intermediate Representation (MLIR) framework. Our approach combines an OpenMP frontend with a domain-specific language (DSL) that specifies how OpenMP constructs are lowered for a target. We call this approach OpenMP meta-lowering, treating lowering as a programmable component rather than compiler-specific logic. This design provides explicit control over code outlining, data sharing, and runtime interfacing across diverse targets. We evaluate our approach on PolyBench/C-OMP across general-purpose and embedded multicore targets. Our results show that the proposed method matches the performance of state-of-the-art compiler toolchains with negligible code-size overhead (< 0.7%). Preserving OpenMP constructs until late lowering stages enables both general-purpose and OpenMP-specific MLIR optimizations. By decoupling lowering from compiler internals, our approach expresses the same OpenMP subset in 5,182 lines of code, ~32% fewer than the corresponding lowering code in Clang and ~76% fewer than in GCC, while supporting the pmsis runtime costs only a few specification lines, enabling rapid support for new runtimes without modifying the compiler.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-02T18:49:59Z
Durmus Karatay, Richard Newman
arXiv categories: cs.LG, cs.PF, cs.PL

Many inference workloads evaluate a trained tree ensemble on row groups that share feature values: discrete-time survival models expand each patient into $G$ time steps, click-through-rate models score every item in a search session, and scenario analyses vary a few inputs while holding the rest fixed. Standard inference treats each row independently and repeats the shared work $G$ times. We present TreeWalker, which applies partial evaluation to grouped inference: constant features are static, varying features dynamic. It walks each tree once per group, partitions a row bitmask at varying splits, and skips empty subtrees. Training is unchanged: TreeWalker reads standard LightGBM and XGBoost models. We prove a structural work decomposition: per-tree work splits into the constant-projected subtree size $|T_c|$, $G$ leaf writes, and a predicate-mask provisioning cost $Q$. For the trace evaluator, per-row work approaches a $(d_v+1)/(d+1)$ fraction of a row-independent walk as $G \to \infty$. On Intel, TreeWalker is 2.5-3.2$\times$ faster than a row-independent traversal at the reference configuration ($T=500$, $L=8$) and 6.8-7.8$\times$ faster at $G=128$ on the survival datasets, with larger gains on Arm. On a scenario-analysis benchmark it is faster in all 16 configurations on both architectures. For f64 models, outputs match treelite's GTIL up to summation order; for f32 models, f64 accumulation is closer to a Kahan-compensated reference than native f32 on 99.98% of rows and never farther.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-02T19:49:43Z
Yusuke Izawa, Junichiro Kadomoto
arXiv categories: cs.PL

In wireless sensor and mesh networks, modular robots, and shape-adaptive computers, computing modules attach, detach, or are replaced while the others keep running with their local state. A value computed under the old arrangement, such as a cached next hop, stays in memory but may no longer describe the current one, so a program can send to a neighbor that has left without any runtime errors. We present morph-aware computing, a programming model in which the application specifies a corrective update of such state, called a repair, and the compiler decides when it runs. In MorphLang, the repair is a Reconfigure branch next to the ordinary branches that handle sends, receives, and sensor samples. MorphC compiles MorphLang to bare-metal RISC-V and inserts a guard before every ordinary branch, so that each module repairs its state before any other branch sees a new topology. Relying on this order, MorphC also rejects sends whose target may be a literal or a value the repair does not always refresh. For a model of the code MorphC generates, we prove in Rocq that the repair precedes every later ordinary branch for any number of roles and topology changes. This shows that send-target checking is sound for a core language. On 19 MorphLang programs derived from seven network stacks, removing the repair worsens destination validity in ten of the 13 programs that declare one and never improves it. In a reduced reproduction of a released Contiki-NG defect, a callback-based version sends to a departed parent after 60 of 384 changes and the MorphLang version after none. The guards cost 12 cycles per loop in a microbenchmark, and on an FPGA the delay from each commit to the first send to the new neighbor matches RTL simulation.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-04T07:12:21Z
Pingchuan Ma, Zhantong Xue, Zongjie Li, Qixin Zhang, Yuxuan Du, Zhaoyu Wang, Yuguang Zhou, Shuai Wang, Xiaoqin Zhang
arXiv categories: cs.PL

Quantum compilers translate programs into native gates, insert SWAP gates to route interactions onto a device, and optimize the result. The output is quantum assembly, a flat gate list that hides the algorithm's structure (QFT, Grover iteration, QAOA layers). Understanding, auditing, porting, or reusing such assembly requires recovering a program that exposes this structure. We present Quelle, a decompiler that recovers structured programs (library calls, loops, functions, symbolic angles) from routed and optimized quantum assembly (OpenQASM) and checks every output for equivalence with its input. Quelle is built on one invariant: every step is either an exact rewrite, checked where it is applied, or a hypothesis, checked against the input before use. It first lifts the assembly into a circuit by removing compilation artifacts, notably un-routing, which recovers the SWAPs that routing inserted, including those merged into other gates. It then recovers algorithm templates (sketches) whose parameters are solved from quantities preserved by compilation, and, for algorithms without a template, library calls and loops by anti-unification. Failed hypotheses are rejected; the corresponding operations remain in gate-level form. On 816 assembly programs from 22 algorithm families and a random-circuit control, compiled at four routing and optimization levels with native two-qubit gates CX, ECR, or CZ, Quelle's output is equivalent to the input for 100% of the inputs, and it fully decompiles 94% of them; compared on the same inputs, it fully decompiles 1.7x as many as the best LLM-based decompiler, which spends 15K tokens per input. On nine algorithm families for which it has no template, the structure it recovers without templates explains 60% of the gates. It checks inputs of up to 2.3 million gates and emits no inequivalent output on 237 real-world QASMBench assembly files.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-04T15:39:10Z
Jonas Mittnacht, Florian Lanzinger
arXiv categories: cs.PL

Pluggable type systems extend the basic type system of a programming language by introducing additional type hierarchies to specify more complex properties and dependencies between variables. We consider the Constant Value Checker, a pluggable type checker for Java implemented using the Checker Framework, which provides various pluggable type systems and corresponding checkers. The Constant Value Checker lets users specify restrictions on the values a primitive integer or boolean variable can hold using a set or range of constant values. However, the current implementation of the Value Checker makes use of a limited set of syntactic typing rules that, in practice, often fail to verify well-typedness of more complex code. In this paper, we introduce an extension to the Checker Framework using Satisfiability Modulo Theories (SMT) solvers to address these limitations by creating corresponding first-order logic formulas for expressions whose type checks fail with the current syntactic typing rules and determining their well-typedness based on the satisfiability of these formulas. Furthermore, we introduce new dependent types for specifying allowed values with expressions that can depend on other variables in the program.

arXiv abstract · PDF

Program analysis · primary corpus · published 2026-10-04T17:12:34Z
Prashanth Vijayaraghavan, Akul Malhotra, Ashutosh Jadhav, Ehsan Degan, Vandana Mukherjee
arXiv categories: cs.PL, cs.AR, cs.CL

Large Language Models (LLMs) are increasingly applied in hardware design automation, demonstrating strong potential in generating and understanding hardware description languages. However, most existing benchmarks focus on Verilog, with limited evaluation of VHDL, which remains widely used in industry and academia for FPGA and safety-critical systems. To address this gap, we introduce VHDL-REPOBENCH, a large-scale, cross-file, repository-level benchmark for assessing LLM capabilities on realistic VHDL design generation and analysis tasks. VHDL-REPOBENCH curates ~100 open-source VHDL repositories, encompassing ~2.5k VHDL files and ~500 testbenches, and provides structured problem statements, module stubs, and self-verifying testbenches. The benchmark enables comprehensive evaluation across syntax, semantic correctness, hierarchical reasoning, cross-file dependency resolution, and functional verification. We evaluate several state-of-the-art models, including GPT-4o, Llama-3-70B, Qwen2.5-72B, CodeLlama-70B, and multi-step reasoning approaches such as Reflexion and CoDes. Results reveal that while current LLMs achieve moderate line- and block-level accuracy, substantial challenges remain in multi-file reasoning, hierarchical design understanding, and specification-to-module generation. VHDL-REPOBENCH represents the first large-scale VHDL-focused benchmark and provides a valuable resource for the hardware design community to evaluate, compare, and advance LLM capabilities for practical VHDL development.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T03:11:24Z
Atsuhide Mori
arXiv categories: quant-ph, math-ph, math.CT, math.MP

Nakayama found the way to limit the contexts in the D\"oring-Isham topos quantum theory and unified such limitation and the definition of probability as a single choice of topology. We explain how this unification supports the Bayesian perspective where the probability changes as data is obtained. We describe this change as a local shift of the applicability of a predictive theory and apply it to quantum computing.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T03:13:09Z
Kazuo Habiro, Mai Katada
arXiv categories: math.RT, math.CT, math.RA

We introduce the notion of a quasi-cellular category, which is a variant of cellular algebras and cellular categories. Many diagram categories, such as the Brauer category and the partition category, are quasi-cellular. We study the Brauer category $B$ over a commutative ring $\mathbb k$ with parameter $\delta$ through its quasi-cellular structure. We construct a linear functor $L:B\to mB$ to the \emph{matrix Brauer category} $mB$, which has the same objects and hom-spaces as $B$ but a matrix-like composition. For a non-singular parameter $\delta$, we show that $L$ is an isomorphism of linear categories, and that $B$ is Morita equivalent to its subcategory $\mathbb S$ spanned by permutations, whose endomorphism algebras are the group algebras of symmetric groups. These results generalize those of Brown and K\"onig and Xi for the Brauer algebras.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T04:31:29Z
Yixia Zhang, Panyue Zhou
arXiv categories: math.CT, math.RT

Canonical ideal quotients of extriangulated categories admit natural one-sided triangulated or pretriangulated structures. A fundamental question is whether these quotient structures still retain enough information to recover higher orthogonality properties of the subcategory being factored out. We show that, for a strongly functorially finite $n$-rigid subcategory, such information is encoded by the nilpotency of the canonical suspension and, equivalently, of the canonical loop. More precisely, this nilpotency characterizes two-sided maximal $n$-orthogonality. We further establish an objectwise recognition criterion that combines one-sided higher orthogonality with the vanishing of the $n$th suspension or loop. In the triangulated setting, our results give a converse to the known truncation construction and show that the quotient is $n$-truncated if and only if the subcategory is $(n+1)$-cluster tilting. Moreover, in the nonsplit case, the nilpotency index is exactly $n$. These results turn truncation from a consequence of higher orthogonality into a sharp criterion for recognizing it.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T10:14:26Z
Mark V. Lawson
arXiv categories: math.CT

Given a monoid that can be embedded in a group and that acts partially on a set, we show that under certain conditions the category associated with the partial action has a groupoid of fractions. By imposing some topological conditions on the action, we show that the groupoid is actually \'etale. This \'etale groupoid arises naturally in $C^{\ast}$-algebra theory.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T13:17:18Z
Fabio Neugebauer, Qi Zhu
arXiv categories: math.AT, math.AG, math.CT

We prove that the sheaf $\infty$-topos associated to a geometric site in the sense of Lurie can be written as a partially lax limit of smaller sheaf $\infty$-topoi. This is thus a formalization of Lurie's vision for fractured $\infty$-topoi to axiomatize the relation between gros and petit topoi. As a consequence, we realize the $\infty$-topos of $\kappa$-small condensed anima as a partially lax limit of sheaf $\infty$-topoi over extremally disconnected spaces, marked at the open embeddings. Moreover, we deduce a gros version of the \'etale exodromy theorem.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T13:20:16Z
James Richard Andrew Gray
arXiv categories: math.CT

We show that under mild assumptions a functor is a prefibration if and only if it has terminal objects in its fibers and admits precartesian liftings of monomorphisms. We use this to show that the following conditions on a pointed category $\mathbb{C}$ are equivalent: (a) The category of morphisms of $\mathbb{C}$ admits generic split extensions; (b) Each functor category of $\mathbb{C}$ with finite domain category admits generic split extensions; (c) $\mathbb{C}$ admits normalizers and generic split extensions; (d) The kernel functor from the category split extensions in $\mathbb{C}$ to $\mathbb{C}$ is a prefibration. In addition we show that the category of morphisms of a pointed protomodular $\mathbb{C}$ admits generic split extensions if and only if for each morphism $f:X\to Z$ the functor sending each object $B$ to the isomorphism class of split extensions in $\mathbb{C}^{\mathbf{2}}$ of $(B,B,1_B)$ with kernel $(X,Z,f)$, is representable.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-28T18:01:07Z
St\'ephane Gaussent, Zuan Liu, Philippe Malbos
arXiv categories: math.CT, math.QA, math.RT

In this article, we introduce a new rewriting method for computing hom-bases of diagrammatic categories. Our approach is based on stratified presentations, obtained by partitioning an equational presentation into strata according to the rewriting behavior of its relations. We establish modularity principles for termination and confluence in stratified rewriting systems with coefficients in a ring. We then introduce a completion procedure that transforms a stratified presentation into a normalized one, in which mixed interactions between successive strata are absorbed into the normalized rewriting rules, thereby inducing modularity of confluence. This leads to a stratified hom-basis theorem for diagrammatic categories. We illustrate the method by applying it to the $q$-Schur category, for which we construct a new hom-basis.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-29T13:10:37Z
Shachar Carmeli, Guy Kapon, Noam Nissan
arXiv categories: math.CT, math.AG, math.AT

We extend a six-functor formalism $D\colon\mathrm{Span}(C,E)\to\mathrm{Cat}$ to a lax symmetric monoidal functor of $(\infty,2)$-categories $\mathbf{Span}^2(C,E)^P_I\to\mathbf{Cat}$, where $P$ and $I$ are the classes of $D$-proper and $D$-\'etale morphisms, respectively. This proves a conjecture of Mann and generalizes a special case of a theorem of Cnossen, Lenz, and Linskens. To prove this result, we develop a theory of internal $\mathsf{E}$-monoidal categories and $\mathsf{E}$-operads, where $\mathsf{E}$ is a local class of morphisms in an $\infty$-topos. These notions generalize the internal symmetric monoidal categories and operads developed by Martini and Wolf.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-29T15:41:18Z
Isaac Carcac\'ia Campos
arXiv categories: math.AT, math.CT

The nerve theorem provides a combinatorial model for the homotopy type of a topological space from a suitable open cover. We extend this local-to-global approach by replacing the intersections of the cover with compatible categorical models. These local models are assembled through the Grothendieck construction, yielding a small category whose classifying space has the weak homotopy type of the original space. Under suitable hypotheses, the resulting category is finite and acyclic. We develop two versions of this construction. The first is indexed by the usual poset of nonempty finite intersections of the cover. The second uses the membership poset, inspired by the finite-space construction of Sancho de Salas, which retains only the membership patterns realized by points of the space and is defined for point-finite covers. The classical nerve theorem and its componentwise variant are recovered as particular cases. The construction is recursive: categorical models of local pieces, together with functors representing their inclusions, can be combined to produce categorical models of more complex spaces.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-30T08:56:11Z
Yang Gao, Yu-xiao Yang, Pu Zhang
arXiv categories: math.CT, math.RT

This paper studies orthogonal model structures, i.e., model structures such that a lifting in the Lifting axiom is unique. Cofibrant (fibrant) objects are defined without initial (terminal) objects. For an orthogonal model structure on a category with enough cofibrant objects and fibrant objects, it is proved that the homotopy category is equivalent to the full subcategory of cofibrant-fibrant objects. TTF model structures, bi-reflective model structures, and torsion model structures, are introduced. They are all orthogonal. One to one correspondences between TTF model structures and TTF triples in an abelian category, bi-reflective model structures and bi-reflective pairs in any category, and torsion model structures and twin torsion pairs in an abelian category, are established in a constructive way. Torsion model structures on a poset, on the category of $G$-sets, and on the category of topological groups, are also constructed. The homotopy categories of all these model structures are computed. In particular, the homotopy category of a TTF model structure is an abelian category.

arXiv abstract · PDF

Mathematical logic · primary corpus · published 2026-09-30T14:07:39Z
Haruhisa Enomoto
arXiv categories: math.RT, math.CO, math.CT, math.RA

B{\o}rve, Horiatakis, and Kalck defined the magnitude of the module category of a representation-finite algebra as the sum of the entries of the inverse of the matrix of Hom dimensions between indecomposable modules. They showed it is an Euler characteristic, the alternating count of vertices, arrows, and meshes of the Auslander--Reiten quiver, and conjectured that it is at least the number of simple modules, with equality precisely for special biserial algebras. We prove this conjecture over an algebraically closed field. For a representation-directed algebra, we relate the magnitudes of the module category, the subcategory of modules without a given simple composition factor, and the ideal quotient by it. By the theory of hammocks of Ringel and Vossieck, this quotient is equivalent to a category of representations of a finite poset, whose magnitude we compute. The general case reduces to the representation-directed case through algebras obtained by grading a standard form.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-09-28T00:49:33Z
Koichi Oyakawa
arXiv categories: math.GR, math.GT, math.LO

We prove that every acylindrical action on uniformly locally finite product of trees induces the hyperfinite orbit equivalence relation on the Roller boundary. As a byproduct, we construct an example of a standard Borel space and two commuting bounded-to-one surjective partial Borel maps that generate a universal countable Borel equivalence relation. This contrasts to Shinko-Weilacher-Yu's theorem on hyperfiniteness of bounded-to-one actions of commutative monoids.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-09-30T14:59:59Z
Kangqiao Li
arXiv categories: math.QA, math.CT, math.RA

Let $B$ and $D$ be both algebras and coalgebras in a braided monoidal category $\mathcal{C}$. In the literature, there are equivalent conditions for $(B,D)$ to form a generalized smash biproduct (or cross product) denoted by $B\times D$, which were mainly given by Bespalov and Drabant in 1999 as well as by Bulacu, Caenepeel and Torrecillas in 2013. This paper is devoted to constructing another biproduct $D\times B^\ast$ when $B$ has a left dual object $B^\ast$ in $\mathcal{C}$. As results, we show that $B\times D$ is left smash over $D\times B^\ast$, and establish a specific isomorphism ${}_{B\times D}\mathfrak{YD}(\mathcal{C})^{B\times D}\cong{}_{D\times B^\ast}\mathfrak{YD}(\mathcal{C})^{D\times B^\ast}$ between the categories of the (left-right) Yetter-Drinfeld modules in $\mathcal{C}$. The constructions and results are provided in three levels: (1) $B\times D$ is an algebra and a coalgebra; (2) $B\times D$ is a bialgebra; (3) $B\times D$ is a Hopf algebra.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-09-30T17:51:43Z
Marianne M. Lawson, Sven A. Wegner
arXiv categories: math.CT, math.FA

We describe hearts of strongly deflation-exact categories with kernels as localizations of categories of three-term complexes up to homotopy, without assuming admissibility of kernels. We construct a calculus of fractions and give explicit formulas for kernels and cokernels. For complete locally convex spaces, whose failure to be quasiabelian was established by Prosmans (2000), our description and its dual provide derived equivalent abelian models through two choices of a notion of exactness. For quasi-complete, sequentially complete and locally (a.k.a. Mackey) complete spaces, we show that the topologically exact sequences form the maximal deflation-exact structure, although these categories are not extension-closed in the category of locally convex Hausdorff spaces. Our results make them nevertheless accessible to homological algebra with respect to the induced notion of exactness. Further applications concern the quasiabelian category of bornological modules equipped with the non-maximal linear split exact structure.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-09-30T20:54:39Z
J\'on H\'akon Gar{\dh}arsson, Paolo Perrone
arXiv categories: math.CT, math.DG

A dagger on a category assigns to every morphism $f \colon X \to Y$ a morphism $f^\dagger \colon Y \to X$, contravariantly and involutively, in the way the transpose reverses a real matrix. We show that on the categories of linear algebra and differential geometry, daggers encode metric and Riemannian structures. As is known, on a single vector space, an anti-involution of the endomorphism ring is the adjoint of a form that is determined up to a scalar. But more generally, on the category of all finite-dimensional vector spaces, a dagger is the adjoint for an involution of the scalars together with a unique unimodular Hermitian form on every space. The same holds for finitely generated projective modules over a commutative ring, and hence, through the Serre-Swan correspondence, for vector bundles, where a dagger is a choice of bundle metrics. The dagger structure expresses notions of orthogonality categorically: orthogonal complements and normal bundles acquire universal properties, and Hermitian modules form a dagger compact category. Moreover, daggers on Lie groups, Lie groupoids and their infinitesimal counterparts capture unitary representations and metric connections: a connection is metric precisely when its parallel transport is a dagger functor, or, infinitesimally, when its splitting of the Atiyah sequence commutes with the daggers. Finally, we classify the daggers on the locally graded category of differential operators of a Lie-Rinehart algebra. They correspond to metric-divergence structures, consisting of a real structure, a divergence, and a unimodular Hermitian form on every finitely generated projective module, and they act on operators as formal adjoints; Green's formula expresses the difference between an operator and its adjoint as a divergence.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-01T09:17:24Z
Yusuke Shiobara
arXiv categories: math.DG, math.CT, math.MG

Following Miyamoto, we consider Q-charts, a class of subductions $\phi\colon X\to Y$ of diffeological spaces along which Blohmann's elasticity descends. We show that the Riemannian apparatus of elastic diffeology---vertical, horizontal and full connections, Riemannian metrics, Levi-Civita connections and geodesics---also descends along Q-charts. More precisely, structures on $Y$ correspond bijectively to structures on $X$ that are invariant under the pseudogroup $\Psi(\phi)$ of fibre-preserving transitions, and torsion-freeness, effectivity, flatness, fullness, the Levi-Civita property and the geodesic equation are preserved in both directions. The key input is that the iterated tangent bundles $T^nX$ and their fibre products $T_kX$ are the pullbacks along $\phi$ of the corresponding bundles over $Y$. For quotients by principal actions of diffeologically discrete groups, we lift geodesics globally, prove that the class of elastic spaces on which $\R$ is a curve object is closed under such quotients, and show that complete geodesic flows descend. As an application, we determine the Riemannian geometry of the irrational tori $\Tor_\alpha=\R/(\Z+\alpha\Z)$ completely. Let $\vartheta$ be the one-form on $\Tor_\alpha$ induced by $dt$ on $\R$. Every Riemannian metric is a positive constant multiple of $\vartheta^2$, and the vertical connections form a one-parameter family of flat effective connections, a single member of which is the unique Levi-Civita connection of every metric. This connection has a complete geodesic flow, yet the induced pseudo-distance vanishes identically.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-01T11:24:41Z
Zhenggang He, Jifen Liu, Jiaqun Wei
arXiv categories: math.CT

Let $(\mathcal{C},\mathbb{E},\mathfrak s)$ be an extriangulated category equipped with a proper class $\xi$ of $\mathbb E$-triangles.We establish stability under iteration for the quasi-$\xi$-Gorenstein projective and injective subcategories and extend the relative Ext-vanishing criteria for their finite homological dimensions to larger coefficient subcategories. An example in a bounded homotopy category shows that $\mathcal{P}(\xi)\subsetneq\mathcal{QGP}(\xi)\subsetneq\mathcal{GP}(\xi)$. For module categories, every quasi-Gorenstein projective module over a left perfect ring or a commutative Noetherian ring of finite Krull dimension is projective. When a commutative ring admits a finite chain of trace and nilpotent quotients ending in an Artinian ring and the endomorphism rings at the trace steps have finite right global dimension, we construct finite families of quasi-projective test modules that detect prescribed upper bounds on projective dimension for modules of bounded cardinality through Ext vanishing in finitely many consecutive degrees.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-01T13:30:25Z
Arnaud Duvieusart
arXiv categories: math.CT

We study the construction of ternary semi-direct products in semi-abelian categories, following a definition of higher semi-direct product previously introduced by Carrasco and Cegarra for groups and Lie algebras. We show that these objects are determined by actions and equivariant morphisms satisfying a certain compatibility condition in the ambient category, and that actions by semi-direct products are a special case of this construction. We also show how their structure can be further simplified in algebraically coherent or locally algebraically cartesian closed categories. We also give a concrete description of the structure of ternary semi-direct products in concrete categories, and how our categorical interpretation of the necessary structure relates to the group and Lie-theoretic versions given by Carrasco and Cegarra.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-02T18:00:02Z
Alonso Perez-Lona
arXiv categories: hep-th, math-ph, math.AT, math.CT, math.MP

We develop a higher-geometric framework for magnetic higher-form symmetries of pre-quantum field theories. The magnetic (topological) charges of a sigma-model with stacky target are encoded by the shape of the target, equivalently of its stack of fields, which is op-dual to the flat automorphism group controlling electric symmetries. Magnetic symmetry backgrounds are obtained by dualizing these charges against a chosen moduli stack of topological field theories, generalizing Pontryagin duality, and act on the theory by stacking. Cohesive modalities allow for targets with non-finite and non-discrete data. When the dualizing stack is a grouplike $E_\infty$-object, we prove a fibration theorem expressing the magnetic symmetries of an electrically gauged theory in terms of those of the ungauged theory and of the gauge group, computed by a homotopy-fixed-point spectral sequence with an explicit first page. For moduli stacks of higher $U(1)$-gerbes with connection, encoding bulk topological local Lagrangians, we prove a factorization theorem: the magnetic symmetry backgrounds of any connected target split, non-canonically, into Pontryagin duals of its integral homology groups, and are necessarily flat, as a consequence of dualizing discrete charges against a target with connections. We illustrate both theorems with pure $\mathrm{Pin}^\pm(2)$ gauge theory: $O(2)$ carries invertible magnetic $\mathbb{Z}_2$ symmetries in form degrees $d-3$, $d-4$ and $d-5$ that are absent for $\mathrm{Pin}^-(2)$, the first two distinguished by a single differential of the spectral sequence. Gauging and physical applications are developed in upcoming work.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-02T18:10:24Z
Antonios Kalampakas
arXiv categories: math.CT, cs.FL

Graphoid automata evaluate graphs by composing relations between words of states. We examine the equations that make this evaluation independent of the chosen graph expression, and what changes when relations are replaced by matrices over a commutative semiring. We prove that the classical graphoid equations are equivalent to the special commutative Frobenius equations together with the required symmetry laws. The known cospan and hypergraph presentations then describe equality of structural and labelled expressions, with the bone law deleting precisely the isolated internal vertices. We use established partition representations to compare this equality with equality of evaluated matrices. For any nonempty finite state set $Q$ and commutative semiring $K$, we give a uniform criterion for two structural expressions to have the same matrix. The criterion determines which isolated-vertex counts are distinguished and when a vanishing scalar makes matrices from different boundary partitions equal. For the canonical structure, the bone law holds precisely when $|Q|\cdot1_K=1_K$. Preserving all relational compositions is a separate requirement, equivalent to additive idempotency for $|Q|\geq2$. We then examine the characteristic matrices of the known relational structures on $Q$ given by disjoint unions of Abelian groups. Their Frobenius equations hold over every commutative semiring, whereas specialness depends on the order of each group and the bone law depends on the number of groups. These conditions specify which equations remain valid when weights are assigned to a graphoid automaton.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-02T22:03:50Z
Kevin Coulembier, Johannes Flake
arXiv categories: math.RT, math.CT

We prove that every finite symmetric tensor category over an algebraically closed field of positive characteristic admits a symmetric tensor functor to a higher Verlinde category. This was conjectured for arbitrary symmetric tensor categories of moderate growth by Benson, Etingof and Ostrik. The proof uses higher Frobenius functors, introduced by the authors in [CF1]. The main effort is directed towards a proof of a conjecture from [CF1] about thick tensor ideals in the representation category of elementary abelian $p$-groups, which implies that the higher Frobenius functors are symmetric monoidal. In fact, we prove a refinement of the latter conjecture that relates tensoring with restricted Steinberg modules to an iterated generalised cohomology of modules of elementary abelian $p$-groups.

arXiv abstract · PDF

Computational complexity · primary corpus · published 2026-10-04T15:31:06Z
Marino Gran, George Janelidze
arXiv categories: math.CT

We show that, under some mild assumptions, every quasi-pointed category C carries a canonical near-torsion theory (T,F), where T consists of the 0-supported objects, that is, those admitting a morphism to the initial object 0, and F consists of the subterminal objects. The coreflection and the reflection of an object A are then given by the projection $A \times 0 \to A$ and by the strong-epimorphic part of $A \to 1$, respectively. Using the general construction of the "largest" non-pointed torsion theory associated with a near-torsion theory, we prove that (T,F) is a (non-pointed) torsion theory in the full subcategory of those objects A for which the canonical sequence $t(A) \to A \to f(A)$ is short exact, in the sense that it is both a kernel and a cokernel diagram. This subcategory is the whole of C whenever C is sequentiable, that is, a regular protomodular and quasi-pointed category. We describe the resulting torsion theories in the category of Lie-Rinehart algebras and in the categories of crossed modules over a fixed group. We also show that (T,F) is a torsion theory in the (non-protomodular) category of monoids over a group G all of whose elements have finite order.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-28T07:50:32Z
Ivo Herzog, Gianluca Paolini, Saharon Shelah
arXiv categories: math.LO

Let $R$ be a countable ring. Given an $R$-module $A$, we call a decomposition $A = \bigoplus_{i \in I} N_i$ a Kaplansky decomposition if each $N_i$ is countable. We characterize the uncountable Polish $R$-modules that admit a Kaplansky decomposition: they are exactly the modules of the form $B \oplus M^{\omega}$, where $B$ and $M$ are countable and $M$ is $\Sigma$-algebraically compact. The countable summand $B$ may moreover be taken to be an elementary submodule satisfying a closure condition, which makes $M^{\omega}$ unique up to isomorphism, and hence an invariant of $A$. We use this to characterize the countable rings admitting a free uncountable Polish $R$-module, generalizing results of Shelah and Solecki. This class of rings has a purely ring-theoretic description: it consists exactly of the countable left perfect and right coherent rings, i.e. the rings identified by Chase's theorem on products of projective modules. We observe that these are also exactly the countable $F$-rings, i.e. those countable rings $R$ for which $R^{\omega}$ is free. Finally, we give a ring-theoretic characterization of the countable rings $R$ for which there exists an uncountable projective Polish $R$-module.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-28T13:36:20Z
Jan Krajicek
arXiv categories: cs.CC, math.LO

The problem to establish a lower bound for $\mbox{AC}^0[p]$-Frege refutations of a system of polynomial equations over ${\bf F}_p$ was in K. (2024) reduced to the existence of a pseudo-solution (a notion defined there) for the system. Here we reduce this further, for the system expressing the negation of the PHP, to a property of search trees querying values of linear maps on the vector space of low degree polynomials over ${\bf F}_p$.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-28T17:32:19Z
Filippo Calderoni, Esm\'e Yanowitz
arXiv categories: math.LO

In this paper we contribute to the study of compactness properties for algebraic structures. We prove two compactness theorems in the context of almost projective modules from $\lambda$-strongly compact and weakly compact, respectively.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-28T17:50:31Z
Giulio Fellin
arXiv categories: math.LO

We present an abstract framework for conservation and translation theorems between logical calculi. Unlike previous approaches, our setting does not require the underlying consequence relations to satisfy structural properties such as cut, allowing in particular for cut-free calculi. Moreover, we study translations between arbitrary calculi rather than only from a stable extension to the original calculus. Translations are formulated at the level of sequents by pairs of functions acting on antecedents and succedents, and the framework is developed for multi-succedent calculi while subsuming the single-succedent case. This yields a uniform treatment of classical results including negative translations, minimality theorems, Orevkov's conservation classes, and a characterisation of the least logic satisfying Kuroda's double negation theorem.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-28T21:46:12Z
Grzegorz Jagiella
arXiv categories: math.LO

We prove that if a minimal ordered structure $(M, <, \ldots)$ with infinite chains in an arbitrary language extending the language of strict orders interprets (in some power $M^n$) the linear order $(\omega, <)$, then this fact can be witnessed for $n=1$ via the incomparability relation of an $<$-definable strict order $R$; that $R$ is unique up to ``almost equality'', i.e., finite rearrangements of elements of $M$; and that $R$ can be defined from $<$ in a constructive way. We also show that several variants of the question whether a minimal ordered structure interprets an infinite linear order are all equivalent.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-28T23:46:44Z
Joonhee Kim
arXiv categories: math.LO

We define a class of classes of complete first-order theories, denoted by $\mathfrak{D}_{n\text{-var}}$, using positive consistency-inconsistency configurations and generalized indiscernibles. It contains the classes of stable, simple, NIP, NTP$_1$, NTP$_2$, NATP, NCTP, and NBTP theories, as well as the classes of theories not having a $(k,1,1)$-weave of depth $\omega$ for any $k<\omega$, theories not having an infinite $k$-grid for any $k<\omega$, and NPM$^{(k)}$ theories for each $1<k<\omega$. For any dividing line $D\in\mathfrak{D}_{n\text{-var}}$ and any complete first-order theory $T\notin D$, we can always find a formula $\varphi(x,y)$ witnessing $T\notin D$ with an indexed set of parameters such that the set of its instances required to be consistent has a realization whose algebraic dimension over the whole set of parameters is $|x|$. We call statements of this form $n$-variable theorems, as they may be regarded as weak versions of one-variable theorems. Under the appropriate hypotheses on $T$, we prove that $T\in D$ if and only if the corresponding theory belongs to $D$ for (i) $T^{gt}$, (ii) $T_P$, (iii) $T^{ind}$, (iv) $T^G_K$, (v) ACF$_T$, and (vi) any completion of $T^\delta_g$. These are, respectively, the theories of generic trivializations, lovely pair expansions, $H$-structure expansions, vector spaces with a dense-codense generic $K$-subspace, algebraically closed fields with a distinguished subfield, and generic derivations of algebraically bounded fields. The $n$-variable theorem is essential in proving (i)--(v). We also introduce a larger class $\mathfrak{D}^h_{n\text{-var}}\supseteq\mathfrak{D}_{n\text{-var}}$, capturing higher-arity dividing lines such as NOP$_k$, NFOP$_k$, and NIP$_k$ for $1<k<\omega$. The $n$-variable theorem and preservation results (ii), (iii), (iv), and (vi) also hold for this larger class, while (i) holds assuming ${\rm acl}={\rm dcl}$.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-29T09:49:11Z
Lorenzo Carlucci, Andrea D'Amico
arXiv categories: math.CO, math.LO

We prove the equivalence of Hindman's finite sums theorem with a natural extension of Ramsey's theorem.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-29T14:33:29Z
Carlos Simpson
arXiv categories: math.AG, math.LO, math.NT

We give an exposition of some of the ideas leading up to Jacob Tsimerman's groundbreaking work developing the theory of o-minimal definability in arithmetic and algebraic geometry.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-30T00:25:04Z
Carl Aza
arXiv categories: math.GN, math.CO, math.GR, math.LO

Let $\Sigma_{1} = \mathbb{N}^*$ and $\Sigma_{k+1} = \overline{\mathbb{N}^* + \Sigma_{k}}$ be the cumulative depth filtration of $\beta\mathbb{N}$, the analogue for $(\mathbb{N},+)$ of a chain of closed ideals that Protasov and Protasova studied for discrete groups, where strict descent follows from a theorem of Lutsenko and Protasov. For every $k$ we give an explicit set whose closure meets $\Sigma_{k}$ but not $\Sigma_{k+1}$. Fix the doubly exponential sequence $e_{n} = 2^{2^{n}}$, partition it into $k$ subsequences $E_{0}, \dots, E_{k-1}$ by the residue of the index modulo $k$, and set $A_{k} = E_{0} + \cdots + E_{k-1}$. We prove that any sum $q_{0} + \cdots + q_{k-1}$ of free ultrafilters with $E_{t} \in q_{t}$ lies in $\Sigma_{k} \setminus \Sigma_{k+1}$. The engine is a master lemma, proved by induction on $j$: if a sum $F_{1} + \cdots + F_{j}$ of subsequences of $\{e_{n}\}$ with pairwise disjoint index sets belongs to a free ultrafilter $s$, then $s \notin \Sigma_{j+1}$. The proof rests on a single rigidity of the doubly exponential sequence: a fixed difference forces the largest index in any shift-intersection, once it is large, to cancel within its own subsequence, which makes every shift-intersection descend by at least one level. The same witnesses lie in the gaps of the pure filtration.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-30T04:41:17Z
Liang Yu
arXiv categories: math.LO, math.CA

We prove that, for every irrational $\xi$, any $F_\sigma$ additive subgroup of $\R$ has an $F_\sigma$ $\Q$-vector space extension of the same Hausdorff dimension satisfying $A+\xi A=\R$. Iteration gives simultaneous surjectivity for any prescribed countable family of irrational multipliers. Such a space exists in every prescribed dimension $d\in[0,1)$. We also construct in ZFC a zero-dimensional lightface $\Delta^0_3$ $\Q$-vector subspace $A$ for which $A+\xi A=\R$ holds for every irrational $\xi$, answering both parts of Question~2 of Ye, Yu, and Zhao. This universal group is a difference of two $F_\sigma$ sets, but is neither $F_\sigma$ nor $G_\delta$. Both constructions use direct inductions on finite binary strings and admit effective versions. As applications, we obtain zero-dimensional $F_\sigma$ groups whose Cartesian squares have Hausdorff dimension one, and relate their dilate sums to Marstrand's projection theorem.

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-30T04:49:16Z
Yunsong Wang, Lukas Zenger
arXiv categories: math.LO

{Non-contingency logic $(\KWL)$ replaces the usual necessity operator of modal logic with an operator expressing that a proposition is necessarily true or necessarily false. Besides its intrinsic logical interest, it admits natural interpretations as knowing whether in epistemic logic and as decidability under the arithmetical interpretation of provability logic. Although the semantics of non-contingency logic have been extensively studied, its proof theory remains comparatively underdeveloped. In this paper, we develop a uniform proof-theoretic framework for $\KWL$ over a broad class of frame conditions. Our approach is based on generalized path conditions (GPCs), a grammar-theoretic formalism that uniformly captures many standard modal frame properties. For every finite set $\gpc$ of GPCs, we construct a corresponding labelled sequent calculus. All calculi share a common set of logical rules and differ only by a single structural rule generated from $\gpc$, which captures the underlying frame conditions. We prove that these calculi are sound and complete with respect to their corresponding frame classes, thereby providing a uniform proof theory for a large family of non-contingency logics.}

arXiv abstract · PDF

Model theory · primary corpus · published 2026-09-30T10:49:39Z
Jonathan Schilhan, Thilo Weinert
arXiv categories: math.LO

Call a linear order type $\varphi$ Hagendorf if it shares two properties with additively indecomposable ordinal numbers without being one itself: $\varphi$ is strictly indecomposable to the right and whenever $\psi < \varphi$, then $\psi$ can be embedded into a proper initial segment of $\varphi$. In the 1970s, J. Hagendorf asked whether such types exist. F. Galvin observed that they must be uncountable, and soon thereafter, J. Larson proved that they cannot be scattered. We provide a simplification of her argument that might give additional insight into the $\sigma$-scattered case. We then show that consistently Hagendorf types exist and that this holds in many models of set theory, for instance under $\mathsf{BA}$ or $\mathsf{MA}_{\aleph_1}$. In fact, their non-existence has large cardinal strength. Furthermore, we construct real Hagendorf types from $\diamondsuit$ and from $\mathsf{PFA}$. This marks the first progress on this interesting problem since its description by Larson four dozen years ago.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-09-30T14:26:27Z
Ruijun Wang
arXiv categories: math.LO, math.CO

For every fixed integer $d\geq2$, we prove that the finite graphs receiving a continuous homomorphism from the standard Schreier graph $F(2^{\mathbb Z^d})$ form a $\Sigma^0_1$-complete set. This extends a theorem of Gao, Jackson, Krohne and Seward when $d=2$. For the positive part of the reduction, we show that if a graph $H$ satisfies a certain property then there is a continuous graph homomorphism from $F(2^{\mathbb Z^d})$ to $H$, in particular, the complete graph $K_4$ satisfies this property. This extends a theorem of Gao and Jackson. We also prove that $\big (\mathcal H_d\big )$ is a strictly decreasing sequence.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-09-30T14:50:31Z
Bruno Le Floch
arXiv categories: math.LO, math.RA

We consider the 653 equational laws of order up to 4 for an associative binary operation, and all of their conjunctions. We determine that there are only 456 equivalence classes of such conjunctions (associative equational theories), and find all implications between them. The conjunction operation makes this set of theories into a semi-lattice. These results are formalized in Lean. This is a semigroup analogue of the Equational Theories Project, but extended to conjunctions of equations.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-09-30T17:38:07Z
\"{O}zlem Beyarslan, Piotr Kowalski
arXiv categories: math.LO

We study the existence of model companions after adjoining an automorphism to field theories in two complementary settings. For bounded PAC fields of characteristic zero containing all roots of unity and admitting a cyclic Galois quotient of prime order, a suitable choice of countably many constants gives a model-complete field theory which has no model companion after adding an automorphism fixing the named constants. This applies, in particular, when the absolute Galois group is free profinite or free pro-$p$ of finite positive rank. Secondly, for every completion of $\ACFA$ in every characteristic, adjoining a second commuting automorphism has no model companion. The two explicit obstructions use a common ordered product of inertia automorphisms along an infinite orbit, combined respectively with an equivariant PAC completion and an algebraically closed difference-field embedding.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-09-30T19:43:19Z
Jos\'e de Jes\'us Pelayo G\'omez
arXiv categories: math.LO

We prove in ZFC that $\mathfrak d=\omega_1$ implies $\mathfrak a=\omega_1$, settling a question of Roitman from the 1970s. Here $\mathfrak d$ is the least size of a family that eventually dominates every function in $\omega^\omega$, and $\mathfrak a$ is the least size of an infinite maximal almost disjoint (MAD) family of infinite subsets of $\omega$. Consequently, $\mathfrak a\leq\mathfrak d$ whenever the continuum $\mathfrak c=2^{\aleph_0}$ is at most $\omega_2$. This answers negatively Shelah's question whether $\mathfrak d<\mathfrak a$ is consistent with $\mathfrak c=\omega_2$, and shows that his model of $\mathfrak d=\omega_2<\mathfrak a=\mathfrak c=\omega_3$ has the least possible values of $\mathfrak d$, $\mathfrak a$ and $\mathfrak c$ among models of $\mathfrak d<\mathfrak a$. The proof also gives a preservation theorem: from any dominating family of size $\omega_1$, we construct a MAD family of size $\omega_1$ that remains maximal in every outer model in which the given family is still dominating. Thus, under $\mathfrak d=\omega_1$, some MAD family is indestructible by every $\omega^\omega$-bounding forcing; it can moreover be chosen almost strongly separable, hence Cohen-indestructible. These results give negative answers, under $\mathfrak d=\omega_1$, to two questions of Hru\v{s}\'ak and to one of Brendle, Guzm\'an, Hru\v{s}\'ak and Raghavan.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T00:14:36Z
Xing-Yu Hu
arXiv categories: math.GN, math.LO

Let \(H(A)\) be the Hattori space associated with \(A\subseteq\mathbb R\), and put \(B=\mathbb R\setminus A\). Kulesza announced at the 2018 Joint Mathematics Meetings that Lindel\"ofness of \(H(A)^{2n}\) forces Lindel\"ofness of \(H(A)^{2n+1}\) for every positive integer \(n\). The meeting abstract states this implication without a proof. This paper proves the case \(n=1\) in ZFC. The same one-sided geometry gives a pointwise half-space criterion for affine discreteness and, when \(H(A)^2\) is Lindel\"of, a four-coordinate obstruction for uncountable closed discrete monotone traces. Known results on mixed Sorgenfrey--Euclidean products lead to hereditary-Lindel\"of criteria for finite powers, a countable-power characterization, and a finite-power Lindel\"of reduction. A transfinite construction gives \(A\subseteq\mathbb R\) for which \(H(A)^2\) and \(H(A)^3\) are Lindel\"of, whereas \(H(A)^4\) contains a closed discrete affine line of cardinality \(\mathfrak c\).

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T02:06:47Z
William Adkisson
arXiv categories: math.LO

We examine the relationship between trees and narrow systems. In particular, we prove that if a tree of height $\kappa$ admits a narrow subsystem, it must contain a well-pruned subtree of height $\kappa$. We extend these results to two-cardinal trees.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T10:30:42Z
Yuki Nishimura
arXiv categories: math.LO

Weak modal logics can be obtained by restricting the axioms and inference rules governing the modal operator. At the extreme, one may consider the least modal logic, in which no specifically modal axiom or inference rule is imposed. We introduce closure semantics, a new possible-world semantics for such weak modal logics, and establish soundness and strong completeness for a range of systems. We also give truth-preserving translations between closure models and other possible-world semantics, including neighborhood, FMT, and Kripke semantics.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T12:16:02Z
Mart\'in Figallo, Jonathan Sarmiento, Luis Pezzini
arXiv categories: math.LO

We study the minimal tense logic $K_t$ from an algebraic and proof-theoretic perspective. We introduce the degree-of-truth-preserving logic associated with the class of tense Boolean algebras. We then introduce a sequent calculus for this logic and establish its soundness and completeness with respect to tense Boolean algebras by means of an adaptation of the Lindenbaum--Tarski construction. Consequently, this calculus provides an additional syntactic presentation of the minimal tense logic $K_t$. We also provide a second, purely syntactic proof of completeness. Furthermore, we establish an algebraic soundness and completeness theorem for Kashima's Gentzen-style calculus. To this end, we develop an adaptation of the Lindenbaum--Tarski construction to Kashima's nested sequent framework, which allows us to construct the algebraic semantics directly from the proof-theoretic system. This yields a direct algebraic completeness proof for Kashima's calculus and connects its nested-sequent formulation with the algebraic semantics of tense Boolean algebras.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T15:56:49Z
Piotr Borodulin-Nadzieja, Miko{\l}aj Marsy, Kamil Ryduchowski
arXiv categories: math.FA, math.LO

We study combinatorial Banach spaces, i.e. Banach spaces induced by families of finite sets, of uncountable density. We prove some general theorems, for example we characterize when such spaces contain isomorphic copies of long $c_0$ and long $\ell_1$. We discuss the existence of Banach spaces which are (complementedly) universal in the category of Banach spaces with unconditional basis of fixed cardinality. We present some examples, in particular we show that the Banach spaces generated by Suslin trees do not contain uncountable equilateral sets.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T16:44:46Z
Patrizio Cintioli
arXiv categories: math.LO

We give a column-avoidance modification of the no-least-join construction of Downey, Greenberg, Lewis, and Montalb\'an. We show that if $C$ is computably enumerable, $A,B<_T C$, and $A\not\leq_T B$, then for every noncomputable set $E$ there is a set $X\leq_T C$ such that $B\leq_T A\oplus X$ and $E\not\leq_T X$. Consequently, for the corresponding Turing degrees $a,b,c$, the degrees $x\leq c$ satisfying $b\leq a\vee x$ have no nonzero common lower bound; equivalently, no nonzero Turing cone contains all of them. This gives a negative answer to their Question 1.19.

arXiv abstract · PDF

Set theory · primary corpus · published 2026-10-01T18:23:46Z
Jialiang He, Jintao Luo, Hang Zhang
arXiv categories: math.LO

We study idealized maximal eventually different families through Van Douwen maximality, productivity, and ultrafilter maximality. We show that Van Douwen $\mathcal{J}$-MED families correspond to $(\mathcal{J}\times\emptyset)$-MAD families, and for coanalytic ideals containing the finite sets they are further reduced to infinite analytic $\mathcal{J}$-MAD families. This yields nonexistence results for analytic Van Douwen families for several standard ideals, together with a characterization of the finite case. We recall the definition of finite productivity and introduce finite-section and $\omega$-centered productivity. Finite-section productivity is equivalent to $\mathcal{U}^*$-maximality for some ultrafilter $\mathcal{U}$ extending $\mathcal{J}^*$, and these notions admit natural Stone-space characterizations. We construct Borel finitely productive families for uniformly weakly Ramsey ideals and Borel $\omega$-centered productive families for uniformly weakly $P^+$ ideals, while no analytic finite-section productive $\mathrm{Fin}$-MED family exists. Finally, for every Ramsey ultrafilter $\mathcal{U}$ and $1\leq\alpha<\omega_1$, there is no analytic $(\mathcal{U}^{\alpha})^*$-MED family, while under $V=L$, there is a $ \boldsymbol{\Sigma}^1_2 $ Ramsey ultrafilter $ \mathcal{U} $ where there is a coanalytic $ \mathcal{U}^* $-MED family.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-01T22:34:36Z
Konrad Burnik
arXiv categories: math.LO, cs.NA, math.NA, math.RT

We study the universal isotypic block-diagonalization problem in the Type-2 theory of effectivity (TTE). We obtain a uniform computability result for the universal block diagonalizer for commutants of given finite group representations. As an application, when the given representation is orthogonal, we compute ordinary $QR$ factorizations blockwise in the isotypic basis. After transforming back to the original coordinates this yields a factorization $A=QX$, where $Q$ is orthogonal and $X$ is generally not upper triangular. Moreover, given a Wedderburn-adapted orthogonal basis, the transformed-back factors can be computed within the commutant.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-02T00:58:09Z
Xiaoquan Xu, Wei Ji
arXiv categories: math.LO

We study Scott-product compatibility and sobriety for countable meet-continuous directed-complete partial orders (dcpos). We construct a countable meet-continuous dcpo $\mathcal R$ whose Scott space is well-filtered but not sober, although the Scott topology on every finite power is the product of the factor Scott topologies. The ideals of $\mathcal R$ admit a unique finite-parameter description. We also construct a countable meet-continuous dcpo $\mathbb{H}$ with a greatest element whose Scott space is coherent and well-filtered, but whose Scott square has a topology strictly finer than the ordinary product topology. These constructions answer negatively two questions about countable meet-continuous dcpos. On the positive side, we prove that a meet-continuous $L$-dcpo, meaning a dcpo whose principal ideals are complete lattices, is Scott sober whenever its Scott square carries the ordinary product topology. This answers Jia's core-compactness question affirmatively for $L$-dcpos without any countability assumption. Finally, we characterize well-filteredness of $L$-dcpos by boundedness of closed Rudin sets and formulate related open questions.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-02T16:16:12Z
Christian d'Elb\'ee, Yanis Davoust, Jules Tindzogho Ntsiri
arXiv categories: math.LO

We prove that NIP nilrings of bounded nilexponent are nilpotent. We also deduce that NIP $\omega$-categorical $n$-Engel Lie algebras of characteristic $p>n$ are nilpotent, yielding a case of the Lie algebra analogous of Wilson conjecture for $\omega$-categorical groups.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-02T17:20:48Z
Juan Pablo Acosta, Yatir Halevi, Assaf Hasson, Will Johnson, Ya'acov Peterzil
arXiv categories: math.LO

We show that every definable function in a weakly o-minimal expansion of a field $K$ is generically differentiable, where the derivative takes values in the Cauchy completion of $K$, i.e. it is a definable nonvaluational cut. As a consequence, every definable field is definably isomorphic to either $K$ or its algebraic closure.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-02T18:28:28Z
Radek Honzik, Ondrej Je\v{z}il, Mykyta Narusevych
arXiv categories: math.LO

We provide a modern overview of several forcing methods in bounded arithmetic and compare them with forcing in set theory. We specifically discuss the countable forcing framework of Atserias and Muller, the restricted ultrapowers of Bydzovsky and Muller, and forcing with random variables developed by Krajicek. We illustrate these forcing arguments by reviewing the Paris--Wilkie forcing and by giving a self-contained construction of the shallow PHP model constructed by Krajicek. We observe that, from a formal point of view, Krajicek's forcing with uncountable structures can be interpreted in the framework of Atserias and Muller after a countable collapse using an LS argument. We further observe that the countable restricted ultrapowers of Bydzovsky and Muller, used to obtain models of the theory $T_{PV}$, can also be interpreted in this framework. This part serves as a primer on modern forcing methods in bounded arithmetic. In the next part, we discuss the analogies and differences between forcing in arithmetic and set theory. We embed Krajicek's Boolean-valued models into generic extensions of models of set theory, observing that the set-theoretic forcing framework can be used to interpret forcing in arithmetics. In our interpretation, set theory offers a convenient method for formalizing forcing arguments with uncountable structures. We end with a question whether analogies with set theory can facilitate the discovery of new uncountable partial orders for arithmetic.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-04T02:21:07Z
Mahmood Etedadialiabad, Su Gao
arXiv categories: math.LO, math.CO, math.GR

Motivated by the EPPA problem for finite tournaments,we consider various extension properties for partial permutations. We show that for any set $\Pi$ of prime numbers, the $\Pi$-extension property is equivalent to the $\Pi$-LERF. As a consequence of known results, the odd-extension property is then equivalent to the EPPA for finite tournaments. To study the $\Pi$-extension property, we reformate the property using the concepts of EP problems and $\Pi$-solutions. We then show that the existence of a $\Pi$-solution for an EP problem depends entirely on its fundamental group. In particular, when the fundamental group is trivial or cyclic, the EP problem has a $\Pi$-solution for any $\Pi$. These extend some known results of Huang, Pawliuk, Sabok and Wise [HPSW19]. We give examples of EP problems without nilpotent-solutions; they witness that the $p$-extension property and the $p$-LERF fail for any prime $p$. Then we consider a special kind of EP problems whose fundamental groups have two generators. We show that any 1-weakly wandering problem has a $\Pi$-solution for any $\Pi$. For 2-weakly wandering problems, we show that they all have odd-solutions and we completely characterize those without nilpotent-solutions.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-04T18:45:54Z
George Crittenden, Matthew Harrison-Trainor
arXiv categories: math.LO

It was recently shown by Paolini and Shelah, with another proof by Laskowski and Ulrich, that torsion-free abelian groups are Borel complete. This means that isomorphism for torsion-free abelian groups is as complicated as possible, so that torsion-free abelian groups do not admit any meaningful complete isomorphism invariants. We give a proof following the ideas of the Paolini-Shelah argument but with several expository advantages. In particular, the combinatorial part of the argument is much simplified. We make use of the ideas of this proof to show that there is a torsion-free abelian group with no computable copy but with a copy computable from every non-computable set. This answers a long-standing question of Downey and Goncharov.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-04T22:19:19Z
Justin Tatch Moore, Stevo Todorcevic
arXiv categories: math.LO

We study which structural results about Aronszajn trees require the Proper Forcing Axiom and which require only MA(aleph1). In particular, we show that MA(aleph1) is consistent with the existence of 2^aleph1 pairwise non-club-isomorphic coherent A-trees.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-04T22:36:00Z
Lucas Polymeris
arXiv categories: math.LO

We show that unlike $\textsf{PFA}$, $\textsf{MA}_{\omega_{1}}$ is consistent with the existence of $2^{\omega_{1}}$-many Countryman lines which pairwise contain no uncountable isomorphic or reverse-isomorphic suborders. This clarifies an issue regarding the claim that $\textsf{MA}_{\omega_{1}}$ implies that there is a finite basis for the Countryman lines. The family of Countryman lines comes from a family of $2^{\omega_{1}}$-many coherent trees which pairwise contain no club-isomorphic subtrees. To prove this, we first construct such a family of trees using $\diamondsuit$, and then we iterate ccc forcings while preserving this property.

arXiv abstract · PDF

Category theory · primary corpus · published 2026-10-04T23:21:02Z
David Gonzalez, Matthew Harrison-Trainor, Julia Knight
arXiv categories: math.LO

We show that for each countable ordinal $\alpha$, there is a $\mathbf{\Delta}^0_\alpha$ operator that, for all $A$ of Scott rank at most $\alpha$, takes copies of $T_A$ to copies of $A$, where $T_A$ is the tree of tuples corresponding to $A$. For finite $\alpha$, we show that this is best possible. The proof that there is a $\mathbf{\Delta}^0_\alpha$ operator uses Harrington's method of workers. The sharpness result, for finite $n$, uses recent work of Harrison-Trainor on ``unfriendly jump inversion.''

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T04:07:52Z
Weijun Luo, Kelvin Luu, Xinyi Liu, Guangze Luo, Miguel Romero Calvo, Soham Dan, Daniel Yue Zhang, Ying Liu, Mohamed Elfeki
arXiv categories: cs.AI, cs.LG, cs.SE

Agentic benchmarks guide model selection and training. Yet an agent can pass a task without demonstrating the intended capability. Such outcomes constitute unearned passes; their proportion among all passes defines the integrity gap. As agents improve, benchmark surfaces that once seemed harmless can become exploitable, making benchmark validity an ongoing maintenance problem. We introduce a process-verification framework that audits passing trajectories, distinguishes evidenced reward hacking from verifier weakness, and localizes exploitable surfaces for repair. Across 3,810 passing trajectories from 29 model-benchmark cohorts, confirmed violations often increase with model generation but not monotonically. On SWEBench Pro V1.0, confirmed violation rates rise from 24% to 73% between Opus 4.7 and Fable 5 on matched tasks; later cohorts fall to 11% for Fable 5.1 and 0% for GPT-6 Astra. These comparisons are descriptive: configurations were not normalized, and the latest models also pass fewer exploitable tasks. Violations concentrate around a small set of recurring surfaces, especially unintended access to reference solutions through git history. Three repair case studies across two benchmarks show why blocking a recorded exploit is insufficient: the same protected information can remain accessible through another route. Therefore, we combine minimal patches with exploit replay and fresh agent evaluation, auditing new passes under the original standard. No evaluated attempt against the final patches reached the protected channel, and every post-patch pass was judged legitimate. Benchmark integrity requires ongoing maintenance: audit passing behavior, repair the enabling surface, and re-evaluate both exploit access and legitimate solvability.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T04:53:45Z
Jingjie Ning, Xueqi Li, Yibo Kong, Dongting Li
arXiv categories: cs.AI, cs.CL, cs.SE

How much of a running workflow should a language model agent revise? ControlScope compares continuing generated code, editing the next tool call's data arguments, and replacing the unfinished workflow from the same public execution state. The nested permissions separate available repairs from the actions an agent selects. We evaluate one-time and repeated reviews across filesystem tasks, ALFWorld, and AppWorld. Across two source programs per task and three reasoning-reviewer draws on 20 filesystem tasks, FULL completes 15-16 tasks versus 13 for KEEP; across four fast draws it completes 10-13 versus 13. Fresh student-record confirmation reproduces a batch-read repair. ALFWorld fast panels yield KEEP/ARG/FULL scores of 85/86/87 on 87 tasks across 52 scenes and 134/134/127 on 134 tasks across four scenes; reasoning on the 87-task cohort also yields 85/86/87 with substantial review cost. An AppWorld V1 official-test panel of 585 task instances from 195 scenario templates shows small net differences. Frozen replays expose viable agent-written replacements interrupted by later revision in two failed file-organization runs. An offline source-trajectory midpoint comparison shows later reviews completing an insufficient repair. Five-call protection saves 19.4% of logged model output and loses one success across 20 fresh source runs. An argument-only shortcut shows that the broader sampled policy can overlook a cheaper successful edit available in both operation sets. These outcomes tie repair access to actual choices and subsequent execution.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T07:14:58Z
Hai Duong, Thanh Le, ThanhVu Nguyen
arXiv categories: cs.LG, cs.SE

Transformer-based models are widely used for reasoning, coding, and multimodal agentic tasks. To provide formal assurance of desirable behaviors, such as robustness, safety, and fairness, neural network verification techniques prove required properties and provide auditable guarantees before deployment. However, prior work remains limited to small or restricted Transformers, and maintaining precision across deep models remains challenging. In this work, we introduce ZonoGPT, an abstract domain for verifying large transformers that maintains a space complexity independent of network depth. ZonoGPT uses a structured zonotope and a generator reduction mechanism to efficiently preserve correlations. To maintain precision, it introduces block-specific fused transformations for Attention and LayerNorm that retain feature relations, along with an affine transform for GELU that preserves generator relations. These mechanisms enable \tool{} to be the first approach to verify standard architectures, scaling to official HuggingFace models up to GPT-2 Medium (24 blocks, 300M+ parameters) and successfully verifying 1,339 instances across text and vision tasks.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T08:12:22Z
Hai Duong, Thanh Le, ThanhVu Nguyen
arXiv categories: cs.LG, cs.SE

Formal verification can play a key role in ensuring the reliability of Deep Neural Networks (DNNs) deployed in safety-critical systems. Modern DNN verifiers employ a branch-and-bound framework, which alternates between branching (splitting into smaller subproblems) and bounding (pruning subproblems) to efficiently explore the verification space. However, existing branching heuristics make greedy decisions based on static scoring functions. They do not anticipate long-term efficiency or leverage the growing availability of verification data to improve performance. This work introduces RSB, a reinforcement learning framework that learns to refine baseline branching heuristics. It trains an actor-critic architecture to maximize cumulative future rewards rather than immediate scores. The actor generates attention weights from observations of raw neuron features and learned graph embeddings, which rescale baseline heuristic scores to guide neuron branching. Evaluation on 600 challenging instances demonstrates that RSB consistently outperforms state-of-the-art branching heuristics, solving 11% more instances while reducing branch exploration by 50%.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T08:48:41Z
Hai Duong, Thanh Le, ThanhVu Nguyen
arXiv categories: cs.SE, cs.LG

Neural network verification (NNV) formally verifies that a network satisfies a specified property for all inputs within a defined region. Modern NNV tools employ abstract domains to compute a sound over-approximation of the network's behavior from the given input region, thus the tightness of these abstractions essentially determines efficiency. A long line of increasingly precise domains has been developed, but they all describe the valid input region in the same restrictive way, e.g., an Lp-norm ball. A practical input region is rarely a simple Lp ball, but rather a combination Lp ball with additional constraints. Verifying a network over such a region with existing abstraction produces a loose over-approximation, which results in either failing to verify a property or spurious counterexamples. We introduce Constrained Lagrangian Abstract Domain (CLAD), a new abstract domain that computes a sound over-approximation of neural networks over input regions defined by a combination of convex constraints. CLAD propagates these constraints and tightens bounds over the true feasible region. However, bounding a neuron over the intersection of these constraints has no closed-form solution, so CLAD relaxes each constraint into the objective with a Lagrange multiplier and solves the resulting max-min problem with a projected primal-dual method, alternating a projected gradient step on the input with a multiplier update. CLAD supports any convex constraint with a subgradient, e.g., from automatic differentiation. We evaluate CLAD on 1,944 instances across four convolutional networks with motion-blur structured perturbations with halfspace or L2-ball constraints. On standard unconstrained Linf property, CLAD verifies as many instances as GCPCROWN at a similar runtime. On constrained properties, CLAD verifies 60\% more instances than GCPCROWN on L2-ball properties, and 22% more in total.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T13:57:29Z
Prateek Kumar Rajput, Abdoul Kader Kabore, Yewei Song, Melissa Tessa, Tailia Malloy, Jacques Klein, Tegawend\'e F. Bissyand\'e
arXiv categories: cs.CR, cs.SE

LLM coding agents can traverse hundreds of intermediate code states before submitting a solution. Evaluating only the final artifact leaves the evolution of security findings unmeasured. We introduce the Security Debt Line Integral (SDLI), which accumulates static-analysis risk when an agent reaches a new best test pass ratio. We instantiate it with four static application security testing (SAST) tools and study artifacts from 830 passing SWE-bench runs, 712 ProgramBench final workspaces, and 13 public MirrorCode trajectories. The two large populations use the final-state special case of SDLI. Two-tool Common Weakness Enumeration (CWE) class agreement occurs in 3.9% of SWE-bench runs and 26.2% of the 80 ProgramBench runs passing at least 90% of official tests. These are scanner findings, not validated vulnerability rates. Excluding three advisory-heavy classes reduces the latter rate to 6.2%. Same-task runs differ in their measured scores, while one reconstructed ProgramBench run exposes persistent findings from its first implementation write. A repair case study reduces the scanner signal while preserving tested behavior, but also reveals sensitivity to equivalent API rewrites. SDLI offers a way to study progress and security findings together. Its value for steering agents and confirming exploitable vulnerabilities remains to be established.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T15:38:52Z
Tianjian Liu, Shicheng Feng, Jin'ao Shang, Xiaoting Lyu, Bin Wang, Zonghua Zhang, Lei Xue, Wei Wang
arXiv categories: cs.CR, cs.SE

Large language models (LLMs) have shown strong potential for assisting software and security analysis tasks, yet their effectiveness in cryptographic symbolic protocol verification remains insufficiently understood. In this paper, we conduct the first systematic evaluation of the capability of state-of-the-art LLMs in cryptographic symbolic protocol verification. To quantify this capability, we propose \textsc{CRoST} (Coverage Rate of Solve Tree), a proof-based metric derived from the verifier's proof skeleton that measures the similarity between generated lemmas and reference lemmas. We then establish the rationale of \textsc{CRoST} through both theoretical analysis and empirical validation. The evaluation results show that state-of-the-art models achieve 38.82\% coverage on average, with 14.4\% of generated lemmas exceeding 80\% coverage, indicating that LLMs can already generate useful lemmas to a certain extent. However, they still exhibit non-trivial failure modes on complex multi-phase protocols, show diminishing returns under naive scaling, and incur substantial verification overhead. These findings clarify the practical potential and limitations of LLMs for protocol verification and motivate future work on complex real-world protocols.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T19:40:35Z
Om Shankar Tiwari, Tangi Vass, Gagan Deep Singh
arXiv categories: cs.SE

AI coding agents fail in two coupled ways. They spend most of their context window rediscovering where things live, and they assert success without evidence when the work gets hard. Repository indexes address the first with cheap context, and orchestration frameworks with adversarial review address the second with accountability. Both describe the same object, the structure of the codebase, at two timescales: what is true of the code now, and what was verified to be true, at which revision, by whom. Assay makes that observation operational. Every claim an agent makes (tests pass, no secrets, behavior preserved) is bound to the Merkle hash of the dependency cone of the code it covers, so the claim is stale exactly when that code or anything it depends on changes. We show the binding is sound and minimal, and that the blast radius of a change is precisely the set of claims it invalidates. On the graph we place a risk-proportional evidence obligation, a bounded review protocol with separation of duties, and a merge gate that consults no model: coverage, freshness, signatures, exit codes, plausibility, evidence monotonicity (the mechanical form of "do not delete the failing test"), and review status. Assay is a dependency-free Python tool with an MCP server. On five public repositories a 600-token brief costs 14x to 114x less than an exploration proxy, warm rebuilds are up to 5x faster than cold ones, cone binding re-verifies 7.9% to 81.9% of claims where repository binding re-verifies all of them while per-module binding misses 23% to 68% of required invalidations, and the gate blocks 9 of 9 scripted adversarial behaviours while admitting the honest ones. Every number in this paper is generated by the released scripts.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-28T20:01:35Z
Jianxing Chen, Xiao Yu, Shipra Agrawal, Zhou Yu
arXiv categories: cs.CL, cs.AI, cs.SE

Computer-use agents (CUAs), while capable of completing computer tasks in everyday and professional workflows, can cause unintended harm even under benign instructions and environments. However, detecting such harm remains challenging. First, it requires careful, task-specific reasoning: verifiers guided only by general safety criteria often overlook many important but subtle harmful behaviors. Second, it requires active investigation: past trajectory screenshots show what the agent did but not always what actually changed in the environment, so LLM-as-a-judge verifiers that rely on screenshots alone may be unable to determine the actual consequences of actions. To address these challenges, we introduce SCOUT, a two-stage agentic safety verifier that synergizes reasoning-intensive rubric generation with tool-intensive evidence gathering. First, our SCOUT rubric generator extensively reasons over the task and the agent's trajectory to determine what successful and safe execution should entail, generating task-specific completion and safety rubrics. Then, our SCOUT probing agent follows these rubrics to interact with the post-execution environment and collect grounded evidence for final safety and completion judgments. We evaluate our framework on two computer-use safety benchmarks. On AutoElicit-Bench, SCOUT achieves 75.4 unsafe F1 and 74.5 completion F1, outperforming LLM-as-a-judge verifiers and naive tool-use verifiers. SCOUT leads on OS-Blind with 76.4% unsafe detection accuracy. Test-time reflection reduces final unsafe execution rates from 30.2% to 17.2% on AutoElicit-Bench. Ablations and analysis show that tool-free rubric generation in SCOUT elicits substantially more reasoning and is crucial for safety detection across verifier backbones, especially non-frontier ones. A preliminary extension to coding tasks shows that SCOUT can support safety verification beyond computer-use.

arXiv abstract · PDF

AI agent assurance · cs.SE candidate · published 2026-09-29T11:50:55Z
Rohith Reddy Bellibatlu, Zichong Wang, Wenbin Zhang
arXiv categories: cs.SE, cs.AI, cs.LG

Tool-using agents are entering settings where a wrong action carries real cost, and the benchmarks certifying them grade what each simulated tool call reports having done, assuming the tool did what its interface advertises. The audit taxonomies we survey publish no category for that assumption, and a defect beneath a score is present on every rerun. We treat a tool's advertised surfaces as an executable contract, check the implementation against it, and trace each score's provenance through the task files and evaluator code to the verdicts that derive from state a defective tool should have written. Across 34 audited mutating tools in four benchmarks we confirm seven tool defects and one evaluator property at pinned commits. On injected defects the checker raised no false positive in 25 flags, flagged 2 of 5 negative controls, and missed most: in 29 of 33 scored misses a clause covered the defect but no probe revealed it. The checker's own static half, run alone, flags 14 of 17 confirmed sites, so on these findings the dynamic half confirms and traces rather than discovers. Twelve further AgentDojo tools, with six held-out tools and the seven audited first, complete its 25-tool mutating surface, on which at least 5 tools diverge from their advertised surface as our contracts read it, a rate for AgentDojo alone. No gold trajectory reaches either tau2-bench defect; on 1,120 paths built to isolate the telecom defect, a number fixed by construction, the evaluator rewards a refuel of a suspended line and fails the repaired tool. The clearest case is a clinical benchmark whose tool tells the agent each write executed under a documented no-write design its interface does not disclose; its grader takes that message as evidence, so its action success rate records whether a request carried the expected payload, not whether any record changed.

arXiv abstract · PDF