arXiv weekly literature review

Proof assistants and mechanized formalization · primary corpus · published 2026-08-03T09:33:20Z
Diego Marmsoler
arXiv categories: cs.LO, cs.SE

This report describes an Isabelle/HOL formalization of a STARK-style transparent proof protocol. The development contains an executable model of the prover and verifier, a finite probabilistic state monad with a weakest-precondition calculus, a zero-failure honestcompleteness theorem, and a staged soundness theorem with an explicit probability bound. The report is written for readers with a formal-methods background. It gives enough cryptographic context to explain the protocol, but its main emphasis is the formal model, the decomposition of the proofs, and the Isabelle source locations of the principal definitions and theorems.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-08-06T16:52:16Z
Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański
arXiv categories: cs.CR, cs.LO

We present HOPSCOTCH, a Lean 4 framework for mechanizing computationally sound, game-based cryptographic proofs. Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm. HOPSCOTCH uses a shallow embedding: oracles and reductions are ordinary Lean definitions, enabling direct integration with the full Lean ecosystem, including general mathematical theories from Mathlib, such as finite-group theory. A game-hopping proof in HOPSCOTCH is represented as an explicit formal object whose constructors correspond to the standard steps of a game-hopping argument, making proofs easier to construct, automate, and inspect. We prove a general computational soundness theorem that interprets these proof objects by constructing reductions against the assumptions they use and deriving a concrete bound on the advantage of any distinguisher. Observational equivalence between oracles is established using a state-abstraction methodology: a simple yet powerful approach that supports transformations such as adding or forgetting state and replacing eager sampling with lazy sampling. We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction. To the best of our knowledge, the last is the first mechanized proof of GGM for non-constant depth.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-08-09T11:30:49Z
A. Mayeux
arXiv categories: cs.LO

The paper \emph{Conjecture: the set of prime numbers is supernatural} conjectures that no non-constant function built from the identity and constants by finitely many pointwise additions, multiplications, and exponentiations maps every positive integer to a prime. We give a complete Lean~4 formalization of that paper over Mathlib: every definition, example, remark, numbered result, and experimental table row has a machine-checked counterpart, with no \lcode{sorry}. The conjecture and similar generalizations are stated exactly, as named open problems. So stated, the conjecture becomes a precise target: an automated reasoning system can now attempt a kernel-checked proof.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-08-03T14:24:12Z
Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi
arXiv categories: cs.AI, cs.LO

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-08-07T16:02:23Z
Zeru Zhu, Jinzheng Li, Yuanjie Ren, Ji Liu
arXiv categories: math.CO, cs.LO, math.SP

Kolokolnikov conjectured that, among finite simple graphs on $n$ vertices with exactly $2(n-2)$ edges, the complete bipartite graph $K_{2,n-2}$ maximizes algebraic connectivity. We prove the conjectured statement for every $n\ge123$: every such graph has algebraic connectivity at most $2$, while $K_{2,n-2}$ attains $2$. The proof begins with explicit Rayleigh-quotient certificates that exclude several local configurations from a hypothetical counterexample. A global degree count then controls the number and total excess of vertices of degree at least $5$ and bounds the edge excess of the subgraph induced by vertices of degree at most $4$. A Moore-type breadth-first-search criterion uses this excess to guarantee a short cycle, while a spectral criterion excludes cycles in the same length range. An explicit arithmetic estimate shows that the two criteria apply simultaneously once $n\ge123$. A Lean formalization covering every $n\ge4$, including the complementary range $4\le n\le122$, has been produced with MerLean and checked by the Lean kernel; the present paper gives a self-contained mathematical account of the large-order component.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-08-07T16:10:35Z
Daniel Goldberg, Antoine Vinciguerra
arXiv categories: cs.LO

We formalize the Dirichlet integral and several of its classical applications in the Lean~4 proof assistant. Since the sinc function is not Lebesgue integrable on the positive half-line, the Dirichlet integral must be represented as the limit of integrals over bounded intervals. To avoid the difficulty of removing an exponential factor from a conditionally convergent integral, we instead pass through the absolutely integrable function \(\operatorname{sinc}^2\). We evaluate its integral by differentiation under the integral sign and dominated convergence, and then recover the Dirichlet integral from an identity between truncated integrals. Using these results, we formalize the convergence of the Dirichlet cutoff to the Heaviside function and derive several quadratic and bilinear trigonometric integral identities. Finally, we formalize Lobachevsky's integral formula for continuous periodic functions satisfying a reflection symmetry, using the density of cosine polynomials obtained from Mathlib's Fourier analysis on the additive circle.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-08-07T16:25:55Z
Daniel Goldberg, Antoine Vinciguerra
arXiv categories: cs.LO

We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem proved through real-variable integration and the Dirichlet integral. As an application, we formalize the Laplace-domain solution of the harmonic oscillator and identify its transform with that of $\sin(ωt)$. We also discuss the principal analytic and formalization challenges encountered in the development.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-03T09:43:58Z
Jort van Leenen, Tobias Kappé
arXiv categories: cs.LO, cs.PL

P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus, a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence. Octopus produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample bit-stream witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes, on consumer hardware. We report on the tool's implementation and evaluate its usability in networking contexts.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE supplement · published 2026-08-03T10:03:29Z
Kexing Ji, Jiachen Liu, Enze Hu, Cuiyun Gao, Keke Lian, Yongheng Liu, Lei Zhang, Tian Dong, Hao Chen, Wang Bin
arXiv categories: cs.SE

Recent advances in LLM-based vulnerability detection have shown promising results, while coding agents further extend this capability from isolated code snippets to complete repositories. This shift requires agents to autonomously explore repositories and locate vulnerability-relevant code, instead of performing detection on preselected functions. However, existing benchmarks primarily focus on vulnerability classification over preselected code snippets, limiting their ability to evaluate coding agents in repository-level vulnerability detection. Moreover, without fine-grained vulnerability trace annotations, the capability limitations underlying the detection process remain difficult to explore. To address these limitations, we present \textbf{VulnGym}, a real-world repository-level benchmark for evaluating vulnerability detection by coding agents. VulnGym aligns reviewed GitHub advisories with their corresponding vulnerable version repositories. It contains 184 advisories and 408 vulnerability entries across 23 repositories, with each entry annotated with line-level entry points, critical operations, and vulnerability traces. Using this fine-grained ground truth, VulnGym defines an end-to-end detection task and three oracle-based subtasks to jointly evaluate vulnerability detection and diagnose limitations in code localization and evidence construction. Our evaluation indicates that current coding agents remain limited in both end-to-end repository-level vulnerability detection and the construction of accurate supporting traces.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE supplement · published 2026-08-03T10:05:08Z
Yuekun Wang, Mingfei Cheng, Xiaofei Xie
arXiv categories: cs.SE, cs.CR

LLM-based code auditors are increasingly integrated into pull-request (PR) workflows, yet their reliability against adversarial changes distributed across repository evolution remains poorly understood. We introduce PRWeaver, a benchmark of 208 execution-validated attacks from ten real-world repositories, each instantiated under four matched review renderings (832 renderings in total). We evaluate three PR-auditing agents across six auditor-model systems. Across all systems, decomposing an attack changes detection by at most five percentage points, showing that commit boundaries alone do not explain evasion. In contrast, per-PR interleaving at $N=16$ and coherent carrier fusion reduce detection by 5-13 and 10-18 points, respectively. Under whole-window review at $N=24$, detection falls to 16-22%, compared with 50-60% under per-PR review. These results show that access to repository history is insufficient: concealment becomes most effective when benign and malicious changes jointly occupy the auditor's active review context or when the stated purpose plausibly accounts for the attack-bearing diff.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-03T12:15:42Z
Oleksandr Mostovyi, Denys Symonov
arXiv categories: cs.CR, cs.PL, cs.SE

This paper proposes an explainable digital twin for vulnerability detection in AArch64 machine code without access to source code. The digital twin reproduces the concrete execution of a program and preserves the state of registers, processor flags, memory, and live allocated blocks. Each instruction is transformed into a trace event containing the instruction name, operand values, and the post-instruction state. Vulnerabilities are represented as symbolic rules in Kleene algebra with tests: each rule specifies an event sequence and predicates over the machine state. This approach enables the detection of not only isolated unsafe instructions but also multi-step execution patterns. The rules are compiled into finite automata that scan the trace without using an SMT solver. The experimental evaluation covers three CWE classes: integer overflow (CWE-190), null pointer dereference (CWE-476), and heap buffer overflow (CWE-122). The system detected all three predefined vulnerabilities and produced no report on the safe trace. Each detection result includes the triggered rule, the trace position, and the concrete state values, thereby providing a reproducible explanation.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE supplement · published 2026-08-04T05:03:11Z
Sungju Yun, Sijune Hwang, Yeonjoon Lee, Kyungtae Kang, Sungbin Park
arXiv categories: cs.CR, cs.SE

Detecting source code vulnerabilities is increasingly difficult as modern security flaws are rooted in complex causal dependencies between execution flows, control conditions, and program states. Despite recent advances in Large Language Models (LLMs) and multi-agent frameworks, existing approaches primarily address superficial similarities between benign and vulnerable functions while failing to capture the complex causal dependencies inherent in security flaws. To address these limitations, we propose Causal Context-based Agentic Reasoning (CLEAR), a novel multi-agent vulnerability detection framework integrated with a causal knowledge graph. CLEAR systematically constructs a Vulnerability Causal Knowledge Graph (VCKG) that models the causal chains between entrypoints, preconditions, root causes, and fix intents across vulnerability instances. Leveraging this structured knowledge, four specialized agents, including the Collector, Claim, Critic, and Judge, collaboratively verify vulnerability hypotheses through retrieved causal contexts. Experimental results on C/C++ and Java vulnerability benchmarks demonstrate that CLEAR improves Pair-Correct (P-C) performance by 130.7% and 71.56% over state-of-the-art approaches, demonstrating the effectiveness of causal knowledge graph-guided reasoning for automated vulnerability detection.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-04T15:45:31Z
Sajjad Khan
arXiv categories: cs.LG, cs.DC, cs.LO, cs.SE

A framework that persists execution state so a run can be interrupted, survive a crash, and continue must decide what a resume means for effects that already happened. Five widely deployed agent workflow frameworks answer differently, none exposes a machine-checkable contract, and measured behavior violates even the fragments they state. The RESUME CONTRACT states six properties over the persistence API (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism), plus fork-intent and liveness obligations. A TLA+ model checks a reference semantics exhaustively, unchanged at scaled bounds (7.4 million states), and the reference conjunction is additionally TLAPS-proved unbounded (196 obligations); a 39-cell fault matrix and two companion modules yield the separating models independence requires. A deterministic, LLM-free harness measures them at pinned releases. LangGraph 1.2.9 durably records a second resume value and never consults it, persists schema-invalid state silently, and re-executes durably recorded work after a real SIGKILL: exactly-once across interrupts, at-least-once across crashes, on one API. CrewAI 1.15.2 re-executes completed effect-bearing methods against its written claim; pydantic-graph 1.x cannot resume after a mid-node crash; no two probed frameworks share a conformance profile. Consume-once holds sequentially and fails under concurrent delivery: k processes resuming one parked interrupt fire the gated effect k times, saturation 1.0 in 36 of 40 cells, and the failure crosses hosts. REMIT, a reference sequencer whose Verus-verified recovery core is line-identical to the shipped executable, repairs the fork and validity cells. The cross-process cell is repaired at the read path: an opt-in gate claims consumption in the shared store, serving one racer and refusing the rest before any node executes.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-05T05:39:05Z
Zinan Gu, Peisen Yao, Kui Ren
arXiv categories: cs.PL

Pointer analysis is a cornerstone of numerous static analysis applications, including compiler optimizations, slicing, bug detection, and verification. While offline simplification is a common approach to boosting performance, existing methods are often tightly coupled to specific analysis algorithms and limited to a set of simplification rules. This paper explores a new perspective: applying semantic-preserving compiler optimizations directly to intermediate representation (IR) before pointer analysis. This strategy is modular, analysis-agnostic, and easily integrates with existing tools. We conduct an empirical study using diverse programs and three pointer analyses. The results show substantial performance gains---up to 3.14x speedup and 1.94x memory reduction---while precision remains largely unchanged. We also analyze the trade-offs between optimization overhead and analysis speedup, quantify changes in IR structure, assess the characteristics of optimization configurations, and identify promising directions for future research.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-05T14:10:51Z
Matthias Hetzenberger, Georg Moser, Florian Zuleger
arXiv categories: cs.LO

Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs. In this paper, we present a cost-aware probability monad for \LH/ that supports reasoning about probabilistic programs together with their expected costs. Our approach combines executable probabilistic programs with refinement-type-based verification and SMT-supported automation. The monad intrinsically tracks probability mass, expected values, and expected costs through refinement types, enabling many quantitative properties of probabilistic computations to be inferred compositionally from program structure. We evaluate our approach on several classical probabilistic algorithms and data structures, including meldable heaps, randomised quicksort and quickselect, randomised splay trees, random permutations, and the hiring problem. The case studies demonstrate different points along the spectrum between automated and interactive verification.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-07T09:39:06Z
Zinan Gu, Haoxiang Yan, Peisen Yao
arXiv categories: cs.PL

Static program analysis infers program properties automatically. Yet precise interprocedural analysis remains challenging, and dynamically typed languages amplify the difficulty. Python is particularly problematic: dynamic dispatch, first-class functions, metaprogramming, pervasive exceptions, and an object model based on descriptors and attribute-driven lookup collectively impede precise reasoning. We present PyFlow, a generic IFDS-based static-analysis framework for Python. PyFlow provides a multi-stage intermediate-representation pipeline and a generic IFDS solver parameterized by abstract domains. Analysis developers implement only the dataflow semantics; the framework constructs the supergraph, performs fixed-point iteration, and caches summaries. We implement a taint analysis in \pyflow and evaluate it against eight Python SAST tools (DevSkim, Dlint, Bandit, Bearer, CodeQL, Pysa, Semgrep, and Snyk) on the synthetic and real-world benchmarks from a recent ICSE~'26 study. On the synthetic benchmark, PyFlow achieves the best aggregate recall and F1 score among all nine tools. On the real-world benchmark, it attains the highest recall and F1 score while maintaining precision competitive with taint-based engines. We conclude with lessons learned from building IFDS analyses for Python.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-07T22:23:49Z
Shabnam Ghasemirad, Christoph Sprenger, Si Liu, David Basin
arXiv categories: cs.PL, cs.DB, cs.DC, cs.LO

We present a mathematically rigorous, systematic approach for the verification of database isolation guarantees, which (i) supports a spectrum of seven isolation levels, (ii) uncovers a fundamental dichotomy among isolation levels: stronger levels can be verified via refinement alone, whereas weaker levels additionally require reduction, and (iii) provides a hierarchy of abstract models that substantially simplifies proofs by factoring out their most labor-intensive parts. In particular, we eliminate the need for per-protocol reduction proofs for the weaker class of isolation levels by performing a once-and-for-all reduction at a high level of abstraction in our hierarchy. To achieve this, we develop and apply a generic theory of reduction, which is also of more general interest. Overall, our approach minimizes the user's proof effort to a single, simpler refinement of the most concrete model in our hierarchy. All our results are formalized in Isabelle/HOL.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-09T18:47:27Z
Konstantin Britikov, Martin Blicha, Grigory Fedyukovich, Natasha Sharygina
arXiv categories: cs.LO

Termination and nontermination of infinite-state systems are complementary problems that, despite their close connection, are typically addressed by separate techniques. The core idea of this paper is to connect termination and nontermination analysis, enabling the two to share intermediate results and guide one another. We present a new termination analysis approach based on the generation of well-founded transition invariants. It leverages Craig interpolation for transition invariant generation, capturing the structural reasons for termination. The proposed technique extends safety-based nontermination analysis, enabling it to prove both termination and nontermination within a unified framework. We implemented our approach in the GOLEM verification framework and evaluated it on benchmarks from the Termination Competition (TermComp). Empirical results demonstrate that combining termination and nontermination is beneficial and yields performance comparable to state-of-the-art tools.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-03T17:58:34Z
Rémy Cerda, Ugo Dal Lago
arXiv categories: cs.LO, cs.PL

We show that the tropical semiring over the natural numbers, when used as the grading space in graded coeffect typing, faithfully models the passage of time while simultaneously guaranteeing productivity of well-typed programs. A grade a, when assigned to a function parameter, indicates that the parameter is not necessarily available immediately, but will become available after a time steps. We investigate this idea through two formal systems. We first introduce a graded type system featuring recursive and polymorphic types, and show that, in this setting, a natural restriction on recursive types is sufficient to guarantee productivity, while still allowing the definition of streams and recursive programs on them. In particular, we prove that Nakano's later modality can be embedded directly into our system. We then show that tropical grading naturally suggests a novel form of intersection typing, in which the role traditionally played by sets or multisets of types is instead taken by "timed" sets, i.e., functions assigning to each type A the earliest time, represented as a grade, from which the underlying term is available with type A. For the resulting system, we prove not only that productivity is guaranteed, but that it is also characterized: the typable terms are exactly those with hereditarily head normal forms. Remarkably, the system is recursion-theoretically optimal, i.e., typability can be directly proved to be a $Π_0^2$ property in the arithmetical hierarchy.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-04T06:00:40Z
Akimasa Morihata
arXiv categories: cs.FL, cs.PL

