arXiv weekly literature review

Dependent and Homotopy Type Theory · primary corpus · published 2026-10-19T18:59:05Z
Yoshihiro Maruyama
arXiv categories: cs.LO

Tripos theory constructs categorical models of higher-order logic from indexed logical data. We develop higher tripos theory and higher tripos-to-topos construction recovering the classical construction on zero-types through a covering criterion. The higher tripos-to-topos construction yields elementary $\infty$-toposes with closed bounded hierarchies of univalent universes, thus establishing a logical adjunction between $\infty$-triposes and elementary $\infty$-toposes with univalent universes. We also construct a logically conservative higher completion of regular $1$-categories with weak section families and a finite-limit-closed projective cover. This completion preserves original maps, predicates, and existing dependent products, and gives criteria for extending interpretations while preserving logical structure. With strongly inaccessible size bounds, Kleene assemblies instantiate the construction, producing a cumulative hierarchy of univalent universes that classifies every family in the completion and recovering the effective topos as the category of zero-types. We then establish an arithmetical completeness result: for a uniformly computably presented family, the numerical index set for identity with a fixed classifier code is $\Pi^0_2$-complete. We also construct two inequivalent univalent classifiers with the same global homotopy type: every internal map from one to the natural-number object is constant, whereas the other admits a nonconstant such map. These reconstruction, preservation, and computability results contribute to the higher effective-topos program of Awodey-Emmenegger and Anel-Awodey-Barton.

arXiv abstract · PDF

Dependent and Homotopy Type Theory · primary corpus · published 2026-10-19T20:36:59Z
Fedor Part, Valery Isaev, Sergey Sinchuk
arXiv categories: cs.LO, cs.AI

This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-L\"of Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.

arXiv abstract · PDF

Dependent and Homotopy Type Theory · primary corpus · published 2026-10-20T15:29:47Z
Niyousha Najmaei, Niels van der Weide
arXiv categories: cs.LO, cs.PL, math.CT

Homotopy type theory (HoTT) provides a natural setting for studying the metatheory of type theory, as it comes with additional extensionality principles compared to ordinary Martin-L\"of type theory. In particular, it is especially suitable for developing semantics of type theory, where one distinguishes two kinds of models: strict models, which give us sound interpretations, and pseudomodels. Pseudomodels are useful as they occur prevalently and can be turned into strict models by constructions called strictifications. However, the commonly used strictifications do not translate well to HoTT, as they require assumptions that are generally not satisfied by concrete examples of models. We show how to carry out the universe model construction, due to Voevodsky, in HoTT. Under this construction, every pseudomodel together with a universe type closed under enough type formers gives rise to a strict model. We also show how to interpret type formers in the resulting model assuming that the universe is closed under them. Finally, we demonstrate that this construction generalises existing instances of strict set models in the literature, and we apply it to more examples, yielding presheaf models and assembly models of type theory in HoTT. Our results are formalised in Rocq using the UniMath library.

arXiv abstract · PDF

Dependent and Homotopy Type Theory · primary corpus · published 2026-10-20T20:33:52Z
Keri D'Angelo, Liron Cohen, Luke Serafin, Dexter Kozen
arXiv categories: cs.LO

Reasoning about higher identity types uses two equalities, strict equality and equivalence of cells witnessed by a path. Strict equality is a congruence for every operation on cells, but associativity and the identity laws fail for it. Equivalence of cells satisfies those two laws, but it is not a congruence. Representations of higher identity types often conflate equational properties that hold strictly with those that hold only up to a path. We separate the two and axiomatize the former, introducing SEq, an equational theory generated by eleven axioms for strict equality between cells. We prove soundness and completeness for homotopy models, and completeness already over finite CW-complexes. Nine of these axioms form a strongly normalizing rewrite system whose normal forms are unique up to picture equivalence, and the resulting word problem is decidable in exponential time. We also give presheaf models over a cubical base category in which composition arises from a pushout in the base category itself, without requiring Kan filling structure. The same pushout structure provides explicit higher-dimensional witnesses for associativity and the identity laws.

arXiv abstract · PDF

Dependent and Homotopy Type Theory · primary corpus · published 2026-10-21T11:26:54Z
Thorsten Altenkirch
arXiv categories: cs.LO

We explain an attempt to define semi-simplicial types (SST) in homotopy type theory by first defining a small type theory whose contexts are exactly the data of semi-simplicial types, constructing $\mathrm{SST}\,n$ uniformly in that syntax, and then interpreting the syntax in the universe. The syntax can be defined without any truncation and without K, and the construction of $\mathrm{SST}\,n$ goes through. The naive interpretation does not: it transports along the semantic images of equations that hold only propositionally, and making these transports agree needs uniqueness of identity proofs (UIP) for the semantic types. Moving the problem into the syntax, by making composition a constructor of a higher inductive-inductive type (HIIT), does not remove it either: it reappears as a coherence problem in the syntax. Fording the HIIT (storing equations instead of computed indices), with conditional rules, makes the syntax provably a set. This is UIP for the syntax, obtained by encode-decode, and it does not by itself restrict the semantics; but the naive interpretation of the conditional rules again needs UIP for the semantic types. A semantics into groupoids that avoids UIP will be discussed in a separate note. The Agda development accompanying this note is in the repository https://github.com/txa/sst-new.

arXiv abstract · PDF

Dependent and Homotopy Type Theory · primary corpus · published 2026-10-25T12:50:42Z
Thierry Coquand
arXiv categories: cs.LO

We present Unit, a type checker for dependent type theory with a module system in the tradition of Automath and a uniform treatment of definitions: two uses of a definition are compared by name and arguments before anything is unfolded, and otherwise the definition declared last is opened. There is no unification, no instance search, no tactics and no unfolding heuristic, so the work of checking can be observed and compared with the informal proof. With Unit we have checked a model of univalent type theory, synthetic algebraic geometry up to Ch\^atelet's theorem, and synthetic Stone duality with its cohomology. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-19T13:07:56Z
Gabriele Buriola, Giacomo Cozzi, Antonia Dammrau, Anton Freund
arXiv categories: math.LO

