arXiv weekly literature review

Proof assistants and mechanized formalization · primary corpus · published 2026-07-28T12:10:26Z
Ibrahim Mian, Shayaan Siddique
arXiv categories: cs.LO, math.NT

The Erdős-Selfridge odd covering problem (Erdős problem #7) asks whether a covering system of $\mathbb{Z}$ exists whose moduli are all odd, distinct, and greater than 1. The problem is open. We present a Lean 4 formalization, checked end to end by the proof kernel, of the exclusion: any covering of $\mathbb{Z}$ by finitely many congruence classes with distinct odd moduli > 1 has lcm of the moduli exceeding 10000. The proof composes a formalized density argument (a covering by divisors of $N$ exceeding 1 forces $2N \le σ_1(N)$, so the lcm is abundant or perfect), a kernel-checked abundancy floor (no odd $N < 945$ qualifies), a family of Chinese-Remainder capacity certificates -- decidable per-$N$ arithmetic inequalities each refuting every covering with distinct moduli > 1 dividing that $N$ -- for all 23 odd abundant numbers below $10^4$, and a kernel-checked enumeration establishing that those 23 are the only odd non-deficient candidates. The result is transported to the official StrictCoveringSystem $\mathbb{Z}$ formulation of Erdős #7 in google-deepmind/formal-conjectures, with a bidirectional periodicity bridge between coverings of $\mathbb{Z}$ and finite checks over $\mathbb{Z}/N\mathbb{Z}$ suitable for consuming future SAT-style search output. All 63 published theorems depend on exactly propext, Classical.choice, and Quot.sound: no sorry, no native_decide, no solver in the trusted base. The mathematical content is known -- the density argument is folklore, and far larger uncertified classifications of covering numbers exist -- so the contribution is epistemic rather than mathematical: these exclusions are theorems of the Lean kernel, with an axiom gate enforced mechanically in continuous integration.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-28T20:10:41Z
Alain Chavarri Villarello, Sander R. Dahmen
arXiv categories: cs.LO, math.NT

Number fields, which generalize the rational numbers, are fundamental objects in number theory. Many of their key arithmetic properties are captured by invariants whose computation is among the central tasks of computational algebraic number theory and a focus of several computer algebra systems and databases. In this paper, we describe a Lean 4 formalization for certifying several of these number field invariants. Building on previous work on certifying rings of integers, we extend this certification approach to further invariants including the signature, the unit group modulo $p$-th powers, and, ultimately, the class group. We also improve discriminant certification, allowing verifications for higher-degree number fields infeasible in previous work. We introduce structures based on representations of algebraic objects suited to computation, including reusable ones for certifying ideal arithmetic. Along the way, we formalize several underlying mathematical results, for instance on real closed fields and pseudo-remainder sequences, which are of independent interest. We apply our framework to verify hundreds of entries of the $\textit{L-functions and modular forms database}$ (LMFDB) concerning the discriminant, signature, class number, and class group structure of various number fields. To this end, we wrote a SageMath script that computes the certificates and outputs Lean proofs of the corresponding statements.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-29T02:53:00Z
Shayaan Siddique, Ibrahim Mian
arXiv categories: cs.LO, quant-ph

The best known lower bound for the minimum Kochen-Specker vector system in $\mathbb{R}^3$ -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-30T16:21:58Z
Pablo Manrique, Stefan Szeider
arXiv categories: cs.AI, cs.LO

Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers. In this work, we introduce a framework that addresses both verification levels in the Lean theorem prover: it can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families; and to check solver-produced certificates for individual instances via translation backends to external formats such as MiniZinc, SMT-LIB, and OPB. Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver. Experimental results show that our framework's verified symmetry breaking also pays off in practice: a single parametric proof per problem family, reused across all instance sizes, reduces solver search effort by a factor of up to 2x10^7, while the entire in-Lean certification stays affordable, taking at most a few minutes for our largest instances.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-30T17:21:14Z
Gilles Barthe
arXiv categories: cs.CR, cs.LO, cs.PL

Proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support certification. This chapter focuses on their applications to system security, language-based security, secure compilation, and cryptography.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-29T16:15:08Z
Shuo Deng, Kenneth W. Shum
arXiv categories: cs.LO

As large language models become increasingly capable of generating mathematical arguments, mathematics is likely to face not a scarcity of proofs but an abundance of plausible ones. In such an environment, verification, exposition, and incorporation into reusable mathematical infrastructure become central tasks. We report on an ongoing Lean formalization of "Measure-Theoretic Probability: With Applications to Statistics, Finance, and Engineering", a fourteen-chapter upper-level undergraduate textbook covering topics from Riemann--Stieltjes integration to martingales and limit theorems. The project produces a machine-checked companion to the textbook and contributes reusable infrastructure for future formalizations involving probability theory. A Lean formalization provides computer-checked statements and proofs, makes hypotheses explicit, and allows readers to inspect the precise logical content of textbook results. A central challenge is to bridge textbook-facing statements with Mathlib's more general measure-theoretic interfaces. We reuse Mathlib results when possible and introduce reviewable interface lemmas when the textbook formulation and library abstraction differ. The project illustrates how formalized textbooks can support teaching, clarify mathematical assumptions, and help build the formal foundations needed for reliable AI-assisted mathematics.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-31T07:40:56Z
Damiano Testa
arXiv categories: math.GR, cs.LO

We define a non-unital, generally non-associative, commutative semiring structure on the collection of normal subgroups of a group $G$. This viewpoint allows us to recast in ring-theoretic terms Fitting's classical theorem that the join of two nilpotent normal subgroups is nilpotent. From this perspective, the two key inputs are a binomial expansion in a non-associative setting and the fact that the commutator subgroup of two normal subgroups lies in each factor. The development is formalized in Lean, making essential use of Mathlib for the core definitions and results.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-07-27T12:59:15Z
Julien Malka, Aman Sharma, Martin Monperrus, Stefano Zacchiroli, Théo Zimmermann
arXiv categories: cs.CR, cs.SE

Ken Thompson's trusting-trust attack, in which a compromised compiler backdoors the programs it builds and reproduces the backdoor in subsequent rebuilds of itself, is widely regarded as a threat specific to compilers. We show that it is not. We construct a complete trusting-trust attack around GNU strip, an ordinary build utility that neither inspects nor generates source code, using only manipulations of finished ELF files. In the bootstrap of the NixOS Linux distribution, a single tampered strip in the binary seed implants a payload that propagates from one generation of strip to the next and survives into the final standard environment after the seed leaves the dependency closure. On a real nixpkgs revision, the attack builds a complete graphical installer without failures and backdoors almost every one of its binaries, enabling arbitrary malicious behavior of the subverted packages.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-07-28T11:50:19Z
Rui Yang, Michael Fu, Kla Tantithamthavorn, Chetan Arora, Joey Chua
arXiv categories: cs.SE, cs.CR

Software engineering teams now deploy AI coding agents (Cursor, Claude Code, GitHub Copilot) as first-class productivity tools, installing domain-specific skill files to tailor agent behavior to project APIs, framework conventions, and organizational workflows. These complex Markdown files are easily downloaded from public registries with a single npx skills add command and no real security screening, representing a novel supply-chain attack surface: a malicious skill file can silently reprogram agent behavior, exfiltrating credentials, injecting backdoors into generated code, or redirecting agent actions to attacker-controlled endpoints. The threat is not hypothetical: recent reports document hundreds of malicious skill packages in public registries, including organized campaigns that distributed credential-stealing infostealers via fake productivity skills. No systematic toolchain defense exists for this attack surface. We present SkillGate, a deployable security gateway that screens AI skill packages before coding agent installation. SkillGate uses a hybrid regex-prefilter + LLM-judge pipeline: safe-signal files bypass the LLM entirely (skip savings); flagged files have only their matched snippet windows sent to the judge, not the full content (snippet savings). We answer four research questions covering detection effectiveness, screening cost, runtime overhead, and false positive behavior on the SkillsBench benchmark against two existing tools. On SkillsBench (n=1,650, 9.1% malicious), SkillGate achieves F1=0.817, FPR=1.13% while reducing LLM input tokens by 77% vs. full-file screening, and outperforming existing tools by 5-6x on threshold-independent AUPRC (0.830 vs. 0.144/0.162).

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-29T01:39:45Z
Hanrui Zuo, Peisen Yao, Kui Ren
arXiv categories: cs.PL

Synthesizing best inductive invariants (BII) is fundamental to program analysis and verification, yet existing approaches face significant efficiency challenges. We introduce a new formulation for the problem through the lens of mathematical optimization over quantified constraints in first-order theories. The formulation offers a constructive and operational perspective on the BII problem and opens new algorithmic avenues. Building on this formulation, we present two new algorithms for bit-vector programs: a strategically guided linear search that exploits the lattice structure and a bitwise greedy approach that resolves bound bits from high to low with a solver-call count linear in bit-width. We evaluate our approach on a comprehensive benchmark suite, demonstrating significant performance improvements over conventional methods based on symbolic abstraction and chaotic iteration. Experimental results demonstrate our approach solves up to 86\% more benchmarks than baseline methods, with improved scaling in solver-call count for high bit-widths and improved verification effectiveness when integrated with k-induction.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-29T22:29:27Z
Tobias Seufert, Christoph Scholl
arXiv categories: cs.LO

Verifying retiming followed by additional sequential resynthesis steps remains challenging for existing tools, limiting aggressive optimizations. Commonly-used equivalence checking tools rely on internal resynthesis operations and error-prone or- chestration of different model checkers, which makes certification difficult or even infeasible. We present an IC3-based technique that uses retiming as a preprocessing step and uses simulation to generate suspected invariants. Our technique efficiently verifies sequential equivalence problems under retiming and arbitrarily strong sequential resynthesis, and has the additional feature of producing certificates all the same. Our results on a selection of retimed and resynthesized open circuit designs show that our rather simple approach vastly outperforms the whole portfolio of the winner of the latest Hardware Model Checking Competition as a representative of general-purpose certifying model checkers. Compared to non- certifying approaches, like the mature equivalence checker of ABC, we are still competitive with additional complementary strengths.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-30T11:54:36Z
Lorenzo Ceragioli, Letterio Galletta, Edoardo Lunati
arXiv categories: cs.CR, cs.LO, cs.SE

Many cloud providers for IoT technologies offer access control mechanisms whose proper configuration is critical for security. However, verifying permissions in isolation is insufficient in a setting where devices have different levels of trust or are compartmentalised in various subsystems. This work analyses IoT access control policies to identify potential security vulnerabilities from unwanted information flow between devices. To this end, we formally model AWS IoT Core's components and define an information flow graph to capture the communication among devices permitted by the access control policies. We build a finite representation of the graph by leveraging an SMT solver, thus enabling the verification of information flow between devices. We implement our approach in a tool called IOT:POKER, and assess it on a realistic scenario and several real-world policies.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-30T17:11:14Z
Ye Ziyang, Makoto Ikeda
arXiv categories: cs.CR, cs.LO

This study presents a logic locking scheme based on the binary Ring Learning With Errors algorithm, implemented in a RISC-V System-on-Chip design. Unlike traditional logic locking methods that require providing users with raw locking parameters, the proposed approach secures critical logic paths in the privilege switching process without exposing these sensitive parameters. The implemented locking module itself consumes 3519 Look-Up Tables and 2645 Registers, leading to an overall overhead of 6.0% in Look-Up Tables and 6.9% in Registers compared to the baseline system. The unlock process requires about 2.6 us, introducing moderate performance impact, primarily affecting system-level operations while preserving user-level computational efficiency.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-31T02:16:55Z
Jiawei Ren, Guanqin Zhang, Zhenya Zhang, Yulei Sui
arXiv categories: cs.LG, cs.LO, cs.SE

Branch and Bound (BaB) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing BaB approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited BaB tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary's position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent BaB-based approaches.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-27T00:14:33Z
Cong Wang, Siyuan Sun, Yusheng Zheng
arXiv categories: cs.PL, cs.OS

eBPF lets developers extend Linux with custom packet processing, tracing, and scheduling logic, and a verifier proves before execution that the code will not crash the kernel. The programming model, however, is fragmented: a single application spans kernel code, a userspace loader, and shared maps, yet the relationships among these pieces go unchecked. E.g. A map or event type defined differently on each side silently corrupts shared state. We observe that these cross-boundary relationships duplicate information that a type system can unify. We present KernelScript, a DSL that types maps, program handles, and execution domains in one source, then compiles to standard C through the original toolchain. We evaluate KernelScript on 43 eBPF workloads covering XDP, TC, kprobe, tracepoint, and struct_ops. KernelScript rejects cross-boundary bugs at compile time that standard C/libbpf still builds and loads, a unified source shrinks the diffs for cross-boundary changes by 5x, and generated code remains compatible with the existing toolchain.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-27T14:36:56Z
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, Martin Odersky
arXiv categories: cs.PL

Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as "retaining only the control-flow capabilities of this closure" or "excluding all thread-local capabilities from this argument" become inexpressible. Both arise in the Scala 3 standard library: "Try" re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and "Future" must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion ("c.only[C]") and exclusion ("c.except[C]"). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-28T04:04:32Z
Wenhua Li, Darius Foo, Quang Trung Ta, Wei-Ngan Chin
arXiv categories: cs.PL

Type safety has traditionally rested on carefully crafted type systems, under the motto "well-typed programs cannot go wrong". Modern demands push type systems past this basic guarantee: toward memory safety (e.g., Rust), stronger data-structure invariants (e.g., GADTs), and broader typability (e.g., MLstruct). The motto absorbs each such property by enlarging the set of states deemed "wrong", but collapses them into one binary verdict: heap ownership, flow-sensitive changes to a variable's type, and the gap between a recoverable and a fatal error are relational, stateful facts about intermediate states that one verdict cannot tell apart. Worse, each demand typically brings its own extension, making it hard to say what each guarantees or how they combine. Floyd-Hoare logic supplies a unified foundation. We present a framework for type-safety verification built from four ingredients: (i) case specifications for path-sensitive typing; (ii) separation types, inspired by separation logic, for flow-sensitive type mutation and must-aliasing; (iii) a disciplined distinction between Err (runtime error values our types track) and Abrt (compile-time errors), yielding the refined motto well-typed programs must never abort; and (iv) type predicates for data-structure invariants. Since all four are ordinary types in one Boolean algebra rather than separate extensions, the framework subsumes both GADTs and liquid types within one type logic, spanning weak specifications that tolerate Err to strong ones that eliminate it. Subtyping reduces to one decidable emptiness test, so a single lightweight procedure serves the whole framework with no SMT oracle in its trusted base. We formalise the Hoare rules and prove soundness in a machine-checked Lean mechanisation; by proof reflection it yields a self-certifying type-checker, evaluated on a benchmark suite.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-29T15:59:21Z
June Wunder, Ankush Das, Marco Gaboardi
arXiv categories: cs.PL, cs.SE

Reactive programming frameworks such as React allow developers to build interactive applications by declaratively specifying how outputs depend on changing inputs. Although this model makes it easy to reason about what an application computes, the temporal behavior of reactive programs remains difficult to understand and verify. Applications implicitly rely on timing assumptions buried in framework runtimes, leading to subtle bugs such as stale reads, transient inconsistencies, order-dependent behavior, and unintended feedback cycles. To address these challenges, this paper presents Willow, a core calculus for reactive programming inspired by React. Willow gives a time-aware operational semantics that models computation in terms of renders, the fundamental evaluation step in which components produce user interface descriptions, and pairs it with a novel type-and-effect system that statically tracks timing behavior as effects. A "next" modality expresses delays measured not only in renders but in any unit the host environment exposes--renders, network requests, or milliseconds. A family of modalities tracks the lifecycle of event handlers: when they are registered, when they fire, when pending events are canceled and when handlers are removed. A key insight is that the resulting effects form a temporal dependency graph, letting standard graph algorithms statically detect render cascades and inter-render loops that cause non-termination or performance degradation. We formalize Willow and prove preservation of the effect system with respect to the time-aware semantics. We also implement a prototype checker with automatic effect inference and evaluate it on representative reactive patterns such as debouncing, form inputs, and API-driven updates. Our results demonstrate that time-aware typing provides a practical foundation for reasoning about the temporal correctness of reactive programs.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-29T18:48:13Z
Nicolai Kraus
arXiv categories: cs.LO, math.AT, math.CT, math.LO

Extension types are a concept in dependent type theory that has appeared in various contexts. The idea is to have types whose terms are partially determined, e.g. via a strict boundary condition. Standard examples are path types of cubical type theories (paths with fixed endpoints), Riehl and Shulman's name-giving extension types (terms fixed on subshapes), as well as the controlled-unfolding mechanism of cooltt and Agda (terms that are fixed if a condition is met). In each case, the type theory is equipped with a (meta-theoretic) face calculus, or shape layer, that governs their rules, and comes with intended semantics. We unify all these occurrences in a single framework where no new axioms or model constructions are needed, namely two-level type theory. This step, too, is free (semantically): the standard models of HoTT are automatically models of 2LTT, and the theory is conservative over HoTT. Extension types are definable, and the definition validates Riehl and Shulman's entire extension-type calculus: the rules hold strictly, and the postulated axioms, such as relative function extensionality, become theorems. In this way, every model of the base theory (HoTT) gives rise to a model of the same theory with extension types; the only genuine assumptions are which maps count as cofibrations. Conservativity makes the framework a tool for comparing type theories. We prove that cubical gluing, in a suitable formulation, is equivalent to univalence. On this basis, we suggest an approach toward the conjecture that cubical type theories are conservative over book HoTT, one of the central open problems of homotopy type theory. All results of the main body of the paper are auto-formalized in Agda --two-level, in a development that combines HoTT-internal arguments with reasoning that is external to HoTT.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-27T03:42:34Z
Zhenghong Yu, Hangdong Zhao, Wanzhu Hou, Paraschos Koutris
arXiv categories: cs.PL, cs.LO, cs.SE

Datalog is widely used to build static analyzers, yet existing engines often force a tradeoff between efficiency and extensibility. In practice, static analyses are not run once and forgotten: users edit facts, tune rules, diagnose bottlenecks, and often need semantics beyond standard Datalog, leaving these tasks to ad hoc tooling or invasive engine rewrites. We demonstrate FlowLog, a Datalog compiler that turns Soufflé-style programs into Differential Dataflow executables for efficient and extensible static analysis. Across 24 benchmarks derived from real-world workloads, FlowLog consistently outperforms state-of-the-art engines in runtime while remaining memory-efficient and scaling better. The demonstration walks attendees through a DOOP points-to analysis. Attendees run it, switching the same program from one-shot to incremental evaluation that retracts a fact and updates results in milliseconds; tune it, inspecting per-operator costs in a browser-based profiler and repairing a bad join order; and extend it with a k-core example that uses semantics beyond Datalog.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-27T17:20:23Z
Dmitri Volkov, Yafei Yang, Chung-Chieh Shan
arXiv categories: cs.PL

We present a new approach for implementing polymorphism for bottom-up relational languages that avoids monomorphization. We begin by introducing semiringKanren, a bottom-up weighted relational programming language. We extend this base language to support polymorphism. We describe a new method to compile polymorphic semiringKanren programs into non-polymorphic ones, based on equality patterns and large-enough instances of polymorphic relations. We explain the correctness of this method. Finally, we consider existing work and suggest directions for future research.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-27T23:22:44Z
Oleg Grynets, Kyrylo Fursov, Vasyl Lyashkevych, Volodymyr Veres
arXiv categories: cs.SE, cs.LO, eess.SY

Large Language Models (LLMs) are increasingly used to generate executable software environments from repository artifacts. However, functional executability does not necessarily imply conformity with architectural, security, workflow, and production intent. This study investigates whether a frontier LLM can generate Dockerfiles and Docker Compose configurations for multi-service applications using repository contents without access to developer-authored deployment artifacts. Three heterogeneous repositories combining Python, Node.js, .NET, React, Rust, Java, Redis, PostgreSQL, and MySQL-compatible infrastructure were evaluated using deterministic end-to-end HTTP oracles and manual structural comparison. All three generated environments became functionally operational, although one required a Rust base-image update from version 1.85 to 1.88. The model correctly reconstructed service topology, application ports, infrastructure dependencies, service hostnames, a background worker, hidden proxy configurations, and a file-based Docker secrets mechanism. However, it consistently omitted network segmentation, multi-stage builds, dependency-layer caching, live-reload volumes, production frontend serving, restrictive backend-port policies, and cross-platform build logic. Based on these observations, the study formalizes the distinction between functional correctness and deployment-intent fidelity and analytically derives a minimal explicit deployment specification for information that cannot be reliably inferred from repository artifacts.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-28T07:28:51Z
Nikolai Kudasov
arXiv categories: cs.PL, cs.LO

We present two small library combinators on top of plain miniKanren, designed to bring bottom-up enumeration with observational deduplication, the standard tool in non-relational program-by-example (PBE) synthesizers, into the relational setting. The first combinator, prune, deduplicates an answer stream by a user-supplied key, typically the input/output behavior of the candidate. The second, defrel/bank, memoizes a relation against canonical fresh variables so that a single pruned answer stream is built bottom-up and replayed at every call site. We also discuss a weighted variant, defrel/bank-w, which attaches admissible upper bounds to immature streams to recover best-first enumeration in cases where the natural depth-first canonical order misses compact representatives. On a preliminary PBE benchmark of arithmetic and string synthesis targets, defrel/bank substantially outperforms the depth-bounded baseline on most deep targets, while losing on a small family where the canonical depth-first enumeration order misses compact representatives. We leave a broader empirical evaluation to an extended version of this paper.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-28T12:38:50Z
Xinyi Yuan, Wei Chen, Jinyi Liu, Pengyu Chen, Jun Wei, Guoquan Wu, Jiaxin Zhu, Tao Huang
arXiv categories: cs.PL, cs.SE

Deep learning compilers (DLCs) are designed to translate deep learning programs into optimized, hardware-specific code. Typically, DLC frontends translate programs into graph-based intermediate representations (IRs) to enable optimizations. Defects introduced during this stage (termed \emph{fBug}s) are severe yet understudied, as prior work predominantly focuses on low-level APIs and operators or treats DLCs as monolithic entities. To bridge this gap, we conduct the first systematic empirical study of \emph{fBug}s in TorchDynamo, the default DLC frontend for PyTorch 2, the most popular DL framework. Leveraging a domain-knowledge-enhanced LLM-aided methodology, we analyze 123 \emph{fBug}s and construct a taxonomy comprising 7 root cause categories and 15 subcategories. Our findings provide actionable insights for DLC development and testing. Furthermore, we leverage the LLM to generate targeted, root cause-aware test cases to detect new bugs. We uncovered 23 previously unknown \emph{fBug}s in recent releases (15 confirmed) across eight (sub)categories, demonstrating the efficacy of our methodology in testing and hardening DLC frontends.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-28T19:12:43Z
Daniel Pang, Stephen M. Watt
arXiv categories: cs.PL, cs.MS, cs.SE

The original SciGMark benchmark adapted the SciMark numerical suite to measure the cost of generic programming in scientific computing. In the twenty years since, generics have become ordinary features of mainstream languages, but their implementation strategies have diversified. This paper reports SciGMark 1.5, a benchmark study of specialized and generic implementations in modern languages. The study has three aims. First, it examines the consequences of the wide variety of generic-realization strategies used in current widely used languages. Second, it extends the benchmark toward symbolic computation by adding finite-field linear algebra, finite-field FFT, and a naïve Gröbner basis computation. Third, it asks how the original floating-point scientific kernels behave in the new language settings. The measurements cover Rust, Java, Go, and TypeScript for the main suite, with additional C++ and Julia measurements for the Gröbner basis benchmark. The study also records representative output artifact sizes, since code generation and runtime packaging are part of the cost model of generic programming. The results confirm that the cost of generic programming is not inherent in abstraction itself, but depends strongly on when type information is resolved, how arithmetic values are represented, and whether the compiler or runtime can recover specific operations in the inner loops. Ahead-of-time monomorphization usually makes generic code close to specialized code in the numerical tests. Erased or objectbased generic arithmetic can introduce substantial overhead, especially in arithmetic- and allocation-intensive code. Runtime specialization occupies an intermediate position, offering flexibility and good steady-state performance when type inference and representation choices are favourable.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-29T11:18:30Z
Hailong Jiang, Emran Hossain, Feng Yu, Chunwei Xia, Mengfei Ren, Jianfeng Zhu, Qiang Guan
arXiv categories: cs.PL

Formalizing compiler-aware numerical correctness requires distinguishing what an observed floating-point difference means, what compiler behavior the evidence supports, and what numerical consequence follows. Existing testing workflows often collapse these questions into a pass/fail mismatch. We introduce Baseline--Mechanism--Outcome Attribution (BMOA), a diagnostic framework that separates the comparison relation and system boundary, the evidence-supported compiler mechanism, and the reference-qualified accuracy outcome. BMOA combines operational strict floating-point, transformation-local, reproducibility, cross-compiler, and higher-precision comparisons, while preserving mixed, ambiguous, and unknown attributions when evidence is insufficient. Each record retains inputs, configurations, numerical metrics, and supporting artifacts for audit. We evaluate BMOA on six scientific-computing kernels, deterministic stress-input families, and controlled Clang configurations on ARM64. A 1,276-record attribution corpus and a 162-instance controlled mechanism matrix show that baseline choice changes diagnoses, compiler-induced deviation does not imply accuracy loss, and cancellation and large dynamic range expose the strongest effects within the targeted matrix. BMOA converts raw mismatches into explicit, auditable, evidence-bounded records. Although it is not itself a proof system, these records provide an empirical foundation for future formal specifications and proof obligations for compiler-aware numerical correctness.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-30T23:37:20Z
Cosmin E. Oancea, Stephen M. Watt
arXiv categories: cs.SC, cs.DC, cs.PL

We report on GPU implementations of block-level addition, subtraction, multiplication and division for midsize integers, with operands of $2^{15}$ to $2^{19}$ bits using the high-level functional language Futhark. Comparing with hand-written C++/CUDA versions and CGBN, we identify which functional constructs compile well, where memory placement and sequentialization are effective, and what compiler support is needed. The results show that high-level code can express the algorithms compactly while approaching competitive performance after certain compiler improvements. In particular, we find that automated placement of arrays in GPU register memory is critical for performance.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-27T10:15:36Z
Chandan Kumar Sah, Li Zhang, Xiaoli Lian
arXiv categories: cs.SE, cs.AI, cs.CL, cs.LG

Repository-level code generation relies on heterogeneous evidence whose relevance, compatibility, and completeness are inherently uncertain. Similar-code examples, repository context, and project-specific APIs may provide complementary information, but can also introduce noisy, redundant, or conflicting signals. Existing retrieval-augmented approaches primarily optimize retrieval relevance without explicitly modeling how uncertainty in retrieved evidence affects downstream generation. We introduce OpenCoder, an uncertainty-aware framework that estimates source-specific uncertainty, uses it to filter and rank heterogeneous evidence, and guides generation, verification, and repair. A factorial analysis over API knowledge, repository context, and similar-code evidence reveals no universal additive source ranking; instead, significant cross-source interactions depend on the accompanying evidence and LLM backend. On an expanded 32-task RepoExec-inline evaluation, OpenCoder improves GPT selected-output correctness over Baseline RAG from 56.25\% to 78.13\%. However, it matches a verification-and-repair control, and the corresponding Gemini improvement is not statistically supported, indicating backend-dependent benefits. Target-aware API refinement also substantially improves API-set retrieval. These findings support treating uncertainty as an actionable control signal for repository-level retrieval, verification, and repair.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-27T15:46:57Z
Zhibin Kang, Hanmo You, Dong Wang, Haiming Zheng, Junjie Chen
arXiv categories: cs.LG, cs.SE

Reinforcement Learning (RL) agents are increasingly deployed in safety-critical domains such as robotics, autonomous driving, and drone control, where unexpected behaviors may lead to severe real-world consequences. Fuzz testing has recently emerged as a promising method for exploring the vast state spaces of RL agents and exposing crashes. Although numerous RL fuzzing methods have been proposed, existing studies often differ in evaluation settings, baselines, and metrics, making it difficult to draw reliable conclusions about their relative effectiveness and practical usefulness. To address this gap, we present the first comprehensive empirical study that systematically evaluates RL fuzzing methods from four complementary perspectives: effectiveness, diversity, efficiency, and practical utility. We benchmark five state-of-the-art methods alongside random testing under unified configurations across three environments of increasing complexity (MountainCar, BipedalWalker, and CARLA), and further assess the downstream usefulness of detected crashes for agent robustness improvement and safety monitoring. Our results reveal several key insights. For instance,throughput-oriented methods like MDPFuzz demonstrate superior effectiveness and efficiency in crash discovery, while methods explicitly designed to encourage exploration like SeqDivFuzz excel at uncovering diverse crash behaviors. We also show that fuzzing-generated crashes can meaningfully improve agent robustness and enable accurate safety monitoring with strong cross-method generalization. Beyond these empirical findings, we distill actionable guidance for both researchers and practitioners, highlighting the benefits of combining complementary fuzzing strategies and adopting multi-level diversity analysis to achieve more comprehensive and practical RL testing.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-27T19:30:56Z
Ishrat Jahan Eliza, Md Dilshadur Rahman
arXiv categories: cs.AI, cs.HC, cs.MA, cs.SE

Multimodal large language models (MLLMs) can connect visualization patterns to external causes, consequences, and domain knowledge, but the evidential basis of these interpretations is often unclear. We present an exploratory study of 102 visualizations from four sources, three MLLMs, and four input conditions that vary access to the image, source-specific accessible chart context, and withheld-context framing. Across 1,224 descriptions, we analyze model-attributed DIRECT, DERIVED, and SPECULATIVE labels and conduct an automated audit of numeric agreement. Accessible chart context shifted Gemini and GPT toward DIRECT claims and improved numeric agreement for some models. Adding the image to the full context did not yield a consistent numeric benefit, and the withheld-context prompt did not reliably increase cautious language. The prompt-defined Real-World Significance section remained predominantly SPECULATIVE. These results motivate accessible description systems that distinguish claims supported by supplied evidence from model-supplied interpretation

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-28T06:33:15Z
Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, Tianyin Xu
arXiv categories: cs.SE, cs.AI, cs.DC, cs.OS

Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-28T07:16:12Z
Genliang Zhu, Chu Wang
arXiv categories: cs.AI, cs.SE

Tool-using agents expose structured calls but commonly attach free-form rationales. Such rationales are neither authorization nor reliable introspection. We present Explanation-Bound Tool Execution (EBTE), a claim-carrying mediation layer that converts decision-relevant rationale content into typed action claims and checks them against server-held intent, policy, payload, tool, risk, provenance, and freshness facts. EBTE cannot widen baseline authority: conflicts deny, incomplete or uncertain claims review, and only matching claims remain eligible for governed execution. We formalize this composition under explicit mediation and trusted-fact assumptions and implement a versioned reference profile with minimized audit packets. Across 136 authored conformance scenarios, the full profile matches all specified dispositions, admits none of 96 designated hard contradictions, and passes 232 metamorphic checks. A draft-only reference integration forwards none of 48 authored hard cases under EBTE while preserving all 16 soft-review and 4 aligned draft paths. In a frozen 2026-07-12 exploratory 224-attempt hosted-model record, the historical generation/runner agreement counts are 71/96, 66/96, and 19/32; a zero-call revalidation of the preserved minimized claims under the current pipeline yields 70/96, 65/96, and 17/32. In an AgentDojo-derived semantic check, existing high-risk controls make all 12 attack proposals non-allow, while EBTE resolves the task--proposal contradictions as deny. Together, these studies establish profile conformance and demonstrate the feasibility of server-checked action claims within the evaluated settings.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-28T10:54:28Z
Chiraag Singh Anand, Xue Wen Tan, Lionel Teo, Eric Tan
arXiv categories: cs.MA, cs.CE, cs.SE

Verifying building compliance requires validating thousands of rules against large Building Information Modeling (BIM) designs, which is laborious, capital-intensive, and unscalable. Existing Automated Compliance Checkers (ACCs) are often difficult to generalize across different scenarios, as they are typically developed for highly specific rule sets and use cases. In addition, many ACCs are proprietary, meaning the underlying verification code is not released to end users, so users cannot verify whether their regulatory intent can be accurately captured. We introduce ARCHER (Agentic Rule and Compliance Harness for Executable Regulations), a test-driven, deterministically orchestrated multi-agent program-synthesis harness that generates auditable verification code from regulatory Codes of Practice, enabling transparent, adaptable, and scalable compliance checking. To characterize what makes agentic synthesis work, we evaluate a taxonomy of six harnesses of increasing agentic sophistication across four backbone models, spanning realistic data-governance tiers (from frontier third-party APIs to a fully on-premise open-weights model) on a novel dataset derived from real-world compliance scenarios. ARCHER's deterministic multi-agent orchestration achieves the highest accuracy for every backbone, improving mean union accuracy by 82% over a naive single-pass prompting baseline. Our cost-accuracy analysis further shows that using the ARCHER harness, a self-hosted open-weights model can reach 97.8% of frontier-API accuracy at a quarter of the cost, making data-sovereign compliance checking practical.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-28T12:31:34Z
Fuyuan Xia, Qixin Zhang, Chenhao Ying, Haojin Zhu, Shuai Wang, Yuan Luo, Pingchuan Ma, Yuxuan Du
arXiv categories: cs.SE, cs.AI, cs.MA, quant-ph

As quantum computing continually improves, ensuring the reliability and correctness of quantum libraries has become increasingly critical. To this end, many LLM-based fuzzing approaches towards quantum libraries have been proposed to uncover potential bugs. However, these methods still suffer from limitations such as insufficient flexibility and low efficiency, which hinder the progress of the quantum computing field. To address these challenges, we propose KQFuzz, a novel knowledge-guided fuzzer for quantum libraries. It leverages comprehensive codebase knowledge to ground LLM-based test generation, synergizing this with fitness-guided evaluation and two-level mutations to explore complex execution paths and trigger potential bugs. Firstly, KQFuzz introduces a novel prompting scheme tailored to quantum programs, which strategically incorporates knowledge of the codebase to efficiently generate high-quality quantum seed programs. Moreover, we develop evaluation and mutation strategies to handle the generated seed programs, facilitating efficient fuzzing execution while further enriching the diversity of the resulting test cases. We implement KQFuzz and conduct fuzzing on three popular quantum libraries, including Qiskit, PennyLane, and Cirq. Experimental results demonstrate that our approach significantly outperforms other state-of-the-art methods, with coverage improved by up to 18.44%. During the development of KQFuzz, we discovered 13 bugs, all of which have been confirmed and 12 have already been fixed by the developers.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-07-28T15:05:50Z
Thierry Lecomte, Vincent Germain
arXiv categories: cs.SE

Can large language models participate in the production and validation of ERTMS/ETCS data without undermining the certification arguments required by CENELEC EN 50128/50716? ERTMS/ETCS is a distributed safety-critical system (trackside, onboard, radio-block centre) whose behaviour is parameterised by large volumes of data drawn from the UNISIG Subsets; errors in that data propagate through the distributed architecture. This paper reports the current status of an ongoing industrial research effort at CLEARSY, ValidAItion, that bridges the ERTMS Operational Simulator to the CLEARSY Data Solver and applies rules expressed in the B mathematical language to that trackside data. During construction, a large language model (Claude) has authored the rule corpus and the parsers through a Model Context Protocol server; every proposal is adjudicated by the downstream toolchain and by systematic human review, and the toolchain has already rejected a syntactically valid but semantically illegal generated scenario. The contribution is architectural and industrial, not algorithmic: the work combines frameworks already in use at CLEARSY (CLEARSY Data Solver, ERTMS Operational Simulator) with a conversational authoring loop, rather than proposing a new formal method. It is a progress report: rule coverage is growing, the human-review campaign is underway, and the quantitative results will be published separately. The paper argues, on the evidence gathered so far, that formal rules in the mathematical language of B must remain the source of truth, while the language model serves as the fenced assistant in a distributed safety-critical railway system: AI proposes, the formal oracle disposes, the human confirms.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-28T22:00:02Z
Lefteris Lazaropoulos, Zoe Paraskevopoulou
arXiv categories: cs.PL

Relating low-level executable code to a high-level account of its behavior has been a central concern of programming-language research for decades. From formally verified compilers to translation validators, certifying compilers, and proof-carrying code, each approach chooses between laborious but foundational mechanized proofs and automation that costs completeness, generality, and an increased trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs at a scale and speed that were previously out of reach. In this paper, we evaluate the capabilities of LLMs to produce foundational, machine-checked proofs of refinement between executable code and its high-level specification, as post hoc, per-artifact certificates. We study this in the context of the Ethereum Virtual Machine (EVM), a low-level virtual machine that executes smart contracts on the Ethereum blockchain. We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a specification language that characterizes the intended behavior of smart contracts, but commits to no source language or compilation toolchain. In EquiVM, refinement is stated for deployed bytecode of arbitrary provenance, interaction with unknown code is part of the semantics, and each proof is a replayable, machine-checked certificate. No previous technique achieves this combination. Using frontier commercial LLMs, twenty-three real-world contracts are proved end to end with minimal human guidance, among them most of the MakerDAO stablecoin system, at up to a hundred million tokens and a hundred hours of proof time per contract. We conclude that foundational mechanized proofs can now be bought at the price of tokens, and that this shift can reshape how verification frameworks are architected.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-29T03:25:07Z
Ziyi Yang, Wenji Fang, Chen Chen, Zhiyao Xie, Hongce Zhang
arXiv categories: cs.LO, cs.AR

Modern integrated circuits (ICs) are becoming increasingly complex, making functional verification a major bottleneck. The dominant hardware formal verification methodology, model checking, verifies each design instance separately and exposes only pass/fail results, so the reasoning behind a proof stays locked inside solver heuristics and is repeatedly reconstructed across related designs. Interactive theorem proving instead yields explicit, reusable proof artifacts, but applying it to hardware remains largely manual, demanding expert effort for formalization, invariant discovery, and proof development. In this paper, we present CircuitProver, an agentic Lean 4-based verification framework supporting proof-accumulation and parameterized verification. CircuitProver automatically translates parameterized hardware designs and their natural language specifications into executable Lean 4 models. It then iteratively constructs machine-checked proofs through Lean feedback to establish that the hardware code complies with the specification. The proving traces and verified theorems are distilled into reusable libraries, where proving strategies guide future agent reasoning and verified lemmas support formal proof reuse across related hardware verification tasks. We further introduce the first benchmark suite for evaluating agentic hardware theorem proving, covering diverse parameterized hardware designs, specifications, proof tasks, and evaluation metrics. Across 63 tasks, CircuitProver successfully proves all benchmarks, while a vanilla agent solves 92.1% of them and requires twice as many proof rounds on average. Ablation studies show that accumulated proof knowledge reduces redundant proof construction across related verification tasks, reducing proof length by 16.3% and verification time by 23.2%.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-30T21:00:27Z
Vasily A. Sartakov
arXiv categories: cs.SE, cs.OS, cs.PL

C underpins operating systems, embedded platforms, and network infrastructure because its abstractions map directly to machine behaviour. Its explicit memory model, predictable data representations, and minimal runtime allow compilers to generate fast, deterministic code. These properties also leave correctness and memory safety entirely to the programmer, making undefined behaviour, pointer misuse, and lifetime errors persistent sources of defects and security vulnerabilities in long-lived C codebases. Rust eliminates most of failure modes through a static ownership and borrowing model that enforces memory safety and aliasing constraints at compile time. However, mature C systems cannot be translated directly: implicit layout assumptions, aliasing patterns, and undefined behaviour must be reconstructed before safe Rust can be produced. This paper presents a migration methodology that first generates a semantics-preserving, non-idiomatic Rust baseline and then incrementally rewrites it into idiomatic Rust using agentic AI, validating each step through compilation and behavioural testing. Applied to iodine (12.5k SLOC), the approach demonstrates that reliable C-to-Rust migration is a structured transformation workflow rather than a single translation step.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-27T00:36:51Z
Eridan Domoratskiy, Dmitry Boulytchev
arXiv categories: cs.LO, cs.PL

We present an efficient algorithm for rational term unification in persistent settings which demonstrates a comparable performance w.r.t. the conventional miniKanren unification with triangular substitution for Herbrand terms. Our algorithm is based on existing Martelli-Rossi approach and uses some adjustments to make the implementation more conventional. We provide certified proofs of principal algorithm properties in the Rocq proof assistant and showcase the results of a comprehensive performance evaluation.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-28T14:43:55Z
René Thiemann
arXiv categories: cs.LO, cs.SC

Automatic deduction tools such as automatic theorem provers, SAT (satisfiability) solvers, SMT (satisfiability modulo theories) solvers, and termination analyzers can be connected to proof assistants using various approaches, notably by certification and verification. This chapter reviews and compares the approaches available, and mentions several successful applications.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-29T14:44:46Z
Amir Hossein Sharafi, Alireza Shahbazi
arXiv categories: cs.AI, cs.LO

Reasoning and planning over Dynamic Knowledge Graphs (DKGs) present significant challenges, especially in open-world environments with incomplete information. Existing action formalisms often face decidability issues and the Ramification Problem, while managing incomplete knowledge via structural abduction requires expansive combinatorial search. This paper introduces a unified framework with two integrated modules---\textbf{PIE-Abducer} (incremental direct-derivation abduction) and \textbf{PIE-APT} (Abductive Planning for Temporal KGs)---operating natively on the highly expressive Description Logic. We model state transitions along a linear timeline as non-monotonic updates to deductively closed DL theories. Treating the incremental reasoner as a black-box and representing actions natively in OWL without external modal operators preserves logical decidability. To address incomplete knowledge, \textbf{PIE-Abducer} circumvents traditional Minimal Hitting Set (MHS) enumeration. Instead of combinatorial syntactic search, it injects the logical negation of a target goal into a consistent branch and extracts missing premises via direct refutation consequences. \textbf{PIE-APT} then employs a recursive \textit{Generate-and-Test} architecture, interleaving backward-chaining A* search with \textbf{PIE-Abducer} up to a bounded causal depth, followed by strict validation via forward-chaining Temporal Projection. We evaluate four OWL benchmarks stressing semantic abilities absent in classical planning: parameterized goals with witness search, mid-search DL entailment, open-world assumption injection, and adversarial contradiction hunting. Results demonstrate qualitative superiority over classical planners and prove our direct-derivation approach quantitatively outperforms an MHS-faithful baseline during abductive enrichment.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-29T20:10:56Z
Stephan Schulz
arXiv categories: cs.LO, cs.SC

In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational definitions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms that shows very promising results.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-30T09:45:22Z
Bente Gortworst, Cem Okulmus, Magdalena Ortiz, Anni-Yasmin Turhan
arXiv categories: cs.AI, cs.LO

SHACL shapes enable data graph validation, making automatic shape learning essential for knowledge graph applications. We investigate the well-known fitting approach to this task: given sets P and N of positive and negative example nodes from an input graph, compute a shape expression C, possibly using shape names defined in a recursive shape catalogue, that validates at every node in P and none in N. We focus on the case where C is written in a core fragment of SHACL corresponding to the Description Logic ELI. For the catalogue, we consider the well-founded, stable, and supported semantics. We address fitting existence and most specific fitting computation, establish tight exponential-time upper bounds for both problems, and obtain polynomial bounds for relevant special cases.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-30T19:05:24Z
Nils Küchenmeister, Alex Ivliev, Dörthe Arndt, Markus Krötzsch
arXiv categories: cs.LO, cs.AI, cs.DB

Combining RDF rule languages, such as N3 or SHACL Rules, with default negation is challenging. Existing methods to stratify negation often fail for RDF rules, since individual triples do not carry enough information to meaningfully restrict potential dependencies. Blank nodes in rule heads further complicate the matter, since the order of rule applications may determine whether new values are created, which in turn can change the applicability of rules with negation. To solve these open problems, we propose chain stratification as a robust new condition that guarantees a well-behaved semantics for RDF rules with negation, and existential rules in general. Our condition combines an elaborate analysis of potential multistep derivations with a mechanism for using integrity constraints to discard impossible cases. Applying rules in any order that respects chain stratification is guaranteed to derive an RDF graph that is unique, lean, and justified under the usual negation-as-failure semantics. To show the practicality, we also provide a prototype implementation.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-31T06:10:12Z
Liam Davis, Haoze Wu
arXiv categories: cs.LG, cs.AI, cs.LO

State-of-the-art neural network verifiers use the branch-and-bound procedure as their core solving mechanism. We introduce an inprocessing framework for neural network verification driven by the lookahead procedure. Under this framework, lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts. We instantiate the framework in two state-of-the-art verifiers, Marabou and $α$-$β$-CROWN, and demonstrate that it improves performance in both, proving up to 34% more instances unsatisfiable.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-31T11:09:22Z
Nick Palladinos
arXiv categories: cs.SC, cs.LO

The matrix-multiplication SAT benchmark of Heule, Kauers, and Seidl asks, among other tasks, for solutions of ten known-satisfiable rank-23 formulas, proofs of unsatisfiability for ten formulas expected to be unsatisfiable, and a rank-23 scheme over $\mathbb{F}_2$ having a summand with no type-3 monomial. We give complete satisfying assignments for the 21 CNFs in the repository's top-level challenge1/, challenge2/, and challenge3/ directories at commit 150b2e2f. The principal finding is that all ten top-level Challenge-2 formulas are satisfiable. A direct audit shows that their hardcoded type-3 pairings are imposed by positive unit clauses on the 621 base variables: the formulas require selected incidences but do not forbid additional type-3 incidences. Starting from exact 23-summand schemes, we use the $\mathrm{GL}(3,2)^3$ isotropy action, cyclic trace symmetry, and perfect matching of transformed summands to constrained slots to construct witnesses for all ten files. For Challenge 3, we combine a locked semantic repair with a two-term identity over $\mathbb{F}_2$ to obtain a distinguished summand of type-3 count zero. Every semantic decomposition has zero residual in all 729 Brent equations. The accompanying DIMACS models assign all 26,541 variables of each formula and satisfy all 2,461,316 clauses across the 21 instances. A separate parser and clause evaluator rechecks the emitted models. A deterministic one-file Python reproducer regenerates the 21 certificates from the original CNFs in approximately nine seconds on the reported test host.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-27T11:19:52Z
Oluwadara Adedeji, Michael Mayowa Farayola, Jeff Brozena, Irina Tal, Regina Connolly, Mark Matthews
arXiv categories: cs.LO, cs.AI, cs.CY

Ethical governance of AI-driven systems is often expressed through high-level principles and static documentation, creating a gap between regulatory requirements and system-level verification. This challenge is particularly acute in digital phenotyping, where continuous behavioural data raises concerns around consent, privacy, and fairness. In this paper, we propose a computational ethical framework for AI-driven digital phenotyping system in which ethical requirements are formalised as deontic temporal logic constraints, alongside a conceptual ethical agent that oversees the system and ensures that any supervised system satisfies the specified constraints. Using a case study involving financial data and mental health, we model key ethical properties and verify them using the Z3 Satisfiability Modulo Theories (SMT) solver. Our evaluation shows that the framework is logically consistent and that violations of the specified ethical properties are ruled out within the formal model through counterexample-based verification. This presents early research enabling continuous, machine-verifiable ethical checking, moving beyond retrospective compliance based on static documentation. We discuss limitations, including the need for real-world verification with data, the challenge with subjectivity and contextual sensitivity, the need for human oversight, and outline how such approaches can support the development of digital phenotyping and AI systems with continuous and auditable ethical guarantees.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-27T11:45:56Z
Igor V. Tarasyuk
arXiv categories: cs.LO

We propose discrete time phased Petri box calculus (dtphPBC), an extension with phase type distributed multiaction delays of discrete time stochastic and deterministic Petri box calculus (dtsdPBC), previously presented by I.V. Tarasyuk. In dtphPBC, transition probability matrices (TPMs) of finite absorbing discrete time Markov chains (DTMCs) with a single absorbing state specify discrete phase type (DPH) distributed delays (including zero delay) of the phased multiactions that generalize stochastic and deterministic multiactions from dtsdPBC. The positively phased (timed) multiactions have positive DPH delays represented by the non-empty TPM matrices over transient states (transient TPMs). The zero phased (immediate) multiactions have zero DPH delay represented by the empty transient TPM. The step operational semantics of dtphPBC is constructed via labeled probabilistic transition systems. The transition systems incorporate the absorbing DTMCs of the DPH delays of the executed phased multiactions via the structural operational semantics (SOS) rules. The SOS rules define a labeling with the empty set on the transitions among transient states of the absorbing DTMC and on the self-loop in the absorbing state of it. The transitions going from the transient states (positive phases) to the absorbing state (zero phase) are labeled with the executions, being the positive phases-superscribed timed multiactions whose (positive) delays are defined by the absorbing DTMC. A series of examples demonstrates how to construct the transition systems of the dynamic expressions, combined from timed and immediate multiactions with different operations of the calculus.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-28T07:08:34Z
Chenyu Zhou, Di Wang, Thomas Reps
arXiv categories: cs.PL

This paper studies how to compute the moments -- mean, variance, and beyond -- of the cost (e.g., running time) of certain probabilistic programs, in which local costs combine not only additively but also via the extremal operations $\max$ and $\min$. Such costs arise naturally -- for instance, the number of rounds of a contention-resolution protocol, the waiting time of a quantum repeater, and the completion time of a fork-join computation -- but fall outside the scope of moment-based analyses developed for additive costs. The difficulty is that $\max$ and $\min$ are nonlinear: the moments of $\max(X, Y)$ are not determined by those of $X$ and $Y$, so propagating moments alone fails. In contrast, propagating full distributions would suffice, but is computationally intractable. We present a compositional cost analysis for a family of probabilistic programs whose cost structure can be represented as a hierarchical cost expression. The analysis proceeds bottom-up through the hierarchical structure, solving local recurrence equations at each node and summarizing each subproblem with a surrogate distribution. Each surrogate consists of an exact short-time prefix and a compact parametric tail. Our approach computes the mean of the cost distribution with a sound error bound, and systematically lifts to second and higher moments. In addition, precision can be increased by refining the surrogate representation, trading additional computation for tighter bounds. We implemented our method in a tool, called DICKENS, and evaluated its capabilities on three problems: quantum repeater waiting times, RFID collision resolution, and completion times of fork-join computations.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-29T11:28:16Z
Jule Schmidt, Maximilian Weininger, Clemens Dubslaff, David Parker, Nils Jansen
arXiv categories: cs.AI, cs.LO

Markov Decision Processes (MDPs) are widely used as decision-making models, commonly specified over factored state spaces through state variables and their valuations. The exponential blowup in the number of states renders many reasoning tasks in MDPs challenging. Abstractions are promising techniques to reduce MDPs and thus mitigate scalability issues. In this work, we introduce a notion of causality on factored MDPs and a novel property-driven causal abstraction technique that retains many characteristics of the original MDP model. For this, we rely on causal relations over state variable predicates and identify those states that share the same reasons for fulfilling or violating a given abstraction property. We theoretically and empirically compare various causal MDP abstractions using different model types such as MDPs, interval MDPs, or stochastic games. Our evaluation demonstrates the potential of our approach: For several standard benchmarks, we obtain small abstractions that allow us to compute near-optimal policies for the original MDP. Furthermore, our causal abstractions often generalize to related large-scale MDP models.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-27T13:44:25Z
Silvia Ghilezan, Paaras Padhiar
arXiv categories: cs.LO, math.LO

The simply typed λ-calculus is a model of computation where typed terms correspond to proofs of intuitionistic propositional logic (IPL) via the Curry-Howard correspondence. Justification logic is an operational modal logic in which the standard box modality is replaced by an explicit proof term, allowing the logic itself to reason directly about proofs of its formulas. Standard justification logics reason about proofs of IPL by embedding Hilbert-style axiomatic proofs of IPL as proof terms of the logic. We instead introduce a justification logic of the λ-calculus, in which the proof terms of the modality are exactly the typed λ-terms themselves: a modal logic that reasons about computation and proof simultaneously, as both notions coincide under the Curry-Howard interpretation. First, we provide an axiomatisation of this logic. We then propose a natural deduction system and a Curry-Howard interpretation, where a formal connection between the term calculus and the proof terms of the logic is provided. To complete the picture, we give a Gentzen-style sequent calculus for which we prove cut-elimination, and consequently obtain a normalisation result by working in the negative fragment.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-27T16:17:50Z
Noah Abou El Wafa, André Platzer
arXiv categories: cs.LO, math.LO

This paper shows that the substructural logic without the identity principle A->A (i.e., subreflexive logic) has principled sound and complete semantics and supports a variety of applications. This decidable generalization of propositional logic naturally interprets implication as robust consequence. Subreflexive logic is proved to admit syntactic cut elimination. Heyting and Boolean semialgebras are introduced as generalizations of Heyting and Boolean algebras and are shown to provide complete algebraic semantics without inadvertently reintroducing reflexivity. Semi-adjunctions on semi-categories and (identity-free) (co-)units are defined to give complete semi-categorical semantics. In the classical case, denotational set semantics that interpret implication as robust material implication are proved complete for subreflexive logic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-28T16:33:36Z
Ryan Simonelli
arXiv categories: math.LO

Recent work in bilateral logic has concerned itself with whether and to what extent strong negation, which "toggles" between assertion and denial, is definable in bilateral systems that lack it. This paper presents a number of results about the definability of strong negation in bilateral systems. First, I show that a constructive Nelson-style Sheffer stroke defines the strong negation of A as (A|(A|A))|A. The same stroke defines the constructive Nelson implication, thus providing a single-connective basis for the strong-negation-and-implication fragment of N4. Second, I provide an exhaustive characterization of the eight combinations of a single "aggregative" connective and a single Nelson-style connective that suffice to jointly define strong negation, with neither defining it individually. One such combination is the material conditional together with constructive co-implication. Third, I show that a constructive and connexive Wansing-style Sheffer stroke (recently referred to as "connexive exclusion") likewise defines the strong negation of A as (A|(A| A))|A and also defines connexive implication. Fourth, I show that, unlike with the Nelson-style connectives, there are no combinations of Wansing-style and aggregative connectives that jointly define strong negation if neither connective defines it individually.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-28T16:57:42Z
Santiago Jockwich, Sourav Tarafder, Giorgio Venturi
arXiv categories: math.LO

We connect modal set theory with Boolean-valued models by developing an \emph{internal} Kripke semantics for modal formulas whose atomic propositions are set-theoretic sentences. Given a complete Boolean algebra $B$, we view its elements as ``local perspectives on truth'' inside the Boolean-valued universe $V^{(B)}$ and interpret the modal operators using an accessibility relation $R$ on $B$ defined by \emph{co-consistency} (equivalently, Boolean compatibility): $aRb$ iff $a\wedge b\neq 0$. Our central conceptual point is that, for set-theoretic sentences $p$, the internal modality $\Diamond p$ holds at $b$ iff there is an ultrafilter $U$ of $B$ containing $b$ such that the classical quotient $V^{(B)}/U$ satisfies $p$. We compute several general and algebra-dependent modal validities, and analyze the special behavior of complete atomic Boolean algebras. Finally, adopting a translation-based semantics on the nonzero part $B^+=B\setminus\{0\}$, we prove a soundness-and-completeness theorem: the normal logic $\KTB$ is exactly the set of modal formulas valid in all translated co-consistency models with parameters.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-30T17:22:45Z
Simone Cuconato
arXiv categories: math.LO

We give a self-contained development of the first-order block calculus in unsigned sequent-style notation: each node of the refutation tree carries a finite block $Π= Γ\cup \neg[Δ]$, negation is governed by explicit rules, and a branch closes on a complementary pair of literals. The calculus is Smullyan's, and so in substance are the theorems; what is offered here is a different arrangement of them. The structural properties are established in the order of dependence familiar from G3-style sequent calculi: closure on arbitrary formulae is admissible, weakening and the substitution of parameters are admissible with preservation of the height, every rule is height-preserving invertible, and cut is admissible, the last being derived from the first three rather than conversely. Soundness, completeness under a fair strategy, countable compactness and the countable model property follow, together with a syntactic criterion under which every fair construction terminates. The correspondence is then proved, in both directions and with cut included, with Gentzen's LK in its usual presentation with explicit weakening, which requires lemmas on parameters that set-based Gentzen systems do not need.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-31T09:13:36Z
Simone Cuconato
arXiv categories: math.LO

Sequent-style tableaux are a one-sided refutation calculus for classical propositional logic, in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data structure and the closure criterion. Building on the correspondence between this block calculus and the cut-free sequent calculus, and following the programme of Kamide and Negri, we recast the calculus as a structural-rule-free G3-style sequent calculus $\mathsf{G3T}$ with shared contexts, and we introduce a G0-style sequent calculus $\mathsf{G0T}$ with independent contexts, explicit weakening and contraction, generalized initial sequents, and a primitive explosion rule. A theorem establishing the equivalence between $\mathsf{G0T}$ and $\mathsf{G3T}$ is proved, and the cut-elimination theorem for $\mathsf{G0T}$ is obtained as a consequence. We then introduce a natural deduction system $\mathsf{NgT}$ with general elimination rules for the same logic, and we prove a full normalization theorem for $\mathsf{NgT}$. The proof is achieved by means of bidirectional translations between $\mathsf{G0T}$ and $\mathsf{NgT}$: normal derivations correspond to cut-free derivations, and full normal form to the discipline in which every major premiss of an elimination rule is an assumption.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-31T12:35:05Z
Jonathan Washburn, Milan Zlatanović
arXiv categories: math.LO

Let $δ$ denote the primitive act of distinction, formally realized as the one-step extension $r \mapsto Sr$ of a finite record. We study the inductively generated $δ$-orbit and its first-order arithmetic presentation $\mathbb{N}_δ$. The corresponding $δ$-calculus is an intuitionistic first-order proof system over the signature $\{0,S,+,\cdot\}$. Every derivation carries a ledger recording the use of the law of excluded middle, the limited principle of omniscience, Markov's principle, and induction on quantified formulas. The last entry does not affect whether a derivation is forced. If a closed formula is derivable in the forced fragment, then it is true in the standard model. Starting from $δ$, we construct a choice-free number tower $δ\leadsto \mathbb{N}_δ\hookrightarrow \mathbb{Z}_δ\hookrightarrow \mathbb{Q}_δ$. The metatheoretic number systems $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ each admit an explicit injection into $\mathbb{N}_δ$. We also classify the recognition quotients of the additive monoid $(\mathbb{N}_δ,+,0)$. Assuming the law of excluded middle, every recognizer is either injective or has a kernel congruence $\equiv_{i,p}$, with index $i$ and period $p$, for a unique pair $i\ge 0$, $p\ge 1$. In the noninjective case the quotient is isomorphic to the finite monogenic monoid $M(i,p)$. We price this classification with the ledger, determining which nonconstructive principles each form requires. If the congruence is decidable and an explicit pair of distinct related elements is given, the classification is forced. If the congruence is decidable and different from equality, Markov's principle is needed. For an arbitrary congruence, the dichotomy requires the law of excluded middle. The reverse implications show that the last two prices cannot be lowered. The main results are formalized in Lean 4.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-27T12:57:42Z
Daniel Max Hoffmann, Krzysztof Krupiński
arXiv categories: math.DS, math.LO

Let $(X,G)$ be a tame flow and let $K$ be an Ellis group of its enveloping semigroup $E(X,G)$. Although $K$ is a compact Hausdorff topological group in its $τ$-topology, the inclusion of $K$ into $E(X,G)$ need not be Borel. We show that normalized Haar measure on $K$ nevertheless determines, via the Riesz--Markov theorem, a canonical regular Borel probability measure $μ_K$ on $E(X,G)$, called its Haar decompression. Our principal structural result states that, for every tame flow, $(E(X,G),G)$ is amenable if and only if $(X,G)$ is hereditarily amenable. For a tame hereditarily amenable flow, every Haar decompression is $G$-invariant whenever $X$ is metrizable or $G$ is countable. For metrizable minimal tame flows admitting an invariant measure, the evaluation pushforward of every Haar decompression at every point is the unique invariant measure. Moreover, every ergodic invariant measure on a metrizable tame flow has minimal support; consequently, every ergodic invariant measure on a metrizable tame ambit is obtained by evaluating a suitable Haar decompression.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-27T16:21:00Z
Yayi Fu
arXiv categories: math.LO

Fix an o-minimal expansion $\mathcal{R}=(\mathbb{R},+,\cdot,0,1 <,...)$ of the real ordered field. Given $C^1$ functions $f_1,...,f_k$, $g_1,...,g_k:M\to\mathbb{R}$ on a definable cell $M$, let $h_{i,0}$ denote $f_i$ and $h_{i,1}$ denote $g_i$. Suppose that for all $τ\in 2^{[k]}$, $H_τ=(h_{1,τ(1)},..,h_{k,τ(k)}) :M\to \mathbb{R}^k$ is regular and proper on $M$, and that for all $i\in[k]$, $\{f_i=0\}$ and $ \{g_i=0\}$ are connected, and $\{f_i=0\}\cap \{g_i=0\}=\emptyset$. We show that then there exists a sequence $(\square_{i,ε}:i\in[k],ε\in \{0,1\})\in\{\leq ,\geq \}^{[k]\times\{0,1\}}$ such that the enclosed region $\underset{i\in[k]}{\bigcap}\{ f_i\square_{i,0} 0\}\cap \{ g_i\square_{i,1} 0\} $ is compact.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-27T20:48:15Z
David Victor Feldman
arXiv categories: math.MG, math.LO

A compact convex body $K\subseteq\mathbb{R}^n$ is a first-order structure in two natural languages: $L_{\mathrm{aff}}$, with a ternary betweenness relation and convex-combination operations, and the sparser $L_B$, with betweenness alone. Isomorphism means affine equivalence in the first and, by a theorem of Shiffman, projective equivalence in the second. We ask when elementary equivalence already determines the body. Main theorem: two compact convex bodies of any dimension, with no regularity hypotheses, are elementarily equivalent in $L_{\mathrm{aff}}$ if and only if they are affinely equivalent. The proof rests on a definable compact family of gauges: simplices stationary for barycentric coordinates, with volume bounded below via the anticomplementary simplex. For $L_B$ we develop an interior von Staudt calculus, all quantifiers ranging over the body, making harmonic conjugacy, rational cross-ratio comparisons, and cross-ratio equality first-order; only the harmonic primitive is needed, with a single interior perspectivity effecting the change of scale. Consequences: the closed unit ball is separated from $\{\sum x_i^4\le 1\}$ in $L_B$ for every $n\ge 2$; and in the plane, projective categoricity holds outright for convex polygons and for bodies with real-analytic, positively curved, non-conic boundary, the latter via a new finite projective invariant, the conic-cluster set: the points whose every boundary arc contains six co-conic extreme points. A general reduction isolates what remains of the projective conjecture: recovery of boundary coordinates in dimension at least three, and a definable compact gauge, obstructed exactly by non-compact projective symmetry, as on the quadric. We also classify the natural noncompact examples.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-28T20:53:07Z
Atticus Stonestrom
arXiv categories: math.LO, math.DS, math.GR

This paper has several parts. We begin by developing a theory of `piecewise (strong) f-genericity' in NIP groups, where we call a definable set piecewise (strong) f-generic if some union of finitely many translates of it is (strong) f-generic. We show that, in an NIP group, the definable sets that are not piecewise (strong) f-generic form an ideal. Our hope is that the corresponding piecewise (strong) f-generic types can provide a substitute in arbitrary NIP groups for the (strong) f-generic types of definably amenable NIP groups, and in the rest of the paper we give several applications. Two of the applications deal with the Ellis group of an NIP group. Let $T$ be an NIP theory, $G$ a definable group, and $M$ a model. In our first result we show that the size of the Ellis group of $G(M)$ is bounded above by $2^{|T|}$, independent of the choice of $M$, giving a substantial step towards the question of whether the isomorphism type is independent of $M$. In our second result, inspired by a theorem of Hrushovski, we show that, if $T$ and $M$ are countable and the formulas of $T$ have uniformly bounded VC-codensity, then the Ellis group of $G(M)$ has `finite Archimedean rank', ie its connected component is profinite-by-Lie. A crucial tool for us in both results is the recent result of Chernikov-Gannon-Krupiński and Basso-Zucker that the $τ$-topology on the Ellis group is Hausdorff. Finally, we use our techniques to obtain a `local' result valid in arbitrary NIP theories, without the assumption of uniformly bounded VC-codensity: for any `bi-invariant' formula $φ(x,y)$, the group $G/G^{00}_φ$ has finite Archimedean rank. More precisely, if the VC-codensity of $φ(x,y)$ is at most $δ$, then $G/G^{00}_φ$ is an inverse limit of compact Lie groups of dimension at most $(4δ)^2$. This connects to, though is different than, a question of Hrushovski's.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-31T10:39:33Z
Martin Lotz, Abhiram Natarajan
arXiv categories: math.AG, math.CA, math.LO

We present a direct and self-contained proof of Khovanskii's Bezout-type bound for the number of nondegenerate solutions of a system of Pfaffian equations. We isolate the ingredients of Khovanskii's original argument and assemble them into a proof that avoids the general theory of integral manifolds developed in his monograph. Our formulation mildly refines the classical statement: rather than depending on the ambient dimension, our bound depends on the maximum number of variables on which any function in the Pfaffian chain depends. As a consequence, we obtain a refined bound on the number of connected components of a Pfaffian set.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-31T12:52:11Z
Mike Stannett
arXiv categories: math.LO

A recent theorem of Madarasz characterises the parameter-free concepts of a finitely field-definable coordinate geometry by invariance under its affine automorphisms. This paper isolates the affine-geometric ingredient in that proof and extends the argument to include additional finite-relational coordinate geometries. The new hypothesis is "semilinear faithfulness": in every ultrapower, each automorphism of the induced geometry factors as an affine automorphism of the geometry followed by the componentwise action of an automorphism of the expanded base structure. Under this hypothesis, every parameter-free ambient-definable relation is a concept of the geometry exactly when it is preserved by the affine automorphism group. A corresponding dual inclusion theorem is obtained for concept sets. The framework recovers the original finitely field-definable theorem and applies beyond pure-field definability, including a named-scalar geometry and a frame-expanded geometry over an exponential field. A final section records the analogous factorisation principle for uniformly coded symmetry groups in arbitrary, including non-geometric, one-sorted structures.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-27T01:31:45Z
Andrzej Roslanowski
arXiv categories: math.LO

We present several remarks on cardinal coefficients associated with the generalized Baire space for an inaccessible cardinal kappa. Our inquiry originates in the work of van der Vlugt arXiv:2307.14118 . We provide evidence that the appropriate coefficients to consider are those determined by binary relations restricted to a club. In other words, we make a case for the systematic use of clubs.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-27T07:33:42Z
Dominic van der Zypen
arXiv categories: math.LO, math.CO

In 1943, Hadwiger formulated his celebrated conjecture, connecting the chromatic number $χ(G)$ of a finite, simple, undirected graph with the cardinality of the largest complete minor, $η(G)$. The disjoint union of all finite complete graphs shows that Hadwiger's conjecture fails for infinite, but a slightly weaker version is true in these graphs, but open for finite graphs. In this note we generalize that weaker version to hypergraphs and providea simple, general, and purely set-theoretical formulation of Hadwiger's conjecture.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-27T13:28:01Z
Mauro Di Nasso, Renling Jin
arXiv categories: math.CO, math.LO

We prove a multidimensional extension of a strong Hales-Jewett theorem that simultaneously and "directly" extends Ramsey's theorem and Hindman's theorem. The proofs show the effectiveness and simplicity of the techniques based on iterated nonstandard extensions that have been recently developed. Unlike existing ultrafilter proofs, our arguments to prove the strong Hales-Jewett theorem assume neither minimal nor idempotent ultrafilters. To demonstrate this, we translate our proof of the strong Hales-Jewett theorem into an ultrafilter proof that requires only non-principal ultrafilters.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-28T09:48:11Z
Mauro Di Nasso
arXiv categories: math.NT, math.CO, math.LO

The hypernatural numbers $\mathbb{N}$ of nonstandard analysis have recently proven to be an effective tool in arithmetic Ramsey theory. After introducing the fundamental ``nonstandard" notions, we present several examples to illustrate the use of this technique in practice. In particular, we provide brief nonstandard proofs of some recent results concerning the partition regularity of certain families of infinite configurations. We also present a new theorem about monochromatic sums and products.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-28T10:18:18Z
Bryan Ford
arXiv categories: math.LO, cs.LO, cs.PL

Informal statements of Gödel's incompleteness theorems often run: "no consistent formal system with arithmetic can be complete" - omitting the fact that the theorems as proved assume classical logic. This paper presents reflective grounded arithmetic (RGA), a paracomplete arithmetic in which truth is grounded in computation rather than assumed by classical fiat, and in which universal quantification is grounded reflectively: a universal statement is true when the system's own proof search certifies its schematic instance, and false when it refutes a particular numeral instance. RGA permits unconstrained recursive definitions, proves the totality of addition and multiplication as internally quantified theorems, and represents exactly the recursively enumerable sets - the ingredient list of the folklore Gödel statement - while remaining consistent. This work proves, with all results machine-checked in Isabelle/HOL: soundness and consistency; open completeness - provability coincides with grounded truth on well-formed statements; N-soundness - every provable totality claim is backed by an actual value; a Church-Turing characterization of RGA's expressive power; and $ω$-incompleteness - grounded truth is recursively enumerable, and therefore some family of statements has every numeric instance provable while its universal closure is not merely unprovable but semantically ungrounded. The resulting logic occupies a Markov-flavored, substructural corner distinct from both classical and intuitionistic arithmetic: double-negation elimination holds, quantified excluded middle fails, refuted universals yield explicit counterexample witnesses, and the deduction theorem's abstraction direction fails precisely at ungrounded hypotheses.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-28T13:36:03Z
Amir Leshem
arXiv categories: cs.IT, cs.LO

We study sequential prediction of individual binary sequences under zero-one loss. No computable master can compete on every sequence with all total computable predictors. We therefore consider rational-valued primitive-recursive forecasters, a broad syntactically enumerable class containing finite-state, context-based, and Prediction by Partial Matching (PPM) rules. We construct a computable probabilistic predictor with an explicit sublinear regret bound relative to every primitive-recursive forecaster on every individual sequence. We further prove that the PPM predictor is primitive recursive. Consequently, our predictor attains the infinite-past Bayes error on every Martin-Löf random realization of every computable stationary ergodic binary source. This optimality extends to finitely many independent such sources interleaved according to an arbitrary primitive-recursive schedule. Finally, we establish strict separations from finite-state prediction and from every fixed primitive-recursive predictor. keywords: Universal prediction, individual sequences, prediction with expert advice, primitive recursive functions, Kolmogorov complexity, PPM.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-28T17:00:01Z
Xing-Yu Hu
arXiv categories: math.LO, math.GN

For a ladder-system space $X_L$ with carrier $S\subseteq E^{ω_1}_ω$, the finite-label uniformization property $M_{<ω}$ characterizes countable metacompactness, and countable metacompactness is equivalent to the $Δ$-property. Both equivalences are known for stationary carriers. For arbitrary carriers, an active-tail formulation gives a direct proof that $M_{<ω}$ is equivalent to the $Δ$-property and leads to a support-finite decomposition theorem, together with club-smallness and trace criteria that avoid explicit ladder-position thresholds. A club-gap argument, combined with Fodor's lemma, shows that finite and countable tail multiplicity determine the same carrier ideal, namely $\mathrm{NS}\restriction S$. Subsets of the isolated part that meet each ladder in only finitely many points have clopen remainder traces, and these traces form a generalized Boolean algebra. All such traces are disjoint from the carrier part of the remainder. Finally, the subcarriers whose restricted spaces are $σ$-closed discrete form an ideal $\mathcal{C}_L$ containing $\mathrm{NS}\restriction S$. If $X_L$ is a $Δ$-space, a threshold-based gluing argument shows that $\mathcal{C}_L$ is a $σ$-ideal. Whether this holds for every ladder system remains open.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-28T21:17:03Z
Bjørn Kjos-Hanssen
arXiv categories: cs.FL, math.LO

Gill (arXiv:2402.13376) introduced the probabilistic automatic complexity $A_P(w)$ of a finite string $w$: the least number of states of a probabilistic finite automaton (PFA) for which $w$ is the unique most probably accepted string of its length. He asked whether $A_P$ is unbounded, noting that no string with $A_P > 3$ was known (Question 4.14 of that paper). We answer the question by proving that $A_P(w)\le 3$ for every string $w$ over every finite alphabet. The witnessing three-state automaton is explicit: its reduced dynamics tracks the pair $(u,u^2)$, where $u$ is the reversed base-$b$ value of the input, and its acceptance functional is a downward parabola peaked at the value of the target string. Combined with Gill's classification of the binary strings with $A_P=2$, this completely determines $A_P$ on binary strings.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-29T06:42:18Z
Zeinab Ashtab, David Fernández-Bretón
arXiv categories: math.LO, math.CO, math.FA

We study (bounded) finitely additive measures on the group of integers $\mathbb Z$, as elements of the Banach algebra $\mathrm{ba}(\mathbb Z)$, viewed as a natural generalization of ultrafilters. The algebraic structure of $\mathrm{ba}(\mathbb Z)$ extends the semigroup structure of the Čech--Stone compactification, allowing methods from ultrafilter theory to be applied in a broader measure-theoretic setting. We investigate idempotent finitely additive measures and establish additive properties of subsets of $\mathbb Z$ having positive measure. We then proceed to study almost translation-invariant and translation-invariant finitely additive measures, showing that these stronger notions yield correspondingly stronger additive conclusions. In particular, we prove that every subset of $\mathbb Z$ whose measure exceeds a certain explicit threshold necessarily is an $\mathsf{IP}_{n}$-set; with stronger properties and lower thresholds depending on the properties of the relevant measures. Several examples illustrating the sharpness and limitations of the results are also presented, together with a discussion of open problems and directions for future research.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-30T12:24:42Z
Quentin Le Houérou, Ludovic Patey
arXiv categories: math.LO

Carlson and Simpson proved that for every finite coloring of the 1-variable words over a finite alphabet~$A$, there is an infinite $ω$-variable word on which all the 1-variable words are monochromatic. This statement for $\ell$-colorings, written $\mathsf{CSL}^1_\ell$, is known to be strictly weaker than $\mathsf{ACA}_0$. We prove that $\mathsf{RCA}_0 + \mathsf{CSL}^1_2$ is a $\forall Π^0_4$-conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Sigma_2$. Among its consequences, it implies that neither the indivisibility of the universal triangle-free Henson graph for 2-colorings, nor the tree theorem for pairs and two colors, imply $Σ^0_2$-induction. This answers a question of Chong, Li, Wang and Yang.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-30T15:20:55Z
Inbar Oren
arXiv categories: math.LO

We introduce a new method for obtaining models of stationary reflection at the successor of a singular cardinal of any cofinality. In particular, starting from a cardinal $κ$ which is $κ^+$-supercompact, we get a model of countable simultaneous reflection at $\aleph_{ω_1+1}$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-30T17:56:28Z
Zhi-Wei Sun
arXiv categories: math.NT, math.LO

In 2016 J. Koenigsmann proved that $\mathbb Q\setminus\mathbb Z$ is diophantine over $\mathbb Q$, i.e., there is a polynomial $P(t,x_1,\ldots,x_{n})\in\mathbb Z[t,x_1,\ldots,x_{n}]$ such that for any rational number $t$ we have $$t\not\in\mathbb Z\iff \exists x_1,\ldots,x_{n}\in\mathbb Q\,[P(t,x_1,\ldots,x_{n})=0].$$ In this paper we show that we may take $n=7$ which improves the previous record $n=10$ obtained by Daans in 2024. (Actually we even extend this to any global field.) This, together with a previous result of Z.-W. Sun, implies that there is no algorithm to decide for any $F(x_1,\ldots,x_{16})\in\mathbb Z[x_1,\ldots,x_{16}]$ whether $$\forall x_1,\ldots,x_9\in\mathbb Q\exists y_1,\ldots,y_{7}\in\mathbb Q\,[F(x_1,\ldots,x_9,y_1,\ldots,y_{7})=0].$$

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-31T16:03:03Z
Platon Sifnaios
arXiv categories: math.LO

An annulment structure consists of a numbered domain of distinctions with a $Σ^0_1$ manifestation predicate; an adjudicator is a partial map assigning to distinctions the verdicts annulled or exempt. We ask which domains admit an adjudicator that is total, correct, and complete in its mission -- annulling every non-manifesting member -- and locate the boundary exactly. On the positive side, domains with decidable manifestation admit canonical adjudicators with certificates, instantiated for Presburger arithmetic and finite-state re-entry systems. On the negative side, adjoining a single nullary gate, by which a distinction may query the verdict passed on itself, destroys decidability uniformly: the extended domain carries a trichotomy in which every adjudicator fails totality, exhaustiveness, or soundness at one distinction fixed in advance. Bounding the depth of self-address refines this: each finite level remains decidable, the hierarchy of iterated verdicts is the synchronous update of a Boolean network on the query graph, deciding stabilisation is PSpace-complete for explicitly presented networks, and periods as large as $2^n-1$ occur at closure size $n$. In the limit what fails is convergence, not decidability; the diagonal distinctions oscillate with period two, and their mean frequency of $1/2$ is the value a reflective oracle is forced to return there. Over the standard domain relative to an oracle $X$, the least Turing degree of an adjudicator with all three properties is the degree of $X'$: adjudication costs one jump per level. The boundary is a three-way trade among determinacy, correctness, and residence at the level adjudicated. The fixed-point core holds over every precomplete numbering in the sense of Ershov. The framework falls on the intensional side of the divide between Kleene's two recursion theorems. Gödel's incompleteness theorems are nowhere used.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-27T14:13:55Z
Philip Hackney
arXiv categories: math.AT, math.CT

A simplicial set is $d$-Segal if and only if it is $(d{+}1)$-coskeletal and satisfies the $d$-Segal condition in the two lowest relevant simplicial dimensions.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-27T17:52:22Z
Johnathon Taylor
arXiv categories: math.CT

In this paper, we introduce the notion of a controlled theory, originally developed in the author's thesis, as a structural tool for the study of higher categorical algebra. We define a notion of deformation for pros and controlled theories in a cartesian closed category. Furthermore, we show that deformations of controlled theories naturally produce Lawvere theories enriched over the same base category. We construct functorial one-dimensional categorifications and homotopifications of controlled theories, yielding Lawvere $2$-theories and Lawvere theories enriched in simplicial sets, respectively. As an application, we obtain a new model for $\infty$-groups and construct a model of coherent group-like $E_\infty$-spaces, which we will show in future work models infinite loop spaces.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-28T07:58:37Z
Arne Mertens
arXiv categories: math.CT

In this short note, we prove that the category of necklaces is a test category. Hence presheaves on necklaces model homotopy types. The proof is analogous to that for the category of cubes with connections.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-28T08:51:33Z
Benno van den Berg
arXiv categories: math.LO

We show how a standard constructive notion of ordinal supports a useful constructive theory of transfinite recursion. We do this by giving constructive proofs of various initial algebra theorems, like Adamek's theorem, and a version of Quillen's small object argument for constructing cofibrantly generated algebraic weak factorisation systems.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-30T17:10:11Z
Johnathon Taylor
arXiv categories: math.CT

We introduce a construction of algebraic coherators for Grothendieck $\infty$-groupoids using the algebraic small object argument, replacing previous approaches we have used based on distributive series of monads with a more direct method for freely adjoining coherence data. Given a controlled theory, we define unreduced and reduced Grothendieck realizations, producing $\infty$-Lawvere theories and extending this construction functorially to connected diagrams of controlled theories. We apply this framework to construct globular models for monoidal $\infty$-groupoids, symmetric monoidal $\infty$-groupoids, coherent $\infty$-groups, and Picard $\infty$-groupoids. We define canonical semi-model structures on categories of models over $\infty$-Lawvere theories and formulate a generalized pushout conjecture that implies the existence of these semi-model structures and the Homotopy Hypothesis for Grothendieck $\infty$-groupoids.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-30T17:41:37Z
Joseph Helfer
arXiv categories: math.CT, math.LO

This paper continues the development of (elementary) 2-topos theory, a foundational theory based on an axiomatization of the 2-category of categories. We prove that any 2-topos contains a model of intuitionistic ZF set theory, and we use this to show that, if appropriate size restraints are not imposed, then a Burali-Forti type paradox can be deduced from the 2-topos axioms. The set-theoretic universe is produced as a special case of a general construction giving an internal category of models in a 2-topos of an arbitrary finite higher-order theory, which in turn is carried out using a notion of "topos sketch". As a byproduct of our construction, we also make contact with the subject of "algebraic set theory", introducing a novel approach to the construction of set-theoretic universes from a "category of classes".

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-27T09:03:12Z
Georgios Dalezios, Juan Omar Gómez
arXiv categories: math.RT, math.AT, math.CT

We introduce the proper stable module category for an arbitrary discrete group over any commutative ring by means of cotorsion pairs and abelian model structures. This category is a well-generated tensor-triangulated category and is compactly generated in case the commutative ring is regular. Our construction resembles the topological approach via proper equivariant stable homotopy theory. Moreover, it agrees with the Mazza-Symonds stable module category, whenever the latter is defined, and with various other stable categories associated to hierarchically defined groups. Along the way, we introduce certain homological dimensions and study them in detail, comparing them with the classical notions.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-27T19:53:37Z
José Miguel Calderón León, Alberto G. Raggi-Cárdenas, Itzel Rosas, Ramón H. Ruiz-Medina
arXiv categories: math.CT

The Burnside ring of a finite category, introduced by Webb, generalizes the classical Burnside ring of a finite group. However, unlike the classical case, the Burnside ring of a finite category has finite rank if and only if the category is equivalent to a groupoid. In this article, we introduce a new invariant associated with a finite category $\mathcal{C}$, called the \emph{simple Burnside ring} of $\mathcal{C}$ and denoted by $B^S(\mathcal{C})$. This construction is obtained from simple $\mathcal{C}$-sets and generalizes the classical Burnside ring of a finite group. Moreover, the ring $B^S(\mathcal{C})$ always has finite rank. We develop the basic theory of simple $\mathcal{C}$-sets and study several structural properties of the ring $B^S(\mathcal{C})$. In particular, we determine all ring homomorphisms from $B^S(\mathcal{C})$ to $\mathbb{Z}$, describe its prime spectrum, and obtain a decomposition theorem expressing $B^S(\mathcal{C})$ as a product of simple Burnside rings of strongly connected subcategories.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-28T00:31:58Z
Ariel E. Rosenfield
arXiv categories: math.CT, math.RA

We show that several categories of hyperstructures, including the mosaics of Nakamura and Reyes and the hypergroups of Marty, are realizable as categories of objects with extra structure within the category of complete atomic Boolean algebras (CABAs).

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-28T09:51:29Z
Alessandro Ardizzoni, Lucrezia Bottegoni, Alan Cigoli, Andrea Sciandra
arXiv categories: math.CT, math.QA, math.RA, math.RT

In this work, we extend the protomodularity of the category of cocommutative Hopf algebras to the quasitriangular setting. Every quasitriangular Hopf algebra admits a minimal quasitriangular Hopf subalgebra and, as we show, can be regarded as a cocommutative bimonoid in the tensor-braided duoidal category of bimodules over it. This leads us to investigate protomodularity in the broader context of Hopf monoids in duoidal categories. To this end, we adopt a slight modification of Böhm's notion of antipode associated with a reversion, further refining an earlier one due to Böhm-Lack. This framework allows us to study Hopf monoids in this setting, Galois and co-Galois maps, and the factorization of Hopf monoids. Using these tools, we prove a factorization of points, the Split Short Five Lemma, and the existence of pullbacks of split epimorphisms along arbitrary morphisms in the category of cocommutative Hopf monoids with monic unit in any tensor-braided duoidal category with a reversion; hence this category is protomodular. As applications, we recover the protomodularity of cocommutative Hopf algebras in symmetric monoidal categories under mild assumptions, and we obtain that of the coslice category of quasitriangular (resp. triangular) Hopf algebras under a fixed subobject; in the triangular case, this can be traced back to a category of generalized internal groups, introduced in the present work. When the fixed subobject is minimal, we infer the protomodularity of the category of quasitriangular Hopf algebras whose minimal quasitriangular Hopf subalgebra is isomorphic to the fixed subobject, which we interpret as the protomodularity of an essential fibre of a functor. As a byproduct, our results extend the double cross product of cocommutative Hopf algebras to the quasitriangular setting.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-28T14:04:27Z
Martin Markl, Dominik Trnka
arXiv categories: math.CT

We show that abelian categories can be characterized as structures consisting of a colax algebra and a lax algebra connected by a lax mixed rewriting rule. To this end we develop a theory of lax rewriting rules for pairs of lax-lax and colax-lax algebras over 2-monads.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-29T10:29:14Z
Tim Netzer, Tobias Fritz
arXiv categories: math.CT, math.OA

An operator system is similar to a module over a ring, with the role of scalar multiplication played by the action of completely positive maps. Using enriched category theory, we make this analogy into a precise categorical equivalence, namely between a certain category of nonunital operator systems and a certain category of left modules over the category of matrix algebras enriched over regularly ordered Banach spaces. Using right modules instead yields an equivalence with a certain category of nonunital dual operator systems. We also develop general separation, representation and extension theorems for modules in enriched category theory. Specializing these to our nonunital operator systems recovers results which partly recover the corresponding classical theorems for operator systems.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-29T11:15:08Z
Torgeir Aambø
arXiv categories: math.CT, cs.LO

In this paper we prove that Dubois--Prade's eight possibilistic operators in Formal Concept Analysis arise canonically from Kan extensions of the underlying boolean profunctor. This provides a conceptual explanation for the result that $NΠ$-pairs are the formal concepts of the complement context. We further prove that the FCA closure operator and the $NΠ$-pairs are the only symmetric or asymmetric operator compositions that give formal concepts. Finally we use these eight possibilistic operators to construct new closure operators on a formal context via standard categorical arguments.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-30T00:22:45Z
Fernando Lucatelli Nunes, Walter Tholen
arXiv categories: math.CT

Grothendieck cofibrations describe transport in a category varying over a base, while factorization systems organize the arrows of a category into two complementary classes. We give a fully 2-categorical account of the passage from the former structure to the latter. The global comma 2-monad on the arrow 2-category encodes Grothendieck transport, whereas the squaring 2-monad encodes factorizations. We prove that split cofibrations are precisely the strict algebras for the comma 2-monad, including their 1-cells and 2-cells, and that normally cloven cofibrations are precisely its normal pseudoalgebras. A canonical colax morphism from the comma 2-monad to the squaring 2-monad then turns cocartesian transport into the cocartesian-vertical factorization of arrows in the total category. At the strict level, this yields the strict factorization system of designated cocartesian and vertical arrows; at the coherent level, it yields the orthogonal factorization system whose left class consists of all cocartesian arrows and whose right class consists of the arrows sent to isomorphisms in the base. We also separate unrestricted global pseudoalgebras, which retain a coherently trivial base action, from fixed-base pseudoalgebras, which correspond to arbitrary cleavages, and record the dual strict result for fibrations. This places the classical cofibration-factorization interaction, in all these variants, within a single change-of-2-monads construction and relates it directly to the existing fibrational and factorization literature.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-30T08:25:35Z
Sebastian Halbig, Paolo Saracco, Tony Zorman
arXiv categories: math.CT, math.QA

We study gabi-monads on skew-closed categories, extending the gabi-algebras of Berger, the second author, and Vercruysse beyond the linear case. Our main reconstruction theorem identifies gabi-monad structures on a monad with skew-closed structures on its Eilenberg--Moore category for which the canonical forgetful functor is strict closed. We compare this notion with closed monads in the sense of Kock, showing that in representation-theoretic cases these notions are quite different. On closed monoidal categories, every left Hopf monad is a normal gabi-monad, but the converse fails in general. We characterise when a gabi-monad is Hopf by the invertibility of the corresponding parametric mates, which recovers the ring-theoretic result that normal gabi-algebras over a commutative base ring are Hopf algebras. The theory of gabi-monads admits several natural examples, such as torsion-free modules, reflexive digraphs, and simplicial complexes, that we will explore in detail; we also study pointed sets as a quasi-example.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-30T10:57:28Z
Andrea Rivezzi, Andrea Sciandra, Thomas Weber
arXiv categories: math.QA, math.CT, math.RA, math.RT

We describe infinitesimal deformations of post-Lie algebras and post-Hopf algebras and prove that the adjunction given by the universal enveloping algebra and primitive elements functors is compatible with the infinitesimal structure. When restricted to connected and cocommutative infinitesimal post-Hopf algebras, this becomes an equivalence of categories, which constitutes an extension of the Cartier--Milnor--Moore theorem. We classify infinitesimal post-Lie structures on $\mathfrak{sl}(2)$, and discuss a class of infinitesimal post-Lie algebras emerging from flat connections with covariantly-constant torsion. Moreover, we classify infinitesimal post-Hopf structures on Sweedler's Hopf algebra. Cocommutative infinitesimal post-Hopf algebras induce a Hochschild 2-cocycle on the associated subadjacent Hopf algebra. Finally, we prove that the quadratic operad of infinitesimal post-Lie algebras is Koszul, by using a filtered distributive law between the operads of Lie algebras and bi-magmas.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-30T12:25:28Z
Leovigildo Alonso, Raúl Alvite-Pazó, Ana Jeremías
arXiv categories: math.CT, math.AC

We propose a notion of homotopy limit in the category of complexes over an abelian category with products by totalizing the classic construction of the Roos' complex that computes derived inverse limits. For complexes of modules over a non-necessarily commutative ring, we show that our construction of homotopy limits computes the derived limit complex, and under an acyclicity hypothesis on the inverse system, we prove that it is quasi-isomorphic to the limit. We further show that, in general, the construction is appropriately dual of the previous construction of homotopy colimits of complexes from [Alonso, Jeremías and Souto: Localization in categories of complexes and unbounded resolutions. \textit{Canad. J. Math.} (2000)], and that there also is a dual behavior between derived limits and colimits in derived categories of modules. Finally, we show that colocalizing subcategories are stable for homotopy limits.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-30T15:40:52Z
Andrea Sciandra, Vito Volpe
arXiv categories: math.CT, math.QA, math.RA, math.RT

We prove that the category $\mathsf{SKB}$ is not algebraically coherent. As a consequence, it is not locally algebraically cartesian closed. Then the same can be deduced for cocommutative Hopf braces.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-30T15:58:54Z
Chunyi Li, Zhiyu Liu, Ziqi Liu, Emanuele Macrì, Alexander Perry, Paolo Stellari, Xiaolei Zhao
arXiv categories: math.AG, math.CT, math.RT

We extend the construction of stability conditions on projective schemes over a field to projective families over an arbitrary base, and prove that they admit proper relative moduli spaces of semistable objects. We also prove a number of complementary results: the existence of mass-Hom bounds for these stability conditions, as conjectured by Halpern-Leistner and Robotis; a comparison with tilt-stability on surfaces and threefolds; a construction of stability conditions on the supported derived category of total spaces of certain vector bundles, including all local Calabi--Yau varieties; and a simple new proof of Bondal and Orlov's reconstruction theorem.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-31T07:31:59Z
Marco Abbadini
arXiv categories: math.CT, math.GN

Lieberman, Rosický, and Vasey proved that $\mathbf{CompHaus}^{\mathrm{op}}$ - the opposite of the category of compact Hausdorff spaces - is not finitely concrete by a route through Hilbert and Banach spaces, commutative unital $C^*$-algebras, and Gelfand duality. We give a short topological proof. Moreover, we strengthen the result by identifying a specific sequential colimit in $\mathbf{CompHaus}^{\mathrm{op}}$ that no faithful set-valued functor preserves.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-27T09:44:17Z
Filippo Bonchi, Cipriano Junior Cioffo
arXiv categories: cs.LO, math.CT

Categories with finite biproducts play a central role in category theory, providing an abstract setting in which additive and linear structures can be studied uniformly. In this paper, we introduce categories with \emph{convex} biproducts, which intuitively restrict the linear structures to convex ones. We show that, whereas categories with finite biproducts give rise to a matrix calculus based on arbitrary linear combinations, convex biproduct categories instead induce a matrix calculus based on stochastic (more generally, substochastic) matrices. This perspective yields a refined algebraic and compositional framework tailored to probabilistic settings. We exploit this connection to establish an isomorphism that underpins probabilistic tape diagrams, a graphical formalism for bimonoidal (also known as rig) categories, and we demonstrate its effectiveness by providing a complete axiomatisation of probabilistic Boolean circuits.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-28T13:27:19Z
Matt Wilson
arXiv categories: math.CT

To better understand the landscape of well-behavedness laws for lenses on strict Cartesian symmetric monoidal categories, we define tagged lenses. We prove that tagged lenses form a strict symmetric monoidal category equipped with a strict symmetric monoidal functor into the category of putget lenses. We then observe compositional entailment for the other two lens laws, identifying change-dependence and first-last dependence of tags as sufficient conditions for getput and putput, respectively.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-28T18:06:08Z
Samson Abramsky, Rui Soares Barbosa, Carmen Constantin, Martti Karvonen
arXiv categories: quant-ph, cs.LO

Measurement-based quantum computation (MBQC) is a universal model of quantum computation whose full power requires adaptivity. Contextuality is known to power quantum advantage in MBQC, yet it has resisted algebraic analysis in the adaptive setting. We show that if an adaptive $\mathbb{Z}_2$-linear measurement-based quantum computing protocol deterministically computes a non-affine Boolean function, then the underlying quantum resource satisfies an inconsistent set of linear equations. This witnesses an algebraic form of strong contextuality generalising Mermin's All-versus-Nothing arguments. Such algebraic contextuality can be detected cohomologically, resolving an open question posed by Raussendorf, who had established cohomological witnesses of contextuality for non-adaptive protocols, but left the adaptive case open. We prove this result constructively: we model adaptive measurement protocols as ordinary measurements on a larger scenario of tree-like measurements, and explicitly build the inconsistent equations inductively.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-29T17:45:10Z
Francesco Dagnino, Jacopo Emmenegger, Andrea Giusto
arXiv categories: cs.LO, math.CT

Jacobs comprehension categories subsume a large class of categorical models of type dependency, supporting also the description of morphisms between types. We study the relationship between comprehension categories and a particular subclass, which we call Lawvere-Ehrhard comprehension categories. First, we characterize this subclass by comparing a fibration of terms and a fibration of type morphisms associated to a given comprehension category. Next, we provide the construction of the free comprehension category over a fibration. Finally, we construct the free Lawvere-Ehrhard comprehension category over a Jacobs comprehension category.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-27T17:32:02Z
Sándor Jenei
arXiv categories: math.RA, math.GR, math.LO

This paper develops a canonical decomposition--reconstruction theory for balanced residuated partially ordered semigroups. The starting point is the intrinsic local-unit map $τ(x)=x\backslash x=x/x, $ whose values are positive idempotents. The primitive fibres of this map are generally too fine to be compatible with multiplication and residuals: the local units of $xy$, $x\backslash y$, and $x/y$ need not be determined by the local units of $x$ and $y$. We therefore construct the residual coherentization $\mathcal C_{\mathrm r}(\mathbf M)$, the finest quotient of the positive-idempotent skeleton on which these three local-unit outputs are well defined at quotient level. The blocks of $\mathcal C_{\mathrm r}(\mathbf M)$ define the canonical components, while the quotient skeleton records the target component for products and residuals. Together with the component algebras, the product-shadow maps $x\mapsto xq$, and the residual-shadow maps $y\mapsto y/q$, these data reconstruct the original algebra. The final part compares this construction with subsemilattice-steady visibility decompositions. At every finite stage of the induced iterative decompositions, the partition obtained from residual coherentization is finer than the partition obtained from any subsemilattice-steady visibility choice. Equivalently, each component produced by the subsemilattice-steady construction is a union of residual-coherent components.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-30T17:00:38Z
Theofanis Aravanis, Costas D. Koutras
arXiv categories: cs.AI, cs.LO

Belief update concerns changes in an agent's beliefs induced by changes in the underlying world. Standard Katsuno-Mendelzon update assumes that an epistemic input can be incorporated from every initially possible world, whereas credibility-limited belief update restricts, for each source world, the successor worlds regarded as credible or reachable. Nevertheless, existing credibility-limited approaches treat the epistemic input as an indivisible whole, and therefore cannot represent cases in which only part of a compound epistemic input can be realized. We introduce selective credibility-limited belief update, in which the epistemic input is transformed, relative to each source world, into a weaker proxy before the credibility-limited transition is performed. We provide semantic and axiomatic characterizations of the resulting class of update operators. We then identify two well-behaved sub-classes; namely, consistency-preserving update operators, which require every transformed epistemic input to be credible from its source world whenever the original epistemic input is consistent, and maximal consistency-preserving update operators, which additionally require the selected proxy to be maximally informative among the credible consequences of the original epistemic input. Finally, we establish the generality of the proposed framework by showing that credibility-limited belief update is recovered as a special case, while Katsuno--Mendelzon belief update emerges when credibility restrictions are removed and the transformation functions are taken to be identities. These results demonstrate that the framework provides a unified and strictly more expressive account of belief update, encompassing established approaches while supporting source-dependent selective acceptance.

arXiv abstract · PDF