Most of the conventional implementations of regular expressions are based on backtracking. Such implementations are slow in the worst case, and thus, we would like to develop a better matching algorithm. However, it is nontrivial to provide an efficient matching algorithm that can deal with practical extensions including submatch addressing. This paper studies regular expression with lookaheads and negative lookaheads, abbreviated to REwLA. First, we propose a transformation from a REwLA of size $m$ to a deterministic finite automaton of $\mr{O}(2^{2^m})$ states. Next, we consider weighted regular expressions, which enable us to calculate submatch addressing. We propose a transformation from a weighted REwLA of size $m$ to a weighted nondeterministic finite automaton of $\mr{O}(2^{2^m})$ states.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-05T05:28:22Z
Hans-Martin Will, Allen L. Brown, Matthew Fuchs
arXiv categories: cs.DB, cs.AI, cs.LO

As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars: a dependent type theory woven through the core, institutions acting as strongly typed integration boundaries, and a content-addressed immutable storage layer. On this foundation, epistemic status (declared/observed/derived/verified) is enforced as a strict commit-time invariant. Cross-system translations (comorphisms) are checked at commit and materialized directly into the graph as durable, first-class resources. To eliminate O(N^2) polystore bottlenecks, shared on-chain intermediate representations (IRs) collapse multi-system translations to identity. Crucially, this architecture unifies both domains of scientific epistemology: it relies on justification logic for empirical science, while embedding a fast, in-process term checker to safely evaluate formal mathematical proofs (via Lean 4) without IPC overhead. In an end-to-end recomputation of a published Nature study from fragile scripts to a materialized evidence graph, all 52 derived conclusions hold from pinned data, surfacing four machine-checked discrepancies in the original study.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-08T03:27:53Z
Yuito Murase, Atsushi Igarashi
arXiv categories: cs.PL

MetaML-style multi-stage programming (MSP) supports quasi-quotation-based code generation, runtime execution of generated code, and cross-stage persistence (CSP). However, its interaction with computational effects is subtle: mutable state can cause scope extrusion, where generated code escapes the scope of variables on which it depends. This paper presents a type system for MetaML-style MSP with mutable state that statically rules out harmful scope extrusion while supporting multi-level code generation, runtime execution, and a variant of CSP. Our system builds on refined environment classifiers (RECs), a discipline that annotates code types with the variable scopes on which generated code depends. To scale RECs to the MetaML-style setting, we refine classifiers so that they track not only variable scopes, but also the scopes of classifiers themselves. Further, we integrated polymorphism over classifiers, enabling more general and reusable code generation patterns in a multi-level setting. For the resulting system, we define an operational semantics via a definitional interpreter and prove type soundness and safety of offline code generation, showing that generated code can be extracted as standalone well-typed programs. We provide working implementations and mechanized proofs in Rocq.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-03T00:42:55Z
Dzmitry Malyshau
arXiv categories: cs.LG, cs.DC, cs.PL

Training and deployed inference often cross export, conversion, and platform-specific runtime boundaries. Meganeura asks whether one compact native compiler can span both phases on consumer GPUs. Its typed static graph, automatic differentiation, optimizer, checkpoint, memory planner, and runtime lower specialized programs through Vulkan and Metal. We compare five matched workloads with PyTorch on NVIDIA and AMD discrete GPUs, an AMD APU, Apple silicon, and an Intel iGPU. The protocol separates strict f32 from validated fast paths and gates forward and backward independently. Forty-eight of 50 device-workload-mode cells pass both gates; the other two share one unresolved backward-reference disagreement on a newly supported APU. In strict f32, Meganeura wins 12 of 20 GPU-referenced minimal-latency cells and has a median valid training gap of 1.8x. On the discrete AMD GPU, four of five inference workloads are within 1.10x of compiled ROCm PyTorch and three training workloads are faster. Under accelerated contracts, the worst training gap is 4.6x. Compilation takes 0.1-2.4 seconds versus 6-96 seconds for torch.compile on supported GPU paths; the stripped binary is 13 MiB. Dispatch profiles localize the largest gaps to convolution derivatives and attention backward. A physical Android XR case study transfers a Meganeura-trained decoder into an Adreno/OpenXR application sharing the graphics queue. The results show that general consumer graphics APIs can support a compact shared train-to-deploy stack at useful, sometimes vendor-competitive performance. The measured gaps point to kernel coverage, scheduling, and arithmetic policy rather than an identified API limitation.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-03T12:42:55Z
Jieke Shi, Junda He, Wenjia Jiang, Weifeng Sun, Shidong Pan, Zhensu Sun, Chengran Yang, Peixin Zhang, Yifan Jia, Zhou Yang, Thong Hoang, Xiwei Xu, Zhenchang Xing, David Lo
arXiv categories: cs.SE, cs.AI, cs.PL

Model checkpoints are growing in both number and size, which makes archival, transfer, and deployment increasingly costly. General-purpose compressors can reduce storage requirements but ignore tensor structure, whereas existing tensor-specific compressors rely on fixed and format-specific pipelines. We present Brevis, which formulates lossless tensor compression as program synthesis. We design a typed domain-specific language (DSL) that captures recurring tensor structures, such as repeated regions and floating-point fields, through a set of reversible operators. Given a tensor, Brevis synthesizes a self-contained DSL program that reconstructs it bit-exactly. A checkpoint-specific production prior, learned from a small representative sample of tensors, guides a bounded A* search to synthesize compact programs, which can later be executed directly for bit-exact decompression. On 10 public checkpoints spanning language, audio, and image generation models, Brevis reduces 2.13 TB of checkpoint data to 1.41 TB, a 33.93% storage reduction. It produces archives up to 30.87% smaller than those of four general-purpose compressors, including zstd and gzip, and smaller archives than the tensor-specific compressors ZipNN and DFloat11. Under a practical concurrency configuration, Brevis achieves 3.60 GB/s compression and 6.61 GB/s decompression while preserving every source byte.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-04T11:13:13Z
Nicklas Nidhögg
arXiv categories: cs.FL, cs.DC, cs.PL

Table-driven DFA lexing is sequential: each transition depends on the previous byte's state. Scanning one input in parallel needs each chunk's entry state, which existing methods recover by simulation, speculation, prescanning, or overlap. We give two conditions under which none is needed. For a longest-match scanner restarting from q0 at every token boundary, a byte b is a certified split symbol when no reachable state other than q0 has a b-transition whose target can reach acceptance, and q0 is not re-entrant if it has one. Every occurrence of such a byte in completely tokenizable input begins a token, so chunks starting there reproduce the serial sequence of kinds and lengths by ordered concatenation. The condition is necessary as well as sufficient, and fragile: one string, comment, or whitespace run can eliminate every useful certificate, and comments and whitespace are usually discarded. We therefore weaken the guarantee to equality after deleting a declared discarded set, and give a second condition, sound and strictly more permissive but conservative rather than exact, decided from the same tables, answered by a second constant-time one-bit query. It recovers newline for a conventional C-like tokenization and tab, newline and carriage return for JSON, without altering their token definitions, and refuses it where block comments are unrestricted. It ships as a query only: the library's planner and every measurement here use the exact condition, so a caller must plan boundaries itself. Splitting at exact certificates in the munch library reaches 92.6-95.3% parallel efficiency at eight threads on a restricted CPU set, on a 512 MiB dense corpus beyond last-level cache, and a 3.46-3.94x end-to-end speedup at four threads, across two benchmark revisions on one machine. It turns delimiter-based parallel lexing from a language-specific assumption into a property a compiler checks.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-04T22:51:25Z
Yugo Otani, Sosuke Moriguchi, Takuo Watanabe
arXiv categories: cs.PL, cs.SE

Emfrp is a functional reactive programming (FRP) language designed for small-scale embedded systems. Time-varying values are the primary abstraction mechanism in FRP and enable concise descriptions of reactive behavior. In practice, however, Emfrp programs are compiled into C and combined with platform-dependent input/output components written in C or C++. Consequently, developers must debug the resulting mixed C/C++ program using conventional debuggers such as GDB, even though the application logic is written in Emfrp. This situation creates an abstraction gap between the source-level FRP program and the executable system. This paper presents a multi-mode debugging framework for Emfrp-based embedded applications. The framework supports debugging at the level of Emfrp abstractions while also allowing inspection of platform-specific C/C++ I/O code. Our approach uses a source code mapping technique that relates Emfrp constructs to corresponding locations in the compiled program. A case study on an ESP32 microcontroller using representative debugging scenarios demonstrates improved debugging efficiency.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-05T22:53:39Z
Zhengyao Lin, Yi Cai, Milijana Surbatovich
arXiv categories: cs.PL, cs.LO

Dataflow architectures have gained renewed interest due to their balance between power efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, which greatly improves data locality and parallelism. However, compiling to dataflow architectures remains an error-prone process, in order to maintain determinacy while enabling pipelining. Determinacy means that the result of a dataflow program is deterministic and independent of the schedule of operator execution, and pipelining is an important optimization in spatial dataflow that enables parallelism across loop iterations. In this work, we present Wavelet, the first effort to formally verify a compiler for asynchronous dataflow. We use a mix of techniques to achieve this goal. Our frontend uses a novel capability type system with fences to synchronize conflicting memory accesses and enable pipelining. We then verify a Lean formalization of two core passes of our compiler that translates elaborated programs from the type checker to dataflow graphs, proving important properties of forward simulation and determinacy. Notably, our formalization semantically propagates the soundness guarantees of the frontend type system, ensuring modularity between simulation and determinacy proofs. In evaluation, we show that dataflow graphs compiled by Wavelet have comparable sizes to those produced by an unverified optimizing compiler for the RipTide spatial dataflow architecture.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-08T07:01:59Z
Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, Margo Seltzer
arXiv categories: cs.OS, cs.CR, cs.PL

Security is among the top concerns of operating system (OS) developers. A secure runtime environment relies on the OS to correctly configure the memory hardware on which it runs. This is mission-critical as it provides essential security-relevant features and abstractions that ensure the integrity and isolation of untrusted applications running alongside each other. Configuring a platform's memory hardware is not a one-off effort as designers constantly develop new mechanisms for translation and protection with different features and means of configuration. Adapting the OS code to the new hardware is not only a manual, repetitive and time consuming task, it may also introduce subtle, but security critical bugs that break security and isolation guarantees. We present Velosiraptor, a system that automatically generates correct, low-level OS code that programs the memory hardware of a machine. Velosiraptor leverages software synthesis techniques and exploits the domain specificity of the problem to make the synthesis process efficient. With Velosiraptor, developers write only a high-level description of the memory hardware's mapping behavior and OS environment. The Velosiraptor toolchain transforms this specification into a verified implementation that can be linked directly with the rest of the operating system. Incorporating the OS environment into this process allows porting an OS to new hardware platforms without worrying about writing code to configure the memory hardware. We can also use the same specification to generate hardware components. This enables research in new translation mechanisms, freeing up OS developers from manually writing OS code.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-08T07:15:48Z
Huiling Wu, Yuxin Deng
arXiv categories: cs.PL

Quantum oracles are essential to many quantum algorithms, and their specifications may involve recursive control flow that depends on runtime quantum data. However, existing reversible compilation frameworks provide limited support for such quantum-controlled recursive structures. We present ReOC, a compilation framework that transforms high-level recursive oracle specifications with quantum control flow into reversible quantum programs. The framework comprises RQIMP, a high-level imperative source language for specifying recursive oracles, and a method of compiling programs in that language into RQC++, an existing high-level quantum recursive language with quantum control flow. In this way, we avoid the tedious and error-prone process of directly writing quantum oracles in RQC++. To manage static storage under dynamic quantum control, ReOC uses an indexed static-register discipline to isolate live variables across recursion layers, enabling safe register reuse while controlling quantum storage usage. Furthermore, to address the exponential time blow-up caused by naive uncomputation in recursive settings, ReOC employs a recursion-aware uncomputation strategy: temporary variables from recursive calls are cleaned using deferred strategies to control time overhead, while those from non-recursive statements are cleaned eagerly to reduce space usage. For linear recursion, this strategy yields overhead linear in recursion depth, parameterized by the per-layer register footprint and primitive-operation costs. Finally, we provide a mathematical proof of compilation correctness from RQIMP to RQC++, establishing semantic preservation and correct uncomputation of temporary quantum variables.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-08T18:39:16Z
Petr Korolev
arXiv categories: cs.CV, cs.DC, cs.PF, cs.PL

GPU language comparisons are almost always run on tiled dense linear algebra, where every toolchain is good and the differences are small. We implement the same hash-blocked TSDF fusion kernel in CUDA C++, in Rust through NVIDIA's cuda-oxide, and in Triton, and measure it on a workload with the opposite character: an open-addressed hash table with compare-exchange insertion, data-dependent per-lane probe depth, and contended scatter. The result is a split. On the regular stage, which walks a truncation band and accumulates, all three languages land within a small factor of each other. On the irregular stage, which probes and inserts, Rust stays close to hand-written CUDA C++ while Triton is more than an order of magnitude slower. Language choice is nearly free on the work that is usually benchmarked and expensive on the work that is not. We attribute both gaps to specific things the languages cannot express, not to ratios. Triton's cost follows from a probe loop that must run to a compile-time bound and from tl.atomic_cas taking no mask, which forces a scratch structure with no counterpart in CUDA. Rust's cost was invisible in every instruction count: its kernel issues fewer instructions, fewer compare-exchanges and fewer registers at identical occupancy, yet was slower. Hardware counters located it in L1 residency. A GPU-scope atomic load must be coherent across SMs, no NVIDIA L1 is, so the type-correct way to read a shared location bypasses the cache on every access. Triton's bounded probe is also a correctness problem for fusion: at load factors an ordinary depth trajectory reaches, it silently discards blocks and the reconstruction loses patches of surface with nothing reported. We also report a defect found and fixed in cuda-oxide itself, now merged upstream: its scoped atomic load and store could not be called at all in the build mode that produces real kernels.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-09T15:28:10Z
Xiaoquan Xu, Chenke Liu, Boning Meng, Zihao Shen, Li Zhou
arXiv categories: cs.PL, quant-ph

The management of ancilla qubits has become a critical technique for reducing quantum circuit width. Dirty ancillas, which may be borrowed from any temporarily idle qubit regardless of their initial states, offer substantial flexibility for width optimization, but their use has so far required manual and error-prone handling. We formalize the dirty-qubit borrowing problem and establish a fundamental computational limit by proving its NP-hardness. To support practical optimization, we present \bona, the first scheduler for dirty-qubit borrowing, built on a novel depth-aware heuristic algorithm. We evaluate \bona~ across a variety of benchmarks, including practical quantum circuits and randomly arranged compositions of real circuit modules, and find that it reduces nearly 99\% of dirty ancillas on average with controlled depth overhead. In particular, for parallel quantum walk---an essential component of parallel Hamiltonian simulation---\bona~ matches the circuit width achieved by the clean-qubit schemes of \citeauthor{jiang2024recycling}~(\citeyear{jiang2024recycling}) and \citeauthor{quantinuum}~(\citeyear{quantinuum}), but attains significantly smaller circuit depth, providing concrete evidence that dirty ancillas offer unique optimization advantages in circuits with certain parallelism.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-03T01:05:06Z
Salma El Yadouni, Guanyi Li
arXiv categories: cs.SE, cs.AI, cs.LG

Tool-using language-model agents repeatedly rediscover procedures they have already executed, producing traces that mix reusable structure with retries, exploration, accidental ordering, and repeated lookups. We present TraceCompiler, a skill-guided system that mines clusters of noisy agent traces and compiles them into executable, mostly deterministic workflows. It admits an inter-tool dependency only when a consumer argument contains a value attributable uniquely to an earlier producer; every hard edge carries an auditable evidence tuple, and ambiguous relations are marked suspected and impose no ordering constraint. Bindings are classified as constants, user inputs, copied outputs, transforms, or residual LLM decisions. On T1, a mechanized form of the rule recovers producer-consumer dependencies at 0.928 precision and 0.943 recall over 15,775 def-use edges of its training split, against 0.711 F1 for adjacency and 0.712 for a frequency-thresholded directly-follows measure on identical data; the compiler skill run blind reaches 0.992 on 250 of those edges. On AppWorld we replay released trajectories in the deterministic simulator to recover masked return values and measure the rule against 563 token edges at 0.993 precision - a self-consistency check, since replay injects tokens by a related heuristic. We compile two recurring intents: a Venmo money-request intent reduces 34 observed API calls to 11 runtime calls and, under leave-one-out execution against the benchmark's own state tests, passes 15 of 21, the failing fold escalating rather than acting because its required branch was never observed; and a Spotify/Todoist intent the compiler correctly refuses to compile, because an irreversible side effect is under-determined. We measure call reduction but not offline compilation cost, so we claim no net efficiency result.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-03T02:22:02Z
Logan Ritchie, Sushant Mehta, Liudas Panavas, Edwin Chen
arXiv categories: cs.AI, cs.SE

Long-horizon tasks require agents to maintain coherent state and goals across nested and branching work. We call this capability goal-directed execution (GDE): the repeated application of four behaviors, namely selecting goals, constructing task-relevant state, maintaining fidelity to higher-level objectives, and verifying completion against the environment. We hypothesize that long-horizon post-training strengthens these behaviors across domains. We test this by post-training Qwen3.5-122B-A10B on 363 Long-Horizon Multi-Tool Agent (LHMTA) tasks drawn from office workflows. The collection contained no software-engineering tasks, yet the model's pass@1 improved by 5.8 points on SWE-Bench Pro. Matched trajectory analysis shows gains in all four GDE behaviors in both office workflows and software repositories. Aggregate SWE-Bench Pro statistics showed related changes in information gathering, implementation, and verification. Together, the results support a behavioral interpretation in which long-horizon post-training changed how the model organized and applied knowledge across tasks, with effects extending beyond the training domain.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-03T05:24:03Z
Shuyang Xie, Shuxiao Xie, Feng Zhu, Yanli Ji, Wangmeng Zuo
arXiv categories: cs.SE, cs.AI