We establish a general result on the proof-theoretic strength of well-ordering principles in reverse mathematics. The novelty is that our result gives information over base theories as weak as $\mathsf{RCA}_0$, while previous results of Arai, Pakhomov-Walsh and Buriola-Weiermann required the stronger base theory $\mathsf{ACA}_0$. On the way, we strengthen a result of Carlucci-Mainardi-Rathjen about the ordinal analysis of theories of the form $\mathsf{RCA}_0+\text{``$\alpha$ is a well-order"}$.

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-19T19:31:19Z
Jonathan Chan, Aaron Stump
arXiv categories: cs.LO

In conventional natural deduction, a proof of a proposition is a derivation tree constructed out of inference rules with some number of premises and a conclusion judgement. For propositional logic, in contrast to the other connectives, the rule for disjunction elimination of $A \vee B$ involves concluding with an auxiliary formula C from $A \vdash C$ and $B \vdash C$. Not only is this asymmetry unsightly, it also introduces the need for commuting conversions across disjunction eliminations to transform between proof derivations that are morally equivalent but not $\beta\eta$-equivalent. To resolve the asymmetry, Jean-Yves Girard suggests a disjunction elimination rule with multiple conclusions A and B, but claims that "we have no way of bringing them back together". In this work, we pursue Girard's proposal using the key insight that proof derivations need not be trees, but may be directed acyclic graphs (DAGs) in general. Derivation rules are represented as nodes, premises as incoming edges, and conclusions as outgoing edges. Treating derivations as DAGs permits using the alternate rule by ensuring that the subderivations pointed at by each conclusion eventually join up at a new concluding node. Commuting conversions can then be formulated in terms of interactions with this join node. We explore ways to design a proof graph language with reduction and commutation rules such that proof simplification retains its concluding judgements, i.e. type preservation. In particular, we examine two styles of reduction rules: a local style, which only requires looking at the relevant subgraph of a whole proof but necessitates a number of extraneous constructs to satisfy type preservation; and a global style, which doesn't require all the extraneous constructs but necessitates looking at the entire proof graph as a whole.

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-20T05:04:13Z
Ludovic Patey
arXiv categories: math.LO

An ordered $\omega$-variable sequence over a finite alphabet~$A$ is an infinite sequence over the extended alphabet $A \sqcup \{ x_0, x_1, \dots \}$, where each variable kind appears at least once, and the last occurrence of $x_i$ appears before the first occurrence of $x_{i+1}$. The Ordered Variable Word theorem states that for every finite coloring of the words over a finite alphabet~$A$, there is an ordered $\omega$-variable sequence~$W$ over~$A$ such that every word induced by substituting variables with letters, and cutting before the first undefined variable, has the same color. In this article, we prove that the Ordered Variable Word theorem is $\Pi^1_1$-conservative over $\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2$. It follows that the tree theorem for singletons by Chubb, Hirst, and McNicholl is $\Pi^1_1$-conservative over $\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2$, answering a long-standing open question. Lemma 3.13 was found by Claude Opus 5.5 (Anthropic).

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-21T15:26:09Z
Thomas Ehrhard (IRIF (UMR\_8243), Inria, PICUBE), Aymeric Walch
arXiv categories: cs.LO, math.CT

Coherent differentiation has been introduced a few years ago as a refinement of the (categorical semantics of the) differential lambda-calculus and of differential linear logic, compatible with the determinism of computation, and hence in categories where addition of morphisms in the hom-sets is only partially defined. In this setting differentiation is implemented by a kind of ''tangent functor'', with the difference that it maps an object to its object of summable tuples rather to a tangent bundle. In our earlier work, these tuples were pairs in the case of simple differentiation, and families indexed by integers when dealing with Taylor expansion and the Fa{\`a} di Bruno formula. We push this idea further, considering now tuples indexed by an arbitrary commutative partial monoid satisfying a nonnegativity condition. The monoid structure on these indices plays a crucial role in the definition of the ''differential'' calculus associated with this ''tangent functor''. In that way, and without changing the general categorical infrastructure of coherent differentiation, this theory accommodates new notions of ''differentiation'' of which we describe several instances. Among many others, such notions include various forms of finite differences as well as Taylor expansion truncated at any fixed degree, and finite Taylor expansion of a fixed finite degree with a remainder.

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-24T22:48:28Z
Michal Garlik, Svyatoslav Gryaznov, Jiaqi Lu, Rahul Santhanam, Iddo Tzameret
arXiv categories: cs.CC, cs.LO

We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as Polynomial Calculus Resolution ($\mathsf{PCR}$), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to $\mathsf{NC}^2$, such as $\mathsf{VNC}^2$ and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below $\mathsf{VNC}^2$ into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Under an algebraic analogue of the Krajicek--Razborov conjecture, our results suggest that proving superpolynomial lower bounds for general algebraic circuits will require stronger reasoning than that used in the rank-based proofs studied here. Specifically, we show the following.

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-25T12:53:46Z
Kenji Tokuo
arXiv categories: cs.LO, math.LO

We propose a typed lambda calculus based on quantum logic. We first present a natural deduction system for quantum logic with the Sasaki hook as its implication operation and then formulate a typed lambda calculus connected to this system through the Curry-Howard correspondence. We prove soundness and completeness of the former with respect to orthomodular lattices and strong normalization of the latter. The resulting lambda calculus has the characteristic feature that only one assumption is available in the typing derivation that serves as the premise of $\lambda$-abstraction. Under this restriction, ordinary currying is not available in general, but it is still possible to perform $\lambda$-abstraction by combining multiple assumptions into a single argument of product type and to construct a term corresponding to a deduction using the Sasaki projection.

arXiv abstract · PDF

Proof Theory and Reverse Mathematics · primary corpus · published 2026-10-25T20:17:08Z
Bryan Ford
arXiv categories: math.LO, cs.LO, cs.PL

What does a recursive definition mean when the logic is grounded, so a sentence is true only if a terminating process makes it so? Kripke's answer for the special case of truth was the least fixed point. This paper takes that answer as a rule. Reflective Grounded Arithmetic (RGA) already writes any recursive definition as one self-referential term, paradoxes included. Inductive Grounded Arithmetic (IGA) adds the elimination rule for every positive one, so that accessibility, the winning positions of a game, and grounded truth itself each come with their own induction principle. The rule is sound for the omega model and the system is consistent, both machine-checked in Isabelle/HOL. With the rule, IGA proves Goodstein's theorem outright, in a logic without implication at an undecided hypothesis, and the Kirby-Paris hydra game for primitive recursive strategies, both with every step of the arithmetic a grounded derivation. It proves the Cantor normal forms well-founded, from which the well-foundedness of the standard $\varepsilon_0$ notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every $\varphi(n,0)$. It defines Kripke truth for RGA's own language as one fixed point that agrees with the omega model exactly. Two equivalences locate what the classical world has and the grounded one does not. IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order, and bivalence of accessibility for an order is sound exactly when the order is well-founded; so $\Gamma_0$ lies at most one instance of excluded middle away, at the accessibility predicate of the notation, and that instance, the well-foundedness sentence and one membership claim in a primitive-recursive form of Kleene's $\mathcal O$ are interderivable over IGA.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-19T03:46:08Z
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, Rocky Liu
arXiv categories: cs.PL

Type systems for metaprogramming take one of two approaches to safeguarding the scopes of variables in generated code. They either use Environment Classifiers (EC) to identify scopes by name (Taha and Nielsen, 2003), or they use Contextual Modal Type Theory (CMTT) to match scopes by structure (Nanevski, Pfenning, and Pientka, 2008). In this paper, we connect these two approaches by compiling a calculus with polymorphic environment classifiers, subtyping, and mutable references to a CMTT-based calculus with polymorphic contexts, mutable references, and first-class substitutions. The key idea is to map each environment classifier to a context. We prove that the compilation preserves types and that compilation preserves the behavior of metaprograms. Both proofs are mechanized in Agda. The compilation shows that CMTT is at least as expressive as environment classifiers. We conjecture that the converse compilation is difficult, because environment classifiers impose a stricter regime on the metaprogram.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-19T12:22:30Z
Christopher Dutchyn
arXiv categories: cs.PL

Static type systems for Scheme have traditionally followed one of two paths: manifest type checking with multi-dispatch (Clifton and Leavens, 2005) or latent occurrence typing tailored for untyped interoperation (Tobin-Hochstadt and Felleisen, 2008). In this paper, we propose Polarized Scheme, a static foundation built upon polarized type theory and the duality of computation. In Polarized Scheme, values are positive data producers (A+) and continuations are negative observation consumers (~A+). Functions operate symmetrically under dual viewpoints: as forward value-transformers and as backward continuation-transformers. Computation exists exclusively at the interaction cut <P|K> executed on a focus-and-context abstract machine separating positive data focus from negative return contexts (R). Delimited control (shift/reset) and continuation marks are expressed directly as Return Stack frame operations parameterized by the prompt's ambient answer type without polluting producer data types. Furthermore, we formalize the hygienic macro system as an interleaved continuation-passing pipeline, where macro expansion erects its own continuation hierarchy nesting into runtime evaluation. We prove Subject Reduction, Progress with respect to prompt-delimited stacks, prove Duality Bisimilarity, characterize Return Stack reclamation for dynamic closures, and report on an executable reference implementation in a verified dialect of Go with a verified cut-elimination dispatcher

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-19T15:41:03Z
Aditya Ranjan Jha, Jason Zhijingcheng Yu, Umang Mathur, Prateek Saxena
arXiv categories: cs.PL, cs.AR, cs.LO

Hardware components communicate through clock-cycle-sensitive protocols. Hardware Description Languages (HDLs), however, provide limited support for expressing these protocols or for checking that independently developed components agree on them. When components disagree, the composed design can perform unsynchronized exchanges or stop making progress. We call these failures communication-safety violations. Communication safety is therefore a global property, determined by interactions between multiple components. This makes it difficult to check modularly. This paper presents Pact, a typed extension of Anvil for modular verification of communication safety in synchronous hardware. Pact types describe message-passing, control-flow, and clock-cycle behaviour. Each component is checked against its type. Compatible types then guarantee that the components compose into a communication-safe system. Pact also supports incremental design. It can check a subsystem before the full system context is available. The check produces a summary type that captures the communication behaviour left for future compositions. To reduce annotation burden, Pact infers types by abstracting payload values while preserving communication, timing, control, and fairness. These inferred types are optimal for the checker: whenever some checker-accepted types can prove compatibility, the inferred types can prove it as well. Type inference and type checking are decidable, and compatibility is decided by a sound and complete algorithm. We implement Pact by extending the Anvil compiler and evaluate it along four dimensions: detecting communication errors during incremental design, expressiveness on ten clock-cycle-accurate translations of open-source hardware IPs, compatibility-checking time, and generated hardware overhead. Pact expresses realistic protocols and verifies all ten benchmarks in reasonable time.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-20T02:34:12Z
Matthew Toohey, Ara Jamalzadeh, Ningning Xie
arXiv categories: cs.PL

This paper introduces a novel calculus that models first-class environments and function application paradigms using standard record types. By proposing new extensions to general record types, we achieve a design that is remarkably simple and principled. We formalise this design in a core calculus and prove several desirable properties, including type soundness, normalization, and a simulation of the simply typed lambda calculus. Additionally, we extend the design with mutable references. The calculus, its semantics, along with the extension, and all stated properties are fully mechanized in the Lean 4 proof assistant, alongside an interpreter formally verified to be equivalent to the operational semantics.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-20T16:59:43Z
Jake Masters, Nobuko Yoshida
arXiv categories: cs.PL, cs.LO

\emph{Multiparty session types} (MPST) is a type discipline for ensuring distributed programs are implemented correctly \emph{by construction}. MPST starts by specifying a choreographic protocol as a \emph{global type} and \emph{projects} it onto each participant, generating \emph{local types} with a guarantee of type soundness and deadlock-freedom. A central issue of MPST is that its type soundness is fragile, as it must be proven each time with respect to a chosen projection algorithm under specific semantics with a specific program correctness goal. To overcome this problem, we propose general criteria for a \emph{good projection} -- a set of requirements for projection algorithms by which type soundness, deadlock-freedom and liveness of distributed programs are \emph{automatically} derived. Using the criteria, we prove that 8 distinct projections in the literature are good under both synchronous and asynchronous semantics, and that 4 are incorrect, failing type soundness. We extend the good projection criteria to mixed choice global types and asynchronous communication optimisations, proposing new ``good projection'' algorithms. We apply properties of good projections to prove \emph{separation} and \emph{expressiveness} results over the projection algorithms and MPST typing systems. Having a generalised typing system that is robust with respect to the good projection criteria, we provide an implementation with mixed choice global types that is \emph{modular} with respect to a chosen projection algorithm and desired program properties. Our separation results help programmers make informed trade-offs between complexity and expressiveness when choosing projection algorithms, and our theory ensures their chosen algorithms are correctly applied.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-21T13:37:45Z
Matteo Acclavio, Giulia Manara, Fabrizio Montesi, Marco Peressotti
arXiv categories: cs.LO

A new approach to the theory of choreographic languages has recently been proposed, based on the interpretation of choreographies with finite behaviors as proofs in an extension of linear logic. This paper further develops this approach to cyclic proofs to be capable of representing infinite behaviors, and prove a completeness result for choreographies with respect to the class of lock-free networks. We show that in a choreographies-as-proofs correspondence, the proof equivalence induced by rule permutations corresponds to bisimilarity, and that, under adequate assumption on the procedure definitions, the proof search procedure has a finite search space, and can be used to extract a choreography from a network.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-22T12:47:06Z
Torben {\AE}gidius Mogensen
arXiv categories: cs.PL

L4 is a generic, reversible, linearly-typed, low-level language intended as an intermediate language for compiling reversible programming languages to reversible machines. L4 is intended to replace and generalise RSSA, a reversible SSA form. Inspiration is drawn from other low-level reversible languages such as HSSA. In this paper, we define L4 first informally, and then give a formal type system and a bidirectional small-step semantics for L4: The rules have direction indicators to determine forwards or backwards execution, and the direction can be changed during execution.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-23T12:40:01Z
Sjors Wortelboer, Dan Frumin, Jorge A. P\'erez
arXiv categories: cs.PL, cs.DC

Session types are a type-based approach to correct message-passing programs, where types specify protocols for channels and type checking guarantees communication correctness. Traditional session types express regular protocols only, which leaves out many protocols found in practice. Aiming at overcoming this limitation, Nested Session Types (NSTs) can specify nested recursive protocols. NSTs are known to be characterised by one-counter machines and deterministic context-free languages. In this paper, we study the expressiveness of ASP (Asynchronous Session Processes), the process model associated with NSTs as introduced by Das et al. We prove that AST is Turing complete by giving a correct encoding of two-counter machines into typed processes. Our encoding uses a non-trivial state-aware representation of counters and instructions that is neatly governed by NSTs.

arXiv abstract · PDF

Type Systems and Program Calculi · primary corpus · published 2026-10-23T17:24:03Z
Toby Ueno, Ezra Cooper, Simon Fowler, Sam Lindley
arXiv categories: cs.PL

React is currently the most popular JavaScript library for front-end web development. It endows UI components with state via the useState construct, through a mechanism that we name hook-indexed state. However, React's implementation of hook-indexed state is both fragile and poorly understood. Programmers frequently experience unexpected behavior, and the benefits of programming in this paradigm are wholly unclear. We define $\lambda^\mathsf{react}_\mathsf{hook}$, a core calculus that captures the essence of hook-indexed state, and give it a type system to statically rule out unexpected behavior. We then translate $\lambda^\mathsf{react}_\mathsf{hook}$ into a calculus $\lambda^\mathsf{react}_\mathsf{ref}$ based on ML-style references, and prove that this translation preserves typability and semantics, thus showing that hook-indexed state is expressible in terms of standard references. The translation is local and admits a compositional definition, but involves significant code duplication. As well as illuminating the essence of state in React, our observations can inform the design of future reactive programming systems.

arXiv abstract · PDF

LLM-Assisted Program Verification · cs.SE candidate · published 2026-10-19T00:44:11Z
Brhane Teamrat Gidey, Tiantian Yang, Nikta Akbarpour, Simone Bartucci, Francesco Calimeri, Song Wang
arXiv categories: cs.SE

Large language models (LLMs) demonstrate strong code-generation capabilities but often struggle with functional correctness due to implicit or ambiguous behavioral requirements. We present CG2, a contract-guided code generation framework that translates natural-language tasks into structured behavioral contracts specifying interfaces, preconditions, postconditions, and invariants. CG2 fine-tunes an LLM to generate these contracts and introduces an iterative semantic validation and repair process to identify and correct incomplete, inconsistent, or incorrect specifications before guiding an unchanged downstream code-generation model. We evaluate CG2 on 1,007 held-out tasks using five code LLMs: DeepSeek-Coder-V2-Lite-Instruct, Ministral-3-14B-Instruct-2512, Qwen2.5-Coder-14B-Instruct, Qwen2.5-Coder-32B-Instruct, and Qwen3.5-27B. Results show that CG2 consistently improves pass@1 over direct code generation by 1.49-3.27 percentage points (7.58%-22.45% relative improvement) and over contract guidance without fine-tuning by 1.19-2.38 percentage points (7.04%-14.65% relative improvement). Manual analysis further reveals that semantically correct contracts are associated with higher code-generation accuracy. These findings demonstrate that explicitly specifying and validating behavioral requirements can improve functional correctness without modifying downstream code-generation models.

arXiv abstract · PDF

LLM-Assisted Program Verification · cs.SE candidate · published 2026-10-19T09:51:05Z
Weiqi Wang, Marie Farrell, Liping Zhao, Lucas C. Cordeiro
arXiv categories: cs.SE

Bounded model checking unrolls a program into a single formula, so a function holding a loop costs the solver a fresh copy of that loop at every call site. Function contracts break that coupling. Verify the body once against its contract, then replace each call by a stub derived from it. CBMC supports this through dynamic frame condition checking, applied at industrial scale, but with no formal account of why the replacement is sound and no characterisation of what the frame check costs. We present the function-contract framework for ESBMC. The clause syntax, both phases, and the first assigns enforcement the tool has had are all introduced here. Its technical core is an observational frame rule: snapshot the locations the contract does not permit the function to write, then compare them at exit. The encoding emits a number of verification conditions set by how many globals the program has, not by how many writes the body performs, while dynamic frame condition checking grows with the write count. That is a property of the encoding rather than a timing, so it moves with neither the machine nor the solver. The rule itself is the classical one; what we add is its bounded form inside a BMC encoding, with the pipeline's algebraic skeleton machine-checked in Lean 4 and the limits of that model stated. We evaluate on synthetic sweeps, SV-COMP tasks, an ANSSI X.509 parser, the FreeRTOS heap_1 allocator, and the ML-KEM reference implementation whose CBMC contracts we reuse unchanged. At the coefficient count FIPS-203 mandates, neither tool finishes on the monolithic route inside ten minutes, and both finish on the modular one. The framework is merged into ESBMC master. Contracts are what is left when unrolling runs out of room.

arXiv abstract · PDF

LLM-Assisted Program Verification · cs.SE candidate · published 2026-10-19T14:15:50Z
Ding Wang, Chao Jiang, Dugang Liu, Zhiwu Xu, Cheng Wen, Zhong Ming, Yuwei Liu, Xinyi Wan, Lin Huang
arXiv categories: cs.SE

Large language models (LLMs) are increasingly used to generate Verus contracts for Rust programs together with the proofs that establish them. Yet verifier acceptance, the common measure of success, shows only that the implementation satisfies the generated contract, so it leaves open whether the contract captures the intended behavior. Assessing specification generation therefore requires an evaluation methodology, not a single metric. We present VerusEval, a framework that evaluates generated contracts along six dimensions, including Verus-native checks for semantic triviality, validated input-output (I/O) suites, and contract equivalence, and that relates them so that the strength and blind spots of each become measurable. Evaluating 13,716 artifacts from four workflows, five LLMs, and two prompting settings on 762 tasks, we find that acceptance overstates quality: only 42.3\% of the accepted artifacts complete all three semantic checks without a flag, and across workflows and models, higher acceptance does not consistently come with more correct contracts. I/O evaluation rejects 23.6\% of the accepted artifacts, yet only 63.2\% of those that pass it are proved equivalent. Of the accepted artifacts flagged by contract comparison, 84.1\% have a rejected completeness obligation, and the direction of a failure prioritizes inspection of the generated contract or the reference; it does not by itself establish which artifact is defective. Screening and review further identify 36 candidate defects among 61 selected reference contracts, and repairing one of them makes 10 of its 11 failing artifacts equivalent. Based on these findings, we derive four actionable lessons for evaluation, generation, and benchmark maintenance.

arXiv abstract · PDF

LLM-Assisted Program Verification · primary corpus · published 2026-10-20T17:33:22Z
Zhe Ye, Udaya Ghai, Zhizhen Qin, Dawn Song, Soonho Kong
arXiv categories: cs.SE, cs.AI, cs.LG, cs.LO, cs.PL

Program optimization aims to improve performance while preserving behavior. Coding agents can already make programs faster by changing algorithms, data structures, and execution strategies. However, existing equivalence checks mostly rely on tests, which agents have been shown to exploit, passing the tests without preserving the intended behavior. We propose agentic verified optimization, in which an agent produces a faster implementation together with a machine-checked proof of equivalence to the existing one. Because the existing implementation serves as the specification, the task avoids the specification-writing bottleneck of verified code generation, and recent advances in theorem proving make the proofs attainable. We formulate the task at the function and repository levels in Lean 4, where programs can be both executed and reasoned about. Few real-world applications are written in Lean, so we develop Aqueduct, an agentic framework that migrates C, C++, Go, and Rust programs into native Lean, validates each port by differential testing against its original. On the 189 reference implementations in Verina, agents produce faster proved rewrites for 156, including algorithmic changes such as replacing exponential recursion with dynamic programming. On 17 migrated applications, their 92 proved rewrites speed up 47 of 51 application scenarios. These application-level gains are smaller than the function-level ones, making the choice of functions to optimize an important problem. Current agents can thus already carry out verified optimization on both standalone functions and applications migrated from real programs. We discuss the remaining challenges and the steps toward verified optimization in production.

arXiv abstract · PDF

LLM-Assisted Program Verification · primary corpus · published 2026-10-21T03:33:10Z
Tengjie Lin, Zhongyi Wang, Haokun Li, Jianwei Yin, Mingshuai Chen
arXiv categories: cs.SE, cs.LO

Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independent verification. Its central bottleneck is specification synthesis: constructing the contracts required for modular verification. Recent advances in large language models (LLMs) have enabled automated specification synthesis at unprecedented scale. However, existing approaches remain fundamentally bottom-up, requiring callees to be verified before their callers. This dependency limits parallelism and provides no principled mechanism for resolving interprocedural inconsistencies that propagate across call chains. We present VERDICT, a multi-agent framework for parallelizing modular deductive verification of large-scale programs. VERDICT is built on two key principles. First, assumption-based parallel specification synthesis assigns an agent to each function and allows it to proceed immediately using assumed contracts for its callees, enabling verification to proceed in parallel across the program. Second, bidirectional interprocedural conflict reconciliation resolves the inconsistencies introduced by these assumptions: when a synthesized contract contradicts an assumption, agents propagate the necessary revisions both up and down the call graph until the contracts converge. Experimental results on real-world C programs show that VERDICT synthesizes higher-quality specifications than existing approaches while substantially reducing verification time. In particular, VERDICT is the first approach that scales to the complete 20,000-line X.509 parser, ruling out nearly all the potential runtime errors within hours, whereas prior tools like PREGUSS fall far short even after days of execution.

arXiv abstract · PDF

LLM-Assisted Program Verification · cs.SE candidate · published 2026-10-21T13:57:03Z
Chao Jiang, Ding Wang, Chaohua Yang, Dugang Liu, Zhiwu Xu, Cheng Wen, Zhong Ming, Yuwei Liu, Xinyi Wan, Lin Huang
arXiv categories: cs.SE

LLM-based verification systems repair Rust proofs by revising programs in response to Verus diagnostics. When several error types are reported, pipelines such as AutoVerus and VeruSAGE select the next repair target using a preset priority. Yet each repair changes the program and the errors that follow, so the same reported types can require different choices at different states. We present VeruSteer, which learns to select error types from the outcomes of alternative repair trajectories. It constructs repair trees offline and compares paths from the same initial program by verification success, repair rounds, and final verification progress. These comparisons supervise a selector that combines step-wise imitation with trajectory preference ranking. The selector uses self-attention over the program, verifier feedback, and earlier selections to rank the currently reported types. It replaces the default priority within a single repair trajectory, keeping the existing repair agents and adding no repair or verifier calls for selection. We evaluate VeruSteer by replaying its choices on stored AutoVerus and VeruSAGE test trees under four generation configurations. Across 1,270 test trees, VeruSteer increases verified outcomes from 185 to 194 (14.57\% to 15.28\%), gaining 12 successes and losing three for a net improvement of 0.71 percentage points. Among trees where the default fails but a recorded alternative verifies, VeruSteer succeeds on 3 of 4 AutoVerus trees and 9 of 11 VeruSAGE trees. Among trees with recorded alternatives where the default verifies, it retains success on 14 of 15 AutoVerus trees and 12 of 14 VeruSAGE trees. It also finds shorter successful trajectories and improves final progress on some trees where all recorded trajectories fail.

arXiv abstract · PDF

LLM-Assisted Program Verification · cs.SE candidate · published 2026-10-21T14:02:02Z
Arslan Bisharat, Mujtaba Nazari, Khushboo Bhadauria, Brian Ortiz, Eric Spencer, Beatriz Santos, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad
arXiv categories: cs.CL, cs.SE

Memorization inflates the benchmark scores of large language models (LLMs), since a model can reproduce answers it saw in training. Researchers test for it with consistent identifier renaming (CIR), which gives every identifier in a task a new name, and treat a lower score on the renamed task as evidence of recall. We test this method on the Temporal Logic of Actions Plus (TLA+) language, whose model checker acts as an oracle by confirming whether a renamed task preserves the exact behaviors of the original. Across 111 TLA+-Bench tasks, renaming lowers the correctness of Claude Opus 4.8 from 28% to 18% and of GPT-5 from 9% to 7%. Most of this decrease comes from how the test grades, which requires exact names that most descriptions never state. Grading by behavior shrinks the decrease to about 3 percentage points for Opus 4.8 and to 0 for GPT-5. In two model families fine-tuned on disjoint halves of the tasks, renaming removes about half of the training gain in likelihood and costs 4.9 percentage points (Qwen) and 1.3 percentage points (Gemma) on unseen tasks. A lower score after renaming therefore mixes memorization, name-based grading, and the cost of new names.

arXiv abstract · PDF

LLM-Assisted Program Verification · primary corpus · published 2026-10-21T20:40:26Z
Muhammad Danial, Muhammad Taimoor Khan
arXiv categories: cs.SE, cs.LO, cs.PL

Recent reports, such as "Who is using AI to code?", indicate that approximately 30\% of Python code contributions to GitHub are AI-generated. Given the inherent unreliability of this code, formal verification emerges as a promising approach to establish trust in software correctness. Although leveraging large language models (LLMs) for formal verification has garnered increasing attention, practical adoption remains limited due to the challenges in writing formal specifications and verifying program correctness against them. Existing tools predominantly support verification for languages such as Java and C, with minimal support for Python. We present TrustedCode, an automated framework for verifying AI-generated Python code. TrustedCode uses LLMs to (i) type-check Python code, (ii) translate it into WhyML via the Why3 framework, and (iii) verify it against formal specifications using Why3 back-end automated theorem provers. Our method integrates chain-of-thought prompting through LangGraph to identify and address LLM limitations in specification generation and proving the specified programs. To evaluate TrustedCode, we conducted experiments on ten Python programs of varying complexity. Our analysis reveals that 50\% of the observed errors stem from domain knowledge gaps, 30\% from syntactic inaccuracies, and the remaining 20\% from semantic and type-related issues. These findings underscore the importance of targeted improvements in LLM-guided formal verification workflows for Python. TrustedCode is an open source tool available at: \href{github.com/mtaimoorkhan/TrustedCode}{github.com/mtaimoorkhan/TrustedCode}. The video demonstration is available at: \href{youtu.be/Nr5I2g8ec-s}{youtu.be/Nr5I2g8ec-s}

arXiv abstract · PDF

LLM-Assisted Program Verification · cs.SE candidate · published 2026-10-22T04:48:23Z
Zian Wang, Qin Li, Weisong Sun, Haibin Cai
arXiv categories: cs.SE

AI-assisted code generation amplifies the demand for automated formal verification. Generated programs must not only be executable but also accompanied by machine-checkable evidence of correctness. Existing approaches can synthesize functionally plausible code or plausible-looking specifications from natural-language prompts; however, they do not explicitly co-design the implementation and specification as a unified artifact optimized for verification. Consequently, automated verifiers often fail to discharge proof obligations. Typical failure modes include missing or implicit proof anchors, program structures that are hostile to automated reasoning, and inconsistencies between code-level state and specification-level requirement facts arising from the independent generation of code and specifications. Even when verification succeeds, it may only establish weak specifications that omit requirement-critical behavior. This paper introduces VeriGen-C, a formal-verification-friendly framework for the joint synthesis of C programs and ACSL specifications from natural-language requirements. Code generation and repair are constrained to expose proof-relevant state, to streamline control flow for deductive verification, and to eliminate implementation patterns that hinder automated proof search. Specification generation and refinement are similarly constrained to mitigate verification timeouts and to ensure alignment with the user requirements. Empirical evaluations on HumanEval-X, FM-Bench, and LiveCodeBench Lite demonstrate that VeriGen-C substantially improves the rate of verified and requirement-aligned solutions relative to an interface-compatible baseline, from 5.5% to 44.5%, from 44.3% to 80.0%, and from 6.5% to 58.7%, respectively.

arXiv abstract · PDF

LLM-Assisted Program Verification · primary corpus · published 2026-10-22T05:27:41Z
Jinyi Zhou, Zenan Li, Yuan Yao, Jun Ma, Taolue Chen, Xiaoxing Ma
arXiv categories: cs.LO

Interactive theorem provers can provide strong correctness guarantees for software, but constructing the proofs remains a challenging and labor-intensive task. Inspired by the recent progress of modern coding agents, we present RAIN, a lightweight proof-specialized agent for Rocq proof generation. RAIN augments an LLM with proof engineering capabilities, including repository exploration, iterative refinement, and checker feedback. This design allows the agent to retrieve lemmas autonomously, revise complete proof scripts instead of isolated tactics, and iteratively refine its proof strategy using enriched proof-state information. Evaluated on a subset from CoqStoq, RAIN shows substantial improvements over the existing baselines, achieving over 90% prove success rate with at least 24.7% improvements. We also compare with general-purpose coding agents, the results show that RAIN maintains comparable prove success rate but with significant lower cost.

arXiv abstract · PDF

LLM-Assisted Program Verification · primary corpus · published 2026-10-23T01:48:36Z
Wenhan Wang, Shiming Chen, Zeyu Sun, Shenghua Feng
arXiv categories: cs.SE, cs.PL

Formal specification generation is a critical step towards formal verification and correctness assurance of software. Recently, large language models have been widely adopted in automatic generation of formal specifications. However, existing LLM-based specification generation approaches often assume that the input program is correct, which deviates from the real purpose of formal verification---to figure out whether the program meets its requirements when its correctness is unknown. Therefore, we conduct an empirical study of LLM-based specification generation under the bimodal setting: given both the natural language requirement and its corresponding code implementation, whose correctness is unknown. We construct a benchmark of 1,403 C programs and evaluate ACSL specification generation with Frama-C verification. Our study reaches several interesting findings: first, when the code implementation is correct, providing the natural language requirement does not further improve the pass rate of generated specifications. Second, when the code implementation is incorrect, LLM-based specification generation may erroneously pass verification by producing weak or implementation-misled specifications, and this cannot be fully alleviated by advanced prompting approaches. Compared with the non-formal HoarePrompt approach, LLM-generated formal specifications are less effective in predicting requirement-code consistency. Our study takes a first look at applying LLM-based formal specification generation to verifying program correctness against requirements, and points to requirement-faithful specification generation as a new direction for future LLM-based formal specification research.

arXiv abstract · PDF

LLM-Assisted Program Verification · primary corpus · published 2026-10-25T10:47:21Z
Anirudh Gupta, Petros Markopoulos, Siddhartha Gadgil
arXiv categories: cs.PL

We present PastaLean, an extensible system for deterministic translation from Python to Lean via the Abstract Syntax Tree of Python. This allows for verification of Python code, especially auxiliary code used by AI. Every program is translated into a provable twin written in the form Lean's verification tooling can reason about, and a runnable twin that gives a fast and correct computation support. We also introduce our Type Inference engine TypeInfer which provides static typing support for untyped Python code. Our tool provides coverage of more than 92\% for LeetCode and HumanEval\textsuperscript{+} and more than 98\% for LiveCodeBench ground truth Python files. Further, at least 97\% of each dataset's (numerical) test cases pass, with 100\% on HumanEval\textsuperscript{+} and LiveCodeBench. The TypeInfer engine is the best-scoring tool on the TypeEvalPy static leaderboard, and on a repository-level TypyBench benchmark it scores above every competing repository-level inference tool.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-19T01:27:16Z
Tetsuya Sato
arXiv categories: cs.CR, cs.LO

Differential privacy (DP) is a gold-standard definition of privacy designed to evaluate the privacy guarantee of databases. R\'{e}nyi differential privacy (RDP) is an important variant of DP that gives tight evaluations of machine learning algorithms. These formulations are easy to understand, but evaluating privacy for actual databases is complicated. Even a small change in the database can break its privacy, and evaluations of DP and RDP themselves are complicated. In particular, RDP evaluations in recent studies have become much harder. Therefore, formal verification of them has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing R\'{e}nyi differential privacy in a general setting. We first formalize RDP for continuous distributions. As a technical basis, we formalize several properties of convex functions and $f$-divergences for nonnegative convex functions. We formalize basic properties of RDP, conversion laws from RDP to DP, the moment accountants in DP, and the Gaussian mechanism and its RDP. Finally, we discuss the stochastic gradient descent mechanism with Gaussian noise and formalize a rough evaluation of its RDP and DP.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-19T14:16:17Z
Georgios Kissas
arXiv categories: cs.LO

When does one equation imply another? Stage 2 of the SAIR Mathematics Distillation Challenge required teams to submit solvers to answer this question for sets equipped with a binary operation. For these sets, associativity, commutativity, or any other algebraic property was not assumed. Each answer required a proof or counterexample that could be verified by Lean. Programs also had to respect fixed resource limits. We present R\'ozsa, a Python solver that searches for both kinds of evidence. It begins with simple tests and considers more extensive searches when those fail. To find a proof, it applies a given equation and derives any further equations as needed, keeping a record of each step. To find a counterexample, it searches for operations on finite sets. It also tests one fixed infinite model. The given equation must hold for every assignment, while the target equation must fail for at least one. In either case, R\'ozsa turns the evidence into a Lean certificate. The submitted solver solved 199/200 problems (99.5%) in the official main evaluation getting the 6th overall position. Additional tests show that the solver can prove many implications linked by long chains of known results, but has limited success with infinite counterexamples. We explain the search methods, how they fit together, and what the unsolved cases reveal about their limits.

arXiv abstract · PDF

Formalization in Proof Assistants · cs.SE candidate · published 2026-10-21T17:19:33Z
Yihan Dai, Xuanlin Liu, Haoxiang Jia, Tianchi Li, Xin Zhang, Sergey Mechtaev
arXiv categories: cs.SE

Formal specifications can make AI-generated code mechanically checkable. Because user intent is typically expressed in natural language rather than formal logic, specifications must first be derived from it, e.g., via LLM-based autoformalization. Yet autoformalized specifications are themselves untrusted, so a key challenge is validating whether they capture user intent without relying on a costly oracle such as human review. In this oracle-free setting, a natural strategy is to vote among model outputs, but because model errors are often correlated, agreement among outputs may reflect shared mistakes rather than correctness. Our key insight is that these errors can be decorrelated through representational diversity. We achieve this diversity with contrapuntal languages: pairs of task-specific formal languages, each designed to express the intended specification, yet admitting no structure-preserving translation between them. An LLM formalizes the intent independently in each language, and we accept a specification only if a solver proves the two formalizations equivalent. To construct such languages, we present a synthesis algorithm that reuses fragments of sampled seed specifications as syntactic sugar over a base specification language. We implement the approach for first-order logic specifications and evaluate it on HumanEval+ and LiveCodeBench using GPT-5.4 mini and Qwen3.6-Flash with and without thinking. Over the strongest baseline, our method increases the proportion of accepted specifications that are correct, i.e., complete and sound, by 12.0% on HumanEval+ and 42.9% on LiveCodeBench. The accepted specifications judged complete reject 98.6% of buggy program variants on HumanEval+ and 96.2% on LiveCodeBench, compared with 92.8% and 78.3% for the strongest baseline.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-21T20:42:43Z
Lorenzo Bresolin, Marcello Mamino
arXiv categories: math.LO

It is known, by works of Werner and Carneiro, that the type theory of Lean (and indeed of CIC plus a version of choice) is equiconsistent with ZFC plus "there are infinitely many strongly inaccessible cardinals". We prove a finer connection between these two formal systems; namely, given any formula in the language of second order arithmetic, that formula is provable in the aforementioned extension of ZFC if and only if the same formula, when viewed as a type in Lean, is inhabited.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-22T03:06:21Z
Ruixuan Deng, Zhengfeng Ji, Jiayu Zhang, Li Zhou
arXiv categories: quant-ph, cs.CR, cs.LO

Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap, establishing a two-factor assurance: unconditional security from physical principles, and machine-checked proofs against reasoning errors. We present FVQKD, a Rocq library for machine-checking QKD security proofs. Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84. The mechanization reconstructs the complete proof infrastructure from first principles, including the smooth entropy framework, the entropic uncertainty relation, and the Quantum Leftover Hash Lemma. It uncovers necessary side conditions that the published argument leaves unstated, one of which reveals a missing proof branch, and it grounds the information-theoretic bound in a formal semantics of protocol execution, which the pen-and-paper analysis lacks. The proof is entirely admit-free, relying only on the Rocq kernel and standard foundational axioms. To our knowledge, this is the first end-to-end formal verification of a QKD security proof. Built on MathComp, MathComp-Analysis, and CoqQ, the development provides quantum-information infrastructure designed for reuse across broader QKD variants and quantum cryptography applications.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-22T06:33:06Z
Haoran Lv (1), Chengjin Ni (1), Manqin Wang (1), Shenli He (1) ((1) BitMiracle AI Lab)
arXiv categories: cs.LO, math.DS, q-bio.MN

We give a self-contained proof that, for a finite detailed balanced mass-action system with positive rate constants, each positive stoichiometric compatibility class contains exactly one positive equilibrium and every positive trajectory converges to it, together with a Lean 4 formalization of the complete argument from persistence to convergence. Boundedness and persistence come from the barrier argument of OpenAI (2026) for weakly reversible systems: an arbitrary-tolerance affine approximation yields a finite-minimum barrier whose superlevel sets confine trajectories and give one logarithmic bound for all solutions from a given initial state. The Horn-Jackson dissipation identity identifies the positive equilibria as an exponential family with parameters in the orthogonal complement of the stoichiometric subspace, which gives uniqueness in each class. A bounded-speed descent argument replaces LaSalle's invariance principle; it uses neither uniqueness of solutions nor continuous dependence on initial data, and it places every cluster point in that family. The route given here is direct and elementary, and its main theorem is checked by the Lean kernel against explicit definitions. The proofs, the Lean development, and the manuscript were produced in ClawsGO Science, an agent harness that packages a complete research environment: Claude Opus 5.5 made the research decisions, GPT 6 Astra carried them out, and the Lean kernel checked every formal step.

arXiv abstract · PDF

Formalization in Proof Assistants · cs.SE candidate · published 2026-10-22T07:42:17Z
Sirui Jiang, Dongming Xiang, Shichao Wu, Yuxuan Zhou, Yihong Wu, Fangze Zhu, Wang Lin, Guanjun Liu
arXiv categories: cs.SE, cs.AI

Formal languages are widely used in software engineering to specify and verify program properties. Because their mathematical notation and logic are hard to read, developers often rely on natural-language documentation to understand the functions in formal libraries. Yet a documentation statement can be provably true and still hold after the function's behavior changes. We call a statement's dependence on the function's specific behavior attribution, and we give a method to check it. We design and implement DocAuth, a documentation-generation method that uses attribution to decide what to publish and attaches to each published sentence the formal property recovered from it, together with checkable evidence. On 150 functions from the Community Books library of the ACL2 theorem prover, three large language models produce proved but non-attributable properties for about a third of the functions. DocAuth matches or exceeds the attribution rate of a mutation-based filter while delivering 37% more attributable sentences. Compared with a pipeline that checks truth alone, it raises the share of published sentences that a second model confirms as attributable from 82.9% to 94.7%. These results show that provable truth does not guarantee that documentation reflects what a function actually does. Attribution complements truth as a criterion for generating and evaluating documentation for formal libraries.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-22T18:46:53Z
Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet
arXiv categories: cs.AI, cs.LO

Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-24T12:03:15Z
Elnaserledinellah Mahmoud Abdelwahab
arXiv categories: cs.LO, cs.CL

This paper presents a model theoretic and computational formalization of AlKhwarizmis treatment of inheritance within the framework of Computational Fiqh. We first show that every inheritance configuration in a specified class is representable as a finite system of rational linear equalities and inequalities, and that such systems are decided exactly by Fourier Motzkin elimination over Q. We then define the fixed dimensional inheritance structure Vd with distinguished claimant coordinates, and prove that every admissible rational linear coordinate realization is isomorphic to Vd, this establishes the algebraic representation as canonical within that class. The complete first order theory Td of Vd is shown to be complete by construction and is explicitly distinguished from the decidability of the inheritance relevant fragment. The methodological principle is then related to a broader formalization of closed Fiqh domains via exhaustive case generation, Horn clause axiomatization, and terminating deduction, yielding domain relative computational completeness.

arXiv abstract · PDF

Formalization in Proof Assistants · primary corpus · published 2026-10-24T19:05:32Z
Justin Asher, Yichuan Cao, Ruichen Qiu, Pietro Pellegrino, Jia Li
arXiv categories: cs.AI, cs.LG, cs.LO, cs.SE

Numina Fuse is an agent-native application for formalizing mathematics in Lean 4. Since Lean can compile while not representing its intended informal meaning, and agents now write Lean faster than people can read it, we built Fuse around human supervision of agent work. A user works with an AI orchestrator on a Lean project and supervises it through views of the blueprint, the dependency graph, and the Lean code, while the backend keeps the project's derived state and runs agents for hours without the user present. We describe the development of Fuse throughout 2026, as it moved from a prescribed pipeline of agents paced by human review to an orchestrator that dispatches specialists, provers, and parallel children on its own. We designed for this shift, keeping project state, tooling, and interface design separate from orchestration so that agents could take over more of the work as models improved. We report Fuse's use in a formalization of the three-dimensional Kakeya conjecture and a study of prover models. We close with lessons for the next generation of autoformalization systems. Fuse Desktop, an open-source local version, is available at https://github.com/project-numina/fuse-desktop.

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-19T01:32:57Z
Charles Koll, Mike Rosulek, Houssam Abbas
arXiv categories: cs.LO

Motivated by the use of third-party testing, this paper presents a privacy-preserving implementation of the robustness monitoring of Signal Temporal Logic (STL). STL is a specification language for systems whose output traces have real-valued timestamps -- most prominently, cyber-physical systems. Its robust semantics, which assign real rather than binary truth values, are an essential ingredient of systems testing and runtime monitoring. In a number of system testing scenarios, the designer and the tester are separate parties. This testing-as-a-service model is common in software, avionics, and semiconductors, and is growing in importance in the red-teaming of machine learning models. In such a model, the designer seeks to preserve the privacy (or secrecy) of its design, while the tester seeks to preserve the privacy of its collateral, including the detailed specification suite. This paper presents a secure multi-party implementation of the robust semantics using arithmetic circuits. This implementation allows one party, which provides a secret trace, and a second party which provides a secret formula, to jointly compute the robustness without either party being able to learn the other party's secret input. We present a number of algorithmic modifications to the robustness computation to enable an efficient multi-party robustness computation. We also present new, semi-linear, robust semantics for STL that take advantage of the efficiencies of arithmetic circuits. The experimental results demonstrate that not only is this privacy-preserving monitor efficient on its own, but also that it can be used in a testing loop without affecting the speed at which bugs are found during robustness-guided system testing.

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-19T11:20:52Z
Martin Kure\v{c}ka, Roman Andriushchenko, Milan \v{C}e\v{s}ka, Nicola Paoletti, Petr Novotn\'y
arXiv categories: cs.LO

Formal methods provide a principal approach to obtaining safety guarantees for autonomous agents. Their key bottleneck is their reliance on a formal model (e.g., a Markov decision process) describing the agent-environment interaction. Learning or crafting the model is an error-prone process, which undermines the guarantees offered by formal methods. Robust models account for modelling uncertainty, but may still fail to capture the true environment. This issue can be addressed through \emph{runtime model monitoring}, which aims to raise an alarm when a likely model-environment discrepancy is detected, while keeping the probability of false alarm bounded. Existing approaches impose various assumptions and do not clearly explain the rationale behind their design choices, leaving the broader design space for these monitors somewhat opaque. In this paper, we formalise the design space of monitors for robust stochastic models through the lens of \emph{parameterised sequential betting} algorithms, highlighting the importance of \emph{observation feature} design (choosing what information about the history the monitor uses) and \emph{bet design} (how rich a family of betting rules the monitor can represent). We show that our framework generalizes the existing approaches, and we use its formalization to propose a new \emph{mixture of linear monitors (ML)} design. We prove that these ML monitors achieve an asymptotically optimal detection time within the class of linear monitors, making them a principled choice for our monitoring problem. Our experiments confirm that ML monitors significantly reduce detection times compared to existing monitors and can effectively exploit more complex observation features.

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-19T15:56:10Z
Gina Belmonte, Laura Bussi, Vincenzo Ciancia, Mieke Massink
arXiv categories: cs.LO

We present the tool VoxLogicA2, a spatial model checker aimed at Computer Vision, with applications in high-resolution 2D and 3D medical imaging. The new version of the tool combines logical primitives, non-logical primitives, and training and prediction primitives of state-of-the-art neural networks, freely interleaved with the symbolic tool functionality. The primary application field is neuro-symbolic medical image analysis. VoxLogicA2 is a fast, parallelising spatial model checker with a declarative domain-specific language, capable of describing both the learning procedures and the spatial logic procedures of an analysis in one program. We validate our approach by verifying its improved efficiency, and by using the new constructs of the language to describe case studies of previous work, which were based on Python, with a specification that uses VoxLogicA2 only

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-19T18:39:34Z
Pietro Bernabei, Rosario Pugliese
arXiv categories: cs.SE, cs.FL, cs.PL

Runtime Verification typically assumes a fixed alphabet of observable actions. This assumption becomes fragile in evolving software systems, where updates, reconfigurations, or architectural changes may rename, split, or fuse actions while preserving the system's high-level intent. In these cases, previously valid monitors and specifications may become misaligned with the running system. In this paper, we study runtime semantic discovery, namely the problem of identifying whether newly observed actions play the same operational role as previously known ones, without reconstructing a global behavioral model. To this end, we propose a local and runtime-computable notion of action similarity based on the neighbor contexts in which actions occur within execution traces. We define a family of k-neighbor equivalences and use them to compare systems whose observable alphabets differ. Our approach is intentionally lightweight: it does not aim to fully characterize behavioral preservation, but rather to identify candidate semantic correspondences between actions in evolving systems. We discuss the expressive power and limitations of neighbor-based equivalence and show how inferred correspondences can support the adaptation of runtime monitors and specifications under selected classes of alphabet evolution.

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-20T00:42:04Z
Charles Koll, Houssam Abbas, Mike Rosulek
arXiv categories: cs.CR, cs.LO

In industries like semi-conductors and aerospace, it is common for the design company to contract out part of the testing process to a Testing-as-a-Service (TaaS) company. In such a setup, both parties want to keep their intellectual property private (i.e. unknown to the other party): namely the design and its output traces for the designer, and the detailed correctness specifications for the tester. We demonstrate a practical way for conducting provably private TaaS using a cryptographically secure multi-party computation protocol. We do so for the common setup where the specification is in Signal Temporal Logic, and testing is done using robustness-guided falsification. Our implementation carefully separates the steps of falsification, and manages to be $\textit{maximally secure}$, in the sense that the parties learn the absolutely minimum necessary for falsification. For up to a 100-dimensional input search space, the generation of one test takes less than 80 msec, and the overhead of the privacy-preserving protocol is less than 6x. These numbers mean that privacy-preserving TaaS is practical, thus enabling TaaS in security-sensitive industries.

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-20T10:16:08Z
Luca D'Agati, Giuseppe Tricomi, Fabio Orazio Mirto, Giovanni Merlino
arXiv categories: cs.PL, cs.CR, cs.DC, cs.SY, eess.SY

In industrial cells, commands from learned policies, operators and schedulers reach the controller after inference, confirmation and transport, and the plant may have changed meanwhile, for instance by an operator pause. Such a command is released, or takes effect, when it is no longer correct. We call this the execution gap and ask which component should make the last check, and against which version of which state. The Action Intent Schema (AIS) is a contract in which a producer states how long its decision stays valid and what it assumes. The runtime XAIR rechecks each intent before release, can commit its authorization atomically in the context store, and can release it as a version-conditional command, which the controller executes only if its version of the state is unchanged. In controlled ablations with declared ground truth on emulated and physical cells, OpenPLC and ARM and RISC-V boards, a check on a replica always left an unprotected interval: a pause written from a few to over 100ms after submission escaped it. Only a check in the scan of a software controller, either a controller-local interlock or the version-conditional command, closed the interval for the state that controller owns; only the version-conditional command also refused commands after a pause that had been undone. A global version revoked up to every valid command under unrelated updates. Versions scoped to what the intent reads, or to the truth of its predicates, did not; with continuous signals on the variables the intent reads, only the latter avoided false revocations, though it burdens the store as predicates accumulate. On one embedded-board core, XAIR validated 148-168 intents/s.

arXiv abstract · PDF

Runtime Monitoring and Temporal Logic Verification · primary corpus · published 2026-10-20T16:15:39Z
Long Qian, Andr\'e Platzer
arXiv categories: cs.LO, math.LO

This article presents an axiomatization of linear differential equations that is complete for topologically open properties with compact initial conditions and time horizons by proving them deductively via a sound reduction to formulas of linear real arithmetic. Indeed, linearity is preserved: linear differential invariants are complete for open properties of linear differential equations and reduce with a linear number of Lie derivatives (per atom) to linear real arithmetic. In particular, this article shows that the linear fragment of differential dynamic logic (dL), a modal extension of standard first-order logic over the reals satisfies these completeness properties. By establishing completeness within decidable linear real arithmetic, the need for proving sophisticated nonlinear formulas of real arithmetic is circumvented. Furthermore, this article establishes generalizations to the nonlinear fragment of dL that enable the practical certification of reachability computations, validating the output of external computations in dL with machine-checkable proofs.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-19T09:16:37Z
Basile Schlosser, J\'er\'emy Thibault, Catalin Hritcu
arXiv categories: cs.PL, cs.CR

The security guarantees of existing formally verified compilers for compartmentalized programs in unsafe languages like C stop at a rather high level, assuming a built-in protection mechanism and a block-based memory model. Verifying a concrete, low-level enforcement mechanism for compartment isolation is still a major challenge for current proof techniques. In particular, Abate et al.'s proof technique fails because one of their proof steps, recomposition, essentially requires hiding all information about the code of each compartment, which is not practically achievable at a low level. We propose an extension of their proof technique to a low-level setting where compartments can fully observe each other's code. To do so, we introduce an overlay semantics that allows us to characterize these observations as a form of undefined behaviour, and we use a novel variant of recomposition that we call blame-aware recomposition, which essentially allows recomposing executions as needed in the original high-level proof technique, even if the low-level context observes the code, because this context is ultimately going to be discarded. We apply this new proof to a compartment isolation mechanism that uses a programmable tag-based reference monitor.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-20T04:35:39Z
Anmol Pandey, Aditya Jain, Liang Chen, Carsten Maple
arXiv categories: cs.CR, cs.AI, cs.LO

Autonomous LLM agents act through tools under per-action authorization: a local guard screens each tool call in isolation. We show that local authorization does not compose into global authorization. A compositional authorization failure (CAF) is a locally authorized execution, or a pair of locally authorized executions, that violates a global policy spanning intent, purpose, provenance, consent, and delegation. We characterize CAFs along two axes, expressiveness (single-trace safety versus relational k-safety) and observability (a ladder of monitor profiles). Our central result is an impossibility: relational purpose violations form a 2-safety hyperproperty with no per-trace locus of blame, so a per-action monitor that never raises a false alarm detects none of them, independent of the underlying model or decision procedure; they become visible only under cross-execution monitoring, which none of the six guardrails we survey implements. We make this constructive with AL-SYNTH, a SAT/SMT synthesizer (using no language model) that emits minimal CAF witnesses, each checked against an exhaustive oracle. The empirical signature is sharp: across nine LLM judges the per-action view approves the synthesized witness almost without exception, blocking it at a rate comparable to a benign control, yet the same models flag it when shown the two executions together. Per-action authorization is therefore structurally insufficient for relational policy conjuncts not reducible to single-trace safety: to bound them, a monitor must compare executions or accept false alarms.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-20T16:30:34Z
Carlo Ciliberto, Alessandro Rudi, Enrico Tassi
arXiv categories: cs.AI, cs.CR, cs.LO, cs.MA, cs.SY, eess.SY

AI agents increasingly act on behalf of people or other agents, purchasing services, exchanging information and delegating work. What an agent must respect is written in instructions, policies or agreements, but text alone cannot make it comply. It may make mistakes, be redirected by what it reads, or pursue different interests. For an economy of such agents to function, parties need agreements they can rely on without inspecting or trusting one another's agents. We introduce Proof-Carrying Contracts (PC2), a framework for making agreed constraints enforceable throughout an agent's interactions with a system. Before a requested operation can run, the agent must supply a machine-checkable proof that it preserves the agreed constraints in every case allowed by its model. An execution system called the Airlock checks the proof and controls access to the operation. The parties specify the conditions to preserve, while the agent supplies the reasoning needed to justify its decisions and remains free to adapt its strategy. This avoids having to design a separate permission policy and prove that every decision it permits is safe. We prove that the constraints hold at every instant during execution, even for an adversarial agent, and identify when this implies safety in the world. Reusable capability modules provide tools and guarantees from which contracts can be constructed. PC2 provides a foundation for an agent economy whose agreements protect both those delegating work and those carrying it out.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-21T09:14:12Z
Ruijie Zhang, Huaxiao Yin, Li Hu, Fanqi Kong, Haozhe Liang, Shaoyin Cheng, Kun Zhang, Bibo Tu
arXiv categories: cs.SE, cs.AI, cs.PL

Policy-as-Code (PaC) has emerged as a foundational paradigm in cloud-native systems. However, repairing Rego policies remains challenging due to their strict syntax, declarative semantics, and specific verification requirements. Existing automated program repair (APR) methods are mainly designed for mainstream languages and struggle to accommodate the unique policy logic and repair workflows of Rego. Thus, Rego policy repair remains a manual process driven by trial and error. To address this, we introduce RegoBench, the first automated Rego policy benchmark comprising 1,159 real-world defects, and propose RegoMender, a feedback-guided multi-agent framework. Collaborating via a shared blackboard and an atomic toolkit, RegoMender dynamically executes patching, rewriting, or rolling back, to resolve complex repair scenarios. Evaluated on RegoBench, RegoMender achieves syntactic and test-based semantic success rates of 82.9\% and 77.9\%, respectively, outperforming the strongest baseline by 13.4\%. Unlike other approaches whose performance drops in complex scenarios, RegoMender maintains effectiveness across single-step and chained repair tasks. Furthermore, it generalizes strongly across HCL and SQL and achieves an 86.4\% repair rate on 132 real-world CVE vulnerabilities, proving its robustness and practical utility for security.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-23T21:31:12Z
Khadim Lo, Soukaina Alaoui Ismaili, Jean-S\'{e}bastien Dessureault
arXiv categories: cs.SE, cs.AI, cs.PL

Language-model agents combine reasoning, tools, memory, delegation, and external effects. Authority is often distributed across prompts, host code, configuration, and logs. Probabilistic Agentic Programming (PAP) makes responsibility boundaries explicit programming abstractions connecting mandate, authority, effects, and evidence. We compare PAP with programming paradigms, agent-oriented and BDI systems, workflow and policy languages, and LLM tool-use frameworks along seven dimensions. A mediation kernel formalizes checks before tool execution, operation-bound approval, resource limits, and evidence. Inductive proofs establish conditional safety for arbitrary model responses, assuming correct guards and complete mediation. A backward simulation matches graph executions to source executions in a defined sequential Touba subset. Its human checkpoints release program continuations; operation-bound approval remains a separate kernel contract. Finite-state exploration checks the model. Scripted enforcement tests exercise selected refusal paths and permitted controls. An exploratory study combines seven business cases, including two three-agent workflows, seven models from three providers, five methods, and five repetitions per case and method. Shared English instructions and exact checks of stored outcomes yield 1,225 assessed observations. Native Touba completes all 35 observations on six models and 30 on the remaining model; structured Touba ranges from 21 to 35. Native matches the highest observed count for each model, including ties with the frameworks. All paired case intervals include zero. These observed counts describe the evaluated tasks; the runtime authority boundary remains fixed. The results connect responsibility contracts, execution rules, and evidence.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-24T07:32:42Z
Yihan Yang, Chenyuan Yang, Zijie Zhao, Anh Nguyen Hoang, Ziqi Zhang, Weidong Wang, Zhiheng Lyu, Lingming Zhang
arXiv categories: cs.SE, cs.AI, cs.CR, cs.PL

LLM agents have been increasingly adopted for security-focused code review, but existing benchmarks mostly derive the reviewed changes from their later fixes instead of the real-world bug-introducing commits. In this paper, we present SecPRBench, the first comprehensive benchmark for evaluating agentic security review on validated real-world code changes. More specifically, we have built an automated agentic pipeline to autonomously harvest, build, and validate massive real-world bug-introducing commits for popular software systems. To ensure precise evaluation, we also adopt LLM-as-a-judge to credit the findings matching ground-truth vulnerabilities. To date, we have collected 265 tasks from nine critical systems, including Firefox, V8, and OpenSSL with millions of lines of code. Across eight frontier models, recall ranges from 32.5% to 78.1%, with Grok 4.6 and GPT-6 sol ranking at the top. Our study also shows that most misses are not simply oversights: in 68% of them, the agent reports on a file that holds the flaw but argues for a different mechanism. Security-focused harnesses also behave differently: OpenAI's Codex Security lowers recall by 8.3 points, mostly by abstaining, while Anthropic's Defending Code harness raises it by 7.7 points, at a higher cost.

arXiv abstract · PDF

Security and Trust in Software Systems · primary corpus · published 2026-10-24T15:47:12Z
Amir Naseredini, Suhas Viswanath, Martin Berger
arXiv categories: cs.PL, cs.CR

Rowhammer is a hardware vulnerability in dynamic random-access memory (DRAM) in which repeated accesses to one or more aggressor rows can induce bit-flips in nearby victim rows. This phenomenon violates a core assumption of conventional programming language semantics: that reading from or writing to one memory location does not modify others. Despite the security importance of this phenomenon, there is no widely established formal framework connecting Rowhammer faults with program behaviour. This makes it difficult to reason rigorously about the efficacy of proposed Rowhammer defences and the program-level guarantees they provide. To address this gap, we present a probabilistic small-step operational semantics for an idealised imperative language subject to Rowhammer-style faults. The semantics is high-level in that it abstracts from DRAM internals and semiconductor physics. A general probabilistic fault model parameterises the semantics, representing Rowhammer-style faults by assigning probabilities to bit-flips during read or write operations within a specified victim region. The resulting distributions are propagated through programs using the standard monadic structure of probabilistic computation. As a case study, we formalise physical separation, a well-known defence that places program variables sufficiently far apart in physical memory that an access to one variable cannot disturb another. We prove a distribution-independent semantic collapse theorem: for every finite execution, including prefixes of terminating and non-terminating executions, the protected projection of the probabilistic Rowhammer semantics is the Dirac distribution of the corresponding Rowhammer-free execution. Furthermore, we develop an observation-parametric account of secure information flow.

arXiv abstract · PDF

Compilers and Binary Analysis · cs.SE candidate · published 2026-10-20T08:54:26Z
Siyuan Li, Jiayi Zhou, Zhiyuan Xia, Weijie Wang, Yaowen Zheng, Weiran Tang, Hong Li, Hongsong Zhu, Shanqing Guo
arXiv categories: cs.SE

Code reuse in modern software ecosystems facilitates the spread of 1-day vulnerabilities, posing significant security risks. Determining if patches are present is crucial, but traditional methods suffer from limited usability and accuracy, often depending on a fragile compilation process. In our prior work, we introduced Lares, the first compilation-free framework for patch presence testing that combines large language models (LLMs) with SMT solvers. However, Lares treats the LLM and the SMT solver as two separate, parallel decision channels: the symbolic channel (Z3) succeeded in only 20% of code cases, and the remaining cases fell back to the neural channel (the LLM) for the final decision. Letting the LLM act as the final arbiter turns verification into an informal, non-deterministic process that is prone to hallucination errors, while the two channels never reinforce each other. To overcome these limitations, we propose SyLares, which reformulates compilation-free patch presence testing as neuro-symbolic reasoning. Instead of letting the LLM emit a final verdict, SyLares uses the LLM as a neural feature extractor that perceives heterogeneous source code and decompiled pseudocode and produces specification-compliant SMT-LIB inputs, and delegates the final, deterministic judgment to the symbolic Z3 solver. This neural-perceives, symbolic-decides coupling is realized by a Code2SMT reasoning engine that combines deterministic syntactic parsing with LLM-driven code normalization and symbol alignment, so that every case is reduced to a formal equivalence query rather than an opaque LLM guess.

arXiv abstract · PDF

Compilers and Binary Analysis · primary corpus · published 2026-10-20T13:49:18Z
Akarsh Ashok, Dinil Mon Divakaran, Vivek Balachandran
arXiv categories: cs.SE, cs.LG, cs.PL

ExeBench is one of the most widely used benchmarks for evaluating LLM-based decompilers. We analyze ExeBench and identify nine issues that affect how faithfully a test measures a decompiler. Three of them prevent LLM decompilers from recovering C code from ExeBench's function. These are ambiguous parameter order when integer and floating-point types are mixed, unused parameters that optimized assembly may drop, and constants stored outside the function's assembly code. Six more affect test validity: non-void functions without a return, placeholder types, static or inline functions removed by the optimizer, functions named main, trivial bodies and truncated definitions. We present ExeBench-FHD, a backward-compatible revision of ExeBench that adds 16 new fields: call-site assembly, data sections, test wrappers, linked-binary disassembly and five warning flags. In ExeBench, 38.9% of functions have at least one of the five flags; dropping records with any of the four warning flags (all except unused_param, which marks functions that the new wrappers make evaluable) keeps 63.9% of the corpus. In an evaluation at -O2 on four architectures, the new fields raise GPT 6 Sol's re-execution rate by up to 26.5%, 19.1% and 21.0% on functions that read data sections, mix parameter types and have unused parameters, respectively.

arXiv abstract · PDF

Compilers and Binary Analysis · primary corpus · published 2026-10-21T09:05:50Z
Shreyas Vinayakumar
arXiv categories: cs.LO, cs.AR, cs.PL

The Open Compute Project's microscaling (MX) family includes MXFP4, which stores 32 four-bit elements with a shared power-of-two scale. When lowering a dot-product reduction, a compiler can apply these scales before the reduction, or defer scaling until afterwards. Although equivalent over real numbers, these formulations can produce different IEEE binary32 results through overflow or underflow, with equivalence also depending on the reduction tree. We study the legality of compiler rewrites in either direction by deriving conditions under which the two formulations are bitwise equivalent. To decide rewrite legality, we construct an integer state machine that exploits the finite element alphabet and shared power-of-two scales, modeling overflow, NaN, and subnormal rounding. We prove its faithfulness under bounded scale codes and integer coefficients, yielding an exact encoding of the equivalence query in quantifier-free linear integer arithmetic (QF_LIA). For MXFP4, we derive a closed-form sufficient upper bound on the sum of scale exponents for any fixed binary reduction tree within the supported coefficient range. This bound depends on the size of the largest proper subtree. For four tree shapes at block lengths $k\in\{2,3,4,8,16,32\}$ and two shapes at $k=64$, SMT finds counterexamples when this upper bound is increased by one exponent step. Against the standard direct encoding in quantifier-free floating-point arithmetic (QF_FP), on matched queries cvc5 proves the integer version in seconds but reaches a configured one-CPU-hour limit on the floating-point proof even at $k=2$. The implementation was cross-checked using an independent floating-point encoding, exhaustive and stratified binary32 execution, and GPU replay of counterexamples. An MLIR lowering prototype demonstrates selection between the two formulations using the certified conditions as static or runtime guards.

arXiv abstract · PDF

Compilers and Binary Analysis · cs.SE candidate · published 2026-10-22T07:56:59Z
Xiaoao Zhu, Ni Zhang, Jie Ren, Zhiqiang Li, Jie Zheng, Zhanyong Tang, Zheng Wang
arXiv categories: cs.SE

Lifting stripped, heavily optimized binaries to a canonical, pre-optimization LLVM intermediate representation (IR) is essential for downstream security analysis and legacy software migration when source code is unavailable. However, aggressive compiler optimizations rewrite control and data flow, remove structural metadata, and introduce type-erased low-level idioms, causing current lifters to produce malformed or semantically divergent IR. We present ATLAS, a multi-agent framework designed to reconstruct formally valid and canonical LLVM IR from optimized disassembly.ATLAS combines (i) Structure-aware, region-level retrieval, which utilizes pseudo-probe attribution to align optimized instructions with canonical IR exemplars, and (ii) a collaborative refinement loop that closes the gap between probabilistic generation and deterministic compiler constraints. Concretely, a Lift agent generates an initial IR draft conditioned on retrieved exemplars, an Advisor agent interprets LLVM verifier/compilation diagnostics and static checks to propose localized repair actions, and a Validation agent applies the edits, re-runs toolchain verification and (when available) runtime checks, and feeds the resulting diagnostics back to the Advisor. The agents iterate until the IR is verifier-clean and behaviorally consistent, or a budget limit is reached. On HumanEval-Decompile and MBPP, ATLAS outperforms seven baselines on lifting LLVM IR, achieving 91.8% re-executability and 89.4% CFG similarity across ARM, x86-64, and RISC-V binaries. Moreover, our evaluation demonstrates that ATLAS also outperforms the Binary to C to IR pipelines in pointer-flow precision and downstream analyzability. By recovering a well-formed, machine-centric representation, ATLAS enables practical cross-ISA recompilation and verifiable binary-only migration workflows.

arXiv abstract · PDF

Compilers and Binary Analysis · primary corpus · published 2026-10-22T14:26:20Z
Lu Maltsis, Dominik Winterer
arXiv categories: cs.SE, cs.PL

Fuzzing software with complex inputs has been a longstanding challenge. Traditionally, fuzzers either programmatically encode language constraints, requiring significant engineering effort, or rely on users to declare grammars and constraints. Recent LLM-based fuzzers address these drawbacks but introduce new issues. Some use LLMs for test generation, sacrificing throughput and producing invalid inputs when the LLM makes mistakes. Others rely on language-specific parsers, static analysis, and AST manipulation libraries. We introduce Typed Template Fuzzing (TTF), a lightweight LLM-based fuzzing methodology. The key idea is to use LLMs in a preprocessing step to transform seeds into typed templates. The typed templates then enable semantically aware, mutation-based fuzzing without language-specific parsers, type checkers, or further LLM queries during fuzzing. By exploiting the correspondence between seeds and templates, TTF can moreover repair LLM mistakes. We have implemented TTF in our tool Typos, which we evaluate across 21 input languages, including C, C++, Go, Rust, SystemVerilog, Scala, and Java, as well as libraries such as PyTorch and Qiskit. In a six-month fuzzing campaign, we reported 135 bugs, 128 of which were previously unknown. Perhaps most notably, on average 96% of Typos's mutants are valid, coming close to the validity rates of domain-specific fuzzers. Our evaluation further shows Typos's benefits over the state of the art.

arXiv abstract · PDF

Logic Programming and Knowledge Representation · primary corpus · published 2026-10-20T10:03:22Z
Guillermo Badia, Carles Noguera, Gaia Petreni, Alice Portone, Val Tannen
arXiv categories: cs.LO, cs.DB

We study the containment problem for (unions of) conjunctive queries ((U)CQs) with negative information on semiring-annotated databases. Our approach to negative information follows the treatment of negation proposed by Gr\"adel and Tannen (2017, 2019, 2021 and 2024) for first-order logic and fixed point logic which applies productively to large classes of semirings, including bounded distributive lattices, as well as the important provenance semirings studied for positive CQ containment by Green (2009). Negation features in (U)CQs along two dimensions: negated equalities (disequations), and negated relational atoms. We study complexity for each of them separately, as well as jointly. For disequations, we extend a methodology that proves the same complexity bounds as the ones already known for the standard Boolean semiring (in the second level of the polynomial hierarchy) for most semirings of interest. Two prominent exceptions are $\mathbb{N}[X]$ and Trio(X) where the complexity bound for containment is in the second level of the counting hierarchy. For CQs with negated relational atoms we show that the complexity, surprisingly, is the same as that of the containment of CQs without negation when one considers model-defining and provenance-tracking interpretations (namely, nondeterministic polynomial time). Interestingly, among bounded distributive lattices, the Boolean two-element case is the only one where the complexity of the problem continues to be hard for the second level of the polynomial hierarchy for model-defining interpretations. Furthermore, we show that the complexity increases again for distributive lattices if we focus on other classes of interpretations. Finally, we consider queries that have both negated equalities and negated relational atoms and show that the complexity of containment continues to be that of the case with just negated equalities.

arXiv abstract · PDF

Logic Programming and Knowledge Representation · primary corpus · published 2026-10-20T20:48:45Z
Peter Flach, Kacper Sokol, Jan Wielemaker
arXiv categories: cs.AI, cs.LO

This paper charts the evolution of the Prolog textbook Simply Logical -- Intelligent Reasoning by Example from print with runnable programmes on a 3.5-inch diskette published in 1994, via various intermediate online versions, to the fully interactive online edition available today. Our aim is to investigate -- from both the writer's and the reader's perspectives -- the potential impact of technology on educational materials. The three authors of this paper present three distinct and complementary points of view, which come together to shape an interactive online book that offers an immersive learning experience. Peter describes the philosophy behind the original book and experiences teaching from it. Jan demonstrates how contemporary web programming has enabled a fully interactive realisation of the book's philosophy. Kacper reports how different technologies can be adopted to build a versatile authoring toolkit that underpins the interactive online edition of the book. Collating these distinct yet coherent perspectives allows us to reflect on future opportunities for interactive Prolog teaching materials arising from the continuous development of web technologies. The insights we offer should be of interest to teachers of Prolog as well as those wanting to find out about the latest educational technologies.

arXiv abstract · PDF

Logic Programming and Knowledge Representation · primary corpus · published 2026-10-21T06:38:18Z
Thomas Eiter, Davide Sold\`a, Hai Xia
arXiv categories: cs.LO

Rule-based link prediction combines symbolic and statistical artificial intelligence methods by inductively learning a set of rules from a knowledge graph (KG), with the aim of completing the graph when a query cannot be answered from the KG alone. Several systems have been proposed, and while they perform well on classical benchmarks, even compared with embedding-based systems, many of them produce a large number of rules. This compromises scalability in the query-answering phase, especially under strong hardware constraints. In this work, we investigate the behavior of AnyBurl, a state-of-the-art rule learner for link prediction, to determine whether running it for a given time and then pruning the learned rules yields better query-answering performance at test time than a simpler approach that stops rule generation earlier.

arXiv abstract · PDF

Logic Programming and Knowledge Representation · primary corpus · published 2026-10-22T13:38:53Z
D\"orthe Arndt, Pierre-Antoine Champin
arXiv categories: cs.LO, cs.AI

Notation3 Logic was introduced as an extension of RDF allowing the user to express rules on top of triples and to make statements about graphs. The original proposal of the logic only came with an informal specification of its semantics which has been refined later on. While this refinement clarified the meaning of rules and implicitly quantified variables, it left the meaning of graphs used as terms - so-called graph terms - open. In this paper we aim to close this gap. We discuss in detail, how graph terms are used in Notation3, which formal requirements they need to meet, and provide examples to illustrate the difficulties when defining their semantics. We then introduce an abstract syntax for the logic and define its semantics in two steps: similarly to RDF's simple interpretations, we define interpretations and basic entailment for Notation3 which covers plain RDF triples but also triples containing graph terms. N3-entailment is then an extension of basic entailment which assigns meaning to the different special predicates of the logic like for example the implication symbol. N3-entailment is defined in a way that it can be extended whenever a new predicate is added to the logic. As Notation3 Logic is currently under development, we expect many predicates to be added. Our research provides and important step towards the full standardisation of the logic.

arXiv abstract · PDF

Logic Programming and Knowledge Representation · primary corpus · published 2026-10-23T13:10:32Z
Dan Bachar, Ehud Shapiro
arXiv categories: cs.NI, cs.DC, cs.PL

Multiagent deterministic GLP (madGLP) runs Grassroots Logic Programs (GLP) as agents that communicate solely by asynchronous message passing, and assumes fair delivery: every message sent is eventually delivered. Each agent runs on a person's smartphone, named by the person's public key. A grassroots platform depends on no global resource but the network, so agents must reach one another over Bluetooth Low Energy, on a local network, and across the Internet from behind NAT, via rendezvous servers anyone can run. What madGLP requires of such a network, and what the network requires of the platform, has not been specified. We specify the networking layer beneath madGLP. Anything that can be done in GLP is done in GLP: the layer provides only what GLP cannot reach - the network stack, the location service, application attestation, and cryptographic primitives. Three transport underlays share one interface. Over PAN and LAN, an agent advertises a rotating recognition token derived from its key and time slot, so a peer who knows the key recognises it before contact and nobody else can track it; whether it answers unrecognised contacts is a per-underlay trust level set by GLP. Over WAN, a rendezvous server is a static-address host running the headless layer and a GLP rendezvous agent that coordinates hole punching, relays no payload, and belongs to no social graph. On every underlay, peers establish a mutually authenticated Noise session from Ed25519 keys, then attest, bound to the handshake hash, that each runs the application published under its developer's key, verified against Apple's and Google's roots with no third party contacted. One message protocol, over UDP datagrams and GATT writes, provides the fair, unordered, atomic and authenticated delivery madGLP assumes.

arXiv abstract · PDF

Logic Programming and Knowledge Representation · primary corpus · published 2026-10-23T15:44:17Z
Yukun Yang
arXiv categories: cs.LO

An explanation may exist in every complete context yet be impossible to select from the information observed. We study this distinction in finite propositional Horn abduction with integrity constraints. Observations are sufficient when each report admits one hypothesis set that is consistent and entails the manifestation in every compatible context. We characterize sufficiency by minimal context families with no common explanation. Their variable spans form a canonical hypergraph whose transversals are exactly the sufficient observation sets. The characterization recovers classical discernibility for unique explanations and supports composition across independent components. Minimal obstructions have unbounded cardinality even for acyclic rules, while rectangular explanation families admit a tight bound given by their largest choice domain. With circuit-defined contexts, sufficiency is $\Pi_3^P$-complete and selecting at most $k$ observable variables is $\Sigma_4^P$-complete, already for unrestricted contexts and acyclic rules. The selection reduction makes observation choices enforce globally fixed existential commitments. Explicit contexts reduce both tasks to NP-complete problems; tabulated explanation families make sufficiency polynomial. These results connect explanatory choice, information requirements, and representation cost.

arXiv abstract · PDF

Modal and Non-Classical Logics · primary corpus · published 2026-10-19T11:17:34Z
Avijeet Ghosh, Fran\c{c}ois Schwarzentruber
arXiv categories: cs.AI, cs.LO

In this paper, we study the theoretical computational complexity of counting trees and graphs that are classified positively by a graph neural networks, or said equivalently that satisfy a given formula of modal logic with counting. We also study convergence.

arXiv abstract · PDF

Modal and Non-Classical Logics · primary corpus · published 2026-10-23T08:29:15Z
Stefan Gebhart, Lutz Schr\"oder, Paul Wild
arXiv categories: cs.LO

Fuzzy logics with truth values in the unit interval vary in their choice of propositional connectives and their semantics, ranging from just minimum and maximum as in Zadeh logics to truncated addition and subtraction as in {\L}ukasiewicz logics or their extensions with truth constants, known as Pavelka logics. In the more specific world of fuzzy modal logics, non-expansive fuzzy modal logic has recently been proposed as a sweet spot between {\L}ukasiewicz (more precisely, Pavelka) and Zadeh fuzzy modal logic; it restricts {\L}ukasiewicz propositional connectives to have one argument constant, equivalently extends the Zadeh propositional base with constant shift operators. It retains reasonable expressiveness both in practical terms and abstractly; in particular, it characterizes the standard notion of behavioural distance on fuzzy Kripke frames. At the same time, it allows for satisfiability checking in the same complexity as for its two-valued correspondent (the modal logic K, or the description logic ALC), in contrast to the notorious computational hardness of {\L}ukasiewicz modal logic. In the present work, we show that non-expansive fuzzy modal logic admits uniform interpolation, a key property in modularization, information hiding, summarization, and other applications that fails for both {\L}ukasiewicz (or Pavelka) and Zadeh modal logic.

arXiv abstract · PDF

Modal and Non-Classical Logics · primary corpus · published 2026-10-23T08:56:52Z
Josef v. H. Doyle, Wesley Fussner
arXiv categories: math.LO

We show that each of the infinitely many extensions of the basic inquisitive logic has the Craig interpolation property, and deduce from this that each of these extensions also has the Beth definability property. These results stand in contrast to existing characterizations of interpolation within lattices of extensions, in which the distribution of logics with interpolation is sparse.

arXiv abstract · PDF

Modal and Non-Classical Logics · primary corpus · published 2026-10-25T14:36:47Z
Pietro Casavecchia, Alberto Paparella, Leonardo Serrentino
arXiv categories: cs.LO

Reasoning tasks over modal logics are notoriously difficult, comprising problems which are often semi-decidable. Hence, it is not rare for applications leveraging such tasks to exploit heuristic approaches able to give results in an acceptable amount of time, at the cost of some inaccuracies. Some approaches may benefit from vector embeddings, allowing for instance to involve neural networks and machine learning models in the reasoning process. This work aims at providing a new way to provide such embeddings specifically for the modal case, aiming for faster reasoning through both mathematical and learning techniques.

arXiv abstract · PDF

Modal and Non-Classical Logics · primary corpus · published 2026-10-25T18:31:29Z
Andrzej Indrzejczak (University of {\L}{\'o}d{\'z}, Poland), Tomasz Jarmu{\.z}ek (Nicolaus Copernicus University in Toru{\'n}, Poland), Mateusz Klonowski (Nicolaus Copernicus University in Toru{\'n}, Poland), Micha{\l} Zawidzki (University of {\L}{\'o}d{\'z}, Poland)
arXiv categories: cs.LO, cs.SC

Non-Classical Logics. Theory and Applications (NCL) is an international conference aimed at presenting novel results and survey papers in the broad field of non-classical logics and their applications. The first two editions were held in {\L}{\'o}d{\'z}, Poland, in September 2008 and 2009. Subsequent editions were organised in Toru{\'n} (2010, 2012, 2015, 2018) and {\L}{\'o}d{\'z} (2011, 2013, 2016, 2022, 2024). The tenth edition of the conference, organised by the University of {\L}{\'o}d{\'z} in 2022, was the first to have its proceedings published in EPTCS. We are honoured and pleased to continue this practice and, for the third time, include all accepted long papers in an EPTCS volume. Furthermore, for the first time, we have also included all accepted extended abstracts in the volume.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-19T04:33:24Z
Wei Wang
arXiv categories: math.LO

An infinite (binary) tree is \emph{positive} iff its set of paths is non-null. As an elementary observation, positives trees always have positive perfect subtrees. Given a positive tree of certain complexity, here we present several theorems concerning the distribution of the Turing jumps or iterated Turing jumps of (positive) perfect subtrees of the given tree in the universe of Turing degrees.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-19T13:45:12Z
Chris Schulz
arXiv categories: math.LO

In 1996, Michaux and Villemaire showed that any nontrivial expansion of $(\mathbb{N}, +)$ defines new unary sets. We conjecture that the same holds over the structure $(\mathbb{N}, +, k^\mathbb{N})$, and we prove a partial result in this direction. To do so, we first show that every nonempty sparse $k$-automatic set is a Presburger-definable image of some Cartesian power of $k^\mathbb{N}$. Using this characterization, we prove that if an expansion of $(\mathbb{N}, +, k^\mathbb{N})$ defines the same unary sets, then every set of sublinear growth definable in the expansion is already definable in $(\mathbb{N}, +, k^\mathbb{N})$.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-20T01:47:58Z
Micha\"el Cadilhac
arXiv categories: cs.FL, cs.LO

A semilinear set is stratifiable if it is a finite union of linear sets whose periods have at most two nonzero coordinates, with no two periods in one component connecting alternating pairs of coordinates. We give a computable many-one reduction from the existence of a rational zero of an integer polynomial to deciding stratifiability. After the classical reduction to quadratic systems, we reduce rational solvability of these systems to a problem we call finite separation by Cartesian products of rational linear forms. Its input consists of rational subspaces $D_1,\ldots,D_k\le\mathbb Q^r\times\mathbb Q^r$. A separator is a map $(\boldsymbol x,\boldsymbol y)\mapsto(u(\boldsymbol x),v(\boldsymbol y))$, where $u,v\colon\mathbb Q^r\to\mathbb Q$ are nonzero rational linear forms. The problem asks whether finitely many separators suffice so that every pair outside $\bigcup_iD_i$ receives, from some separator, a value attained at no pair in that union. We then reduce this problem to stratifiability. Ginsburg and Spanier's characterization of letter-bounded context-free languages} also induces a reduction from rational polynomial solvability to context-freeness of letter-bounded languages specified by semilinear exponent sets. An OpenAI preprint claims undecidability of rational polynomial solvability; if correct, our result settles the decidability of general stratifiability, a problem open since 1966.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-20T21:05:10Z
Ivan Drecun
arXiv categories: cs.SC, cs.LO

Solvers for graph isomorphism and related problems are widely used in both theoretical and applied domains, but their complexity often requires users to trust their correctness without verification. We present a certifying algorithm for computing a generating set of the automorphism group of a given graph, meaning that it produces an independently verifiable certificate that the output list of automorphisms generates the entirety of the automorphism group. The problem of constructing a certificate is reduced to certifying that a system of multivariate polynomial equations is infeasible. An individualization-refinement algorithm produces a derivation within an algebraic proof system, representing a Nullstellensatz certificate of infeasibility. We provide an implementation of both the certifying algorithm and a certificate verifier, and demonstrate their viability on graphs with hundreds of vertices.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-21T23:08:30Z
Pelle Brooke Borgeke
arXiv categories: math.LO

In this article, we use the PBNF-transform, or Polynomial Boolean Normal Form, described earlier in two articles and now extended to higher arity, to solve Boolean satisfiability problems (SAT), which are part of the P versus NP problem. SAT consists of a statement of conjunctions of clauses, and in our SAT-solving models, we dualize the logical equations, inverting the problem by \emph{multiplying} letters (literals) in the transferred clauses, now phrases: $pqrs\cdots s_{\ell}$, and using a binary iterated composition based on \emph{adding polynomials} for the conjunctions in our solution formula. We obtain Polynomial Boolean Equations, PBE=0, by also renaming the truth value $1\mapsto 0$(T). To find a solution, we look for repeating literals in the clauses to factor out. With reversed literal repetition, we can even reduce the CNF to the sum of the transformed clauses.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-22T00:44:36Z
Ruofei Xie, Xuanheng Zhao
arXiv categories: math.LO, math.FA

For every right-c.e.\ real $p\in(1,2)$, $L^p[0,1]$ has a computable presentation. The proof combines an effective stability modulus for almost isometric embeddings with a Fra\"{\i}ss\'e-style construction in which the exponent varies. In the same range, if $\ell^p$ has a computable presentation, then $p$ is computable. Combining these with the known results gives the computable presentability classification for all separable Lebesgue spaces. We also formulate an effective Fra\"{\i}ss\'e theorem for Banach spaces and apply it to obtain a computable presentation of the Gurarij Banach space.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-22T00:55:02Z
Xuanheng Zhao
arXiv categories: math.LO

Let 2 be the two-element structure in the empty signature. We build a computable presentation Q of the Borel randomization $2^{[0,1)}$ in which neither constant random variable is a computable point. Consequently, Q is not aware. This gives a negative answer to a question of Cuervo Ovalle and Goldbring \cite{CG}. We also construct a countable structure $M$ with no computable presentation but $M^{[0,1)}$ has a computable presentation. This answers another question and establishes the necessity of the awareness condition stated in one of the main theorems in \cite{CG}.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-23T11:56:01Z
Remi Pallen
arXiv categories: math.LO, cs.CC

The Medvedev lattice is a tool used to classify the complexity of effective closed sets. In this article, we are interested in the complexity of using this tool. In particular, we study the complexity of deciding whether two effective closed sets have the same degree, when one is fixed and the other is given as input. This problem is naturally~$\Sigma^0_3$, and among other results, we show that for all degrees except the maximal one, the problem reaches its maximal complexity. It turns out that the argument is not uniform and depends on the self-similarity of the fixed degree, a notion that we introduce in this article. The complexity of having maximal degree is particularly difficult to establish, but we obtain a lower bound that almost matches the upper bound. We also show that deciding whether an effective closed set has a degree incomparable with a fixed degree $d$ is $\Pi^0_3$-complete whenever $\mathbf{0}_s <_s d <_s \mathbf{1}_s$.

arXiv abstract · PDF

Computability and Complexity · primary corpus · published 2026-10-25T19:18:36Z
Reijo Jaakkola
arXiv categories: cs.CC, cs.LO

The Minimum Equivalent Expression problem (MEE) asks, given a propositional formula $\phi$ and an integer $k$, whether $\phi$ is equivalent to a formula with at most $k$ occurrences of propositional variables. While the problem is clearly in $\Sigma_2^p$, its completeness under polynomial-time many-one reductions has remained open since at least 1979. Buchfuhrer and Umans showed in 2008 that it is $\Sigma_2^p$-complete under polynomial-time Turing reductions. In this note, we present a proof discovered by GPT-Sol-6.1 which establishes that MEE is $\Sigma_2^p$-complete also under polynomial-time many-one reductions.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-19T03:09:32Z
Yifan Hu
arXiv categories: math.LO, math.CO

We establish a precompact transfer theorem for big Ramsey structures and a uniform envelope theorem for valuation hypergraphs. These yield big Ramsey structures for generic injective relational structures in languages with finitely many symbols of each positive arity, answering the existence part of Problem~6.3.2 of Balko et al.\ [M.~Balko et al., J.~Eur.~Math.~Soc.\ 28, 2101--2150 (2026)], and refute Conjecture~4.7 of Braunfeld et al.\ [S.~Braunfeld et al., Adv.~Comb., Paper No.~4 (2024)]. We also construct a finitely constrained free amalgamation class in a finite language of maximum arity three whose Fra\"iss\'e limit has infinite singleton big Ramsey degree, giving a negative answer to the existence question in Problem~6.3.3 of Balko et al.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-19T10:59:08Z
Jan Hubi\v{c}ka, Mat\v{e}j Kone\v{c}n\'{y}, Jaroslav Ne\v{s}et\v{r}il, Norbert Sauer
arXiv categories: math.CO, cs.DM, math.LO

Let $S\subseteq \mathbb R^+$ be a subset of positive reals. We say that a metric space is an $S$-metric space if the range of the metric is a subset of $S\cup \{0\}$. In 2007, Delhomm\'{e}, Laflamme, Pouzet, and Sauer characterized those sets $S$ for which the class of all finite $S$-metric spaces has the amalgamation property. Given an amalgamation class, a natural question is what its Ramsey expansion is. Ramsey expansions are known for classes of $S$-metric spaces for which $S\cup\{0\}$ carries a natural distance monoid structure, for example for $S=\mathbb Q^+$ or when $S$ is topologically closed. In this paper, we extend this result to all amalgamation classes of finite $S$-metric spaces, thereby completing the Ramsey-theoretic classification of amalgamation classes of finite $S$-metric spaces.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-19T13:07:46Z
Marcos Gir\'on
arXiv categories: math.LO

We establish a general decomposition for regular closed semilinear sets, derived from a detailed study of their topological boundary. As an application, we characterize stable semilinear sets in ordered vector spaces over an ordered field, extending previous results of Hoffmann, Tran, and Ye.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-20T10:07:50Z
Martin Bays
arXiv categories: math.NT, math.LO

We consider the problem of reducing Zilber's pseudo-exponentiation conjecture to mere exponential-algebraic closedness, assuming Schanuel's conjecture but not Zilber-Pink. Generalising work of Mantova, we show that it would suffice to show that perfectly rotund varieties have non-dense intersection with finitely generated subgroups of the graph of exponentiation in which the exponentials live in a number field.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-20T16:27:59Z
Gal Binyamini, Avner Kiro, Gady Kozma, Jonathan Pila
arXiv categories: math.CA, math.LO

We establish o-minimal definability results and develop point-counting machinery applicable to the zeros of a Bessel function of fixed non-negative real parameter. We also give an Ax-Schanuel theorem for Bessel functions of fixed (complex) parameters and exponential functions. We combine these to prove a sparsity result (weak Manin-Mumford) for points on an algebraic variety whose coordinates are zeros of a Bessel function of fixed (non-negative real) parameter. We apply this result to improve density results on spectral sets for the unit ball motivated by Fuglede's conjecture.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-21T05:06:29Z
Thang Do, Arnulf Jentzen, Benno Kuckuck
arXiv categories: math.DS, cs.LG, math.AG, math.CA, math.LO

We prove that for every open $ U \subseteq \mathbb R^n $ the spherical projection of every gradient trajectory $\theta(t)$, $t \geq 0$, of a definable $C^1$-potential $F \colon U \to \mathbb R$ has finite length and, in particular, converges (directional convergence). In other words, every gradient trajectory of a definable $C^1$-potential has finite total angular motion. Here, definable means definable in an arbitrary o-minimal structure expanding the real field. Notably, the gradient trajectory in this result is an arbitrary solution of the gradient flow differential equation (whose solutions may not be unique) with no further assumptions: The gradient trajectory may be unbounded and diverge to infinity or it may be convergent. The established theorem therefore provides affirmative answers to both the gradient conjecture at infinity for definable potentials and the definable Thom gradient conjecture. We apply our theorem to the training of deep neural networks (DNNs) to conclude that, in the case of definable and continuously differentiable activation and loss functions, the spherical projection of the DNN training flow must always converge (directional convergence).

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-22T05:34:24Z
Pablo Cubides Kovacsics, Mariana Vicar\'ia, Jinhe Ye
arXiv categories: math.LO, math.AG

We study the analytification and tropicalization of algebraic varieties over valued fields via Jun's spaces of hyperfield points. Our main new objects are a family of power-tropical hyperfields $H_n$ and their inverse limit $H$, recording at each level the class of a leading term modulo $n$-th powers of the residue field. They yield an enhanced tropicalization of the associated space $X(H)$, strictly finer than the Berkovich one exactly when the multiplicative group of the residue field is non-divisible: it specialises to the Berkovich analytification when the residue field is algebraically closed, to the real analytification of Jell-Scheiderer-Yu when it is real closed, and to a new $p$-adic analytification when it is $p$-adically closed. Over henselian valued fields of equicharacteristic $0$ we then construct a model-theoretic avatar of $X(H)$: the space $\widehat{X}_T$ of definable types orthogonal to the value group, which sharpens the geometry in the spirit of Hrushovski and Loeser and recovers their space over algebraically closed valued fields. We show that $\widehat{X}_T$ is strictly pro-definable, satisfies a model-theoretic Payne theorem, and definable compactness in such spaces satisfies a Heine-Borel type characterization. As an application, we analytify $p$-adic semi-algebraic sets and prove a strong density theorem for their tropicalizations, the exact $p$-adic counterpart of the real one of Jell-Scheiderer-Yu.

arXiv abstract · PDF

Model Theory and Definability · primary corpus · published 2026-10-22T17:31:49Z
Tom Leinster, Maia Woolf
arXiv categories: math.CT, math.LO, math.RA

A hard theorem of Givant classifies the finitary algebraic theories for which every algebra is free. From it, one easily deduces that all such theories are minimal (adding any further equations makes them trivial) and have a well-defined notion of dimension (free algebras on sets of different cardinality are never isomorphic). We prove both these properties directly, without the aid of Givant's theorem.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-19T19:20:18Z
Jananan Arulseelan, James E. Hanson
arXiv categories: math.OA, math.LO

Combining a modification of the recent counterexample to the quasitrace conjecture with model-theoretic reductions due to the first author, we exhibit a counterexample to the monotone completeness conjecture. We fully reproduce the disproof of the quasitrace conjecture by a modified construction and arguments.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-20T01:44:30Z
Atticus Cull, Felix Weilacher
arXiv categories: math.LO

We prove that a Borel strict partial order is an increasing union of wellfounded Borel partial orders if and only if it admits an (injective) Borel homomorphism to the eventual domination order.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-20T14:28:49Z
Jialiang He, Jiaheng Zhuang, Yi Zhou
arXiv categories: math.LO

Motivated by the existence of closed maximal $\mathcal{I}$-eventually different ($\mathcal{I}$-MED) families, we study uniform combinatorial properties of ideals. For a fixed ideal, a property is uniform if its witnesses can be chosen by a single Borel map. We prove that every $\boldsymbol{\Sigma}^0_3$ ideal is uniformly weakly $P^+$. We also prove that the classes of Farah and weakly Farah ideals coincide, answering a question of Hru\v{s}\'ak and Meza-Alc\'antara. We then show that every weakly Farah ideal is uniformly weakly Ramsey. As an application, we obtain closed $\mathcal{I}$-MED families for $\boldsymbol{\Sigma}^0_3$ ideals and weakly Farah ideals.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-21T01:36:29Z
Remi Salinas Schmeis
arXiv categories: math.CO, math.LO

Given a poset $P$ with no maximal element the question naturally arises of when $P$ can be partitioned into $\omega$-chains. In this paper we give general criterion for when this can be done. We show that in the case when a poset with no maximal element is countable or a well-founded forest, then it can always be partitioned into $\omega$-chains. We then introduce the lifting property for posets with no maximal element and show that a poset can be partitioned into $\omega$-chains if and only if it has the lifting property.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-21T13:53:43Z
Brinda Venkataramani
arXiv categories: math.LO

We study the countable partition model over a set of atoms of arbitrary uncountable cardinality $\kappa$. Its supports are partitions of the atoms into countably many blocks, and a permutation fixes a support when it preserves each block setwise. This model was proposed by Bruce and studied by Banerjee. We prove that dependent choice holds for every $\kappa$, although the filter of subgroups is not closed under countable intersections. Choice for well-orderable families holds exactly when $\kappa<\aleph_{\omega_1}$; when $\kappa\ge\aleph_{\omega_1}$, an $\omega_1$-indexed family witnesses its failure. The Hartogs and Lindenbaum numbers of the set of atoms are both $\omega_1$. The proofs use permutations matching blocks of equal cardinality and establish shift completeness of the filter. Together with Banerjee's failure of $\mathsf{DC}_{\omega_1}$, these results determine which dependent choice principles hold in the model.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-22T10:17:46Z
Chris Scambler, Cesare Straffelini
arXiv categories: math.LO

After defining the concept of inevitability for statements with the modal logic of forcing, we raise the question of which statements are inevitable under $\mathsf{ZFC}$ and under large cardinal hypotheses. We show that $\mathsf{SOA}$ (defined as $\mathsf{ZFC}^-$ + $\mathsf V=\mathsf{HC}$) plus the $\boldsymbol\Sigma^1_2$-perfect set property is $\mathsf{ZFC}$-inevitable, and that Projective Determinacy is inevitable in the theory of $\mathsf{ZFC}$ with a proper class of Woodin cardinals. We then discuss the possible conceptual significance of these results for the foundations of set theory.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-22T10:32:13Z
Ruijun Wang
arXiv categories: math.LO

Rosendal proved that any $K_\sigma$ equivalence relation is Borel reducible to $\ell_\infty$. We prove that for every $F_\sigma$ equivalence relation $F$ on a Polish space, there is an $F_\sigma$ real linear subspace $H$ of $\ell_2$ such that the coset relation $x\mathrel{E_H}y$ if and only if $x-y\in H$ has no Baire-measurable reduction to $F$. In particular, there is no $F_\sigma$ equivalence relation universal under Borel reducibility for all $F_\sigma$ equivalence relations. This answers a question of Rosendal.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-22T16:53:58Z
Rapha\"el Carroy, Julien Melleray
arXiv categories: math.FA, math.GR, math.LO

We develop a method for studying centralizers of generic elements in some large Polish groups. We identify a condition which enables us to show that the range of each power map is comeager; a strengthening of this condition allows us to prove that a generic element embeds in a flow (a continuous, one-parameter subgroup). This approach enables us to answer the question that motivated this work : we prove that a generic isometry of the Urysohn space (or the Urysohn sphere) embeds in a flow. We also obtain information on the centralizer of a generic isometry; we show that it contains an infinite-dimensional torus and that torsion elements are dense in it. To illustrate the flexibility of our method, we apply it to two other Polish groups. The first is the group of measure-preserving automorphisms of a standard probability space, and we recover results of King and of de la Rue and de Sam Lazaro. Finally we apply our technique to the group of nonsingular automorphisms of a standard probability space, and we deduce that a generic nonsingular automorphism embeds in a flow, answering a question of Danilenko and Silva.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-22T17:32:55Z
Hakk{\i} Ka\u{g}an Yumak
arXiv categories: math.LO, math.GR

In this paper, we prove that the set of groups satisfying the minimal condition on centralizers is a complete co-analytic subset of the Polish space of countable groups. This answers a question of Wesolek and Williams.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-23T01:29:39Z
Anush Tserunyan, Robin Tucker-Drob
arXiv categories: math.LO, math.DS

We study the structure of amenable subrelations of treeable measure-class-preserving equivalence relations, applying the Radon--Nikodym topography perspective initiated in our companion paper [TTD25]. For a nowhere smooth amenable subrelation, we show that the ends selected by each class in Adams's end selection theorem are precisely those which are nonvanishing along that class. From this, we derive a number of structure results about nowhere smooth amenable subrelations of treeable equivalence relations. For example, we show that every nowhere smooth amenable subrelation is contained in an essentially unique maximal amenable subrelation. This yields an anti-treeability criterion, which we use to show that every nonamenable locally compact second countable group with noncompact amenable radical is not treeable, and that every nonamenable nonunimodular treeable group has a compact open subgroup.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-24T18:01:21Z
Daniel Max Hoffmann, Krzysztof Krupi\'nski
arXiv categories: math.DS, math.LO

We are developing some topological dynamics below a given ambit. We define and study Bohr compactifications below ambits and other related objects. We describe a natural epimorphism from the Ellis group of an ambit to the Bohr compactification below its Ellis semigroup ambit. The first main result says that, assuming tameness and hereditary amenability, this natural map is an isomorphism of topological groups. This is an abstract dynamical generalization of Newelski's conjecture, or rather a theorem of Chernikov and Simon that a natural map from the Ellis group of the flow $(S_G(M),G)$ to the definable Bohr compactification of $G$ is an isomorphism when $G$ is a definably amenable group definable in a NIP structure $M$. We give two proofs of our main result: a shorter dynamical proof and an analytic proof. In the course of the dynamical proof, we prove some results on the universal compactification flow and on the generalized Bohr compactification below a given ambit which admits a left continuous semigroup operation extending the action of $G$. The considerations around the analytic proof yield a description of the measured structure of amenable tame minimal flows, which is the second main result of this paper. We also study specializations of the above abstract topological dynamics context to model theory contexts to recover some known and to obtain some new notions and results. The main new results in the model theory contexts are: (i) a description of the Bohr compactification of the group of automorphisms of a sufficiently saturated model $\mathfrak{C}$ of a first order theory $T$ below a certain fundamental ambit associated with $\mathfrak{C}$; (ii) transfer of amenability of a NIP theory $T$ to amenability of the Ellis semigroup ambit; (iii) a version of Newelski's conjecture for spaces of local types with a description of Bohr compactifications below such spaces.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-25T09:57:29Z
Shimon Garti
arXiv categories: math.LO, math.CO

Let $\lambda$ be a Magidor cardinal and let $\alpha\in[\alpha_M,\lambda)$. We show that $\lambda\rightarrow[\lambda]^{\aleph_0-bd}_{\alpha,<\alpha}$. We prove the consistency of a similar statement for J\'onsson cardinals.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-25T14:33:18Z
Damien Gaboriau, Antoine Poulin, Anush Tserunyan, Robin Tucker-Drob, Konrad Wr\'obel
arXiv categories: math.GR, math.DS, math.LO

In this article we show that all the nonamenable Baumslag-Solitar groups with nonunimodular Bass-Serre tree, i.e., $\mathrm{BS}(p,q)$ with $|p|,|q| \neq 1$ and $|p|\neq |q|$, are measure equivalent to each other, thereby completing the measure equivalence classification of Baumslag-Solitar groups: each $\mathrm{BS}(p,q)$ belongs to one of three measure equivalence classes according to whether it is amenable ($|p|=1$ or $|q|=1$), virtually isomorphic to $\mathbf{F}_n \times \mathbf{Z}$ ($|p|=|q|\neq 1$), or is nonamenable with nonunimodular Bass-Serre tree ($|p|,|q| \neq 1$ and $|p| \neq |q|$). More generally, we obtain the similar classification of the generalized Baumslag-Solitar groups of rank $1$ (i.e., groups that act cocompactly on a tree with edge and vertex stabilizers infinite cyclic). Our proof also establishes a classification of all treeable lcsc groups into exactly six measure equivalence classes. Our new contribution which completes this taxonomy is: all nonunimodular nonamenable treeable lcsc groups are measure equivalent. Along the way we obtain several results about type $\mathrm{III}$ equivalence relations and graphings of independent interest. For example, we show that every ergodic type $\mathrm{III}_0$ graphing admits an ergodic hyperfinite subgraph for which the natural factor map of Krieger flows is an isomorphism.

arXiv abstract · PDF

Higher Categories and Homotopy Theory · primary corpus · published 2026-10-21T05:47:05Z
Abhiram Srinivas Yedathore
arXiv categories: math.AT, math.CT

We freely enrich the pointed homotopy category of CW complexes over abelian groups and equip the resulting functor category with the enriched Day convolution induced by the smash product. After identifying the convolution unit and recording the coherence maps, we compute the convolution of the homotopy-group functors. For integers $n,m\geq 2$ we construct a natural isomorphism $\pi_n\star\pi_m\cong\pi_{n+m}$ induced by the external smash product; equivalently, the external smash product is the universal natural pairing of homotopy groups. Under this identification, the symmetry interchanging the two factors acts on $\pi_{n+m}$ by multiplication by $(-1)^{nm}$.

arXiv abstract · PDF

Higher Categories and Homotopy Theory · primary corpus · published 2026-10-21T16:24:35Z
Tobias Dyckerhoff, Till Heine, Simon Schneider, Kostiantyn Tolmachov
arXiv categories: math.AG, math.CT, math.RT

Higher categorical methods allow us to view recollements as lax descent data and build a corresponding descent theory governed by an $\infty$-bicategorical theory of limits. We demonstrate some concrete innovations brought along by these new techniques in the classical context of constructible and perverse sheaves on stratified spaces. Our first application uses partially (op)lax descent to recover the famous result of Beilinson telling us how to glue perverse sheaves in terms of vanishing and nearby cycles. The remainder of the article is concerened with establishing a uniform view on a series of classification results for perverse sheaves culminating in recent work of Kapranov-Schechtman. Namely, we use lax descent to establish a ``foliated'' variant of Verdier duality which, informally speaking, identifies the derived constructible category of a suitably foliated space with sections of a categorical cosheaf on the leaf space whose stalks are the categories of sheaves along the leaves. Again, this is obtained as an application of lax descent, and seems to provide a reasonable framework to formalize the idea of ``mixed sheaf-cosheaf objects'' promoted by Kapranov and Schechtman.

arXiv abstract · PDF

Higher Categories and Homotopy Theory · primary corpus · published 2026-10-22T15:12:18Z
John Bourke, Gabriele Lobbia
arXiv categories: math.CT

In previous work, we constructed a closed skew monoidal structure on the category of Gray-categories and Gray-functors whose internal hom Psd(A, B) captures pseudomaps and pseudo-transformations. In the present paper we give a symmetric description of the Gray-category Psd(A,B) and use this to prove that the skew monoidal structure is symmetric skew monoidal.

arXiv abstract · PDF

Higher Categories and Homotopy Theory · primary corpus · published 2026-10-22T15:44:18Z
John Bourke, Gabriele Lobbia
arXiv categories: math.CT

We introduce several flavours of semi-strict 4-category as enriched categories. This is done using the framework of enrichment over skew monoidal categories of Gray-categories and their associated multicategories, as developed in our previous work. We give the axioms for semi-strict 4-categories in elementary terms and describe a wide range of examples. In particular, we answer the question of what exactly Gray-categories and the higher transformations between them form: namely, a left-sharp 4-category G-Cat$^4$. In addition, we describe examples arising from braided monoidal 2-categories, monoidal Gray-categories (herein defined) and Gray-categories with structure. We use the concepts introduced here and the relationships between them to unify various concepts in the literature, such as Crans' 4-teisi. In the second part of the paper, we investigate homotopical aspects. In particular, we classify the equivalence n-cells in the left-sharp 4-category G-Cat$^4$ for each n. Using this, we show that the left-sharp skew monoidal structure on the category of Gray-categories induces a symmetric monoidal closed structure on the homotopy category of Gray-categories.

arXiv abstract · PDF

Higher Categories and Homotopy Theory · primary corpus · published 2026-10-25T21:45:51Z
Federico Bambozzi
arXiv categories: math.CT, math.AG, math.RA

We compare homological and homotopical epimorphisms of associative algebras in monoidal $\infty$-categories. Assume that geometric realizations and pushouts of associative algebras exist and that tensoring preserves geometric realizations. Then every homological epimorphism is homotopical. If, in addition, the ambient category is additive and tensoring preserves finite coproducts, the converse holds. This extends the result of Chuang and Lazarev for dg-algebras. In the symmetric monoidal setting, we discuss consequences for centers and commutative refinements, as well as applications to derived analytic geometry.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-20T12:46:45Z
Florian Warg
arXiv categories: math.CT, math.AT, math.KT, math.QA

The classical Dold--Kan correspondence identifies simplicial modules with connective chain complexes. Using Morita theory, we construct a Dold--Kan-type correspondence for every linear category carrying a suitable action of the maximum-preserving simplicial operators. The construction functorially assigns a Morita-equivalent normalized category to every such linear category. In particular, we obtain Dold--Kan-type correspondences for all crossed simplicial groups. We prove a rank formula for the normalized hom-modules and show that a crossed simplicial group is self-dual precisely when its underlying simplicial set of automorphism groups has dimension one. Furthermore, we construct normalization-compatible self-dualities and recover the Dwyer--Kan correspondence for duplicial, paracyclic and N-cyclic modules.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-21T07:50:58Z
Yusuke Shiobara
arXiv categories: math.DG, math.CT

We develop curvature theory on Blohmann's elastic diffeological spaces. We introduce curvature-tensorial connections, whose curvature factors uniquely through $T_3M$, and show that this property holds on finite-dimensional manifolds and is preserved on mapping spaces. Using a plotwise commutator identity and the elasticity axioms, we establish the classical curvature symmetries for curvature-tensorial Levi-Civita connections. We define sectional curvature and a curvature form on the algebraic exterior square, and demonstrate an obstruction to the usual Ricci trace construction: on $C^\infty(S^1,S^2)$, the relevant curvature endomorphism extends boundedly to the $L^2$ completion but is not trace class. We prove the second variation formula, identify the energy Hessian with the index form, and characterize its null space. Under additional hypotheses, we establish existence and uniqueness of Jacobi fields with prescribed initial data. Finally, non-positive sectional curvature excludes conjugate points, while a negative index direction obstructs length minimization.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-21T14:02:54Z
Ivan Di Liberti, Umberto Tarantino, Lingyuan Ye
arXiv categories: math.CT, cs.LO, math.LO

We study the relationship between doctrines, encoding 2-categories of theories in predicate logic, and fragments of geometric logic, defined through Kan injectivity in the 2-category of topoi. After a brief historical account of the notion of doctrine, we propose our working definition. Our main result then establishes a Galois connection between doctrines and subgeometric logics. This connection suggests a mirror symmetry between the world of doctrines and the world of logics, in which constructions and results on either side admit counterparts on the other. We develop this symmetry through constructions of syntactic categories and classifying topoi in both settings, recovering the familiar examples from categorical logic. We prove paired Diaconescu-type theorems and give symmetric universal characterisations of the two closure operators induced by the Galois connection. Finally, we show that passing from a doctrine to its closure induces a reflection between the corresponding 2-categories of algebras, and we relate this reflection to conceptual completeness.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-22T00:18:22Z
Robin Cockett
arXiv categories: math.CT

The localizing/separating factorization, which is the analogue, for restriction categories, to the surjective/embedding factorization for topoi, is developed at both the mere restriction category and join restriction category level. The factorization system at both the ordinary and join level is approached using the notion of a density, which is a stable and universal suborder of the restriction order. The main technical results of the paper construct the join localization and establish its basic properties. The paper gives several examples of localizations. In particular, examples of localization on commutative rigs are provided which give a way to construct categories of schemes. The Zariski spectrum and the Pierce spectrum are, in particular, developed.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-23T09:26:02Z
Carlyle Stewart
arXiv categories: math.CT

In this paper we prove that the Mal'tsev condition expressing the existence of group operations is not equivalent to a categorical property. More precisely, using pseudo-invertible idempotents, we construct two varieties $\mathcal{V}$ and $\mathcal{V}(f)$ which are equivalent as categories, and such that $\mathcal{V}$ admits group operations, whereas $\mathcal{V}(f)$ does not. We also show that those Mal'tsev conditions which are equivalent to a categorical property have a trivial spectrum.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-23T11:28:30Z
Florent Afsa, Tim Van der Linden
arXiv categories: math.CT, math.KT

We explore sufficient conditions for the higher \v{C}ech derived functors of a Birkhoff reflector to agree with its ordinary, Barr-Beck comonadic homology. Using categorical Galois theory together with a spectral-sequence argument, we prove that this is the case for the reflector from any semi-abelian variety onto a subvariety: for every $n\geq 1$, the $n$th \v{C}ech derived functor of the reflector coincides with its $(n+1)$st comonadic homology object. More generally, the comparison holds for any Birkhoff reflector of a semi-abelian category equipped with a comonad satisfying Quillen's conditions.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-24T08:39:45Z
Boris Chorny, Giuseppe Leoncini
arXiv categories: math.CT, math.AT

We generalize to the enriched setting the classical theorem of Freyd, that the free cocompletion ${\mathscr PA}$ of a category ${\mathscr A}$ is complete if and only if ${\mathscr A}$ is approximately complete. The work of Day and Lack, arXiv:math/0610439, has laid the foundations for such a generalization and has had multiple applications in homotopy theory and in category theory. Our result allows us to expand on some of these applications.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-24T20:30:14Z
Jeremy Edison, Alexander Sistko
arXiv categories: math.CT, math.CO, math.RT

In this paper, we show how to associate a family of binary linear block codes to the class of admissibly cofinitary objects in any proto-exact category with rank function. This family naturally generalizes the well-studied family of binary Reed-Muller codes, and recovers this classical family for suitable choices of category. We also expand the list of known examples of proto-abelian categories to include incidence categories of posets. As an application of this result, we construct a binormal, combinatorial, proto-abelian category of Kashiwara crystals associated to any root system. In the case that the proto-exact category is a category of $\mathbb{F}_1$-representations of quivers, we show how to reconstruct our family via the language of algebraic geometry codes, in particular motivating an extension to arbitrary finite fields. We provide explicit computations of the dimension and minimum distance for select families of $\mathbb{F}_1$-representations of quivers.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-19T11:24:33Z
Jing Yu
arXiv categories: math.CT

In this paper, we investigate monoidal derived equivalences between tensor categories with infinitely many isomorphism classes of simple objects. We introduce the notion of a simple-shifted monoidal derived equivalence and prove that a simple-shifted monoidal derived equivalence gives rise to a tensor equivalence. In addition, we investigate which tensor categories have the property that every monoidal derived equivalence between them is necessarily simple-shifted, and we establish some sufficient conditions for this property. As a corollary, we prove that if a tensor category is monoidally derived equivalent to the finite-dimensional representation category of either the quantized enveloping algebra $U_q(\mathfrak{g})$, the quantized Borel subalgebra $U_q^{\geq 0}(\mathfrak{g})$, or the quantized coordinate ring $\mathcal{O}_{q}(G)$ (for a suitable $q$), it is tensor equivalent to the corresponding category.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-19T15:53:47Z
Mengzhen Zhu, Yuefei Zheng, Xianhui Fu
arXiv categories: math.RT, math.CT

In this paper, we investigate the behavior of approximability under separable extensions of triangulated categories. Let $\mathcal{B}$ be an approximable triangulated category and let $\mathbf{T}=(T,\theta,\mu)$ be a smashing, stably separable exact monad on $\mathcal{B}$. Assume that the category of $\mathbf{T}$-modules $\mathbf{T}\text{-}\mathrm{Mod}_{\mathcal{B}}$ admits a canonical triangulated structure. We prove that if $T$ is right $t$-exact with respect to a $t$-structure in the preferred equivalence class of $\mathcal{B}$, then $\mathbf{T}\text{-}\mathrm{Mod}_{\mathcal{B}}$ is again an approximable triangulated category. As an application, we show that, under suitable assumptions, a smashing localization functor on an approximable triangulated category induces a recollement of approximable triangulated categories, thereby yielding a converse-type result to the gluing theorem of Burke--Neeman--Pauwels. Finally, under suitable hypotheses, we prove that separable extensions restrict naturally to the intrinsic subcategories associated with approximable triangulated categories.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-20T17:07:25Z
Rapha\"el Paegelow
arXiv categories: math.RT, math.CT

We study the $2$-representation theory of the Taft category, the tensor category of finite-dimensional modules over the Taft algebra. This category has two left cells. We first classify suitable transitive modules over its based representation ring. For the upper cell, we recall a construction by Etingof and Ostrik giving an infinite family of pairwise nonequivalent simple $2$-representations. For the bottom cell, we pass to the semisimplification of the Taft category and identify a distinguished fusion subcategory with an adjoint $\mathfrak{sl}_2$ Verlinde category. Using algebra objects associated with $\mathsf{ADET}$-diagrams and categorical Clifford theory, we classify the regular exact indecomposable module categories of this semisimplification. For these regular module categories, the split Grothendieck group is a complete invariant. Finally, we identify the two cell $2$-representations of the Taft category.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-23T17:25:31Z
David E. Evans, Andrew Riesen
arXiv categories: math.QA, math.CT

For every odd integer $N\geq3$, we construct an untwisted Haagerup--Izumi fusion category $\mathcal H_N$ on the negative spherical branch and a simple, self-contragredient, regular, $C_2$-cofinite vertex operator algebra $E_N$ of central charge $-16N$, together with an equivalence of modular fusion categories: \[ \operatorname{Rep}(E_N)\simeq Z(\mathcal H_N). \] The VOA $E_N$ is rational, has exactly $N^2+3$ irreducible modules, and is lower bounded and integer graded, with least conformal degree $-(N-1)/2$. The proof begins with a CFT-type cyclic Virasoro extension of central charge $-5N$, whose regularity we establish. Two categorical condensations recover $\mathcal H_N$, and a finite extension by shifted lattice modules removes the auxiliary pointed factor. We identify the complete ribbon modular data of $Z(\mathcal H_N)$ with $\mathrm{MD}_{-}(\mathbb Z/N;\mathbb Z/(N^2+4),b\mapsto b^2/(N^2+4))$ in the notation of Gannon--Schopieray--Yadav, for every odd $N$.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-25T07:36:53Z
Hideto Asashiba
arXiv categories: math.RT, math.CT, math.RA

Let $\Bbbk$ be an algebraically closed field of characteristic different from $2$. We realize the four-dimensional selfinjective algebra $\Omega(1)$ as an admissible infinite cyclic orbit algebra of the repetitive Kronecker category. Thus an algebra long stated to be nonstandard is of Euclidean type in the orbit-algebra sense. We also identify a gap in an earlier proof of its nonstandardness and give an independent proof by determining all connected Galois covering sources of $\Omega(1)$. Together, these results disprove the implication from Euclidean type to standardness in the equivalence explicitly stated by Bocian--Holm--Skowro\'nski (2004) and Bocian--Skowro\'nski (2005). They also contradict the standardness conclusion of the Proposition in \S2.1 of Skowro\'nski (1989); its main theorem in \S1.5 assumes standardness and is not contradicted by this example.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-25T14:47:12Z
Alexandru Chirvasitu
arXiv categories: math.QA, math.CT, math.RA, math.RT

We prove that the cofree Hopf algebra on a cocommutative bialgebra is again cocommutative, and in fact coincides with the latter's largest Hopf subalgebra. This answers a question of Ardizzoni-Menini-Saracco and provides a proof for a statement to the same effect in the literature, whose original justification contains an apparent gap. The result relies on (and is in fact equivalent to) the observation that cocommutative bialgebra quotients of arbitrary Hopf algebras are automatically Hopf. This latter statement strengthens the analogue due to Newman, which assumes cocommutativity for the Hopf domain. One application of the above is the following quantum-rigidity result for Hopf algebras acted upon by a covariant quantum group: an action by one Hopf algebra on another which preserves the unital-algebra structure and the comultiplication factors through an action by a cocommutative Hopf algebra which moreover preserves the entire Hopf structure.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-25T15:16:30Z
Nikita Monchenko
arXiv categories: math.CT, math.RT

From the perspective of homological algebra, exact categories are interesting because they possess derived categories. Typically, an additive category admits many exact structures. If the original category is sufficiently nice (for example, quasi-abelian), a classification of exact structures can be given in terms of certain Serre subcategories in the category of contravariant functors. It turns out that the derived categories of different exact structures are functorially related. This work is concerned with sufficient conditions for the derived equivalence of different exact structures on certain categories.

arXiv abstract · PDF

Tensor Categories and Representation Theory · primary corpus · published 2026-10-25T17:42:16Z
Liangyu Zhu
arXiv categories: math.AG, math.AC, math.AT, math.CT, math.RT

Over a noetherian scheme, classical cohomological support determines thick tensor ideals of perfect complexes. In half-bounded derived categories, complexes with the same support can generate different radical thick tensor ideals. We study how these distinctions affect the Balmer spectrum and localization. For a commutative noetherian ring $R$, we prove that $\operatorname{Spc}(\mathbf D^-_{\mathrm{fg}}(R))$ is noetherian if and only if $R$ is artinian. For a nonempty noetherian scheme $X$, the corresponding condition is $\dim X=0$. For such a ring $R$ and a finite group $G$, $\operatorname{Spc}(\mathbf D^-_{\mathrm{fg}}(RG))$ is noetherian if and only if $R$ is artinian and $|G|$ is invertible in $R$. Using the Sanders--Zhang classification over a discrete valuation ring, we compare objects whose annihilator exponents grow at different rates in different degrees. We lift the relevant generation relations before changing coefficients and obtain spectral retractions. These comparisons persist after thick quotients and algebraic localization under explicit uniform annihilation and nonvanishing conditions. A second argument uses nonnilpotent classes of positive degree and passes from cyclic subgroups to finite groups. Applications include relative results for schemes and bounded-below spectra with degreewise finitely generated homotopy. We also describe the cohomological information shared by the resulting ideals. The localization comparisons for bounded-below complexes of finitely generated modules and for bounded-below derived objects with finitely generated cohomology are established separately.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-19T02:05:58Z
Oleg Grynets, Vasyl Lyashkevych, Andrii Salyk, Dmytro Koziuberda, Dmytro Kostetskyi, Oleh Kaskun, Olena Pochernina, Alona Seletska, Oleksii Ilchuk, Viktoriia Tsymbal, Daryna Tukalo, Bohdan Saukh, Ivan Fedorchuk, Hryhorii Petrenko
arXiv categories: cs.LO, cs.AI, cs.SE

Public leaderboards rank large language models (LLMs) in general, but an engineer has to choose a model for a specific application, architecture and cost. This paper presents a method for application-specific capability profiling of LLMs and its realization as a containerized testbed. The method treats each application as a unit of extension: an Oracle-to-PostgreSQL migration agent, a documentation-grounded chatbot or an enterprise-support automation agent runs in its own container behind a small contract, brings its own dataset, evaluator and owned attributes, and is onboarded together with its dashboards. Measurements accumulate in a versioned, sparse metamodel of every model. The method separates the model under test from judges and agents, freezes and hashes plans, refuses to compare values from different contexts, diagnoses the instrument before the system, and applies a null-agent check and a noise rule whose operating characteristics are quantified by simulation. In the evaluated automation conditions, model choices produced larger differences on selected observable outcomes than framework choices, although the experimental design does not establish a general causal ranking of these factors. The experiments also show that instruction tuning is deployment-specific and that system-reported success can exceed independently observed success: of 216 migration units checked against a real Oracle database, 108 were demonstrably correct. These measurements establish application-specific observations, not a universal model ranking.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-20T14:25:13Z
Azul Fatalini, Luke Serafin
arXiv categories: math.LO

In the context of intergenerational equity it is natural to ask that social welfare orders have th properties of finite anonymity and strong Pareto efficiency. Such social welfare orders can be constructed from nonprincipal ultrafilters over the set of natural numbers, and the existence of ultrafilters of this kind is known to be equivalent to the existence of a fair voting system for a countably infinite population in the sense of Arrow's theorem. Unfortunately, the existence of this variety of social welfare order, which we call anonymous Pareto, implies the existence of nonmeasurable sets of real numbers. For some, such as Litak, this entails that such social welfare orders are inadmissible for use in theoretical economics because they are non-constructive in nature. The authors seek to give nuance to this view, proving that anonymous Pareto and other social welfare orders can exist in the absence of nonprincipal ultrafilters over the set of natural numbers.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-20T18:27:38Z
Alexander Nadel, Yogev Shalmon, Ofer Strichman
arXiv categories: cs.LO, cs.DC

Constrained-random verification tests hardware designs by sampling solutions of Boolean formulas. Existing samplers largely follow one of two approaches: CPU-based SAT samplers (e.g., CMSGen), which remain effective even at rare targets but offer limited throughput, and GPU-based gradient samplers, which achieve high throughput at high-probability targets but collapse at rare ones. We introduce Gpap-S, the first GPU sampler built on Boolean constraint propagation (BCP). At its core is Gpap, a new GPU engine for BCP that efficiently propagates many independent partial assignments concurrently on a shared Boolean formula. This capability allows Gpap-S to combine the rare-target robustness of SAT-based sampling with the throughput of GPU parallelism by exploring thousands of decide-and-propagate trajectories simultaneously. On the benchmark families used to evaluate prior GPU gradient samplers, Gpap-S is 2.2-18.7x faster at the high-probability targets considered in those evaluations. At rare targets, where those samplers often fail to generate any samples, Gpap-S achieves a geometric-mean speedup of roughly two orders of magnitude. Across all benchmarks, Gpap-S is also 83.4-1,571x faster than the CPU-based CMSGen. This throughput does not come at the expense of sample quality: under Barbarik, the statistical tester used to evaluate CMSGen, Gpap-S is accepted on every instance we test, as is CMSGen. We release Gpap as a reusable GPU library for high-throughput BCP.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-20T22:09:44Z
Weizhe Xu, Jialiang Fan, Essien Taylor, Zijun Wang, Russell Joseph, Fanxin Kong
arXiv categories: cs.RO, cs.AI, cs.LO

Safe robotic task planning requires planners that can reliably achieve task goals while satisfying safety constraints. Classical planners search over explicit symbolic task representations and can provide formal guarantees with respect to encoded safety constraints, but require rigid input formats. Their computational cost also increases rapidly with the search space. In contrast, large language models (LLMs) offer flexible task interfaces and strong generalization capabilities, but they are large, power-hungry, and pre-trained with little robot-specific safety data and knowledge. Thus, they can be difficult to deploy locally on robotic systems with limited resources. To address these limitations, we present SLoSa, a neuro-symbolic compression and fine-tuning framework for training foundation-model-based robotic task planners with Small size, Low power demand, and Safety awareness. The framework first constructs a safety-aware dataset using classical planners, an advanced teacher LLM, and formal verifiers, followed by two training stages: supervised fine-tuning and reinforcement learning (RL) fine-tuning guided by a verification-based reward machine to enforce safety alignment. We evaluate SLoSa across four Planning Domain Definition Language (PDDL) domains, two household simulation environments, local edge platforms, and a desktop robotic arm. Across the PDDL tasks, verifier-guided post-training raises the success rate of compact 4B-14B planners to 70.5-76.0%, while INT4 deployment on a Jetson Orin requires 17.85-26.41 W of average power. Results in household simulators and on the physical robot further demonstrate the applicability of SLoSa across diverse robotic task settings.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-22T09:13:10Z
Kangming Lu, Qingguo Li, Shengwen Wang, Rongqi Xiao
arXiv categories: math.GN, cs.LO

In this paper, we introduce a new class of spaces, termed U_c-admitting spaces, and investigate their relationships with U_s-admitting spaces and well-filtered spaces. Adopting the perspective of H-sobriety, we show that every U_c-admitting space is H-sober, so that U_c-admitting spaces arise as a special case of H-sober spaces. Consequently, the category U_c-Sob of U_c-admitting spaces and continuous maps is complete and forms a reflective subcategory of Top_0. In addition, we prove that a T_0 space X is U_c-admitting if and only if its Smyth power space is U_c-admitting. Finally, we present the standard U_c-completion of an arbitrary T_0 space.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-23T20:08:04Z
Karan Yadav
arXiv categories: cs.CL, cs.CE, cs.LO

Content moderation compresses a graded, contested human judgment into a binary act (leave up / take down) over billions of items, at a scale where running a frontier LLM on every post is uneconomical. A new class of frozen "System One" models returns typed, calibrated decisions instead of text at ~USD 0.000025 per call and ~100 ms. We run the first independent audit of one such model on 142,658 human-labeled comments, and benchmark it against 14 frontier reasoning models (the GPT-5.x, Claude, Gemini 3, and Grok families) on a shared probe set. Two findings stand out. First, the cheap model is accuracy-competitive: its zero-shot classification AUROC (0.83) is not statistically separable (paired bootstrap, n=56; a failure to reject parity, not proof of equivalence) from 13 of the 14 frontier systems while costing 1-3 orders of magnitude less, and it is no worse calibrated than several of them. Second, "confidence" conflates two uncertainties that come apart: human disagreement (where annotators split on satire and coded language) and decision risk (where the automatic action is costly-wrong). Under an asymmetric moderation loss these call for opposite escalation signals, so no single confidence number serves both. Because the model prices extra questions at nearly zero, decomposing the judgment into parallel sub-questions and reading their spread recovers a human-disagreement signal that the model's native confidence misses -- but this remedy is specific: it helps the weakest, disagreement-blind models and only when the decomposition aligns with the sources of disagreement; a specialist toxicity model and the strongest LLMs do not need it, and the effect is distribution-sensitive. We will release the instrument, the cached runs, and the analysis.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-25T02:16:32Z
Chong Li, Ga\'etan Hains
arXiv categories: cs.DC, cs.PF, cs.PL

This paper introduces the Scatter-Gather parallel-programming and parallel-execution model in the form of a simple imperative Scatter-Gather Language (SGL). Its design is based on past experience with bulk-synchronous parallel (BSP) programming and BSP language design. SGL's novel features are motivated by the last decade's move towards multi-level and heterogeneous parallel architectures involving multi-core processors, graphics accelerators and hierarchical routing networks in the largest multiprocessing systems. The design of SGL is coherent with L. Valiant's Multi-BSP while offering a programming interface that is even simpler than the primitives of Bulk-Synchronous Parallel ML (BSML). SGL appears to cover a large subset of all BSP algorithms while avoiding complex message-passing programming. Like all BSP-inspired systems, it supports predictable, portable and scalable performance. Moreover, SGL's explicit data distribution will allow automatic or programmable load-balancing.

arXiv abstract · PDF