Online-judge verdicts and the datasets and benchmarks built on them are treated as ground truth for evaluating and training large language models for code. Yet prior audits have sounded a warning: official suites accept buggy submissions. These audits, however, stop at the warning and offer no practical remedy. Our remedy has two parts: an off-the-shelf coding agent, serving as a test-suite auditor, both builds adversarial test suites to expose what official suites miss and supplies these suites where no official suite exists; a certification chain determines whether each agent-flagged submission is genuinely buggy without relying on the official judge: multiple independently written accepted solutions agree on the expected output for every test, brute-force solutions settle disagreements, and a per-problem validator certifies each failing input legal. One such agent identifies 589 verified accepted-but-buggy submissions among AtCoder's 20,375 audited accepted submissions; extending the same certification to all five agents yields a union floor of 906 such submissions. Five agents, scored separately, each stay within 1.7pp of official-suite coverage on logic bugs those suites catch. On post-cutoff Codeforces problems with no available official suites, the same test-building method leads all five reproduced baselines at every tested input budget. Where an official suite exists, the agent audits suite adequacy instead of assuming it; where none exists, agent suites catch the most buggy submissions among methods we reproduced and tested.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-03T06:34:31Z
Kaustuv Mukherji, Jaikrishna Manojkumar Patil, Colton Payne, Paulo Shakarian, Dana Warmsley, Nigel Stepp, Evelyn Kim
arXiv categories: cs.CR, cs.AI, cs.LO, cs.SE

Large language models are increasingly used to reason about software vulnerabilities, but their outputs can silently violate domain knowledge, limiting their reliability in safety-critical settings such as medical devices. Prior work either treats that output as a prediction to be scored or constrains it to walks within a single knowledge graph; neither checks whether reasoning over a binary is consistent with an independent body of domain knowledge. We present EntailLLM, which validates each LLM-proposed analyst path by entailment: the path is a traversal of the binary's function call graph, the domain knowledge is represented in a separate graph, and verification aligns the two under temporal annotated logic. Across three CWE classes, four LLMs, three prompting strategies, and seven binaries varying in size from 405 to 12,696 function call-graph nodes, domain knowledge raises pooled entailment from 78% to 98%, with entailment decreasing in only 3% of the experiments. EntailLLM is deployed end-to-end on real medical-device binaries, reaching 98% pooled entailment without per-device tuning. Our system inherits the formal guarantees of generalized annotated logic, providing logical verification of LLM output that is both explainable and grounded in well-defined semantics.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-03T08:10:15Z
Kyutae Park, Jungwon Kim, Daeyeol Shim
arXiv categories: cs.CR, cs.SE

AI coding agents accept free-form natural language prompts that may inadvertently contain credentials, personally identifiable information (PII), or proprietary business data. Existing data loss prevention (DLP) solutions rely on rigid regex patterns, model fine-tuning, or vendor-managed classifiers with limited customizability. We present PolicyGuard, a pre-model interception framework that classifies user prompts using an LLM guided by a natural language policy file. Our key contributions are: (1) the policy-as-prompt paradigm, where DLP classification criteria are defined entirely in a plaintext policy document editable by non-engineers without code changes or model retraining; (2) a sealed evaluation protocol with template-family-level data splits, hidden holdouts, and frozen test sets to rigorously assess generalization; and (3) a comprehensive empirical evaluation across 2,000 multilingual prompts demonstrating 96.5% effective block rate (EBR) with only 3.0% false positive rate (FPR) on a frozen test set of 927 prompts, and perfect 100% accuracy on a 217-prompt hidden holdout. Information-matched baseline experiments show that PolicyGuard's natural language format significantly outperforms equivalent content in JSON format (McNemar chi-squared = 31.58, p < 0.001) and dramatically outperforms zero-shot classification (Cohen's h = 0.915). Cross-model portability experiments demonstrate that the same policy achieves 86.4-96.5% EBR across four different LLMs without modification.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-03T09:00:49Z
Zhongxin Liu, Zhonghao Jiang, Zhifan Ye, Haoye Wang, Jiakun Liu, Xiaoxue Ren
arXiv categories: cs.SE, cs.AI

LLM-based repository-level code generation aims to generate code using the context available in a software repository, requiring LLMs to reason over complex code dependencies. Due to limited context windows and insufficient repository-specific understanding, LLMs typically rely on retrieval-augmented generation (RAG) to incorporate relevant code. Early RAG approaches primarily employ similarity-based retrieval, which often fails to retrieve code snippets that the target function depends on. Recent work introduces graph-based retrieval to model such dependencies, but typically relies on manually designed rules and static global graphs, leading to limited flexibility and high construction and maintenance costs. In contrast, human developers collect helpful context by implicitly constructing a partial dependency graph and iteratively inspecting along it. Inspired by this behavior, we propose DyRetriever, an efficient context retrieval method via partial dependency graphs. DyRetriever uses an LLM to first select a set of entry-point functions and then perform multi-hop reasoning along the code dependency graph. During multi-hop reasoning, it uses the LLM's semantic understanding to validate whether a function can help generate the target function, eliminating manually designed rules and enabling flexibility across scenarios. Instead of statically constructing a global dependency graph, DyRetriever builds a partial graph on demand and discards it after use, reducing construction and maintenance costs. We integrate DyRetriever with a similarity-based code retriever to build DyCoder and evaluate it on CoderEval and DevEval. Experimental results show that DyCoder achieves relative Pass@1 improvements of 25.63% and 59.73% on CoderEval and DevEval, respectively, compared with existing RAG-based methods, while being 7.4x faster than baselines based on static dependency graph construction.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-03T16:34:46Z
Sunny Dubey
arXiv categories: cs.AI, cs.LG, cs.SE

LLM agents fail mid-episode -- they loop, cascade tool errors, drift off goal, fabricate results, or silently absorb corrupted content -- and the standard remedy, judging every step with a second LLM, costs more than the agent itself. We ask how much detection is achievable from observable step telemetry alone, using monitors costing microseconds per step and trained only on healthy runs. On 2,823 committed agent episodes across three frameworks, three local models (qwen2.5 7b/3b, llama3.1 8b) and a commercial API (gemini-2.5-flash), a one-class echo-state-network ensemble with CUSUM alarms detects 0.71 of failures at a 5% false-alarm budget (AUROC 0.872). Its advantage over a memoryless baseline is a monotone function of post-onset horizon (+0.09 at <=3 steps, +0.40 at >=9), predicting its own failure region out of sample on AFTraj-2K. Ranking transfers with no retraining to two corpora from other groups (AFTraj-2K 0.745, ATBench 0.779). Monitors carry two burdens: a per-deployment healthy null (they do not transfer -- AUROC 0.527 cold against 0.885 recalibrated) and a residual false-alarm rate. We add a layer carrying neither: deterministic verification, which recomputes a run's stated total from the tool results it actually received and confirms every required call was made. Head-to-head it catches 60% of failures (96% with the coverage check) at 0 of 63 false positives against the monitor's 54% at 17%, transfers unchanged to llama3.1:8b (110 of 110 at 0 of 10), and trips on 0 of 1825 healthy episodes. Detection is then closed into repair: each flagged run is rolled back and re-run live, recovering 45% of failures against a 16% resampling control (p=0.0005) and lifting task success from 52% to 73% for about one extra model call per run. The system runs at ~200 microseconds per step, three orders of magnitude below a judge call. Code, traces and results are released.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE supplement · published 2026-08-04T06:01:14Z
Xiaonan Xu, Wenjing Wu
arXiv categories: cs.CR, cs.SE

Language-model agents that execute multi-step workflows through tool calls operate under access-control policies that restrict which operations each role may perform. The APIs serving these agents expose a reasoning-effort parameter that operators adjust for cost and latency. Whether this parameter also changes the rate of unauthorized tool use has not been tested by direct manipulation within a single model. We vary reasoning effort (low, max) inside GPT-5.6 across the 14 confirmatory scenarios of TRIO-20, a suite of 20 matched workplace triads in which a policy-prohibited tool call is effective and its effect on the target metric is stated in the environment, effective but discoverable only through rule inspection, or ineffective. The three conditions derive from one code base and differ in two configuration fields, with identical prompts and tool sets. All analyses were prespecified in a frozen plan before confirmatory collection. Across 840 trajectories and two model tiers, no unauthorized tool call occurred. Exact one-sided 95% limits place each arm's violation rate below 3.50% (Terra, n = 84) and 5.21% (Sol, n = 56). The interaction estimand, with a simultaneous exact 95% interval of $\pm 4.34$ percentage points on Terra, lies inside the $\pm 7.01$-point equivalence margin. Raising effort did change behaviour, but only in inspection: rule-probe rates rose in all conditions, most where probing carried no instrumental payoff, a pattern inconsistent with the hypothesis of targeted search ($-14.3$ points, 95% CI $-27.4$ to $+1.2$). Raw trajectories are released at https://github.com/WenJing95/trio-20.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-04T12:42:11Z
Corrado Priami
arXiv categories: cs.PL, cs.AI, cs.SE

AI coding agents are stochastic workflows: prompts are interpreted, artifacts are sampled, validators produce observations, and orchestrators commit or repair. Small prompt or specification changes can therefore alter program-behavior distributions even when the texts appear synonymous. Existing systems evaluate correctness, but lack a compositional criterion for safely replacing a prompt, contract, generator, or program inside a complete agentic workflow. We introduce GenOS, a probabilistic operational semantics for this replacement problem. Each layer is modeled as a Markov kernel, and each interface carries an observer-relative equivalence. We prove that equivalence-compatible kernels descend to quotient classes and that quotienting commutes with distributional extension and sequential composition. Hence, equivalent prompts induce equal probabilities for all downstream equivalence-closed events, including verified commit. We also establish workflow bisimulation, guarded-commit safety under sound validation, total-variation non-expansiveness, and an additive robustness bound that attributes approximation error to individual pipeline layers. An executable insertion-sort audit instantiates the theory with natural-language paraphrases, a formal contract, six programs, two observers, and exhaustive execution on 121 inputs. Equivalent prompts yield identical code-class and commit distributions; a prompt assigning 5% probability to an in-place contract is distinguished by a mutation observer, while downstream distances remain within the predicted bound. Across 20,000 randomized finite-kernel trials, no exact or approximate law is violated. GenOS is model-parametric: compatibility is a measurable property to test, not an assumption about language-model behavior.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-04T17:47:25Z
Hailong Jiang, Feng Yu, Emran Hossain, Jianfeng Zhu, Mengfei Ren, Qiang Guan, Chunwei Xia
arXiv categories: cs.PL, cs.AI

Optimizing compilers miss profitable transformations when their enabling semantics are absent from the analyzed program representation. We ask whether large language models (LLMs) can recover such semantics from heterogeneous C/C++ context and realize them as validated, contract-preserving artifacts. We introduce SeGaBench, an executable benchmark containing 100 synthetic and 20 source-backed cases spanning low-level assumptions, data-structure invariants, and high-level semantic lifting. Each case includes hidden enabling semantics, an oracle artifact, correctness and semantic validators, and a reproducible performance protocol. We evaluate five LLMs using five independent responses per case. The strongest model produces correct artifacts in 94.8% of responses, achieves at least 1.05x speedup in 83.3%, and obtains a performance success on 93.3% of cases. Nevertheless, correct artifacts often close only part of the oracle gap. These results show that LLMs can complement compiler analysis as speculative semantic proposers, provided that their artifacts are validated and evaluated.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-05T13:37:25Z
Louis Mandel, Guillaume Baudart, Mandana Vaziri, Martin Hirzel
arXiv categories: cs.LG, cs.PL

Building reliable applications that leverage large language models (LLMs) remains a significant challenge. While LLMs offer impressive capabilities across diverse tasks, their outputs often lack accuracy and provide no clear measure of confidence. This uncertainty compounds in flows of multiple calls to LLMs and other tools, making it difficult for developers and end-users to trust the results. This paper introduces a probabilistic language for programming LLM-based flows. It enables developers to quantify and propagate uncertainty throughout the application's flow, and experiment with different inference scaling techniques without adding a single line of code beyond the flow's logic. We present an experimental study to demonstrate this capability, and a case study building a theorem proving agent for the Rocq theorem prover.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-05T21:29:12Z
Ahmed Ryan, Md Erfan, Akond Ashfaque Ur Rahman, Md Rayhanur Rahman
arXiv categories: cs.LO, cs.LG

Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness. A formal proof checker verifies whether each proof step follows established logical rules. Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept. This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects. Each LLM received one attempt per theorem with the temperature set to 0, and Coq checked every proposed proof in the theorem's original project environment. We counted a proof as successful only if the Coq kernel accepted it. Gemma 4 verified 12 of 100 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. Qwen 3.5, Mistral Small 3.1, and GPT-OSS verified none. The 21 successful model-theorem results covered 15 distinct theorems, 11 of which were not solved by a baseline of standard Coq tactics. All verified theorems had short or medium human-written reference proofs; no model verified a theorem with a long reference proof. Because the proof-length analysis was exploratory, this pattern does not establish that proof length caused the difference. For the three models with at least one success, the total generation cost per verified proof ranged from 741 to 36,193 output tokens, 14.9 to 178.0 seconds, and 0.0167 to 0.2000 aggregate GPU hours. We could not calculate these ratios for models with no verified proofs. Across 600 attempts, the models produced 21 kernel-verified proofs, giving an overall success rate of 3.5%. The study reports descriptive differences among the models but does not statistically test whether one model outperforms another. Therefore, the results do not establish a universal ranking of the six models.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-06T00:44:46Z
Kevin Cheang, Geoff Hulette, Rahul Kumar, Felipe R. Monteiro, Federico Mora, Robin Salkeld, Lin Tan, Serdar Tasiran
arXiv categories: cs.PL, cs.AI, cs.CL, cs.SE

Language models (LMs) are increasingly used to interact with external services via programs written in domain-specific languages (DSLs). Unfortunately, since DSLs are often low-resource and esoteric, LMs frequently produce syntactically invalid programs in these languages. Grammar-constrained decoding can eliminate such failures, but requires syntactic constraints. These are usually in the form of a context-free grammar for the target language, an artifact that is hard to come by for third-party DSLs. In this work, we define an agent, called Autogrammar, that automatically learns context-free grammars from documentation and execution data. Autogrammar is formalized as a Kripke structure whose nondeterministic choices are resolved by a language model, enabling declarative control of agent behavior via linear temporal logic constraints. We evaluate four versions of Autogrammar on three DSLs (i.e., Amazon CloudWatch Logs Insights, Dynatrace Query Language, and Datadog Search Syntax) and find that it generates grammars that achieve near perfect precision on unseen data; that temporal restrictions reduce execution time by 3.8x without incurring statistically-significant loss in precision; that execution data is crucial while documentation is dispensable; and that grammar-constrained decoding using Autogrammar-generated grammars significantly improves end-to-end LM performance on eight out of ten real tasks, matching or exceeding the performance of a professionally-maintained grammar. In comparison, the context-free grammars generated by existing LM baselines and a state-of-the-art formal technique perform significantly worse over the same evaluation.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-08T03:41:59Z
Calvin Higgins, Marco Alvarez
arXiv categories: cs.LG, cs.PL

Recent advances have highlighted the potential of machine learning, particularly Large Language Models (LLMs), for analyzing and optimizing programs. We present the first application of program embeddings from LLMCompiler---an LLM massively pretrained on intermediate representation (IR) code---to representative program analysis and optimization tasks. We generate program embeddings directly from source and IR code using a simple approach: split programs into chunks, independently embed each chunk with pretrained LLMs, and then aggregate the chunk embeddings into a single program embedding. Our experiments show that combining source and IR code embeddings achieves an error rate of 1.54\% in algorithm classification, a 12\% improvement over the current state-of-the-art, and a competitive accuracy on heterogeneous device mapping. These findings suggest that training a performance-aware LLM for embedding IR code might yield state-of-the-art results in code optimization tasks.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-08T13:22:30Z
Florentina Voboril, Stefan Szeider
arXiv categories: cs.AI, cs.LO, cs.SE

The runtime of Constraint Programming (CP) solvers is highly sensitive to modeling choices, such as symmetry breaking, implied constraints, global constraints, constraint reformulation, and variable representation. Improving these constraint models has traditionally required human expertise, and existing automated reformulation systems are restricted to a predefined library of hand-crafted transformation rules. We introduce an agentic framework that instead reformulates a constraint model from an open-ended space and establishes correctness empirically rather than by construction: a Large Language Model (LLM) agent, given a model and three training instances, proposes alternative formulations, validates each by injecting its solution back into the original model, and diagnoses and repairs failures, returning the best variant it finds in a median of about fifteen minutes. The models are expressed in the CPMpy modeling library, and each proposed model is evaluated on three larger test instances. Across nine combinatorial optimization problems, the generated models outperform the originals on 21 of 27 test instances, and on some problems solve more than two orders of magnitude faster. A comparison against non-agentic baselines that reuse the same validation and selection tools indicates that the gains stem from the agent's iterative diagnosis and repair, not merely from sampling several candidates. These results demonstrate that autonomous agentic methods can support the improvement of constraint models.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-08T22:39:12Z
Ye Xiong, Xiangyu Gao, Qiaochu Chen, Mingyu Li, Haibo Chen
arXiv categories: cs.PL

Compiler bugs are pervasive in modern compiler systems, but the test programs that trigger them are often too large for practical debugging. Program reduction addresses this by minimizing test program size while preserving the original bug-triggering behavior. Existing approaches mainly rely on syntax-guided, rule-based deletion strategies that iteratively remove parts of the program in a trial-and-error manner. While effective in reduction quality, these approaches suffer from slow reduction speed. This paper presents SimP, a program reduction framework that combines traditional reduction with LLM-based syntax- and semantic-guided reduction. SimP leverages customized prompt design to guide the reduction process. SimP synergistically combines rule-based and LLM-based reduction stages to optimize the reduction performance. The results show that SimP improves reduction efficiency while achieving comparable reduction quality, with negligible LLM monetary cost.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-04T07:51:03Z
Raja O. P. Damanik, Alwen Tiu
arXiv categories: cs.LO, cs.CR, cs.FL

The intruder deduction problem is central to symbolic security-protocol analysis: it asks whether an attacker can derive a target message from observed messages using (cryptographic) operators available to the attacker. Although convergent rewrite systems provide canonical normal forms, deduction modulo convergent theories remains undecidable in general, and existing decidable fragments are often shaped by practical cryptographic examples. In this paper, we study deduction from a minimal structural perspective. When all function symbols are unary, terms collapse to words and deduction becomes a right-divisibility problem for semi-Thue systems: given words $u$ and $v$ decide whether there exists $w$ such that $wu \equiv_S v$. We investigate this problem for several classes of semi-Thue systems and prove, to the best of our knowledge, new decidability results for convergent prefix-erasing and convergent suffix-erasing systems. We then extend this perspective to term rewriting systems whose rules erase contexts while lifting selected subterms or variables. Although these classes suggest possible decidable generalisations beyond the unary setting, we show that deduction is already undecidable for a convergent simultaneous variable-lifting system. This exposes both the potential and the limits of extending the right-divisibility results to richer equational theories.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-04T14:57:06Z
Jannick Strobel, Muqsit Azeem, Stefan Leue
arXiv categories: cs.AI, cs.LG, cs.LO

Explaining the predictions of neural networks is a central challenge in trustworthy AI. Existing explanation methods, such as those based on feature attribution or minimal sufficient sets, typically treat input features as independent, which can yield misleading explanations when inputs exhibit structured dependencies. We address this by formalizing explanations as Halpern-Pearl (HP) actual causes, modeling input dependencies using Boolean Structural Causal Models (SCMs). We compute HP causes by applying bound propagation and branch-and-bound techniques, while providing formal guarantees of completeness and minimality. Our experiments show that we substantially outperform brute-force and ILP baselines in scalability, and outperform heuristic search as graph size grows, computing all minimal actual causes on instances with search spaces of up to $2.3\times10^{13}$ candidate (cause, contingency) pairs, on SCMs with up to 28 nodes, within a 180s per-instance budget. In a case study, we further show that ignoring input dependencies inflates the number of reported causes, 14.9% of which are spurious under our SCM.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-04T19:46:57Z
Mario Leiva, Yue Ma, Qinru Qiu, Gerardo Simari, Paulo Shakarian
arXiv categories: cs.AI, cs.CV, cs.LG, cs.LO

Deploying pre-trained perception models in novel environments degrades their accuracy under distributional shift, and assembling them alone does not recover it: combiners such as majority voting trade recall for precision and are brittle to coordinated failures. Prior metacognitive methods learn logical rules that flag a model's errors, but rely on hand-authored domain-knowledge cues (object-size priors, segmentation masks) that do not transfer to genuinely novel scenes. We show that this metacognitive layer can be learned without any domain knowledge by exploiting vector-space geometry: per-model Label Vector Pools (LVP), built from each model's own training embeddings, yield error-detection rules from the geometry of detections relative to training-determined prototypes, reaching parity with domain-knowledge rules to within $0.002$ every F1 on test set. Because the approach remains neurosymbolic, these geometric rules share a single logical framework and can still be complemented by domain knowledge when available. We frame the fusion of multiple imperfect ViT-based detectors as a consistency-based abduction problem solved at test time by an exact Integer Program (IP) and a polynomial-time heuristic. On an aerial-imagery benchmark of 15 weather-shifted test sets and six ViT detectors, our domain-knowledge-free layer matches the strongest majority-vote variant on clean data (within $0.005$ F1) and, unlike every majority-vote baseline, retains its performance under a coordinated label-flipping attack: at a $90\%$ flip rate it averages $0.42$ F1 versus $0.35$ for MV-Plurality (a $22\%$ relative gain) and attains the highest F1 on \emph{every} test set once the flip rate exceeds $0.4$

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-05T13:35:35Z
Marek Dančo, Karel Chvalovský, Mikoláš Janota
arXiv categories: cs.LO

Incremental Linearization has previously been proposed for solving SMT problems over quantifier-free nonlinear integer arithmetic and has proven effective despite its conceptual simplicity. In this paper, we introduce a revised axiom set that improves convergence on polynomial constraints built from higher-degree monomials, such as powers and mixed products, a class of problems on which prior axiomatizations struggled. We present a standalone implementation built on top of Z3 for linear integer arithmetic and evaluate it on the NIA benchmark set from SMT-LIB. Our results show that the approach is competitive with state-of-the-art solvers overall and substantially outperforms them on benchmarks dominated by such polynomial constraints.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-05T18:53:11Z
Omer Rappoport, Orna Grumberg, Yakir Vizel
arXiv categories: cs.LO, cs.PL

Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors ($\mathcal{T}_B$) is fundamental to bit-precise program verification. However, state-of-the-art CHC-solvers often struggle with $\mathcal{T}_B$, limiting scalability in bit-precise reasoning. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo $\mathcal{T}_B$ by combining reasoning in $\mathcal{T}_B$ and the theory of Integer Arithmetic ($\mathcal{T}_I$). Given a CHC set modulo $\mathcal{T}_B$, Mosaic partitions it into two fragments interpreted over $\mathcal{T}_B$ and $\mathcal{T}_I$. Moreover, it implements an algorithm that reasons about the fragments in a modular fashion, exchanges information between them via sound translations across theories, and determines satisfiability w.r.t. the original CHC set. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms Spacer on these benchmarks.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-06T01:20:13Z
Jesse Looney, Jonah McDonald, Allison Klingler, Gloria Wu, Jonad Pulaj, Haoze Wu
arXiv categories: cs.LO, cs.DM, math.CO

We present a method for partitioning the solution space of statements in extremal set theory. Compared with domain-agnostic partitioning methods like look-ahead, we perform case analysis on the strategies by which a candidate solution can be constructed. We demonstrate that our approach can decompose problems in extremal set theory more effectively than look-ahead. Combining this new partitioning strategy with an exact proof-producing MILP solver, we are able to verify larger finite cases of Chvátal's Conjecture---a long-standing open question in extremal combinatorics---compared to previous work.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-06T12:04:56Z
Lisa-Marie Jaser, Jacobo Torán
arXiv categories: cs.CC, cs.LO

The red-blue pebble game is a well known two-player game on graphs that has been used in the past as a tool to analyze complexity measures in several computation models as well as proof systems. We define a new way to measure the cost of the game, the blue cost, which only counts the number of pebbles that are colored blue during the game. This new measure characterizes exactly several space bounds in tree-like and negative Resolution. In particular we prove that for any unsatiafiable formula $F$, the clause space requirements of the formula in tree-like Resolution, exactly coincide with the minimum blue pebbling cost of the game played on a refutation graph of $F$ (not necessarily a tree). This exactly parallels the known result for general Resolution in terms of the standard black pebble game, and improves the existing approximated characterization of tree-like space in terms of reversible pebbling. We show that the blue pebbling cost is also well suited for analyzing the space requirements of the lifted pebbling formulas $Peb_G[\vee]$ and $Peb_G[\oplus]$ in the two Resolution restrictions. In the case of tree-like Resolution, the clause space of $Peb_G[\vee]$ asymptotically coincides with the blue cost of the underlying graph $G$. For the case of negative Resolution, we obtain almost matching upper and lower bounds for the space in the two classes of lifted formulas, similar to the ones existing for general Resolution. We also prove a close to optimal space separation between tree-like and negative Resolution, presenting a class of formulas with $n$ variables that require clause space $Ω(\frac{n}{\log n})$ in negative Resolution, but have constant space tree-like refutations. This contrasts with the fact that negative Resolution can simulate tree-like Resolution with only a small increase in size.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-06T12:10:09Z
Edward Liem, Clemens Dubslaff
arXiv categories: cs.LO, cs.SC

Prime implicants (PIs) are central in computer science, with applications in logic minimization, diagnosis, explainable formal methods and AI. Algorithms for the computation of PIs were first-and-foremost considered on the full input space, not considering the case where the input space might be constrained by context or structural dependencies. To filter out those PIs that do not fulfill the constraints, existing methods rely on an explicit post-processing step after computing all PIs, which leads to scalability issues due to the number of PIs being exponential. We propose end-to-end symbolic algorithms that implicitly represent the set of PIs under side constraints. For this, we extend the prominent Coudert-Madre method based on decision diagrams and implement a modular tool chain that separates decision-diagram construction, PI computation, and filtering.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-06T19:52:05Z
Sam Nicholas Kouteili, William Fishell, Mark Santolucito, Ruzica Piskac
arXiv categories: cs.LO, cs.FL, cs.SE

Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with polynomial-time synthesis that natively encodes assume-guarantee properties present in most hardware and robotics domains. In this paper, we present GR1MINE, a SAT-based tool for efficiently learning GR(1) formulas from examples. We exploit the GR(1) temporal skeleton to incrementally enumerate formula candidates, leveraging learnt clauses to avoid recomputation. On the Boolean GR(1) Syntech suite, GR1MINE learns a realizable formula for all 60 benchmarks over 30X faster than generic and constrained LTL mining tools. On non-GR(1) specifications from SYNTCOMP, GR1MINE is still able to recover >2X more realizable specifications than baselines within the timeout.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-07T22:26:54Z
Saugata Basu, Hamidreza Amini Khorasgani, Hemanta K. Maji, Hai H. Nguyen
arXiv categories: math.CO, math.AG, math.LO

We develop a symbolic elimination theory for finite systems of recursive containment inequalities whose unknowns are convex subsets of a finite-dimensional real vector space. The right-hand sides are formal expressions generated from variables and parameters by convex linear combinations, finite union, and a positive geometric join encoding strict convex combinations. We prove that every parameter assignment has a unique smallest convex-set-valued solution and give a finite Gaussian-elimination-type procedure that eliminates the unknowns while preserving this solution and produces parameter-only expressions for its coordinate sets. More generally, let $\mathcal B$ be a family of subsets containing $\emptyset$ and closed under finite unions, nonnegative dilation, Minkowski sums, positive geometric joins, and convex hulls. If all parameter sets lie in $\mathcal B$, then every coordinate set of the smallest solution lies in $\mathcal B$; when these operations are effective, so is the resulting description. In particular, if the parameters are finite unions of hemihedra---where a hemihedron is a bounded convex semi-linear set, equivalently a convex finite union of relative interiors of polytopes---then each coordinate set is a hemihedron and admits a quantifier-free semi-linear description. We apply this theory to lamination hulls. For \[ V=U\oplus\bigoplus_{i=1}^{k}W_i,\qquad \dim W_i=1,\qquad Λ=\bigcup_{i=1}^{k}(U+W_i), \] we prove that the lamination hull $G_Λ^{(\infty)}(S)$ of every finite $S\subset V$ is semi-algebraic and effectively computable by a quantifier-free formula over the reals.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-09T02:32:31Z
Bernardo Subercaseaux, Benjamin Przybocki
arXiv categories: math.LO, cs.LO

Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 elementary identities. Surprisingly, Wilkie showed that the following identity is valid over the positive integers and yet does not follow from Tarski's axioms: \begin{align*} &\left((1+x)^y + (1+x+x^2)^y\right)^x \cdot \left((1+x^3)^x + (1+x^2+x^4)^x\right)^y = \\ &\left((1+x)^x + (1+x+x^2)^x\right)^y \cdot \left((1+x^3)^y + (1+x^2+x^4)^y\right)^x. \end{align*} Gurevič gave an algebra on 59 elements that satisfies Tarski's axioms but not Wilkie's identity, and over the years several authors whittled down the size of such a countermodel, culminating in a countermodel of size 12 due to Burris and Yeats. On the other hand, Zhang proved that there is no countermodel with fewer than 11 elements. Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats. Moreover, we show that there are exactly 8,957,952 countermodels on 12 elements up to isomorphism and provide a simple classification of them. Our SAT approach outperforms dedicated tools for finding countermodels in equational theories, namely Mace4 and SEM. Furthermore, using autoformalization, we prove the correctness of our main result in Lean.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-03T13:07:59Z
Zhiming Chi, Ying Liu, Andrea Turrini, Lijun Zhang, David N. Jansen
arXiv categories: cs.AI, cs.FL, cs.LO

In this paper, we consider the parameter synthesis and optimization problem for parametric Markov decision processes (pMDPs), the extension of classical MDPs where exact probability values are replaced by parametric expressions. Computing the rational function $f_{\lsf}$ that maps parameter valuations to the satisfaction value of a PRCTL property $\lsf$ is a computationally expensive task, particularly for pMDPs where the optimal policy may vary across the parameter space. We adopt the \emph{scenario approach} to efficiently synthesize a probably approximately correct (PAC) approximation $\ApproxFunOfProperty{f}$ of $f_{\lsf}$: by sampling parameter configurations and solving a linear program, we obtain a polynomial approximation whose error margin $\margin$ is guaranteed, with prescribed confidence, for all but an $\errorRate$-fraction of the parameter domain under the sampling distribution. We further show how this PAC framework can be combined with statistical model checking (SMC), enabling the analysis of black-box parametric models. Building on the PAC approximation, we integrate the DIRECT (DIviding RECTangles) algorithm for derivative-free global optimization over the parameter space. We establish conditional optimality-gap guarantees: under explicit Lipschitz and PAC-good-set assumptions, the difference between the true optimum $f_{\lsf}(\parameters^{*})$ and the value found by DIRECT is bounded by a partition-diameter term and, in the PAC case, an additional approximation-error term. An empirical evaluation on 2997 benchmarks focuses on the new DIRECT-based optimization component. The results show that DIRECT variants solve fewer instances than the scenario optimizer, but on their common successful instances they often return slightly better objective values and usually run faster, while remaining close to the scenario values within the PAC margin.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-03T16:30:26Z
Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo, Moshe Y. Vardi
arXiv categories: cs.AI, cs.FL, cs.LO

Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-04T11:25:44Z
Simos Gerasimou, Xingyu Zhao
arXiv categories: cs.SE, cs.AI, cs.LO

Combining Bayesian learning and quantitative verification is a powerful toolset for analysing key quantitative properties of software systems, like reliability and response time. However, the accuracy and robustness of verification results strongly depend on the prior knowledge (PK) underlying Bayesian inference. This knowledge reflects original beliefs about the probability of events and typically depends on domain expertise. Using inaccurate or uninformative PK can negatively affect quantitative analysis, yielding incorrect verification results. Our EPIK approach tackles this important challenge by eliciting and embedding PK in quantitative verification equipped with Bayesian estimators. Unlike existing approaches that require PK on formal model transition parameters, EPIK leverages system-level properties that are directly observable and are linked to real-world semantics. EPIK formulates a twofold optimisation problem to derive the distributions of unknown transition parameters and then embeds these distributions to verify new or difficult-to-measure (elusive) properties. The detailed experimental evaluation using multiple variants of real-world case studies and diverse EPIK instantiations shows its effectiveness, flexibility and generality.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-04T14:00:19Z
Amir M. Ahmadian, Hazem Torfah
arXiv categories: cs.LO

Formalisms for hyperproperties provide a solid foundation for studying the verification problem across classes of relational properties, such as those in information flow control (IFC). However, existing formalisms remain limited in expressiveness when it comes to capturing practical aspects of real-world systems. In particular, they do not adequately account for the quantitative nature of such systems. In this paper, we address this gap by revisiting the specification and verification of hyperproperties from a quantitative, measure-based, perspective. We introduce Quantitative Hyper-Logic (QHL), which replaces qualitative trace quantifiers with measure-based ones and extends temporal predicates with richer quantitative expressions. We further study the verification problem from a statistical verification point of view, and develop algorithms for the statistical verification of QHL specifications. For the introduced measure-based quantifiers, we particularly provide an analysis in terms of sample complexity and achievable statistical guarantees. In particular, we show how statistical methods such as Hoeffding's inequality and extreme value theory can be combined to develop statistical verification algorithms for nested measure-based quantifiers. Our approach provides quantitative alternatives for where traditional verification methods become infeasible. We demonstrate both expressiveness and efficacy on benchmarks from quantitative IFC, comparing against qualitative methods.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-06T09:41:57Z
Stefanie Muroya, Krishnendu Chatterjee, Thomas A. Henzinger
arXiv categories: cs.PL, cs.FL, cs.LO

While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We consider the error models published by quantum hardware vendors to give a hardware-dependent semantics to quantum programs. This work presents a comprehensive study of noise-aware quantum programming, ranging from logical foundations to automated verification and synthesis. We develop a noise-aware quantum Hoare logic, and use it to derive algorithmic methods for the bounded verification of quantum programs on specific hardware, and for the automatic synthesis of noise-optimal loop-free quantum programs. In this way, we synthesize hardware-dependent subroutines that commonly occur in quantum algorithms, such as parity checks, quantum state preparation, and quantum state discrimination. We evaluate our method on the hardware specifications provided by the IBM Qiskit toolkit. Besides finding different optimal subroutines for different noise models, our synthesis tool also shows that classical probabilistic branching is needed for optimality in quantum programming.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-06T13:48:05Z
Bernd Finkbeiner, Jakob Hirschler, Frederik Scheerer, Sebastian Schirmer
arXiv categories: cs.LO

Stream-based monitoring enables the concise specification of complex temporal properties. However, existing stream-based monitors are limited when dealing with large external data sources, a task that is better handled by specialized data management systems. We address these limitations by extending stream-based monitors with the ability to query external data sources. We implement this approach in RTLola and investigate challenges such as handling delayed responses, type checking of returned data, and runtime error management. A unified interface enables the seamless integration of existing systems into our approach, such as static databases or dynamic endpoints, e.g. a weather API. Our evaluation using specifications from the aviation domain also shows that a custom geospatial backend based on k-d trees outperforms state-of-the-art database systems.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-06T14:31:37Z
Jan Baumeister, Bernd Finkbeiner, Eduard Müller, Frederik Scheerer, Julia Tillman
arXiv categories: cs.LO

RTLola is a stream-based specification language designed for asynchronous real-time systems. While many temporal specifications naturally refer to future behavior, RTLola currently offers no mechanism to express such future-dependent properties. In this paper, we extend RTLola with two complementary mechanisms to reason about the future. First, we introduce a prediction operator that extrapolates future stream values at arbitrary timestamps based on past observations. Second, we add a discrete future offset operator, which provides access to precise future values by delaying the evaluation of the dependent stream expressions. While the former enables immediate, but possibly imprecise predictions, the latter ensures exact values once the required information becomes available. We formalize both extensions in the RTLola semantics and evaluate their implementation on runtime and memory consumption.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-07T14:48:33Z
Wayne Wang, Archit Bhatnagar, Tongyuan Miao, Saniya Kalamkar, Wenqi Cui, Inigo Incer, Ang Chen
arXiv categories: eess.SY, cs.DC, cs.LO

Data centers are among the power grid's fastest-growing loads. Since data center servers are sensitive electronic components, they need to be protected against the grid's voltage disturbances during grid faults. While disconnecting from the grid achieves this, it can further destabilize the power system if many data centers trip at once. To address this emerging concern, voltage ride-through (VRT) grid codes have been proposed to standardize data center behavior. They require a data center to stay connected for a period of time through the disturbance, hold an active power floor, and recover its draw within a deadline upon restoration. However, systematically designing and certifying controllers that satisfy these coupled temporal and operational requirements remains challenging. We propose SolVRT, a system that synthesizes a grid-code-compliant VRT controller for a given data center using formal methods. We develop a specification language that expresses a grid code in Signal Temporal Logic (STL) as the basis for formal reasoning. Our encoding algorithm takes the specification, along with a model of the data center's power topology, and translates the constraints into a controller synthesis problem. This step produces a correct-by-construction controller if a solution can be found, or a proof that no such controller exists. For the latter case, SolVRT provides a diagnostic step: it traces the facility's "conflict frontier," isolates the conflicting clauses that led to non-compliance, and computes the smallest hardware or workload change that would enable compliance. We evaluate SolVRT through closed-loop simulations of a 200 MW data center connected to a 140-bus transmission system. The results demonstrate that SolVRT can synthesize compliant VRT controllers, certify infeasibility when compliance is unattainable, and identify targeted modifications that enable compliance.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-09T09:05:51Z
Maria-Nicoleta Crăciun, C. -H. Luke Ong, Tom Schrijvers, Sam Staton
arXiv categories: stat.ML, cs.LG, cs.PL, stat.CO

Hamiltonian Monte Carlo (HMC) is a successful generic inference method in probabilistic programming, but in its ordinary formulation it needs gradients and finite-dimensional parameter spaces. In Haskell, lazy evaluation lets probabilistic programs express stochastic processes and other non-parametric Bayesian models over implicit infinite-dimensional spaces. This paper develops new formulations of gradient-based HMC for this infinite-dimensional setting, via lazy evaluation. For automatic differentiation, we provide an analysis based on a new notion of "piecewise analytic under cylindrical analytic partition" (PACAP), to show that even if a program is infinite-dimensional and defined lazily, the gradient of the likelihood function is finitely supported. For the Monte Carlo method itself, we develop several HMC variants and a No-U-Turn Sampler that operate over the infinite-dimensional parameter space but are still productive because of lazy evaluation. Experiments cover Gaussian mixture clustering, random walks, and piecewise-constant regression with Poisson-process changepoints.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-04T13:53:09Z
Joseph McDonald, Filip Jankovec
arXiv categories: math.LO

The purpose of this study is to investigate the bitopological duality theory of De Morgan algebras equipped with a closure operator, known as S4 De Morgan algebras. We first introduce certain expansions of pairwise Stone spaces, which we call pairwise S4 De Morgan Stone spaces (henceforth, PS4D-spaces). These consist of a pairwise Stone space $X$ equipped with a twist continuous involution $g\colon X\to X$, as well as a binary relation $R\subseteq X\times X$ that is reflexive and transitive. We first demonstrate that the bitopological spectrum $S_0(A)$ of prime filters of an S4 De Morgan algebra $A$ gives rise to a PS4D-space. A topological representation is then obtained by exhibiting an isomorphism from $A$ to the S4 De Morgan algebra $A_0(S_0(A))$ of $(τ_1,δ_2)$-biclopen subsets of $S_0(A)$ whose operation of De Morgan involution is defined through $g$ and whose closure operator is defined through $R$. We then provide an algebraic realization theorem by showing that every PS4D-space $X$ is bihomeomorphic and relationally isomorphic to the bitopological spectrum $S_0(A_0(X))$ of prime filters of $A_0(X)$. With the introduction of suitable bicontinuous frame morphisms, we show that the category $\mathbf{S4D}$ of S4 De Morgan algebras is dually equivalent to the category $\mathbf{PStone_{S4D}}$ of PS4D-spaces. As an application, we provide bitopological characterizations of filters and ideals in general De Morgan algebras under our established duality as well as bitopological soundness and completeness results for an S4-type modal extension of the calculus FDE of first-degree entailment.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-04T20:44:18Z
Christoph Benzmüller
arXiv categories: math.LO, cs.LO

Gödel's ontological argument is modal by design. Possibility and necessity are among its central concerns, and connected interpretation decisions -- extensions or intensions for the positive properties, constant or varying quantifier domains, the choice of modal logic, etc. -- subtly shape the argument and, in particular, whether the modal collapse is implied or not. It is tempting to abstract the modality away and to read the positive properties as merely forming an ultrafilter -- which, however, may replace Gödel's argument with a perhaps more manageable alternative that may have little to do with Gödel's original intention. In this spirit, Odifreddi and Gomes argue that modal collapse is an intrinsic structural feature of any theory that characterises positive properties as an ultrafilter and identifies God as its principal generator. This comment shows, with machine-verified counterexamples, that the structural claim does not hold: what drives the collapse is primarily not the filter structure but the rigidity of positivity -- itself a thoroughly modal condition. Moreover, two claims of Odifreddi and Gomes are corrected: one on the derivability of Gödel's Theorem IV, one on the extensionality of positivity. All results are machine-checked in Isabelle/HOL.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-05T09:25:04Z
Mashu Noguchi
arXiv categories: math.LO

Just as Visser showed that the formal propositional logic $\mathbf{FPL}$ can be embedded into Gödel-Löb provability logic $\mathbf{GL}$, Petrukhin proposed a propositional logic $\mathbf{SPL}$ that can be embedded into Solovay's non-normal provability logic $\mathbf{S}$. In this paper, we fix Petrukhin's proof and extend the result to Japaridze's provability logic $\mathbf{D}$, and propose a propositional logic $\mathbf{DPL}$ that can be embedded into $\mathbf{D}$.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-06T03:06:26Z
Litan Kumar Das, Kumar Sankar Ray, Prakash Chandra Mali
arXiv categories: cs.LO

Fitting's finite Heyting-valued modal logic interprets modal formulas over a finite Heyting algebra. We use a relational bitopological representation to obtain a finite-state reduction. For a finite model and a finite vocabulary, the modal subalgebra generated by the atomic valuations determines a state-evaluation map. We prove that the observational quotient is isomorphic to its finite image in the bitopological dual and that the quotient relation is the restriction of the canonical dual relation. Hence every formula over the vocabulary preserves its exact truth value, and the quotient is minimal among surjective reductions through which all generated observations factor. In addition, for any formula and state, we construct a finite tree-like exact-value certificate whose depth is bounded by modal depth and whose branching depends only on the height of the truth-value algebra and the number of boxed subformulas. Failed formulas therefore admit bounded reduced counterexamples preserving their precise failure values.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-07T12:34:55Z
Juan P. Aguilera, Grigorii Stepanov
arXiv categories: math.LO

We prove that the polymodal logic $\mathsf{J}$ is strongly complete with respect to \textit{$\mathsf{J}$-bouquets}, a topological refinement of its Kripke semantics. In particular, it is strongly topologically complete. This yields the following completeness result for the provability logic $\mathsf{GLP}$: a countable set of formulae $Γ$ is consistent with $\mathsf{GLP}$ if and only if there is a $\mathsf{J}$-bouquet $B$ and $r\in B$ such that $B, r\Vdash \mathsf{GLP}$ and $B, r\VdashΓ$. In contrast, we exhibit counterexamples showing that $\mathsf{GLP}$ is not strongly complete with respect to Beklemishev-Gabelaia spaces.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-07T13:18:46Z
Daniele Sansoni, Ranald Clouston
arXiv categories: cs.LO, math.LO

We present a new proof of the embedding of the classical modal logic S4 into the logic of Boolean Bunched Implications (BBI). While the original proof is semantical, this proof is entirely syntactical. It proceeds via Hilbert-style calculi, and is built by analogy with a recently discovered proof by Godel of the embedding of intuitionistic propositional logic into S4. We present the first full proofs of deduction theorems for BBI, which are used to show that the embedding is preserved by reasoning with assumptions, including where those assumptions are organised into bunches. Unlike the existing proof, our proof is stable under arbitrary axiomatic extensions of S4, and applies to all known axiomatic extensions of BBI in the literature. We observe how this embedding is related to semantical properties of both logics. Moreover, the proof extends gracefully to language extensions of BBI, as we show with hybrid BBI, classical BI, and sub-classical BBI.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-07T16:34:05Z
Alexander W. Kocurek, James Walsh, Yale Weiss
arXiv categories: math.LO

The logical problem of conditionals, as conceived by Stalnaker, amounts to axiomatizing a particular semantics for conditionals which utilizes selection functions that take propositions (i.e., sets of worlds) as arguments. While the sentential form of this semantics is recursively axiomatizable, we prove that its enrichment with first-order quantifiers is not---that is, we show that Stalnaker's logical problem of conditionals is unsolvable in the language with first-order quantifiers. We demonstrate this by showing how to interpret arithmetic in the logic. In the conclusion, we discuss the implications of this result for the study of conditional logic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-08T14:08:14Z
Paul Tarau
arXiv categories: cs.LO

We model in intuitionistic implicational logic the key enabler of today's GenerativeAI: the next-token prediction in autoregressive causal neural networks. In our framework, next-token prediction corresponds to modus ponens, and sequence processing becomes constructive proof extension under the Curry-Howard correspondence. Our Prolog-based specialized theorem provers validate fundamental properties of the neural models, among which relations between commutative vs. non-commutative sequencing and single-token vs. multi-token prediction choices. We derive a neural architecture equivalent to multiplicative RNNs that arises naturally from a proof-theoretic interpretation of next-token prediction as nested intuitionistic implication and position the model relative to transformers, state-space models and recursive LLMs.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-08T17:26:16Z
Evgeny Kuznetsov
arXiv categories: math.GN, math.AC, math.LO

For a commutative Bezout ring R, we give a criterion, in terms of colon ideals with principal radical, for the lattice $\mathring{\mathcal{K}}(\mathrm{Spec}(R))$ of compact open subsets of $\mathrm{Spec}(R)$ to be a Heyting algebra. Bezhanishvili and Tressl showed that $\mathring{\mathcal{K}}(\mathrm{Spec}(C(T)))$ is pseudocomplemented whenever T is a basically disconnected compact Hausdorff space, and asked whether $\mathrm{Spec}(C(β\mathbb{N}))$ is actually an Esakia space. We show it is not: applying our criterion to $C(β\mathbb{N}) \cong \ell^\infty(\mathbb{N},\mathbb{R})$ produces a diagonal counterexample, and the same obstruction rules out $βD$ for every infinite discrete D. A grid-existence theorem for $σ$-complete Boolean algebras lets us push the construction to every basically disconnected compact Hausdorff space, settling the Bezhanishvili-Tressl question completely: for no infinite compact Hausdorff space T is $\mathrm{Spec}(C(T))$ an Esakia space.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-09T15:12:16Z
Litan Kumar Das
arXiv categories: cs.LO

We establish a Lindström-style maximality theorem for Maruyama's exact-truth-test presentation of Fitting's modal logic over a fixed finite Heyting algebra and crisp Kripke frames. Unlike the existing characterization over finite MTL-chains, no linearity or distinguished coatom is assumed. Exact truth tests yield Boolean tests for designated and non-designated values and a derived existential modality sufficient for the saturation argument. We prove that every abstract extension which is compact, has the Tarski Union Property, and is strongly invariant under bisimulation is $1$-expressively equivalent to Maruyama's version of Fitting's Heyting-valued modal logic. As a consequence, every exact-value fibre of an extension formula is definable in Maruyama's exact-truth-test modal language.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-03T10:11:34Z
Emanuel Kieroński, Sebastian Rudolph, Mantas Šimkus
arXiv categories: cs.LO

A prominent research question in computational logic is how to restrict first-order predicate logic (FO) in such a way that the satisfiability problem becomes decidable. Among others, past efforts have identified two prominent decidable FO fragments of high expressivity: the guarded fragment (GF), and the two-variable fragment (FO2). These fragments are of high interest and crucial importance as they provide significant insights into decidability and expressiveness of other prominent (computational) logics like Modal Logics (MLs)} and various Description Logics (DLs)}, which play a central role in Verification, Knowledge Representation, and other areas. In this article, we show that GF and FO2 can be combined into a new fragment that subsumes both, while maintaining decidability of the satisfiability problem. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF by requiring guardedness of quantification only for subformulae with three or more free variables. We show that, when restricting the use of equality, satisfiability in TGF is N2ExpTime-complete, dropping to NExpTime-complete when the maximum predicate arity is fixed (a natural assumption in the context of MLs and DLs). We further establish that the problem is NP-complete in terms of data complexity, which is again in line with data complexity results for basic expressive DLs. We observe that many natural extensions of TGF, including the liberal use of equality, lead to undecidability. We also establish that TGF has the finite model property (providing a tight doubly exponential bound on the model size), whence finite satisfiability coincides with satisfiability.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-03T10:17:47Z
Xiaoduo Wang
arXiv categories: math.LO

We develop a cell decomposition framework for o-minimal structures equipped with a generic derivation. To a $δ$-cell we associate source cells and finite configurations in ordinary o-minimal sorts, allowing differential-topological questions to be studied through finite jet spaces. We then introduce a metric space of definable curve germs and identify its local half-space pieces with Cartesian powers of the maximal ideal of the Hardy field of definable germs. Using this germ-space description, we prove an abstract curve selection theorem for the $δ$-topology. In the case of closed ordered differential fields, we further describe concrete asymptotic representatives for the abstract curve germs.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-04T17:53:51Z
Mostafa Mirabi
arXiv categories: math.LO

We study when finite-dimensional asymptoticity transfers through uniform interpretations and definable quotients. Ambient counting yields finitely many asymptotic alternatives, but the corresponding parameter cells may fail to be definable in the interpreted language; in general, one obtains only weak asymptoticity. We isolate "trace reflection", a one-sided descent condition that removes this obstruction. For interpretations with definable selectors, trace reflection transfers asymptoticity with explicit denominator bounds. For general definable quotients, invariant asymptotic profiles replace definable choice and yield a quotient-transfer theorem. We identify an intrinsic visible denominator and prove that it is the least possible asymptotic denominator, with a coprime-witness criterion for when the interpretation-dependent bound is sharp. We also establish formula-wise, syntactic, and semantic descent criteria, prove composition theorems, and show that trace reflection is strictly weaker than uniform weak bi-interpretability. A framed-profile argument removes the noncanonical coordinate parameters introduced by uniform finite-field reconstruction. As applications, we study projective quotient traces and prove that, for every fixed $k\geq2$, the pure incidence structures arising from graphs of polynomials of degree less than $k$ over finite fields form a full $k$-dimensional asymptotic class. The denominator $k$ is minimal, and every member is $K_{k,n}$-free for all $n\geq2$.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-05T00:39:08Z
Alexander Berenstein, Kyle Gannon, Shichang Song
arXiv categories: math.LO, math.FA

This paper deals with the model theory of convolution algebras $(L^1(G),*)$ for locally compact groups $G$, seen as Banach lattices equipped with the convolution product $*$. We first prove transfer principles for elementary equivalence and elementary embeddings when the underlying group $G$ is discrete, namely, $(\ell^1(G),*) \equiv (\ell^1(H),*)$ implies $G \equiv H$, while the converse holds when $G$ and $H$ are $ω$-saturated (likewise for elementary substructures). Without $ω$-saturation, the converse fails. Although pure Banach lattices are model-theoretically tame, our results imply that adding convolution yields wild behavior. For example, we prove that if $G$ is any locally compact, non-discrete group, then the formula $d(x,x*y)$ is unstable with respect to $\mathrm{Th}(L^1(G),*)$. Moreover, we show that if $G$ is discrete and contains a particular configuration of amenable subgroups, then the formula $d(x*y,z)\mathbin{\dot{-}}\frac{1}{2}$ witnesses $\mathrm{TP}_2$ with respect to $\mathrm{Th}(\ell^1(G),*)$. As a consequence, if $G$ contains an infinite abelian subgroup, then $\mathrm{Th}(\ell^{1}(G),*)$ has $\mathrm{TP}_{2}$. We prove similar results in the locally compact non-discrete setting using the notion of an approximate identity. Finally, we prove a `continuous-by-discrete' approximation theorem. Namely, convolution algebras of connected abelian Lie groups admit metric embeddings into ultraproducts of convolution algebras over finite abelian groups.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-07T17:23:42Z
Tomás Ibarlucía
arXiv categories: math.LO, math.FA, math.GR

We prove a Bauer-Poulsen dichotomy theorem for simplices of invariant measures associated with permutation groups. More precisely, let $G$ be a transitive group of permutations of a countable set $\mathcal{S}$, and let $H$ be the stabilizer of a point of $\mathcal{S}$. Let $\overline{G}$ and $\overline{H}$ denote their closures in the topology of pointwise convergence. Assume the Polish group $\overline{H}$ has relative Property (T) in $\overline{G}$. Then the simplex $\mathcal{M}_\mathrm{inv}(2^\mathcal{S})$ of invariant probability measures for the induced action $G\curvearrowright 2^\mathcal{S}$ is Bauer if and only if $\overline{G}$ has Property (T), and is Poulsen otherwise. This addresses some examples and questions considered by Austin. We deduce this result from a more general model-theoretic statement of independent interest. To this end, we initiate the study of existentially closed models in affine logic.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-07T21:54:14Z
Pedro Teixeira Yago
arXiv categories: math.LO

We study when embeddings lift from structures to their ultrapowers, and when an ultrapower embeds into its direct power. We offer a generalization of Blass's theorem on the Rudin-Keisler order and introduce cardinal invariants $τ_\mathcal{A}$ characterizing the embeddability $\mathcal{A}^I / \mathcal{U} \hookrightarrow \mathcal{A}^I$. In infinitary languages, the criterion becomes necessary and sufficient: embeddability holds iff $\mathcal{U}$ is $κ^+$-complete, when $τ_{\mathcal{A}^I / \mathcal{U}} = κ$.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-09T02:49:21Z
Junhong Chen, Yi Zhang
arXiv categories: math.LO

We investigate the first-order theories of full \(n\)-branching ordinal trees \(\mathfrak{T}_α^n\). We obtain a complete classification of the standard trees up to elementary equivalence: every \(\mathfrak{T}_α^n\) is elementarily equivalent to one of four canonical types determined by the ordinal \(α\). For each canonical type we establish effective quantifier elimination and prove decidability of the theory. Along the way we develop the realizability theory of colored ordinal characters and obtain a sharp bound on the length of minimal witnesses. We also clarify the relationship between these trees and monadic second-order logic over ordinals, and show that the equal-height relation is not first-order definable in any standard tree.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-09T12:00:05Z
Yilong Zhang
arXiv categories: math.LO

We study the expansion of the real field by the graphs of power functions on the unit circle. Under a natural number-theoretic conjecture, we prove that adding such dense subsets does not increase the topological complexity of definable sets: every open definable set remains semialgebraic. The proof uses a two-sorted structure that separates the linear and algebraic data, inspired by Zilber's raising to powers. Using Hrushovski's amalgamation method, we construct and axiomatize a class of rich structures, and then show that the intended structure is a model. This provides a new example of a tame expansion of the real field by dense trajectories.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-03T07:30:27Z
Xing-Yu Hu, Zhang-Yi Luo
arXiv categories: math.LO, math.GN

For each countable ordinal $α\geq 2$, Filipów, Kowalczuk and Kwela introduced an ideal $\mathsf{conv}_α$ on the countable compact ordinal space $ω^α+1$. Kowalczuk later proved that, for each countable limit ordinal $λ$, the ideal $\mathsf{conv}_{<λ}$ is the greatest lower bound of $\{\mathsf{conv}_β:β<λ\}$ in the Katětov order. At the first uncountable level, let $A\subseteq[2,ω_1)$ be uncountable and let $D$ be a countable dense subset of $X_A=\prod_{α\in A}(ω^α+1)$. The coordinate ideal $\mathsf{Conv}(A,D)$ on $D$ consists of those $B\subseteq D$ with $π_α[B]\in\mathsf{conv}_α$ for every $α\in A$. For a pair $D\subseteq E$ of countable dense sets, call $α$ non-small if $π_α[E\setminus D]\notin\mathsf{conv}_α$. In ZFC, if at most countably many coordinates are non-small, then $\mathsf{Conv}(A,D)\equiv_K\mathsf{Conv}(A,E)$. Under CH this countability bound is sharp: for every $A\subseteq[3,ω_1)$ with $|A|=\aleph_1$, there are countable dense sets $D\subseteq D^*\subseteq X_A$ such that $\mathsf{Conv}(A,D^*)\leq_K\mathsf{Conv}(A,D)$ but $\mathsf{Conv}(A,D)\not\leq_K\mathsf{Conv}(A,D^*)$, and in particular $\mathsf{Conv}(A,D)$ and $\mathsf{Conv}(A,D^*)$ are not Katětov equivalent. The non-reduction is obtained, under CH, by diagonalizing along $ω_1$ coordinates against the elements of $ω^ω$ that code retractions $D^*\to D$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-03T12:21:17Z
Akihito Kajikawa, Masamori Kaku, Takayuki Kihara, Satoshi Nakata
arXiv categories: math.LO, cs.LO

In recent years, there has been rapid development in the foundational study of oracle computability from the perspective of Lawvere-Tierney topologies and their sheaves. In this article, we formulate and analyze the notion of reducibility within the framework of total computability. Then, using sheaf subtoposes derived from oracles in the total computable setting, we establish separations between various hierarchies of logical principles, including the hierarchies of the weak law of excluded middle $\mathbf{WLEM}$, the lessor limited principle of omniscience $\mathbf{LLPO}$, and Markov's principle $\mathbf{MP}$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-04T05:19:31Z
Colin Geniet, Roohani Sharma
arXiv categories: cs.DM, cs.CC, cs.LO, math.CO

Lokshtanov, Ramanujan, Saurabh, and Zehavi [ICALP 2018] proved that for any CMSO formula $φ$, testing $φ$ on arbitrary graphs can be reduced to testing it on $(q,k)$-unbreakable graphs for appropriate parameters. Their proof is non-constructive, and they ask whether it can be made constructive. We prove that this is impossible: specifically, the parameter $q$ cannot be a computable function of $φ$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-04T07:10:38Z
Koshiro Ichikawa
arXiv categories: math.LO

We study a refinement of the analytic hierarchy over second-order arithmetic under the arithmetical Church thesis, the assertion that every set of natural numbers is arithmetical. The thesis is false in the full standard model, but it is naturally satisfied in the $ω$-model consisting of the arithmetical sets. Over $\mathsf{ACA}_0^\ast+\mathsf{ACT}$, second-order quantifiers can be replaced by quantification over codes for arithmetical sets, and this gives normal forms which distinguish first-order and second-order quantifier alternations more finely than the usual analytic hierarchy. As an application, we use these normal forms to answer a question of Frittaion on fragments of uniform reflection in second-order arithmetic: the choice assumption in his separation theorem cannot simply be omitted.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-04T17:53:00Z
Zhi-Wei Sun
arXiv categories: math.NT, math.LO

Let $K$ be any quadratic number field, and let $O_K$ be the ring of algebraic integers in $K$. In 1975 J. Denef proved that Hilbert's Tenth Problem over $O_K$ has a negative solution. In this paper we establish the following undecidability result: There is no algorithm to decide whether an arbitrarily given polynomial equation $P(z_1,\ldots,z_{16})=0$ (with integer coefficients and 16 unknowns) has solutions over $O_K$. Moreover, when $K$ is a real quadratic field, we show that $15$ unknowns suffice for undecidability.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-05T10:11:44Z
David Gonzalez, Paul Shafer
arXiv categories: math.LO

We investigate the encoding ability of the cohesive power construction. We compute a graph $\mathcal{G}$ where the cohesive power $\prod_C \mathcal{G}$ of $\mathcal{G}$ by any $Δ_2$ cohesive set $C$ has degree $0''$. That is, $0''$ computes a presentation of $\prod_C \mathcal{G}$, and every presentation of $\prod_C \mathcal{G}$ computes $0''$. We also compute a linear order $\mathcal{L}$ where no cohesive power of $\mathcal{L}$ has a computable presentation. We accomplish this by ensuring that if $\mathcal{P}$ is a presentation of a cohesive power of $\mathcal{L}$, then $\mathcal{P}''$ has $\mathrm{PA}$-degree relative to $0''$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-05T12:38:30Z
David Fernández-Duque, Andreas Weiermann
arXiv categories: math.LO

Goodstein's theorem states that a certain sequences based on exponential notation for the natural numbers are always finite. The result is independent of Peano arithmetic and is a prototypical example of a proof of termination by transfinite induction. A variant based instead on the Ackermann function has more recently been proposed by Arai et al., and instead is independent of the more powerful theory ${\sf ATR}_0$. However, this result is contingent on rather elaborate normal forms for natural numbers based on a `sandwiching' procedure. This leaves open both the question of whether the sandwiching procedure can be eliminated while retaining the full strength of the Ackermannian Goodstein principle, and whether other normal forms can lead to non-termination. In this article we settle these questions by showing that {\em any} Goodstein process based on the Ackermann function is terminating, and indeed the sandwiching procedure gives rise to Goodstein principles of maximal length. We thus obtain an equivalent principle which does not involve normal forms at all and immediately implies all Ackermannian Goodstein principles that have been considered. Our techniques provide a new approach to termination proofs, where terms in a sequence do not necessarily decrease in complexity, but instead are majorized by some ``master'' process, already known to be terminating.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-05T14:01:07Z
Kirill Osipov
arXiv categories: cs.LO, cs.CC

We introduce bounded step recursion and a three-parameter hierarchy refining the Grzegorczyk hierarchy. For a strictly increasing function $\varphi:\mathbb N\to\mathbb N$ with $\varphi(x)\ge x+1$, its generalized inverse $$ρ_\varphi(y)=\min\{z:\varphi(z)\ge y\}$$ replaces the ordinary predecessor and generates the descent schedule $y,ρ_\varphi(y),ρ_\varphi^{[2]}(y),\ldots,0$. From a Grzegorczyk basis $B_m$, composition, and bounded step recursion with step $g_n^{[l]}$, we define classes $H^m_{n,l}$, where $m$ measures the initial-function strength, $n$ selects a growth scale, and $l$ fixes the stride through its canonical layers. For all $n,n'\ge2$, we obtain an exact criterion for $H^a_{n,l}\subseteq H^b_{n',l'}$. Below horizontal collapse, fixed strides are ordered by reverse divisibility: inclusion at equal row is governed by $l'\mid l$, not by the numerical order of $l$ and $l'$. All fixed strides collapse from initial basis $m=n$, and the common class equals the ordinary bounded-recursion class $E^m$ exactly from $m=n+1$. Positive inclusions use exact-depth simulations; separations use a direct piecewise-monotone trace theorem and a canonical-zone invariant for selected dependency chains. The doubling row $g_1(x)=2x+1$ is exceptional at low bases. We prove $H^m_{1,l}=E^m$ for all $m\ge3$, construct the first vertical bridge at basis $2$, and show that every fixed-arity function in $H^2_{1,l}$ is binary polynomial-time computable, with $H^2_{1,l}\subsetneq FP$. Equality $H^2_{1,l}=E^2$ would imply $P=NP$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-05T22:23:54Z
Amir Leshem
arXiv categories: math.LO, cs.IT, cs.LO

Sequential prediction naturally induces an innovation sequence consisting of the prediction errors produced by a causal predictor. We use the collection of all such innovation sequences to define the \emph{innovation spectrum} of an individual binary sequence and, from it, a new reducibility based on sequential information extraction. We show that this reducibility refines truth-table reducibility while exhibiting a fundamentally different geometry. The degree structure decomposes into two canonical regions: a truth-table spine, whose induced order is isomorphic to the truth-table degrees, and a complementary reservoir-immune region, consisting of sequences from which no infinite computable predictable reservoir can be extracted. We establish bridge constructions connecting the two regions, prove that reservoir immunity is preserved under sequential innovation, and show that the Martin--Löf-random degrees form a proper downward-closed substructure inside the reservoir-immune region. These results reveal a new geometric organization of individual sequences based on causal predictability rather than classical oracle computation.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-07T09:58:37Z
Fedor Pakhomov
arXiv categories: math.LO

We study a Lévy-Montague reflection scheme $\mathsf{Rfn}$ in second-order arithmetic: for each formula $\varphi$, the scheme asserts that every set belongs to a countable coded $ω$-model such that $\varphi$ is absolute, at all parameters from the model, between the model and the universe. Our central result is a model extension construction: every countable model of $\mathsf{RCA}_0$ can be extended, without changing its first-order part, to a model of $\mathsf{WKL}_0$ together with the full scheme $\mathsf{Rfn}$. It follows at once that $\mathsf{WKL}_0+\mathsf{Rfn}$ is $Π^1_1$-conservative over both $\mathsf{WKL}_0$ and $\mathsf{RCA}_0$, that its first-order part is exactly $\mathrm{I}Σ_1$, and that it is $Π^0_2$-conservative over $\mathsf{PRA}$. The result opens an avenue for adopting, within a theory conservative over $\mathsf{PRA}$, Feferman's $\mathsf{ZFC}$-formalization of universe-based category-theoretic arguments that was achieved using Lévy-Montague reflection. The conservation proof itself, however, is non-finitary. The extension is the union of an $ω_1$-tower of forcing extensions, and its uncountable cofinality is what secures reflection. We are only able to prove the conservation in $\mathsf{PRA}+\text{1-Con}(\mathsf{Z}_2)$. The results were obtained with extensive use of Anthropic's large language model Fable 5.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-07T18:21:16Z
William Adkisson
arXiv categories: math.LO

The strong tree property and the super tree property (also called ITP) are generalizations of the tree property that characterize strong compactness and supercompactness up to inaccessibility. That is, an inaccessible cardinal $κ$ is strongly compact if and only if the strong tree property holds at $κ$, and supercompact if and only if ITP holds at $κ$. Generalizing a result of Golshani and Hayut, we show that from large cardinals it is consistent for ITP to hold simultaneously at any countable initial segment of successors of singular cardinals. More formally, given any countable ordinal $θ$, we construct a forcing extension in which ITP holds at the first $θ$ successors of singulars. We then extend this result further to obtain the strong tree property on long segments of successors of singular cardinals of multiple cofinalities simultaneously.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-08T16:40:29Z
Silvan Horvath, Tan Özalp
arXiv categories: math.LO, math.CO

We show that, up to isomorphism, the number of $Q$-points is either finite, $2^{\mathfrak{d}}$ or $2^{\mathfrak{c}}$. This answers a question asked by Borodulin-Nadzieja, Martínez-Celis, Morawski and Świerczyńska, and by Halbeisen and the authors. We also show that under mild hypotheses, the existence of infinitely many $Q$-points implies the existence of non-atomic $Q$-measures, and of $2^{\mathfrak{c}}$-many Tukey-top $Q$-points, strengthening results of Raghavan and of Borodulin-Nadzieja et al..

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-09T08:54:48Z
Haosui Duanmu, Xinyu Liu, David Schrittesser
arXiv categories: math.LO

Loeb measure theory stands as one of the most influential concepts in nonstandard analysis, underpinning nearly all applications in probability, stochastic processes, and mathematical economics. The paper resolves a fundamental open problem in Loeb measure theory originally posed by Keisler and Sun: let $(Ω,\mathcal{F},μ)$ and $(Ω,\mathcal{G},ν)$ be two Loeb equivalent internal probability spaces, and $\mathcal H$ be the internal algebra generated from $\mathcal{F}\cup\mathcal{G}$. Does there exist an internal probability measure $P$ on $\mathcal H$ such that $(Ω,\mathcal{H},P)$ is Loeb equivalent to $(Ω,\mathcal{F},μ)$? While arXiv:2112.13955 recently provided a positive answer for hyperfinite probability spaces, the problem remained open for general internal probability spaces. We establish the existence of such an internal probability measure for all internal probability spaces.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-03T14:12:30Z
Johnathon Taylor
arXiv categories: math.CT

In this paper, we introduce a new symmetric monoidal structure on $\mathbf{Cat}$, called the \emph{graph tensor product}, with unit given by the terminal category. This tensor product falls in the middle of a factorization between the funny tensor product and the Cartesian product, giving a factorization connecting these two classical monoidal structures. We extend this construction to a symmetric monoidal structure on $2\mathbf{Cat}$, again with unit $D^0$, which provides an analogous factorization between the funny tensor product and the Cartesian product of $2$-categories. Using the $(\mathrm{bo},\mathrm{lff})$ factorization system on $2\mathbf{Cat}$, we construct a new symmetric monoidal closed model structure on $2\mathbf{Cat}$ whose tensor product restricts to the Cartesian product on the subcategory of flexible $2$-categories. Finally, we prove that this symmetric monoidal model structure fits into a square of weak symmetric monoidal Quillen equivalences relating the Gray tensor product and the flexible tensor product.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-03T17:24:58Z
Simon Henry
arXiv categories: math.CT

We show that the methods of rewriting theory to establish coherence theorems can applied at the level of quasicategories. More precisely, for any category C which admits a presentation by a convergent rewrite system, we show that the corresponding weak (infinity,1)-category admits an Amick-Groves-Squier style presentation whose generators correspond to (some of) the critical branchings of the rewrite system. This follows entirely from reinterpreting K. Brown's simplicial proof of the usual homological Anick-Groves-Squier presentation in terms of the Joyal model structure instead of the Kan-Quillen model structure. We give several applications of this to the theory of quasicategories, including a relatively general coherence theorem for loop-free planar category theoretic diagrams and a new proof that pushout of Dwyer maps are homotopy pushouts.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-03T17:57:33Z
David Gepner, Hadrian Heine
arXiv categories: math.AT, math.CT

In higher category theory, lax colimits are often understood to be a more useful and powerful generalization of usual (homotopy) colimits, which can be recovered from the lax colimit by a suitable localization. However, lax colimits do not provide the correct notion of gluing from the geometric perspective. Indeed, they are incompatible with the notion of categorical dimension, the Gray tensor product, and other basic geometric operations. In this paper, we develop the theory of oriented colimits, which correct the defects of lax colimits, and agree with lax colimits in dimension less than or equal to one. In order to study oriented colimits, we introduce a version of the Grothendieck construction which is compatible with enrichment in the Gray tensor product. We prove that the Grothendieck construction induces an equivalence between cartesian fibrations and presheaves of $(\infty,\infty)$-categories, which is enriched in the Gray tensor product of $(\infty,\infty)$-categories. Oriented colimits simultaneously generalize the concept of lax colimits and the Gray tensor product, and differ from lax colimits in much the same way in which the Gray tensor product differs from the cartesian product. We demonstrate the necessity of oriented colimits by showing that various fundamental constructions in higher category theory fail to be lax colimits but are instances of oriented colimits. As applications, we classify higher-categorical principal bundles, represent higher dimensional adjunctions by bicartesian fibrations of $(\infty,\infty)$-categories, and obtain higher categorical versions of Quillen's Theorems A and B, which admit very natural formulations in our framework.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-04T21:06:00Z
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras
arXiv categories: cs.LO, math.AT

Computational paths record equality as explicit finite traces of primitive steps. We give a topological semantics for a scoped rewrite presentation whose steps have continuous geometric realizations and whose named rewrites carry endpoint-fixed homotopies. For every presentation we construct a quotient arrow space with a canonical final-domain groupoid structure: multiplication is continuous on the quotient of explicitly composable representatives. We prove an exact four-way criterion for this final composable topology to agree with the ordinary pullback topology, together with a compact-Hausdorff sufficient condition. Thus the unconditional construction exposes, rather than hides, the product-quotient issue in ordinary topological groupoids. The realization map to geometric homotopy classes is a continuous groupoid morphism and is faithful exactly under a separate geometric-completeness condition. In the universal presentation, a continuous section identifies the coherent-path quotient homeomorphically with the usual quotient-topologized fundamental groupoid. We then give finite-generator circle and genuine torus examples, with winding-based normal forms and classifications by Z and Z^2. A Lean 4.24.0 development checks the theorem package; the mathematical presentation is independent of the implementation.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-05T06:57:37Z
Emile Bouaziz
arXiv categories: math.CT

We record a general condition guaranteeing that the animation of a small $1$-category remains a $1$-category. The proof is extremely elementary universal algebra. This recovers as a very special case the striking observation of Antieau, \cite{Ant}, that the animation of $\fnt^{\mathrm{op}}$ is a $1$-category. Our result is a fair amount more general, and for example applies to $\fnt^{\mathrm{op}}_{\mathcal{G}}$ with $\mathcal{G}$ a groupoid, as well as beyond this.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-05T12:58:35Z
Dipankar Maity
arXiv categories: math.AG, math.AT, math.CT

We promote the $n$-birational motivic homotopy category $S\mapsto \mathcal{H}^n(S)$ to a $Pr^L$-valued presheaf on $Corr(\mathrm{Sch})_{uglt,sm}$. As a consequence, for any unibranch scheme $X$, its (zeroth) birational motivic homotopy category $\mathcal{H}^{b\mathbb{A}^1}(X)$ decomposes as the product of the birational motivic homotopy categories of its function fields; in particular, for a variety $V$, $\mathcal{H}^{b\mathbb{A}^1}(V) \simeq \mathcal{H}^{b\mathbb{A}^1}(k(V))$. This implies that birational equivalences of unibranch schemes in $Sm_S$ can be detected by the birational contractibility of their generic fibers. Finally, we establish that stably birational morphisms and purely transcendental field extensions induce fully faithful embeddings of birational motivic homotopy categories.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-06T14:38:57Z
Phil Pützstück
arXiv categories: math.AT, math.CT

For each prime $p$ and integer $n \geq 1$, we construct a $p$-local spectrum $X_n$ with $X_n^{\otimes n} \not\simeq 0$ but $X_n^{\otimes (n+1)} \simeq 0$. This refutes the retract conjecture of Hovey-Palmieri. Our construction also allows us to determine the cardinality of the Bousfield lattice to be $2^{2^{\aleph_0}}$, answering a question of Dwyer-Palmieri.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-06T20:07:28Z
Thorger Geiß
arXiv categories: math.CT, math.AT

We prove that, under mild assumptions, the limit of a cofiltered diagram of $\infty$-categories is a reflective (resp. coreflective) localization of its oplax (resp. lax) limit. This gives rise to a number of exceptional 'stability' results for categorical properties under such limits, in particular one for adjunctions. As an application, we recover a push-pull formula describing certain filtered colimits in the $\infty$-category $\mathrm{Pr}^L$ of presentable $\infty$-categories.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-03T01:23:01Z
Pavel Etingof, Serina Hu
arXiv categories: math.RT, math.CT, math.QA, math.RA

Let $k$ be an algebraically closed field of characteristic $p\geq 5$, and let $\mathrm{Ver}_p^+$ be the even part of the Verlinde fusion category $\mathrm{Ver}_p$, the semisimplification of $\mathrm{Rep}_k(\mathbb Z/p)$. Let $\mathfrak g$ be a linearly reductive Lie algebra in $\mathrm{Ver}_p^+$, i.e., one whose finite-dimensional representations are semisimple. A basic class of examples is obtained by semisimplifying a simple Lie algebra over $k$ equipped with the action of $\mathbb Z/p$ by a principal unipotent element, when $p$ exceeds its Coxeter number. We prove that $\mathfrak g$ is invariantless, i.e., that the unit object is not a summand of $\mathfrak g$. For odd $m$ with $3\leq m\leq p-2$, set $\mathfrak{g}_m:=\operatorname{Hom}_{\mathrm{Ver}_p^+}(L_m,\mathfrak g)$ and $E_{\mathfrak g}:=\bigoplus_{3\leq m\leq p-2,\ m\ {\rm odd}}\mathfrak g_m^{(1)}[m]$, where $(1)$ denotes Frobenius twist. Our main result is an isomorphism of graded algebras $H^\bullet_{\mathrm{CE}}(\mathfrak g)\cong\bigwedge^\bullet E_{\mathfrak g}^*$. We also identify this algebra with the de Rham cohomology $H^\bullet_{\mathrm{dR}}(G)$ of the group scheme $G=\exp(\mathfrak g)$ and show that the induced graded Hopf algebra structure agrees with the standard one on the exterior algebra. Moreover, if $V$ is a simple $\mathfrak g$-module on which $\mathfrak g$ acts nontrivially, then $H^\bullet_{\mathrm{CE}}(\mathfrak g,V)=0$. Hence for every finite-dimensional $\mathfrak g$-module $V$ one has $H^\bullet_{\mathrm{CE}}(\mathfrak g,V)\cong\bigwedge^\bullet E_{\mathfrak g}^*\otimes V^{\mathfrak g}$. This recovers the theorem of Borel and Chevalley on the cohomology of complex semisimple Lie algebras and its analogue in sufficiently large positive characteristic.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-03T08:48:11Z
Francesco Dagnino, Fabio Pasquali
arXiv categories: math.CT

The extensional quotient completion of relational doctrines provides a common generalization of both the exact completion of categories with weak finite limits and the elementary quotient completion of existential elementary doctrines. In this paper, we study projective objects in relational doctrines with quotients, characterizing those obtained through the extensional quotient completion as those admitting a projective cover. We apply this result to doctrines of algebras for monads on relational doctrines with quotients, describing in which cases these arise as the extensional quotient completion of their restriction to (appropriate subcategories of) free algebras. This extends a similar result for monadic categories over exact ones, covering also more examples such as monads over the category of metric spaces giving rise to variants of quantitative algebras.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-04T06:49:45Z
Nao Mochizuki, Hiroyuki Nakaoka, Yasuaki Ogawa
arXiv categories: math.CT, math.RT

The heart of a $t$-structure and the ideal quotient by a cluster tilting subcategory are classical constructions that produce abelian categories from triangulated categories. Their higher analogues, namely $n$-extended hearts and ideal quotient categories by $(n+1)$-cluster tilting subcategories, are generally no longer abelian, but are known to carry both pretriangulated and extriangulated structures when the underlying triangulated category is algebraic. In this article, we introduce the notion of an abelian $n$-truncated category as a common framework for such higher constructions. We extend the heart construction for cotorsion pairs to $n$-cotorsion pairs on arbitrary triangulated categories, and prove that the resulting extended heart naturally carries compatible pretriangulated and extriangulated structures forming an abelian $n$-truncated category. This construction simultaneously generalizes the $n$-extended heart of a $t$-structure and the ideal quotient by an $(n+1)$-cluster tilting subcategory. It may also be regarded as a higher-dimensional generalization of the general heart construction for cotorsion pairs on triangulated categories. Finally, we show that the heart can be realized as an extriangulated localization of a suitable relative extriangulated structure on the ambient triangulated category.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-04T15:47:14Z
Jérémie Marquès
arXiv categories: math.LO

We organize and generalize several dualities involving continuous posets. The main theorem reads $\mathbf{St}_α\mathbf{Inf}_{α'}\mathbf{Cont}_{β'}\mathbf{Sup}_β\simeq (\mathbf{St}_β\mathbf{Inf}_{β'}\mathbf{Cont}_{α'}\mathbf{Sup}_α)^{\mathrm{op}}$, where $\mathbf{St}$, $\mathbf{Inf}$, $\mathbf{Cont}$ and $\mathbf{Sup}$ refer to stability, completeness, continuity and cocompleteness. The indices are "ladders", i.e., classes of sets $λ$ stable under dependent sums and quotients, with associated notions of $λ$-small infima and $λ$-filtered suprema. In the second half of the paper, we discuss algebraicity, proximity lattices and perfect maps.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-05T12:16:11Z
Pei Luo, Zhongkui Liu
arXiv categories: math.CT

This paper establishes three main results on the extension dimension of syzygy module categories:(1)we prove that excellent ring extensions preserve extension dimensions of syzygy module categories,including syzygy categories of modules of finite projective dimensions;(2) for cleft extensions, we investigate the behavior of extension dimensions under natural nilpotency and projective conditions;(3)for commutative Artin rings, we establish local-global characterisations for the extension dimension.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-05T13:42:05Z
Alexandru Chirvasitu
arXiv categories: math.QA, math.CT, math.RA, math.RT

We prove a number of Jacobson/solvable/nilpotent-radical (co)invariance results for finite-dimensional associative or Lie (co)module-algebras over Hopf algebras $H$, provided the characteristic, if positive, is large relative to the dimension of the algebra and the (co)actions satisfy trace-preservation conditions automatic when $H$ is involutory. This generalizes a number of such radical-invariance criteria in the literature, due to A. Gordienko, V. Linchenko, Pagon-Repov{š}-Zaicev and others, providing a uniform enriched-categorical framework for those results.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-05T14:23:49Z
Ishan Levy, Jiacheng Liang, Vladimir Sosnilo
arXiv categories: math.AT, math.AG, math.CT, math.KT, math.NT

We develop a comprehensive theory of dualizable additive categories. We provide several equivalent characterizations, notably identifying them as separated Grothendieck prestable categories satisfying the $\mathrm{AB4}^*$ and $\mathrm{AB6}$ axioms. We establish a connection to almost mathematics by demonstrating that they arise precisely as the categories of connective almost modules over connective $\mathbb{E}_1$-rings. Furthermore, we prove that dualizable additive categories are generated by flat objects, and that the passage to flat objects yields an equivalence between dualizable additive categories and compactly assembled additive categories. As a primary application within analytic geometry, we characterize the category $\mathrm{Nuc}(R)_{\geq 0}$ of connective nuclear modules (in the sense of Clausen--Scholze) over an adic $\mathbb{E}_\infty$-ring $R$ via a universal property, identifying it as the additive rigidification of the category of connective complete $R$-modules. Finally, we construct the universal finitary stable localizing invariant for dualizable additive categories, the presentable stable category $\mathcal{M}\mathrm{ot}_{\mathrm{pst}}$ of prestable motives, and demonstrate that its unit corepresents nonconnective algebraic $K$-theory. We prove that the motives of small additive categories and those of dualizable additive categories generate the same presentable stable subcategory.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-05T15:06:04Z
Mo Huang, Hao Xu, Zhi-Hao Zhang
arXiv categories: math.QA, math.CT, math.RT

We show that every symmetric fusion category over $\mathbb{R}$ is equivalent to the category of finite-dimensional semi-linear representations of a $\mathbb{Z}_2$-graded finite super group. The proof uses Galois descent for tensor categories over $\mathbb{C}/\mathbb{R}$, reducing the classification to semi-linear $\mathbb{Z}_2$-actions on symmetric fusion categories over $\mathbb{C}$. As a further structural result, we establish a Tannaka-Krein type correspondence between symmetric fusion categories over $\mathbb{R}$ and finite groupoids with a $\mathbb{Z}_2 \times \mathrm{B} \mathbb{Z}_2$-action. This gives a complete real analogue of Deligne's classification result.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-05T17:28:24Z
Joseph McDonald
arXiv categories: math.LO

Partial orthomodular lattices are an intermediate class of algebras between ortholattices and orthomodular lattices. In this short note, we obtain a duality for partial orthomodular lattices via a subcategory of the category of spectral spaces, independently of the Axiom of Choice.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-06T14:08:56Z
Yue Meng, Zhiqiang Yu
arXiv categories: math.QA, math.CT

A fusion category $\mathcal{C}$ is said to be $\mathbb{Z}/2\mathbb{Z}\times \mathbb{Z}/2\mathbb{Z}$-quadratic if the group $G(\mathcal{C})$ of invertible objects is isomorphic to $\mathbb{Z}/2\mathbb{Z}\times \mathbb{Z}/2\mathbb{Z}$, and the remaining simple objects form an orbit under the action of $G(\mathcal{C})$. In this paper, we give a partial classification of $\mathbb{Z}/2\mathbb{Z}\times \mathbb{Z}/2\mathbb{Z}$-quadratic fusion categories of rank six. More precisely, we show that its Grothendieck ring $\mathcal{K}_0(\mathcal{C})$ must be one of nine fusion rings if the fusion rule multiplicities are less than $20$, and the categorifications of five of them are previously known. We prove that one of the last four fusion rings can be realized as de-equivariantization of a near-group fusion category of type $\mathbb{Z}/2\mathbb{Z}\times \mathbb{Z}/4\mathbb{Z}+8$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-07T01:51:25Z
Shengyong Pan
arXiv categories: math.RT, math.CT

We construct an explicit tilting equivalence between the incidence algebra of every rational Dyck staircase and a canonical idempotent corner of a higher Auslander algebra of type~$A$. In the coprime case, this corner identifies with the algebra $B_0$ introduced by Xing. The resulting Dyck-corner equivalence supplies the missing link in the previously known chain of equivalences and thereby proves the Chapoton--Ladkani--Rognerud conjecture for coprime positive integers. The Dyck-corner equivalence itself requires no coprimality hypothesis and is compatible with replicated algebras. Our main tool is a linear-categorical extension of the interval-tilting mechanism of Chapoton--Ladkani--Rognerud. The relative theorem applies to finite $\kk$-linear categories under finite-global-dimension assumptions on the total category and its fibers. In contrast with the incidence-category setting, it allows arbitrary finite-dimensional $\Hom$ spaces and zero composites of nonzero morphisms, and it does not require the diagonal endomorphism algebras to be semisimple. The tilting object is constructed from exact right Kan extensions of fiberwise representables. We compute its opposite indexed endomorphism category, including all forced-zero compositions, and hence its opposite endomorphism algebra. Iterating this construction one coordinate at a time yields an explicit derived equivalence between the incidence algebra of every finite coordinate staircase and an idempotent corner of a higher Auslander algebra of type~$A$. We further realize the resulting staircase derived categories as triangulated subcategories generated by product Lagrangians in partially wrapped Fukaya categories of stopped-disk symmetric products and, in the coprime Dyck case, as Fukaya--Seidel categories of symmetric Brieskorn--Pham singularities.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-07T06:27:46Z
Geoff Vooys
arXiv categories: math.AG, math.CT, math.DG

In this largely expository paper we provide a deep and explicit exploration and exposition of the tangent structure on the category of schemes $\mathbf{Sch}_{/S}$ whose tangent functor $T(X) = T_{X/S}$ is the relative tangent scheme of Grothendieck described in \emph{Éléments de Géométrie Algébrique} 4. In particular we provide explicit descriptions of the ways that the bifibration of quasicoherent sheaves and bifbration of quesicoherent sheaves of algebras over schemes may be built from the ways in which the bifibrations of modules and commutative algebras over commutative rings interact. We also show the ways in which these interactions give rise to an explicit description of the standard tangent structure on the category of schemes in terms of sheaves of Kähler differentials, properties of the relative spectrum functor, and more. Finally, we show that quasi-coherent sheaves can be reconstructed from their category of differential bundles by showing that for quasi-separated schemes $X$ and $Y$, there is an isomorphism $X \cong Y$ if and only if there is an equivalence of categories $\mathbf{DBun}(X) \simeq \mathbf{DBun}(Y)$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-07T16:22:18Z
Stefano Ambra, Arnaud Duvieusart, Andrea Montoli
arXiv categories: math.CT

We show how the direction functors can be used to develop a cohomology theory for Barr-exact and S-Maltsev categories, where S is a suitable class of split epimorphisms with a fixed section. Using the fact that, for any set B, the category of small categories with B as set of object is S-Maltsev with respect to the class of Schreier points, we show that the cohomology theory of small categories arising from the direction functors coincides with the one introduced by Hoff and Golasinski.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-08T03:06:43Z
Changjian Fu, Zhanhong Liang, Ming Lu
arXiv categories: math.RT, math.CT, math.RA

For any symmetrizable generalized intersection matrix (GIM) $C$, we construct an acyclic valued quiver $(Q,\mathbf{d})$ endowed with an involution $θ$. Let $\mathcal{D}$ be the bounded derived category of finite-dimensional representations of $(Q,\mathbf{d})$, and let $Σ$ stand for the suspension functor of $\mathcal{D}$. We show that the orbit category $\mathcal{D}/(θ\circΣ)$ carries a canonical triangulated structure and is $2$-periodic. Applying Peng--Xiao's construction to this orbit category, we prove that the GIM algebra $\operatorname{gim}(C)$ is isomorphic to the integral Ringel--Hall Lie algebra associated with $\mathcal{D}/(θ\circΣ)$. As a further application of the above machinery, we investigate elliptic Lie algebras of types $D_4^{(1,1)}$, $E_6^{(1,1)}$, $E_7^{(1,1)}$ and $E_8^{(1,1)}$. For each elliptic Dynkin diagram, we define a finite-dimensional algebra $A$ by taking an appropriate quotient of the acyclic quiver $Q$ attached to the GIM matrix $C$. From the resulting $2$-periodic triangulated categories, we build the corresponding Ringel--Hall Lie algebras, and establish a surjective Lie algebra homomorphism from each elliptic Lie algebra to its integral Ringel--Hall counterpart. This map is conjectured to be injective, and its injectivity on real root spaces is confirmed.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-04T03:38:42Z
Yuxu Chen, Hui Kou, Zhenchao Lyu
arXiv categories: cs.LO

We introduce the category \(\FVA\) of finite-valuation approximable domains, a full subcategory of continuous domains contained in the category of pointed countably based FS-domains. We prove that \(\FVA\) is Cartesian closed and closed under both the subprobability and probability valuation powerdomains. Hence the valuation monads \(\Vsub\) and \(\Vone\) restrict to \(\FVA\), yielding a positive answer to the generalized form of Jung--Tix problem, one of the longest-standing open problem in domain theory since 1990s. The proof is divided into two steps. First, for every finite poset \(P\), we construct an increasing FS approximate identity on \(\Vsub(P)\), and thereby show that \(\Vsub(P)\) is a countably based FS-domain. Second, we call a domain finite-valuation approximable when its identity is the pointwise supremum of an increasing sequence of maps factoring through spaces \(\Vsub(P_n)\), where each \(P_n\) is finite. A finite-separation saturation theorem and a unified kernel-lifting theorem then show that \(\FVA\) is closed under Scott-continuous retracts, finite products, function spaces, \(\Vsub\), and \(\Vone\).

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-05T06:54:24Z
Pooya Farshim, Martti Karvonen, Andre Knispel, Markulf Kohlweiss, Philip Wadler
arXiv categories: cs.LO, cs.CR, math.CT

Category theory is a mathematical theory of composition, widely used in logic, computing, and physics. Here we apply it to give a theory of secure composition. In particular, we provide a categorical treatment of Canetti's Universal Composability (UC) framework for systems with a static number of parties and sessions, often termed UC for static systems, yielding four benefits. First, we present our results graphically yet retain rigor by applying a standard categorical technique known as string diagrams. In particular, our formulation of the composition theorem can be graphically verified with a short sequence of diagrams, while remaining translatable to equations and amenable to formal verification. Second, categories let us generalize so that our results extend beyond interactive Turing machines to other forms of computation, such as quantum computation or domain-specific languages. Third, categories help us drop some unnecessary restrictions of UC (e.g., our adversary can be a computational network rather than a single Turing machine); we prove equivalence between our variant and the usual UC, showing no expressiveness is lost. Finally, the categorical perspective leads us to identify and correct some minor technical oversights in the standard formulation of simple UC.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-05T08:02:46Z
Bonan Su, Yuan Feng, Li Zhou, Mingsheng Ying
arXiv categories: quant-ph, cs.PL

Fault-tolerant quantum computation enables the deployment of practical quantum algorithms but incurs substantial overhead from error correction, making resource estimation a central concern. Beyond case-by-case analyses, existing quantum programming languages either require programmers to manipulate low-level hardware details, rendering fault-tolerant implementations cumbersome, or abstract away the underlying error-correction schemes, reducing the effectiveness of resource utilization and estimation. To address these limitations while preserving programmability, we present a quantum programming language that enables efficient resource utilization, together with a resource-estimation framework for comprehensive resource analysis. Our framework features programmer-visible abstractions of error-correction schemes and cross-layer program-hardware analysis, allowing systematic exploration of resource trade-offs. We evaluate our approach on detailed fault-tolerant implementations of practical large-scale quantum algorithms, including components typically treated as black boxes in existing frameworks. The results demonstrate that our framework enables substantial resource savings while delivering detailed, fine-grained, and accurate resource estimates for fault-tolerant quantum programs.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-05T10:05:38Z
Bruno Rucy Carneiro Alves de Lima, Victor Henrique Cabral Pinheiro, Evgenii Dolzhkov, Joseph Haske
arXiv categories: cs.PL

Quantum annealers solve problems by finding the lowest-energy (ground) state of a programmable physical system, a 2-local Ising model, whose energy function is the Hamiltonian. We compile recursive Datalog programs into such models so that the ground state projects onto the program's minimal Herbrand model. The compiler has four stages: binarization, grounding, reduction to a Min-Ones SAT formula, and Ising encoding. Each rule becomes an energy penalty on the one assignment that violates it, and a small uniform cost on every true atom selects the minimal model. We contribute both in theory and in practice with per-stage correctness lemmas and a correspondence theorem, verified in Lean 4, establishing that the ground state of the compiled model projects onto the program's minimal Herbrand model. We map the compiled models onto the topologies of commercial annealers and characterize, under classical and simulated-quantum annealing, whether and when that certified ground state is attained.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-06T14:51:20Z
Renato Neves, Bruna Salgado
arXiv categories: cs.LO, math.CT

Motivated by the need to reason about case statements quantitatively, we extend quantalic linear lambda-calculus with additive disjunction. We show that the resulting equational system is sound. We also show that when certain continuity properties (of the underlying quantale) are adopted, it is additionally (approximately) complete. We present several models of the extended calculus, involving for example meta-theoretical properties in categorical logic (gluing), probabilistic, and quantum computation. As a concrete application, we illustrate how a probabilistic model, based on Banach spaces, can be synergistically used with the calculus' equational system to reason about Cauchy sequences of random walks. This highlights the emergent shift from "program semantics as the science of program equivalence" to flexible, quantitative perspectives, involving functional analysis and beyond.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-07T13:35:26Z
Lukas Müller
arXiv categories: math-ph, math.AT, math.CT, math.QA

Topological defects in quantum field theories are believed to assemble into higher categories with extra structure. This has been made precise for defects in $2$- and $3$-dimensional oriented topological quantum field theories by Davydov, Kong, and Runkel and by Carqueville, Meusburger, and Schaumann, respectively. In this paper we study the extra structure present on these categories when the topological field theory is additionally reflection positive. We define reflection defect TQFTs as symmetric monoidal functors out of a defect bordism category that intertwine orientation reversal with complex conjugation; they are reflection positive if they satisfy an additional positivity condition. Our main result is that in two dimensions the bicategory of defects $\mathcal{T}_\mathcal{Z}$ associated to a reflection defect TQFT carries the natural structure of an $O(2)$-dagger bicategory, a structure we define explicitly. If the theory is reflection positive, $\mathcal{T}_\mathcal{Z}$ can be equipped with additional structure closely related to the definition of a 3-Hilbert space (the two agree up to some finiteness and completeness conditions).

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-03T12:24:43Z
Jakub Smolík
arXiv categories: math.LO

Assuming the axiom of choice, we show that a weakened version of Nash-Williams' theorem about infinite trees can be recovered while completely avoiding better-quasi-orderings. In particular, we give a direct proof that the class of all order-theoretic trees is well-quasi-ordered by the tree-homomorphism relation.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-03T15:28:32Z
Yiyang Yu
arXiv categories: cs.AI, cs.LO, q-bio.NC

Predictive processing theories portray the brain as a hierarchical prediction engine that minimizes prediction error, yet they lack operational definitions for the structure of a "prediction," the standardized response to a prediction error, and the mechanism that maintains consistency across successive updates. Bayesian cognitive science attempts to subsume all uncertainty under probabilistic belief updating, but it presupposes a closed hypothesis space and provides no generative account of how the objects over which probabilities are distributed become discrete, identifiable referents in the first place. This paper introduces Predictive Set Theory (PST), a formal generative framework that reconstructs cognitive architecture from first principles. PST anchors cognition in a minimal set of operations---a sensor formalized as an identity function, set-theoretic state refresh, and three fundamental forms of reference chains (reference, counter-reference, and semi-reference)---and rigorously derives core cognitive functions including state sequences, demand, comparison, efficiency, and finite-horizon probabilistic planning. Rather than modeling neural mechanisms, PST constitutes a design specification for any system that must maintain internal consistency while acting under incomplete information and irreversible risk. The framework offers novel resolutions to classical problems such as Russell's paradox, the cognitive status of Gödelian incompleteness, the grounding of negative feedback, and the comprehension of film editing. The primary purpose of this paper is to establish, through the public academic record, the originality and completeness of the Predictive Set Theory framework.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-03T16:04:08Z
Matouš Schnabel
arXiv categories: math.LO

A real number can have more than one name: $0.5$ and $0.4999\ldots$ denote the same thing, and which numbers enjoy such a doubling depends on the base one writes in. We make that dependence the object of study. Fixing a system function $\vartheta$, which assigns a base $\vartheta(n)\geq2$ to every position independently, we build the real numbers as equivalence classes of digit functions $f:ω\rightarrowω$, where the equivalence is generated by two local carrying moves, contraction and broadening, and tested by agreement on finite initial segments. Each class turns out to contain at most two canonical representatives (up to a sign representation), its primary and secondary auxiliary functions, so the doubling above is a theorem of the theory rather than a convention imposed on it. We define order, addition and multiplication and verify the axioms of a Dedekind-complete ordered field, so that by categoricity every choice of $\vartheta$ delivers $\mathbb{R}$ itself. The models are therefore indistinguishable as ordered fields and differ only in how their elements are named, and since $\vartheta$ ranges over an uncountable parameter space, that naming can be chosen to suit a problem. We show what this buys: in any base whose partial products absorb every denominator, a non-zero real number is rational precisely when it has a second name, and Cantor's 1869 irrationality criterion for Cantor series follows from the representation theory rather than from number theory.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-03T22:31:30Z
Irene Tsapara
arXiv categories: cs.AI, cs.CL, cs.LO

We revisit higher-arity atomic concept learning through the geometry of hypercubes and hyperplanes of ground instances. Our starting point is the observation that the ambient r-dimensional hypercube of ground atoms is not structurally uniform. Its logical complexity is organized by hyperplanes: every hyperplane other than the full diagonal collapses into finitely many elementary-equivalence classes, with a bound independent of the term depth, while the full diagonal is exceptional and its class count grows without bound. This asymmetry is not merely geometric. It reflects the reduction-theoretic structure of the concepts themselves. Building on a higher-dimensional framework developed in the author's earlier work, we reinterpret these results through canonical simple concepts, minimal orderings, and representative reductions. This yields a taxonomy of hyperplane behavior in higher dimensions and shows that complexity is localized rather than spread uniformly through the instance space. The paper includes a fully worked binary case, an explicit treatment of the ternary hypercube, and an unpacked account of the reduction machinery that drives the collapse. The three-dimensional case already exhibits the essential phenomenon of orthogonal families, partial diagonals, and the exceptional full diagonal. This geometric-logical perspective clarifies where complexity is concentrated in atomic concept learning and suggests a modern interpretation in terms of constrained hypothesis spaces and structured classification.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-04T18:05:41Z
Tong Zhang, Zhiyuan Shi, Yun Peng, Tao Xie
arXiv categories: cs.CV, cs.CL, cs.LO

Can a model look at a river delta and a lightning bolt and see that they share a structure? We introduce GEB-Bench, a benchmark whose unit is an abstract structural motif--self-reference, a strange loop, a Mobius twist--in the spirit of Godel, Escher, Bach. Each motif is told in several voices: a natural scene whose composition is the structure, a folk story whose telling enacts it through a mechanically checkable form device, a mathematical theorem, and a programmatic skeleton; surface parameters are declared nuisance variables and never scored. Motifs, voices, and the structural changes between them form a small cross-modal category, and GEB-Bench's tasks are its questions. Evaluating twelve open and proprietary models, we find that abstraction failure is lawful. The central finding is a gap between recognition and cross-voice mapping: models identify a structure within one voice far better than they carry it across voices; every model pays this tax, and mapping strong enough to narrow it appears only at the frontier tier. Two patterns support it. Errors align more strongly with the designed formal geometry than with measured perceptual geometries, and frontier models from different vendors converge on the same wrong answers; and surface complexity taxes every model that reads structure, with capacity buying headroom rather than immunity. GEB-Bench is fully generative and released with its pipeline.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-06T21:11:30Z
Ivo Düntsch, Rafał Gruszczyński
arXiv categories: math.LO

We study a discrete representation of contact relations on bounded distributive lattices and some of their reducts. In the course of the paper, we apply ideas and techniques developed by Ivo Düntsch, Dimiter Vakarelov, and Michael Winter, and we show---among others---that contact relations on a distributive join semi-lattice $L$ with the bottom element correspond to reflexive and symmetric relations which are closed in the product of the Stone space of $L$.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-08T13:13:09Z
Giacomo De Colle, Helena Blackmore, Chris Partridge
arXiv categories: cs.AI, cs.DB, cs.LO

In this paper we discuss the foundations behind a novel methodology for the validation of semantic mappings between different data sources based upon different foundation ontologies, where the methodology builds a framework based upon the metaphysical commitments of the ontologies. We provide as example the test case of mappings between IES and BFO, and we especially focused on providing cardinality constraints on the mappings between the two ontologies. In order to demonstrate the applicability of our method, we showcased how these principles can be operationalized through SPARQL queries validating the results of a mapping pipeline.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-08T18:16:14Z
Martino Lupini
arXiv categories: math.FA, math.LO, math.NT

We completely classify the possible complexity classes of non-closed operator ranges on separable Banach spaces over a Polish non-Archimedean non-trivially valued field. These are precisely $\boldsymbol{Π}_{1+λ+n+2}^{0}$ for a countable ordinal $λ$ that is either zero or a limit ordinal, and a finite ordinal $n$. Considering Fréchet spaces produces the additional complexity classes $\boldsymbol{Π}_{λ}^{0}$ for a countable limit ordinal $λ$.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-09T14:16:49Z
Tomasz Kania
arXiv categories: math.LO

The stability programme initiated by Ulam asks when approximate solutions to algebraic identities must lie near exact ones. For lattices, this leads to the question of when a map that nearly preserves joins and meets can be approximated by a genuine lattice homomorphism. Badora--Kochanek--Przebieracz developed a neighbourhood-based framework for distributive lattices, centred on a separation (sandwich) lemma that constructs an exact join homomorphism between a join-subhomomorphism and a join-superhomomorphism via an order envelope. We revisit this mechanism and identify the single step at which distributivity is used: a decomposition identity for elements lying below a join. Without distributivity, separation can fail already in the modular lattice $M_3$ and in a small finite orthomodular lattice. On the positive side, we show that separation holds in arbitrary lattices whenever the lower bounding map is isotone. For orthomodular lattices---algebraic models of quantum logic---we develop a blockwise stability theory on Boolean blocks. Approximate identities on compatible pairs yield exact homomorphic selections on each block (for joins, for meets, and for both operations under bi-admissibility). We present several gluing criteria for assembling blockwise selections, and we give a concrete finite example showing that gluing can fail when block overlaps are non-trivial. Finally, in the spirit of Kalton--Roberts, we obtain blockwise approximation results for nearly additive functions on orthomodular lattices by finitely additive measures, with an illustration on finite-dimensional projection lattices.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-09T21:45:34Z
Karl Svozil
arXiv categories: quant-ph, cs.LO

The term ``partition logic'' denotes two constructions at different levels. In automaton and generalized-urn models, selected partitions generate Boolean event algebras whose contextwise union forms a concrete pasted event structure; in Ellerman's framework, whole partitions are classifications governed by refinement and partition operations. For a finite set $U$, Ore's correspondence maps each generator $π$ to its Boolean algebra $\BA(π)$, but it neither identifies the pasted carrier with $\Part(U)$ nor makes pasting a partition operation. It yields $\BA(π\wedgeσ)=\BA(π)\cap\BA(σ)$ and $\BA(π\veeσ)=\langle\BA(π)\cup\BA(σ)\rangle_{\rm BA}$, where $\langle\cdot\rangle_{\rm BA}$ denotes Boolean-algebra generation. Thus meet captures the common event algebra, whereas join gives the ambient Boolean closure. Chinese-lantern, Firefly, and triangular examples distinguish shared events, atomic intertwining, and inherited concrete order. Ellerman's direct-sum decompositions (DSDs) provide a vector-space analogue: component projections of an orthogonal DSD resolve the identity and encode exclusive outcomes, but its components are not equivalence classes of vectors. Gleason and Kochen--Specker applications require globally context-consistent valuations on those projections.

arXiv abstract · PDF