arXiv weekly literature review

Proof assistants and mechanized formalization · primary corpus · published 2026-08-24T08:03:56Z
Yusheng Zheng, Xiaoyu Song, Yanpeng Hu, Lebin Cheng, Yuxi Huang, Wei Zhang
arXiv categories: cs.PL, cs.CR

Agent runtimes can Checkpoint an execution, Fork it, Restore a checkpoint, or Merge branches without restarting a task. We call these operations execution edits, with Checkpoint recording the current execution for later use and Fork, Restore, and Merge changing what the Agent will do next. An execution edit cannot undo an earlier authorization or a tool request already sent. An unsafe edit can therefore authorize the same tool action twice, discard a result the task still requires, or conflict with a call that began before the edit. The Agent is untrusted, so the runtime uses its execution record to determine which past actions an edit must account for and which required results it must preserve to keep the subsequent execution safe. Yet existing Agent systems support such operations without deriving what each edit must preserve from the running execution, whereas prior methods for computing safe behavior take that requirement as input. We give an algorithm that decides exactly whether an edit is safe. It returns all safe ways to continue, or proves that none exists. To make this decision, the algorithm lists every way the task can finish without violating policy. It removes any way that could make a still-required result impossible to finish later. If none remain, it returns a checkable proof that no safe implementation exists. Otherwise, the remaining ways describe exactly what the runtime may allow. Our formal results cover Checkpoint and the six forms of Fork, Restore, and Merge, together with extensions, atomic enforcement, and the information every exact checker needs. Lean mechanizes the finite checker and runtime invariant, and tests validate all six edit forms. The source code, Lean proofs, and executable tests are available in the public GitHub repository at https://github.com/eunomia-bpf/agent-check-restore-safety.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-08-24T14:29:41Z
Matthew Keenan, Nishant Kheterpal, Jean-Baptiste Jeannin, Cyrus Omar
arXiv categories: cs.PL, cs.CY

Proof assistants offer instant feedback and incremental proof scaffolding to users. Both of these features have long held promise in improving mathematics education in classroom settings, where manual grading is costly, and students often struggle with knowing how to proceed in their proof. However, they have been difficult to deploy in classroom settings due to two main concerns: (i) students struggle with the intricacies of full-scale proof assistants; and (ii) proof assistants are ineffective in support of student learning, and knowledge transfer to on-paper assessments without the tool. We present Hazel Prover, a classroom proof assistant for teaching equational and inductive reasoning, with a design informed by criteria encompassing ease-of-use of the tool, student engagement with underlying mathematical ideas, transfer to pen-and-paper proof, and classroom logistics. We synthesized these criteria from observations made in prior deployments of proof assistants to the classroom. We engaged in an iterative design and evaluation process, deploying Hazel Prover in two different classes and conducting in-depth analyses of fine-grained usage logs, survey data, and student exam responses. Our analysis demonstrates that students were able to learn to use the tool effectively, and that students became more capable with inductive proof as they progressed through problems. However, the first design did not effectively achieve transfer to pen-and-paper proofs. We hypothesized that this was due to the tool offering too much help to students in the equational reasoning steps. Based on this negative result, we enforced more manual student engagement with equational steps, which led to more effective transfer in the second deployment. We believe that our analyses offer generalizable insights relevant to the designers of future classroom proof assistants for a variety of mathematical domains.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-08-25T12:23:54Z
Max Kurze, František Farka, Sebastian Ertel
arXiv categories: cs.PL

The Network-on-Chip (NoC) is the communication backbone of any multiprocessor chip. A failure of the NoC has severe consequences for the whole system. Yet, no approach exists that provides formally-verified NoCs with strong guarantees but without tedious verification effort. Any library that generates formally-verified NoCs needs to be parametric in the structure of the NoC. This requires a hardware description language (HDL) that allows for parametric and concurrent yet efficient hardware designs as well as the necessary program logic to reason about them in a modular fashion. So far, HDLs fall short in both aspects. In this paper, we implement NoC-Out, the first library/generator for formally-verified k-dimensional NoC designs. In order to build NoC-Out, we extended Kôika, a rule-based HDL in the Rocq theorem prover, with support for concurrent yet efficient NoC designs and a program logic for modular, automated reasoning. Given a configuration, NoC-Out produces a k-dimensional torus NoC in Kôika, which can then be compiled to Verilog. Each produced NoC is equipped with a proof that it refines our formal NoC specification; no additional verification effort is required. Our specification proves a strong liveness guarantee, which consequently applies to all generated NoCs. In our evaluation, we find that our verification approach is even required to synthesize efficient NoCs in rule-based HDLs.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-08-26T07:12:54Z
Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlassis Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Mohamed, Bilal Aytekin, Jiewen Lang, Zezheng Song, Furong Huang
arXiv categories: cs.CL, cs.AI, cs.LO

Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-08-28T15:16:25Z
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng
arXiv categories: cs.AI, cs.LO, cs.MA

Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification (as well as the underlying mathematics) and the significant time required for writing formal proofs. AI coding agents have dramatically reduced these barriers; human users can now use natural language to prompt agents to write complex proofs in Lean. This opens up the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked. To realize this possibility, we introduce Prove2Me (https://prove2.me), an open collaborative platform for formalizing mathematics. Users launch formalization "missions", to which AI agents contribute formal proofs toward completion. We designed mechanisms and a specialized harness in Prove2Me that enable large-scale collaboration so that agents can build on one another's work and freely reuse existing results. In doing so, Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-08-25T08:57:13Z
Nicholas Miazzo, Marco Alecci, Jordan Samhi, Jacques Klein, Eleonora Losiouk
arXiv categories: cs.SE, cs.CR

Taint analysis is a fundamental technique for detecting sensitive data leaks in Android apps. However, traditional static tools, such as FlowDroid, still face well-known challenges due to the complexity of accurately modeling the Android framework. In this paper, we investigate whether off-the-shelf Large Language Models (LLMs) can effectively reason about taint flows in Android apps. Our preliminary approach relies on an agentic interaction strategy, enabling the LLM to iteratively explore code and reason about data flows. We conduct an initial evaluation on the DroidBench benchmark against FlowDroid, where our approach outperforms the baseline: Gemini-3 Flash achieves an F1-score of 0.96, compared to 0.55 for FlowDroid. In particular, we observe improvements in challenging categories such as inter-component communication (0.95 vs. 0.17), implicit flows (0.94 vs. 0.00), and reflection (1.00 vs. 0.50), where FlowDroid typically struggles. On a small set of real-world apps, the LLM-based approach also identifies additional potential data leaks not reported by FlowDroid. These preliminary findings suggest that LLM reasoning may effectively complement traditional static taint analysis, motivating future research on hybrid LLM-enhanced taint analysis pipelines.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-25T10:50:46Z
Kunlin Liu, Zhenbang Chen, Piyi Zu, Yide Du, Ji Wang
arXiv categories: cs.PL

Pointer analysis is a fundamental technique for compiler optimization and program analysis. Flow-sensitive pointer analysis provides high precision but is difficult to scale to large projects. Tailored for rapid iteration scenarios where software evolves continuously, we introduce IncSFS, the first incremental full-sparse flow-sensitive pointer analysis algorithm for C/C++ programs. IncSFS first transforms the value-flow graph into a constraint graph and performs strongly connected component detection to ensure precision. It then propagates increases and decreases in points-to sets in an interleaved manner, supporting code deletion and insertion within a single analysis pass. IncSFS is guaranteed to terminate and compute the least fixed point when the points-to relation remains object-acyclic during analysis. Experiments on six large-scale real-world projects show that IncSFS is precise and efficient, achieving average speedups of 9.60x over full flow-sensitive pointer analysis and 5.84x over the traditional reset-recompute approach. It also improves efficiency by 15.8% over state-of-the-art incremental pointer analysis algorithms that propagate points-to-set changes.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-25T14:20:08Z
Promit Panja, André Platzer
arXiv categories: cs.LO, eess.SY

Control invariance validates that dynamical systems have a control input that preserves a given property at all times. This paper introduces a set of sound axioms and proof rules in differential dynamic logic (dL) that enable verification of control invariance. First, the scalar and vector comparison principles, relating a system of differential equations to a comparison system such that invariance properties can be established more easily, are axiomatized in dL. This axiomatization primarily utilizes differential ghosts, which are proof-theoretic generalizations of comparison systems. Next, with the comparison principles serving as the basis, comparison invariants are introduced, and sound axioms and proof rules are derived. Comparison invariants reduce the question of control invariance to a functional inequality on its Lie derivative for a suitable class of functions, moreover, the right choice of function can result in decidable arithmetic. Furthermore, the perennially popular control barrier functions (CBFs) used in safety-critical control are shown to be a special instance of comparison invariants. This yields an axiomatization of CBFs that leads to a dedicated set of proof rules. The rules allow for the verification of CBFs, which are traditionally used for synthesizing safe controllers without verification. Lastly, comparison invariants are shown to unify several other safety verification techniques, including Darboux invariants and differential invariants, further cementing their versatility.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-25T14:23:04Z
A. R. Balasubramanian, Dmitry Chistikov, Rupak Majumdar
arXiv categories: cs.FL, cs.CC, cs.LO

Many problems in the verification of recursive programs can be reduced to pushdown model checking. In this problem, we are given as input a pushdown automaton (PDA) over a constant-sized stack alphabet, and a description of undesirable behaviors given by an intersection of NFAs, and the problem is to decide if there is a behavior of the PDA that belongs to the set of undesirable behaviors. It is well-known that there is an algorithm for this problem that runs in time $O(n^{2k} |Σ| + n^{3k})$, where $n$ is the maximum number of states of the PDA and the NFAs, $Σ$ is the common input alphabet, and $k-1$ is the number of NFAs. Despite the importance of this problem, no better algorithm is known for it. In this paper, we provide an explanation for this lack of progress using the lens of fine-grained complexity theory. We prove that if the $3k$-Clique hypothesis (resp. combinatorial $3k$-Clique hypothesis) is true, then for any $ε> 0$, there is no algorithm (resp. combinatorial algorithm) that solves this problem in time $O((n^{(ω-1)k} |Σ| + n^{ωk})^{1-ε})$ (resp. $O((n^{2k} |Σ| + n^{3k})^{1-ε})$) where $ω$ is the matrix multiplication exponent. Furthermore, using the combinatorial hypothesis, we also show that pushdown model checking over constant-sized input alphabets cannot be solved in time faster than $O(n^{3(k-1)-ε})$ for any $ε> 0$. Finally, we investigate the possibility of an $O(N^{3k-ε})$ time algorithm for this problem where $N$ is the total bit size of the input. We formulate a new hypothesis, the 2NPDA$(k)$ hypothesis, that helps explain the lack of $O(N^{3k-ε})$ time algorithms for this problem. To corroborate this hypothesis, we show a web of linear-time reductions between the 2NPDA$(k)$ hypothesis, pushdown model checking, and other problems in formal language and automata theory.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-08-26T05:47:17Z
Ranit Debnath Akash, Ashish Kumar, Gang Tan, Saeid Tizpaz-Niari
arXiv categories: cs.SE, cs.AI, cs.LG

Data-driven software systems are increasingly deployed in high-stakes socio-economic domains, from criminal justice to financial lending. However, these systems often exhibit individual discrimination---unjustified disparities in which a program yields different outcomes for similar individuals who differ only in their protected attributes (e.g., race, gender, age). While existing research has focused on detecting and quantifying these bugs, there remains a critical lack of principled mechanisms to explain and localize individual fairness bugs. Current explanation techniques are largely designed for single-input decisions rather than the relational nature of discrimination, which inherently involves a comparison between an original and a counterfactual pair. We present REMI, a framework for the automated localization, explanation, and mitigation of individual discrimination. Inspired by loop-invariant synthesis in formal methods, we treat counterfactual fairness as a relational invariant discovery problem. We introduce a bidirectional relational explanation framework that learns over paired examples $(x, x')$ to identify regions of the input space where fairness is violated. Unlike traditional one-way implication pairs used in invariant inference, our approach enforces bidirectional constraints: requiring identical outcomes for both original and counterfactual samples. REMI utilizes three data-alignment techniques to infer interpretable rule-based models that act as "fairness invariants." These rules serve as guardrails to selectively block or relabel unfair predictions without requiring model retraining. Our evaluation on symbolic and neural network programs demonstrates that REMI localizes ground-truth fairness bugs in over 83% of cases, significantly outperforming state-of-the-art baselines and reducing discriminatory decisions in black-box models by up to 70%.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-08-27T06:55:24Z
Yuhao Liu, Yingnan Zhou, Weijie Liu, Yan Jia, Zheli Liu
arXiv categories: cs.CR, cs.SE

As the most widely used container orchestration platform, Kubernetes provides flexible privilege configuration by allowing developers to manage Linux capabilities via manifest files. However, developers rely on default settings or coarse-grained security contexts in practice, violating the principle of least privilege and enlarging the attack surface of containerized workloads. Existing studies either detect vulnerable patterns in Kubernetes manifests or infer required capabilities for standalone Linux programs, but they do not directly address capability minimization in Kubernetes. To bridge this gap, we first conduct an empirical study on three open-source datasets, revealing that 74.67% of projects lack capability configurations. Motivated by our observations, we propose KubeCap, a framework for Kubernetes capability minimization. KubeCap translates deployment specifications into deterministic manifests, locates container entrypoints, performs reachability-guided system call analysis, and leverages LLM-assisted rule specification to derive syscall--parameter--capability relations from Linux kernel code. Based on these results, KubeCap infers the minimal capability set required by each workload and automatically generates repaired manifests. Evaluation on 10 representative Go-based Kubernetes projects shows an average capability reduction rate of 54.97%, outperforming rapid type analysis and class hierarchy analysis baselines while maintaining practical analysis cost. These results demonstrate KubeCap's effectiveness in enforcing least privilege in Kubernetes.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-08-27T09:24:20Z
Stian Lybech, Eun-Young Kang, Riccardo Tonello, Anders Dalskov
arXiv categories: cs.CR, cs.PL

This paper develops a model of a smart-contract language for a blockchain architecture with off-chain components. Off-chain components are pieces of smart contracts that execute at designated locations outside of the network of blockchain nodes, but remain synchronised with the on-chain contract state. They react to changes to the on-chain state, but may also notify the on-chain component about events in the world, e.g. stock prices, weather data etc., or even act as a bridge between different blockchains. This affords greater flexibility for the developer, but may also enable new vulnerabilities. As a concrete example, we use the model to study the problem of ensuring integrity and secrecy of data between the on-chain and off-chain components, using static information flow control techniques. This fails, even in the absence of a loop construct, because off-chain components act as separate threads and can encode a blocking construct e.g. through recursive method calls. We end the paper with a discussion of possible ways to remedy this situation.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-08-28T07:34:57Z
Animesh Shaw
arXiv categories: cs.CR, cs.AI, cs.MA, cs.SE

Large language models are increasingly used to author Infrastructure-as-Code (IaC), where a single insecure default can be deployed directly into production. Prior evaluations report raw vulnerability counts for model-generated IaC, but without a human baseline they cannot determine whether models are actually worse than engineers. We introduce GenIaC-SecBench, a benchmark of 100 deployment scenarios stratified by architectural complexity, evaluated across 12 model configurations from four vendors, producing 1,196 IaC artifacts scanned by three independent policy engines (Checkov, Trivy, KICS). Critically, we also scan 634 human-authored IaC templates with the same toolchain, providing the first size-matched human security baseline. Vulnerability density is strongly inverse to artifact size (Spearman $ρ= -0.55$, $p < 10^{-77}$), meaning unmatched comparisons measure size rather than security. When matched on declared-resource count, all model configurations fall within 3.21x--3.87x the human vulnerability density, with the gap widening for simpler tasks (4.9x at one resource, 1.4x at twenty or more). We decompose reasoning into standard generation, prompt-engineered chain-of-thought, and vendor extended-thinking APIs. Vendor extended thinking significantly outperforms prompted chain-of-thought ($-12.0\%$, $p = 0.0013$), while prompted chain-of-thought is indistinguishable from standard generation ($-1.3\%$, n.s.). Token instrumentation shows extended thinking uses under 1\% of the output budget, explaining its bounded effect. Two negative results also emerge: deployability does not correlate with vulnerability ($r = 0.158$, $p = 0.625$), and classical complete-case Friedman testing is infeasible for realistic benchmark designs, motivating the Skillings-Mack statistic. All code, data, and regeneration scripts are released.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE selected for review · published 2026-08-28T16:29:10Z
Mennatullah T. Khedr, Mengwei Xu, John S. Fitzgerald, Peter Gorm Larsen
arXiv categories: cs.SE

Current approaches to engineering dependable Digital Twins (DTs) of Cyber-Physical Systems lack practical guidance on how qualities such as relevance, verifiability, substitutability and fidelity may be formalised and verified. This need is amplified in Systems-of-Systems (SoS), where reliance is placed on the composition of DTs. The goal of this study is to identify foundational challenges that a framework for DT validation and verification should address in an SoS setting, and to investigate the formalisation of individual DT artefacts as a step towards compositional reasoning. We present a case study based on a DT-enabled greenhouse SoS modelled in VDM-RT (Vienna Development Method, Real-Time), including executable formal models, a property-based account of DT qualities, and an analysis of the obstacles arising when attempting to compose these artefacts at the SoS level. We consider how DT qualities may be operationalised as sets of verifiable properties. Formal modelling and analysis techniques and tools supporting their verification are identified. The study reveals how interpretations of DT qualities must adapt to different architectural roles and how local quality guarantees form assumptions for compositional reasoning. Full formalisation and verification of SoS composition is identified as future work.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-24T09:00:33Z
Patrick Cousot
arXiv categories: cs.LO

Similar to Skolem's nonstandard models of Peano's naturals, we show that axiomatic semantics based on Hoare logic has nonstandard models and so does not specify a unique, well-defined, and formal operational semantics of programming languages. We propose to enrich axiomatic semantics with additional proof obligations to solve this ambiguity problem. These proof obligations are always satisfied for standard trace models so that Hoare logic proofs are unchanged for these standard models.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-25T13:48:03Z
Aditya Thimmaiah, Tong-Nong Lin, Milos Gligoric
arXiv categories: cs.PL, cs.DB

ISO Graph Query Language (GQL) is the first international standard for property graph-based graph query languages, standardized as ISO/IEC 39075 in 2024. However, ISO/IEC 39075 codifies its semantics informally across 600+ pages of prose, making it difficult to formally reason about the standard or for a standard-faithful implementation. Existing formalizations are not adequate because they either: (1) significantly reduce the semantic complexity by omitting bag semantics, schemas, and composite queries on multiple graphs; (2) or significantly reduce the syntactic complexity by only considering isolated fragments such as pattern-matching, leaving the full query pipeline unformalized. Yet it is these semantic-syntactic features that make formalizing GQL non-trivial. We present MGQL, the first mechanized, small-step operational semantics for a substantial read-only fragment of GQL that is grounded in the ISO/IEC 39075 standard. Our formalization models multi-graph property graphs with mixed edge directionality and supports a large fraction of GQL pattern constructs: quantified paths and edges, directional and undirected matching, label expressions, pattern lists, and composite queries. The semantics is supported by a schema-aware type system that refines variable types via closed-graph schemas, tracks nullability, supports multiple composite query operators, and models quantified-path bindings with list types. We prove that our type system is sound, ensuring an end-to-end guarantee of well-formed queries yielding results that conform to their declared schemas. MGQL provides the first bridge between GQL's informal specification and a mechanized implementation, enabling formal reasoning about correctness.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-26T08:22:19Z
Yifan Shi, Wei Zhang, Tianyi Cui
arXiv categories: cs.PL, cs.SE

Modern software -- from plugin systems to self-evolving agent harnesses -- increasingly requires dynamic composition, yet its formal foundations remain underdeveloped. We identify two orthogonal dimensions of the problem: temporal composability, the ability to completely revert a component's side effects upon removal, and spatial composability, the ability to declare and reactively manage inter-component dependencies. We address the two dimensions by lifting classical effect and coeffect concepts to runtime mechanisms. In particular, we formalize revertible effects, in which every context transformation carries an inverse that the runtime holds, establishing temporal composability local to one component. We formalize reactive coeffects, in which every context change is classified against a component's coeffect specification to drive its activation and deactivation, establishing spatial composability local to one component. We then unify the effect context and the coeffect context into a single context type and mediate every effect and coeffect through it, yielding a discipline we call the context paradigm; the mediation induces an observational equivalence up to which the effects of distinct components interleave without disturbing one another. Combining these mechanisms into the notion of a component, we give a calculus of dynamic composition whose metatheory carries spatiotemporal composability from a single component to a whole system of interleaved components. We implement these ideas in Cordis, a meta-framework of spatiotemporal composability that provides a core library with effect tracking and coeffect resolution, as well as a declarative component loader with configuration reconciliation and hot module replacement.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-27T14:28:11Z
Vincent Wang-Maścianica
arXiv categories: cs.PL, cs.LO

A functor is a familiar model of an implementation, where every operation in a specification is assigned a concrete instantiation at the outset. But some tasks are less eager: we often want to assemble systems while leaving backend choices such as data representations and algorithms for later. We observe that cofunctors admit a direct reading as such partial implementations, which are implementations whose extra argument is a state-dependent family of deferred choices. While cofunctors (also called retrofunctors) are not novel, their conceptual and purposive reading in this manner appears to be

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-27T17:59:01Z
Chiké Abuah
arXiv categories: cs.PL, cs.SE

Empirical comparisons between systems are a standard form of evidence in computer science research, but few are checked for statistical validity: most are never framed as statistical tests at all. Existing multiple-comparison procedures could control the resulting error, but need inputs (what an analysis examined, and how its observations are arranged) that are not recoverable from a list of p-values. We introduce Tacet, a language in which an analysis declares what it generated, states what it expects to find, and is refused any claim it cannot afford or cannot properly test. Its core calculus T pairs a free estimation sublanguage, carrying a reported footprint and a purity bit that records whether any outcome was consulted in building a value, with a priced claim sublanguage, carrying a wealth transformer, connected only by a mechanism that prices a comparison. A sample selected by reading outcomes sets the purity bit and is recorded as having examined everything it read, permanently, so it can never be granted a one-sided or confirmatory price, without the system ever asking whether the analyst intended to cherry-pick. Whether a comparison is paired or clustered is computed statically from the artifact schema, from declared functional dependencies between key fields alone and before any data is read, and a mechanism that assumes that structure away is refused rather than priced. Because the wealth transformer is antitone in the realized p-value, affordability can be checked before the analysis runs too, turning pre-registration into a typing rule. We prove the metatheory machine-checked in Lean 4 with no admitted gaps, and demonstrate the approach on a reference implementation and two case studies on published artifacts, the SWE-bench Verified leaderboard and BIG-Bench Hard.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-08-28T00:29:48Z
Jack Liell-Cock, Sam Staton
arXiv categories: cs.PL

The algebraic effects and handlers paradigm separates the concerns of the interface and implementation of computational effects in programming languages. We present Cambria, a language that extends this framework to the parametrized setting. Effect signatures may use abstract parameter types that are instantiated by the handler along with the operation implementations. Parameters abstract over resources, such as memory locations or thread IDs, permitting algebraic effects to encode dynamic allocation. They are first-class in the type system but erased at runtime, requiring no coercions or type-directed reduction. We prove parametricity via a step-indexed logical relation, formalizing the abstraction guarantee provided by parametrized handlers. We also establish type safety and classify the annotations needed for completeness of the type inference algorithm. We demonstrate Cambria's practicality with a working implementation and provide examples including local state, Pólya's urn, and concurrent thread management. The last is a parametrized effect whose abstract thread IDs are shared between concurrent computations, going beyond standard instances. Cambria is the first calculus with user-defined resource-allocating effects that guarantees, via parametricity, that client code cannot depend on how a handler represents its resources.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-25T14:54:24Z
Adam T. Burke
arXiv categories: cs.SE, cs.AI, cs.PL

This paper introduces an environment for constructing literate programs in concert with language-aware machine agents. This environment includes a grammar for executable program essays, a parser that treats names as first-class objects, an internal name-graph which relates prose, names and executable artifacts, and a binding mechanism for existing languages and testing toolsets. This supports co-location of code with its most relevant natural language and structured data context, making better use of Large Language Model (LLM) context windows. It also provides LLM coding agents with a toolset more analogous to the symbol-aware search and usage information available in human programmer-facing Integrated Development Environments (IDEs). We describe a working implementation with bindings to three established programming languages, and several example programs.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-26T19:41:04Z
Parker Ziegler, David Minh-Duy Cao, Justin Lubin, Sarah E. Chasins
arXiv categories: cs.PL, cs.HC

Decades of programming languages research has contributed novel approaches to program editing that go beyond modifying text, including direct manipulation programming, structure editing, and automated refactoring tools. However, the rapid growth of natural language programming largely reinforces a view of programs as text and program editing as (unstructured) text transformation. How can we develop unified programming systems that bridge the gap between these approaches, supporting multiple editing paradigms in concert? We take a first step toward answering these questions by introducing a framework that enables program editing via both direct manipulation and natural language, and instantiate this framework in a variant of the $\texttt{cartokit}$ direct manipulation programming system. Our key insight is to treat programs as sequences of structured edits and to use an edit language as a shared interface for both direct manipulation and natural language interactions, leveraging constrained decoding to support the latter. Using our instantiation, we conducted a within-subjects study ($N$=18) to understand how the combination of direct manipulation and natural language as editing modalities changes the programming process compared to each modality alone. Perhaps surprisingly, we found that study participants overwhelmingly chose to edit via direct manipulation when both modalities were available, performing just 6.14% of edits via natural language. Our thematic analysis of study sessions revealed that direct manipulation aided task decomposition, encouraged incremental editing, and helped mitigate known challenges in natural language programming related to understanding model capabilities and model-generated code. Our edit-based framework and study findings lay out a possible pathway for future research on programming systems that blend natural language with alternative editing modalities.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-27T17:52:31Z
Mehul Shah, Robert Fiszer, Marek Perkowski
arXiv categories: quant-ph, cs.LO

Quantum algorithms promise advantages beyond classical reach, but running them on error-corrected hardware requires translating Boolean specifications into reversible circuits, and the resources that translation demands determine what is executable. Established methods minimize a Boolean expression and map it to a circuit, assuming the minimized form is best. Here we show that minimized expressions retain algebraic structure minimization cannot reach, arising from containment and complementary-polarity relationships among their terms, and that extracting it yields circuits cheaper to execute despite having more operations. The decisive quantity is not a circuit's operation count but the control count of its widest operation, a superlinear cost; extracting shared factors trades a few wide operations for many narrow ones and reduces qubit count. Across benchmarks and oracles from quantum search and factoring algorithms, at the representation level the transformation never increases either cost measure, a guarantee from its construction. Translation to an executable circuit returns part of that advantage, since auxiliary lines must be uncomputed, yet the factorized circuit still left a leading circuit-level optimizer reaching lower final counts, and faster, than unaided. The representation of a computation is therefore itself a resource, optimizable before compilation and distinct from both logic minimization and circuit-level optimization.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-08-28T11:23:11Z
Francisco J. Moreno Velo, Almudena García Jurado-Centurión
arXiv categories: cs.PL

This paper presents the definition of a simple programming language used as the basis for developing a practical compiler design course. The course explains step by step how to build a compiler, from the initial analysis stages to code generation. The developed compiler generates code for various processors (MIPS, Intel, and RISC-V) and operating systems (MS-Windows and Linux). The course can be adapted to different levels of difficulty and can be used as a starting point for explaining more advanced topics.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-08-24T14:06:21Z
Radouane Bouchekir, Damir Safin, Tomas Bueno Momcilovic
arXiv categories: cs.SE

Large Language Models (LLMs) agents deployed in vehicles must satisfy a written operating policy on every turn: a single hallucinated identifier, omitted mandatory side-effect, or premature completion claim fails the task. We present AgentGuardUtil, our entry to CAR-bench Track~1, which treats the AI planer (LLM) as a fallible proposer inside a grounded verify-and-revise loop. Its core novelty is a runtime policy compiler: the natural-language policy shipped with each conversation is compiled, once per policy, into typed machine-checkable rules, a subset of which receive an executable form. A deterministic obligation engine interprets these rules against live tool results and the simulated post-write state of the draft itself, emitting the exact remedial calls with computed arguments rather than natural-language reminders. Around this engine, 25 deterministic gates (identifier provenance, schema and enum validity, gather-before-act, confirmation and future-time protocols) and an LLM critic produce tiered findings that drive a bounded revision loop tuned for the pass k metric.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-24T15:17:58Z
Aldo Gangemi, Emanuele Bottazzi
arXiv categories: cs.AI, cs.LO

Large Language Models (LLMs) recognise patterns but do not natively track the path of exclusions that a coherent discourse demands. When an input rests on a fabricated authority, a misapplied mechanism, or a surreptitious analogy, an unsteered LLM tends to engage with it as if it were grounded, and to reify the misstep into any structured output it generates. Logic-Augmented Generation (LAG) with POLANYI++, an LLM-steering method that uses heuristics, ontologies and problem solving methods for tacit knowledge extraction, produces an Extended Knowledge Graph (XKG) in OWL2, but inherits the same vulnerability: a sophisticated nonsensical input is reified into the graph alongside the legitimate triples, and is hardly detectable by automated reasoners since the XKG is generated jointly with the wrong assumptions. We introduce DARKSIDE, a coherence auditing method on top of POLANYI++. It formalises the trail as an explicit data structure of accumulated exclusions over discourse time, complemented by a warrant axis that classifies each named referent as Warranted, Unattested, Misattributed or Fabricated, with an escalation rule that pushes the DelegationRiskAssessment to UNSAFE when the fabricated rate is positive or the unsupported rate exceeds a threshold. We evaluate DARKSIDE as a steering layer over a Gemini 3 on BSBench, a 100-item adversarial corpus of sophisticated-sounding nonsense across software engineering, finance, healthcare, physics and law, with Claude Sonnet 4.6 as an independent judge. The empirical evidence supports an architectural claim: when an LLM forward pass is wrapped in an ontology-mediated negative-trail apparatus, the structural pattern-vs-path gap can be partially scaffolded. The XKG functions as the missing memory, and the warrant axis as an epistemic firewall.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-24T23:51:02Z
Andrei Mikhailov, Mikhail Burtsev, Alsu Sagirova
arXiv categories: cs.AI, cs.MA, cs.PL

Large Language Models excel at code generation, yet competitive programming exposes a persistent failure mode: existing multi-agent pipelines distribute work over generic planner, coder, and debugger roles and delegate the choice of algorithmic technique to the backbone alone. We present MARS (Multi-Agent Relay of Specialized LLMs), a prompt-only framework in which each agent is a topic specialist---dynamic programming, graphs, strings, geometry, and so on---grounded by retrieval-augmented generation over an algorithm-theory corpus. Given a problem, retrieval selects a small team of relevant specialists; a starter writes an initial C++17 solution, and each subsequent turn runs the candidate against public examples in a sandbox, lets the active specialist keep, repair, or hand off the draft, and forwards a structured packet to the next specialist. A single infrastructure-fixer pass normalizes boilerplate at the end. On the CodeContests test split with Gemma 4, MARS reaches $0.624 \pm 0.006$ pass rate at $2.3$ recorded pipeline stages per task ($+14.4$ percentage points over direct prompting), closing most of the gap to CodeSIM ($0.731$) at $3.3{\times}$ lower wall-clock cost and substantially smaller variance in per-task token spend. The source code is available on GitHub: https://github.com/fckand/mars.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-08-25T03:48:16Z
Wenbiao Li, Yuqiao Xu
arXiv categories: cs.CR, cs.SE

LLM agents routinely include privacy-sensitive data (PSD) in tool call arguments beyond what the invoked tools require, crossing trust boundaries to third-party services on every invocation. A controlled measurement on three production LLMs (GPT-4o, Claude 3.5 Sonnet, Llama-3.3-70B) shows that 81--88\% of tool calls include unnecessary PSD under default prompts; explicit privacy instructions still leave 36--76\% over-sharing. Existing defenses gate calls (allow/block) or label flows (information-flow control) but cannot \emph{rewrite} argument values, and PII detection tools miss implicit PSD like ``Memorial Sloan Kettering'' (a hospital name that implies a diagnosis). We present \system{}, a middleware that intercepts tool calls and rewrites their arguments to the minimum data necessary for tool functionality, combining schema-aware necessity analysis with four operations: removal, generalization, substitution, and truncation. Live validation on 307 tool calls across the three LLMs above reduces privacy cost by 81.2--92.0\% at 100\% argument-level task validity (TOST equivalence $p{<}0.001$ at $Δ{=}1.0$); on 25 unannotated Model Context Protocol (MCP) schemas, by 79.0\% with no \texttt{minimum\_necessary} metadata. An optional LLM content-necessity layer strips task-irrelevant PSD from otherwise-necessary free-text fields, raising live-LLM reduction to 85.1--95.6\% and author-schema reduction from 71.1\% to 90.9\%. Median latency is 1.77\,ms.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-25T08:26:31Z
Weihan Peng, Yuling Shi, Yingwei Ma, Longfei Yun, Beijun Shen, Xiaodong Gu
arXiv categories: cs.SE, cs.CL, cs.PL

Answering developer questions about a software repository is a critical yet under-explored problem in software engineering. While existing repository understanding methods have advanced the field, they predominantly rely on surface-level code retrieval and lack the ability for deep reasoning over multiple files, complex software architectures, and grounding answers in long-range code dependencies. To address these limitations, we propose DeepRepoQA, a novel question answering (QA) framework for repository-level code understanding. DeepRepoQA builds on an agentic framework where LLM agents find answers through a systematic tree search over the repository structure. A Monte-Carlo Tree Search (MCTS) mechanism is employed to empower agents to dynamically search, navigate, and inspect code, enabling effective multi-hop reasoning over long-range code dependencies. Comprehensive experiments on the SWE-QA benchmark demonstrate substantial performance gains over strong baselines, validating the effectiveness of systematic MCTS-guided exploration for multi-hop repository reasoning.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-25T18:57:39Z
Gokul Karthik Kumar, Yotam Perlitz, Corey Lammie, Andrea Giovannini, Katja Hose
arXiv categories: cs.CL, cs.AI, cs.DB, cs.LG, cs.PL

GPUs increasingly accelerate database systems, but query-specific peak performance still often relies on hand-written kernels. Existing LLM kernel benchmarks focus on machine learning operators, leaving irregular, heterogeneous, data-movement-heavy database-style operators untested. We introduce DataKernelBench, which translates SQL into validated PyTorch TorchPlan programs and evaluates LLMs that optimize either the core tensor-bounded snippet or the full query in CUDA or Triton through execution-guided repair. Across ten proprietary and open-weight models on TPC-H SF10 with an H100 GPU, the strongest full-query CUDA configuration achieves $2.11\times$ speedup over the TorchPlan baseline at full pass rate. We find that higher-performing implementations commonly use kernel fusion and execution-strategy changes, stronger models benefit most from full-query specialization, and workload context matters more than hardware context. To handle data larger than GPU memory, we extend TorchPlan with Dask-cuDF for on-demand partition loading on TPC-H SF100 with four H100 GPUs, achieving $2.54\times$ speedup. Project page: https://kerneldf.github.io/datakernelbench

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-25T23:19:41Z
Henry Robbins, Connor Lawless, Madeleine Udell, Ellen Vitercik
arXiv categories: cs.AI, cs.LO, math.OC

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing computationally efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. Reliable automation requires robust methods for verifying that proposed formulations preserve the underlying optimization problem. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference formulation. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE's accuracy but produces no certificate. These methods enable reliable verification in automated optimization modeling.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-26T11:38:24Z
Tilman Hinnerichs, Sebastijan Dumancic, Neil Yorke-Smith
arXiv categories: cs.AI, cs.LG, cs.PL, cs.SE

Large language models (LLMs) excel at programming, but not when the task fixes the target language: prompted with a grammar rare in their training data, their programs usually break the grammar or fail the given specification. Enumerative synthesizers search the space of syntactically correct programs systematically guided by LLMs; the state of the art guides them by approximating LLM proposals into rule frequencies, which loses where each construct belongs and prunes every rule the proposals miss, exactly when the proposals are wrong. We present Narcissus, a synthesizer that keeps the proposals as syntax trees and scores each expansion of a candidate program in its context: does a proposal with the same surrounding structure continue the same way, and does the expansion rebuild a fragment the proposals repeat? A regularization term keeps every rule reachable, so wrong proposals delay the solution but cannot hide it. Across five domains and two search backends, Narcissus beats static guidance at every budget and consistently outperforms re-prompting the LLM to fix its own proposals; it reaches proposal-like programs an order of magnitude sooner and solves $40\%$ of ARC tasks where the raw proposals solve $13\%$, all without a single LLM call during search.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-08-26T12:44:32Z
Zhiyuan Xu, Muhammad Firhard Roslan, Joseph Gardiner, Sana Belguith, Lichao Wu
arXiv categories: cs.LG, cs.AI, cs.CR, cs.SE

Safety evaluation is critical for assessing whether aligned Large Language Models (LLMs) remain robust against jailbreak attacks. Existing automated testing methods, however, largely rely on response-level feedback: each candidate prompt typically requires generating a target-model response to evaluate its attack effectiveness. This process is expensive and, more importantly, provides only sparse guidance on strongly aligned models, where most candidates are rejected with the same failure outcome. This paper presents NeuronFuzz, a white-box fuzzing framework that exploits internal safety neurons as continuous execution feedback for LLM safety evaluation. A SafetyOracle converts safety-neuron activations into a continuous safety alarm score that serves as feedback for fuzzing and can be obtained during prefill, eliminating response generation from the fuzzing loop. To construct the SafetyOracle, NeuronFuzz uses template-invariant harmful and benign inputs and stability-aware selection to identify a compact set of safety neurons whose activations capture harmful-intent recognition. Moreover, since the safety alarm score is differentiable, NeuronFuzz uses its gradients to identify safety-sensitive template positions and a masked language model to generate fluent, context-compatible mutations while preserving original harmful payload and avoiding additional optimization variables. We evaluate NeuronFuzz across 21 text and multimodal models. Across five white-box source models, it achieves a 76-100% jailbreak discovery rate, outperforming baselines by up to 48 percentage points. Its optimized templates further transfer zero-shot to open-weight and six proprietary target models, achieving average ASR and top-5 ensemble ASR (EASR) of 69.6%/92.6% and 44.1%/60.0%, respectively.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-08-26T20:57:15Z
Ghfran Jabour, Sergey Ivanov
arXiv categories: cs.SE, cs.PL

Generated computer-vision code can be runnable without satisfying the task contract enforced by a downstream evaluator. We study that gap with Spec2Vision, an experimental framework for producing and evaluating specification-grounded CV pipeline bundles through a staged runtime that keeps the task contract explicit across synthesis, screening, testing, and bounded repair. The benchmark evaluates 17 CV tasks, 10 executable conditions, and 5 repeats per task-condition cell, for 850 primary runs. In the primary 850-run evaluation, Spec2Vision reaches 81/85 evaluator-test passes; removing structural repair drops to 55/85, compatibility scaffolding to 58/85, and generator preflight to 39/85. The executable single-agent baselines expose progressively richer task specifications to the model, culminating in direct source-spec exposure, yet remain much weaker overall, from 17/85 for lightweight task grounding to 35/85 evaluator-test passes. The lightweight baseline nevertheless remains core-runnable in 85/85 runs but reaches only 17/85 evaluator-test passes and 6/85 strict-delivery successes, showing that runnability is not equivalent to delivery. Across this benchmark, the strongest evidence comes from keeping the task contract explicit across staged generation, checking, and repair. Artifacts are provided to support audit of run bundles, model-visible inputs, and derived tables.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-08-27T13:59:04Z
Xiaokun Guo, Zhen Xu, Dongdong Huo, Yanqiu Zhang, Wei Wang, Qinfu Yang, Dongjin Yu, Yu Wang
arXiv categories: cs.AI, cs.SE

Tool-augmented LLM agents must rely on untrusted runtime Observations to complete open-ended tasks; however, when tool outputs no longer merely provide data but begin to specify concrete actions, they effectively become ``commands'' that can drive real-world side effects beyond user intent. We argue that this risk arises from conflating action induction with execution authorization. To address this distinction, we propose SARA, which treats action induction and execution authorization as distinct runtime roles and separates action provenance from execution authority. On the Observation side, a context-isolated Action Probe exposes action-inducing semantics and persistently records action-origin provenance across steps as a review signal; on the execution side, actual tool calls are authorized only against the user objective and audited evidence from authorized successful executions, while satisfying goal, execution-chain, and argument-level support. To preserve this separation across multi-step execution, SARA applies No-History-Promotion to prevent historical recurrence from laundering action origins into execution authority. Across AgentDojo and AgentDyn, SARA limits ASR to no more than \(0.63\%\) across four primary evaluation settings while maintaining competitive task utility, and consistently reduces ASR across additional Agent backbones.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE selected for review · published 2026-08-27T16:03:57Z
Xingbang He, Yuanwei Chen, Yi Qian, Haiyang Wei, Ligeng Chen, Zenan Fu, Linzhang Wang, Hao Wu, Bing Mao
arXiv categories: cs.CR, cs.SE

Instruction hierarchy is a model-side defense that assigns instructions different levels of privilege according to their sources. These levels constrain which content may direct model behavior. During agent execution, however, agent harnesses construct context for each model invocation. This construction can elevate low-level content to a higher instruction level and grant it greater model-facing privilege. We introduce instruction privilege escalation. In this attack, an attacker induces an agent to elevate low-level malicious content to a higher instruction level. The elevated content then causes the agent to execute instructions it would not follow at their original level. We evaluate this threat by using multi-agent mechanisms to achieve 13 attack objectives across six coding-agent harnesses. These objectives span confidentiality, integrity, availability, and remote code execution. With unrestricted action execution, the attacks achieve all 13 objectives on all six harnesses. Under automatic permission review, the attacks achieve all 13 objectives on all three harnesses that provide this mode. We further reproduce the vulnerability using harness-provided persistent goals and scheduled tasks. These results demonstrate the generality of instruction privilege escalation.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-25T08:49:28Z
Gábor Kusper
arXiv categories: cs.LO

CSFLOC is a non-CDCL SAT decision procedure based on counting subsumed full-length ordered clauses. The classical CSFLOC loop traverses the ordered space of full-length clauses by a monotone counter: if the current full-length clause is not subsumed by the input formula, its negation is a satisfying assignment; otherwise, a subsuming clause determines a counter jump. The main bottleneck is the repeated search for such a subsuming clause. This paper presents CSFLOC-WL, and its current implementation CSFLOC-WL3, in which this search is replaced by watched-literal prefix propagation over the negation of the current full-length clause represented by the counter. The central mechanism is early conflict detection: if propagation under a common prefix derives opposite unit consequences for the same variable, then the two reason clauses are resolved immediately and the resolvent is used as a new counter-jump cause. The resulting solver is not a CDCL solver: it has no CDCL decision tree, no restart policy, and no first-UIP backjumping loop. It remains a counter-guided full-length-clause-counting solver, but it imports the watched-literal data structure and reason clauses as engineering tools for discovering jumps. Experiments on selected UNSAT SATLIB instances compare CSFLOC-WL3 with CSFLOC21TU and CaDiCaL 3.0.0. The results are mixed: CSFLOC-WL3 is strong on several random 3-SAT instances near the random-3-SAT satisfiability threshold, whereas CSFLOC21TU remains faster on several structured cases, apparently because it contains a more mature cache mechanism that is not yet present in CSFLOC-WL3.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-25T11:21:53Z
Joris Nieuwveld
arXiv categories: cs.LO, cs.FL

For multiplicatively independent natural numbers $α$ and $β$, Villemaire showed in 1992 that the first-order theory of Presburger arithmetic expanded with both Büchi predicates $V_α$ and $V_β$ is undecidable, as it encodes multiplication. In recent years, Hieronymi and Schulz showed that Presburger arithmetic expanded with the weaker power predicates $α^\mathbb{N} = \{α^n: n \in \mathbb{N}\}$ and $β^\mathbb{N}$ is also undecidable, while Karimov et al. showed that the existential fragment of this theory is decidable. These results left open the natural problem of determining the decidability of the existential fragment of Villemaire's original expansion. We settle this question for coprime $α$ and $β$. Specifically, we give a quantifier-elimination argument that proves the decidability of the existential fragment of $\mathsf{FO}(\mathbb{Z};<,+, V_α, V_β)$.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-25T16:19:02Z
Bao Gia Hoang, Tuyen Van Kieu, Khanh Van To
arXiv categories: cs.LO

Peak power limits restrict concurrent tasks and may increase assembly-line cycle time. To the best of our knowledge, this study is the first to minimize cycle time for the simple assembly line balancing problem type 2 (SALBP-2) with a fixed number of workstations and a fixed limit on total instantaneous power. An exact satisfiability (SAT) method finds feasible schedules, searches systematically for shorter cycles, and proves optimality when possible. Two reproducible formulas define looser and tighter power limits for 72 cases based on the standard SALBP library, with Gurobi and CPLEX providing commercial MIP and CP comparisons. Relative to standard SALBP-2 optima, the two limits increase the best-known cycle time by 16.49% and 61.02% on average. The best-performing SAT configurations find a feasible solution for every case, solve more cases to optimality than each commercial solver, and when both prove optimality, are almost always faster under the reported settings.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-26T04:14:59Z
Huy Tuan Nguyen, Duc Trung Kim Nguyen, Khanh To Van
arXiv categories: cs.LO

The Job Shop Scheduling Problem with Power Requirements (JSPPR) extends the classical job shop scheduling problem by imposing time-varying limits on instantaneous power consumption. Previous studies have used a mixed-integer linear programming formulation and the GRASP x ELS metaheuristic, but no SAT-based exact approach or constraint programming model has been reported. This paper develops the first exact SAT and constraint programming (CP) formulations for the JSPPR. On the 35 published benchmark instances, both SAT and CP prove global optimality for all instances and obtain identical optimal makespans, substantially improving upon the best previously reported results. They also establish four improved makespan values over the GRASP x ELS results reported in the original study. CP proves optimality faster than SAT, while both exact approaches substantially improve the optimality coverage of the MILP formulations, which prove optimality on only 6 and 10 instances using CPLEX and Gurobi, respectively. The certified optimal solutions also reveal inconsistencies in several previously reported benchmark results, including makespans below the proven optimum. We provide corrected optimal makespans and a complete set of certified optimal results for the JSPPR benchmark, establishing a reliable reference for future studies.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-26T16:53:25Z
Fredrik Rømming, Mantas Bakšys, Martin S. Fixman, Sean B. Holden
arXiv categories: cs.AI, cs.LG, cs.LO

An automated theorem prover builds a proof step by step, choosing at each point what to add and what to remove. We cast this construction as a policy acting in a transition system induced by a formal calculus, which fixes which steps are sound: for clausal connection tableaux, leanCoP-style search and plCoP/rlCoP-style planning then become stateful policies over one interface, and policy-learning methods apply directly. We equip such policies with a graph neural network that scores proof edits from structure that transfers across problems, train it by imitation learning from found proofs, and measure how performance holds as we remove search scaffolding, from full symbolic backtracking to a policy the network drives alone. Within a fixed step budget on M2k, MPTP2078-bushy, and TPTP v9.2.1, learned policies solve up to 46% more problems than leanCoP, and reach proofs in an order of magnitude fewer steps.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-27T13:10:06Z
Julie Cailler, Noé Delorme, Sophie Tourret
arXiv categories: cs.LO

We introduce a new family of benchmarks for the problem of diagrammatic equivalence between circuits. Three variants of this problem are considered, ranging from basic to challenging, and benchmarks are generated for each variant. We provide first-order encodings in both TPTP and SMT-LIB formats, together with scripts that automatically generate benchmark instances, and evaluate these benchmarks on state-of-the-art automated theorem provers and SMT solvers.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-08-28T01:46:39Z
Shuai Tang
arXiv categories: cs.AI, math.LO

Evidential argumentation extends Dung's abstract argumentation by requiring arguments and interactions to be backed by chains of evidence rooted in prima-facie elements. However, existing formalisms lack a unified treatment of evidential support, higher-order relations (attacks and supports targeting arbitrary elements), and collective interactions (sources as sets). In this paper, we introduce the Evidential-Based Higher-Order Set Argumentation Framework (EHSAF), which conservatively generalises several existing frameworks within a single expressive setting. We develop two complete semantics for EHSAFs: an \emph{adjacent complete labelling semantics} that admits multiple truth values (true, false, undecided) for arguments in support cycles, reflecting an open epistemic attitude toward future evidence; and an \emph{extension-based complete semantics} that follows a strict evidentialist stance, accepting only arguments with well-founded support chains. We show that these two semantics diverge in the presence of support cycles, and prove their equivalence under support-acyclicity. To enable computational reasoning, we provide a normal propositional encoding of EHSAFs and prove that, in three-valued Łukasiewicz logic, its models correspond precisely to the adjacent complete labellings. We further extend this encoding to continuous fuzzy logics (G{ö}del, Product, and Łukasiewicz), defining a continuous fuzzy normal encoded semantics. We establish that this fuzzy semantics satisfies key properties---continuity, monotonicity, boundary conditions, and solution existence---and that its ternarisation recovers the adjacent complete labellings under natural t-norm conditions. Our framework thus unifies expressive argumentation with principled three-valued and fuzzy semantics, bridging the gap between qualitative and quantitative reasoning about evidence.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-24T11:03:20Z
Rayhana Amjad, Rob van Glabbeek, Liam O'Connor
arXiv categories: cs.LO

Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context, such as when testing or monitoring a system, only a finite prefix of the system's behaviour can be observed. For some properties, these finite prefixes may be definitive---a yes or no answer can be given without further observation. By enriching the semantics of LTL with these definitive prefixes, we give a proper inductive accounting of the semantics of LTL$_3$, a multi-valued variant of Linear-time Temporal Logic for run-time verification applications. The semantic descriptions of LTL$_3$ in previous work are given only in terms of their relationship to conventional LTL. We show that the semantics of LTL and of LTL$_3$ are isomorphic. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification contexts, and show its soundness and completeness up to finite traces with respect to our semantics. Then, we turn to linear-time properties more generally: using our theory of definitive prefixes, we re-prove the well-known safety-liveness decomposition theorem, and reconstruct the topology of infinite traces. We define monitorability for properties, providing neat topological characterisations for various monitorability classes, and arrange them into a hierarchy. All of our definitions and proofs are mechanised in Isabelle/HOL.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-25T20:45:32Z
Arnd Hartmanns, Robert Modderman
arXiv categories: cs.FL, cs.LO

Path abstraction originated as a technique for counterexample refinement in probabilistic model checking. Given a discrete-time Markov chain, it summarises the probabilities passing through a subset of the states onto new transitions of a smaller chain. In earlier work, we proved its correctness and that it is monotonically absorbing. In this paper, we extend path abstraction from reachability probabilities on discrete-time Markov chains to expected rewards on Markov reward models. Working in a novel free monoid view of Markov chains throughout, we prove that path abstraction preserves the Markov reward model structure when abstracting over arbitrary sets of states, and that it remains monotonically absorbing. Finally, we give a numerical recipe, accompanied by a reference implementation in PARI/GP, that computes path abstraction by solving linear equation systems. Its correctness rests on the relationship between expected rewards and expected visiting times of transitions.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-08-28T14:48:01Z
S. Krishna, Kaushik Mallik, Abhilasha Sharma Suman
arXiv categories: cs.LO, cs.FL, cs.GT

We consider two-player GR(1) games on graphs, where the system player Eve must satisfy \[ \Box\Diamond A_1\land\cdots\land\Box\Diamond A_m \;\implies\; \Box\Diamond G_1\land\cdots\land\Box\Diamond G_n \] against the environment player Adam. Here $A_1,\ldots,A_m$ are assumptions on the environment, $G_1,\ldots,G_n$ are guarantees the system must provide, and $\Box\Diamond S$ denotes ``always eventually $S$''. Traditional static strategies are overly conservative: they may actively violate assumptions to trivially satisfy the implication, or abandon all guarantees when any assumption is violated. Existing methods to prevent such behaviors incur doubly exponential blowup. We introduce an adaptive framework treating Adam as a non-adversarial agent with unknown objectives. Eve monitors which assumptions Adam actually meets and adapts her strategy at runtime to maximize satisfied guarantees. Central to our approach is a novel algorithm for monitoring liveness properties $\Box\Diamond S$, enabling Eve to maintain real-time likelihood estimates of which assumptions will be fulfilled. Eve pre-computes strategies optimal for different assumption subsets, deploying a probability distribution over them that dynamically adjusts based on monitor outputs. We prove that when assumptions are violated, Eve's randomized adaptive strategy converges asymptotically to the deterministic strategy maximizing guarantees. A prototype demonstrates effectiveness and superior computational performance compared to the state of the art.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-24T05:37:34Z
Yuto Takeda
arXiv categories: math.LO

We study the reverse-mathematical strength of frame definability in modal logic. The central principle is the Valuation Extension Lemma (VEL), which asserts that every assignment of propositional variables on a frame extends to a full valuation. We show that, over $\mathrm{RCA}_0$, VEL is equivalent to $\mathrm{ACA}^{+}_0$, and as are frame-definability principles for Geach axioms and for $\mathbf{GL}$. We also obtain analogous $\mathrm{ACA}^{+}_0$-equivalences for the Barcan and Converse Barcan formulas in modal predicate logic. Finally, we examine variants of VEL for $\mathbf{CTL}$ and $\mathbf{LTL}$ and locate their strengths between familiar subsystems of second-order arithmetic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-26T12:10:47Z
Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia, David Fernández-Duque, David Gabelaia
arXiv categories: cs.LO

We introduce spatio-temporal polyhedral reachability logics, extending dynamic topological logic with polyhedral semantics and a path-based spatial reachability operator. Formulas are interpreted over polyhedra, with admissible valuations ranging over polyhedral subsets; the spatial modality is interpreted as interior, the binary operator $γ(\varphi,ψ)$ expresses reachability of a $ψ$-point through a $\varphi$-region, and the temporal modalities are interpreted by a PL-homeomorphism and its inverse. We define h-dynamic reachability spaces and axiomatize the corresponding h-dynamic extensions of the known reachability logics of topological, finite, Alexandroff, and polyhedral spaces. The main result is soundness and completeness for the intended classes of invertible dynamical systems.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-27T09:36:14Z
Lingyuan Ye, Yiqi Xu
arXiv categories: math.CT, math.LO

We answer the question whether all Heyting algebras can appear as the lattice of subterminal objects of an elementary topos in the negative. Concretely, we have shown that the free Heyting algebra on two generators cannot be such a Heyting algebra. The mathematical results in this document were obtained with the help of ChatGPT 5.6 Sol, although the document itself was written entirely by us and we take full responsibility for its contents.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-08-28T15:31:14Z
Marcelo E. Coniglio, Héctor Federico Mallea
arXiv categories: cs.LO

RmbC is a self-extensional paraconsistent logic in the family of Logics of Formal Inconsistency (LFIs). This system is obtained from mbC (the basic LFI) by adding the replacement property via two global inference rules. RmbC is characterized by a non-explosive negation $\neg$ and a consistency operator $\circ$, which recovers the principle of explosion in a controlled way. Together with its principal axiomatic extensions, RmbC admits a standard Lindenbaum--Tarski algebraization, with Boolean algebras with LFI operators (BALFIs) as its algebraic semantics. In this paper, we study how far this self-extensional paraconsistent behavior can be extended axiomatically, starting from RmbC. We classify pairs of very natural consistency axioms according to whether they preserve paraconsistency or force classical collapse; identify six algebraically equivalent explosive cores; and isolate a separate structural obstruction for the combination of excluded middle for $\neg$ with an involutive negation. We also investigate, for the first time, the decidability of this family of self-extensional LFIs. As a first result, we prove the finite model property for RmbC with respect to BALFI semantics via an algebraic filtration, which yields decidability, and transfer this result to several paraconsistent axiomatic extensions of RmbC. Finally, we establish a 2-EXPTIME upper bound for the validity problem of RmbC and a coNP-hardness lower bound.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-25T14:27:24Z
Gabriel Conant, Kyle Gannon, James E. Hanson
arXiv categories: math.LO

Given a first-order theory $T$ (in discrete or continuous logic) and a Borel-definable global Keisler measure $μ$ in $T$, we show that the following conditions are equivalent: $(i)$ $μ$ is a frequency interpretation measure; $(ii)$ $μ$ is definable and its canonical "random extension" $r_μ$ is generically stable in the randomization theory $T^R$; $(iii)$ $μ$ is "self-averaging". This result establishes a robust notion of generic stability for Keisler measures, which resolves a long-term research objective from previous work. The implications $(i)\Rightarrow(ii)\Rightarrow (iii)$ were previously established by the authors (for $T$ discrete). The primary focus of this paper is the reverse implications $(iii)\Rightarrow (ii)\Rightarrow(i)$, which we obtain through the use of AI models.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-25T15:46:37Z
Michael C. Laskowski, Danielle S. Ulrich
arXiv categories: math.LO, math.RA

We prove that for any countable ring $R$ (not necessarily commutative), if the associated left $R$-module ${}_R R$ has a strictly descending sequence of pp-definable subgroups, then the theory $Th(R^{(ω)})$ of the infinite dimensional direct sum is Borel complete. From this, we conclude that if $R$ is countable and not left perfect, then the theory of $R$-modules is Borel complete, and we give a full characterization of which countable simple rings have Borel complete theories. One special case is that the complete theory $Th({\mathbb Z}^{(ω)})$ is Borel complete, which strengthens the existing proofs of the Borel completeness of TFAB, the theory of torsion free abelian groups. The proof also introduces, relative to the chosen pp-chain, a proper two-sided ideal $L^R$, and a notion of f.g. hulls which, for countable rings and countable parameter sets in theories satisfying $T=T^{\aleph_0}$ exist and are unique up to isomorphism. These constructions may be of independent interest in the model theory of modules.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-08-26T07:32:30Z
Hongyi Gou, Mostafa Mirabi, Mihir Mittal, Chieu-Minh Tran, Zhenyu Yang
arXiv categories: math.LO, math.CO

We study multipartite hypergraphs definable in $1$-semi\-equational theories and prove almost-linear Zarankiewicz bounds in every fixed arity $r\geq2$. More precisely, if $T$ is a $1$-semi-equational theory, then, for every formula $\varphi$ and every $t\geq2$, and every $r\geq2$, there is a constant $c$ such that each $K_{t,\ldots,t}$-free $r$-partite hypergraph defined by $\varphi$ on $n$ vertices has $O_{T,\varphi,t,r}(n^{r-1}(1+\log(1+n))^c)$ edges. In the bipartite case, a Boolean combination of $m$ $(k,1)$-semi-equations has $O_{k,t,m}(n(1+\log(1+n))^{(m-1)(k-1)})$ edges whenever it is $K_{t,t}$-free. In particular, a relation defined by one $(k,1)$-semi-equation or its negation has a linear bound. The proofs are based on incidence estimates for $k$-wise laminar indexed set systems.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-24T15:46:44Z
Zachiri McKenzie
arXiv categories: math.LO

The weak set theory $\mathsf{ReR}$ is obtained from Kripke-Platek Set Theory ($\mathsf{KP}$) by replacing the bounded collection scheme with the bounded replacement scheme. We show that $\mathsf{ReR}$ proves $\mathsf{TCo}$, which asserts that every set is contained in a transitive set. This is used to show that the theories obtained by adding the negation of the axiom of infinity to $\mathsf{ReR}$ and $\mathsf{KP}$ have the same consequences. Our proof of $\mathsf{TCo}$ relies on the availability of a fragment of class foundation in $\mathsf{ReR}$. To demonstrate the necessity of this reliance, even in the presence of infinity, we build a model of a significant fragment of $\mathsf{ZF}$ that includes bounded separation and collection, infinity, powerset, regularity and the axiom of choice, in which $\mathsf{TCo}$ fails.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-25T07:55:19Z
Tom Benhamou, James Cummings, Yair Hayut, Gabriel Goldberg, Alejandro Poveda
arXiv categories: math.LO

We continue the study of compactness phenomena between the set-theoretic universe and $\mathrm{HOD}$ initiated by Goldberg--Poveda \cite{GolPov}. We focus on compactness phenomena around the power-set functions of $V$ and $\mathrm{HOD}$. We prove: (1) A singular strong limit cardinal with uncountable cofinality cannot be the first place where $\mathcal{P}(\cdot )$ and $ \mathcal{P}^{\mathrm{HOD}}(\cdot)$ disagree. (2) Assuming the existence of a measurable cardinal, $\aleph_ω$ can be the first place where $\mathcal{P}(\aleph_ω)\neq \mathcal{P}^{\mathrm{HOD}}(\aleph_ω)$, answering a question of Hayut. (3) If $κ$ is strong limit singular of uncountable cofinality, $\mathrm{HOD}$ is correct about cardinals less than or equal to $κ^+$ and the GCH holds in $\mathrm{HOD}$ below $κ^+$ then $(\mathrm{HOD}, V)$ has the $\mathrm{cf}(κ)^+$-cover property. We also show that the GCH assumption in (3) is necessary, which demonstrates that Magidor's classical Covering Theorem is optimal.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-25T15:34:34Z
Alberto Marcone, Gian Marco Osso
arXiv categories: math.LO

The Laver Partition Theorem is a fundamental tool in the analysis of Laver and Hechler forcings. It is also connected to determinacy and the Galvin-Prikry theorem: indeed it can be seen as the common core of these two theorems. We study the reverse mathematics and Weihrauch degrees of the Laver Partition Theorem restricted to open and clopen sets. We obtain upper and lower bounds on the proof theoretic strength of this result, as well as a precise picture of the (arithmetical) Weihrauch degrees of the problems related to it.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-26T03:46:09Z
Yamato Miyata, Keita Yokoyama
arXiv categories: math.LO

The thin set theorem $\mathsf{RT}_{<\infty,\ell}^{n}$ asserts that for every natural number $k$, each coloring $c\colon[\mathbb{N}]^n \to \{0,1,\dots,k-1\}$ admits an infinite set $H$ such that $|c([H]^n)| \le \ell$. Within the framework of the reverse mathematics of second-order arithmetic, $\mathsf{RT}_{<\infty,\ell}^{n}$ implies the $Σ_{n+1}^{0}$-bounding principle ($\mathsf{B}Σ_{n+1}^{0}$) over $\mathsf{RCA}_0$ for all natural numbers $n, \ell \ge 1$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-26T15:36:51Z
Miara Sung
arXiv categories: math.LO, cs.LO

The Turing jump has no fixed point on the Turing degrees: $\mathbf a <_T \mathbf a'$ for every degree $\mathbf a$. After passing to the ideal completion, however, a natural fixed-point phenomenon appears. We study the Scott-continuous lifting $Γ:\operatorname{Idl}(\mathbf D_T)\to\operatorname{Idl}(\mathbf D_T)$, given by $Γ(I)=\downarrow\{\mathbf a':\mathbf a\in I\}$. Starting from the computable degree, Kleene iteration reaches its first fixed point at stage $ω$, namely the Turing ideal of arithmetical degrees; more generally, above $\mathbf a$ the least fixed point is the ideal of degrees arithmetical in $\mathbf a$. To pass beyond this fixed point, we introduce a limit-uniformization operator. Although the ideal of finite jumps contains every $\mathbf 0^{(n)}$, it does not contain the uniform limit oracle $\mathbf 0^{(ω)}=°_T\!\left(\bigoplus_{n < ω}0^{(n)}\right)$. The uniformization operator adjoins this oracle only when all finite jump degrees are present. It is monotone but not Scott-continuous. Composing jump closure with one such gate yields closure ordinal $ω\cdot 2$; gates at $ω,2ω,3ω,\ldots$ yield closure ordinal $ω^2$. Thus non-uniform closure under relativized halting problems is Scott-continuous and reaches fixed ideals, while uniform coding of an entire prior hierarchy is infinitary, discontinuous, and reopens diagonalization. This gives a domain-theoretic semantics for the successor/limit distinction in transfinite Turing-jump hierarchies and links failures of Scott continuity with closure ordinals.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-26T16:49:55Z
Constance Bromham, Asaf Karagila
arXiv categories: math.LO

In [10] it was suggested that the countable chain condition should be defined in the absence of choice as "every predense set contains a countable predense subset". During his tutorial at the "120 Years of Choice" conference in 2024, Philipp Schlicht remarked that this definition does not have an iteration theorem in $\mathsf{ZF}$. We provide a proof of this claim. Specifically, we show that if every finite support iteration of ccc forcings is again ccc, then the Axiom of Choice for countable families of countable sets must hold. However, we prove that under the assumption of the Principle of Dependent Choice, the finite support iteration of ccc forcings is again ccc. This requires correcting some issues with the definition of properness (and therefore Mekler's definition of ccc) from [1]. We then study Knaster principles and their relations to this version of ccc.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-26T23:09:28Z
David Chodounský, Osvaldo Guzmán, Jonathan Verner
arXiv categories: math.LO

We provide an easy proof that there are no P-points in the models obtained by adding many Silver reals with countable support to a model of CH.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-27T10:05:59Z
Noam Greenberg, Daniel Turetsky
arXiv categories: math.LO

We show that there is a $Π^0_2$ subset $B$ of the Euclidean plane, of Hausdorff dimension 1, such that for every line $\ell$ through the origin with hyperarithmetic direction, the projection of $B$ onto $\ell$ has Hausdorff dimension 0, thus is exceptional for Marstrand's projection theorem. It follows that for any computable ordinal $α$, being $α$-random does not guarantee the ``almost-all'' statement of the projection theorem.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-27T13:15:12Z
Vladimir Vovk
arXiv categories: math.LO

The usual definitions of stochasticity are very different from Kolmogorov's original definition as given in Shen's notes from November 1981. This note simplifies Kolmogorov's definition and shows that the universal machine generates nonstochastic objects with surprisingly high probability.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-08-28T16:36:10Z
Lorenzo Notaro
arXiv categories: math.LO

In 1972, Jech asked whether there exists a Suslin $(ω_1, ω_2)$-forest in the constructible universe. As reported by Jech, Laver gave a positive answer, but his proof was never published and appears no longer to be available. In 2015, Eskew introduced the combinatorial principle $W^*_κ(λ)$, a strengthening of Silver's principle, and used it to construct a coherent Suslin $(κ, λ)$-forest. He then asked whether the principle $W^*_{κ^+}(κ^{++})$ holds in $\mathsf{L}$ for every regular cardinal $κ$. We give an affirmative answer to Eskew's question, thereby also settling Jech's question.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-26T11:58:33Z
Max Blans, Thomas Blom
arXiv categories: math.AT, math.CT

In this paper, we prove a product rule for Goodwillie derivatives: given a differentiable $\infty$-category $\mathcal{C}$ whose stabilization is equivalent to the $\infty$-category $\mathrm{Sp}$ of spectra, we show that the derivatives functor $\partial_* \colon \mathrm{Fun}^ω(\mathcal{C}, \mathrm{Sp}) \to \mathrm{RMod}_{\partial_*\mathrm{id}_\mathcal{C}}(\mathrm{SSeq}(\mathrm{Sp}))$ is strong symmetric monoidal, where the source is equipped with the pointwise tensor product and the target with Day convolution. Since the Koszul dual of $\partial_*\mathrm{id}_\mathcal{C}$ can be recovered as a coendomorphism operad from Day convolution, this product rule is useful for calculating the operad $\partial_*\mathrm{id}_\mathcal{C}$ in examples. We derive the product rule as a consequence of the more general statement that taking derivatives preserves cartesian products on the $(\infty, 2)$-categorical level. In fact, the main theme of this paper is that the extraction of Goodwillie derivatives preserves a lot of structure when regarded as a functor of $(\infty, 2)$-categories: apart from products, it also preserves cotensors and certain pullbacks. We illustrate how our results can be used to calculate Goodwillie derivatives by determining the operad structure on the derivatives of the identity functor in pointed spaces, algebras over an operad and sheaves on a site.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-27T15:14:15Z
Rongge Xu, Holiverse Yang
arXiv categories: math-ph, cond-mat.str-el, math.CT

Building on our previous work on 2-Morita equivalence for $E_2$-algebras using topological pictures, we develop a systematic framework for Morita equivalence of topological orders in different dimensions in terms of $n$-Morita categories $\mathrm{Mrt}_{E_n}(\mathcal{C})$. In this framework, various notions of $n$-Morita equivalence are unified as equivalences of objects in $\mathrm{Mrt}_{E_n}(\mathcal{C})$. We also compare the constructions of higher Morita categories due to Haugseng and to Gwilliam--Scheimbauer. For $n=1,2$, we prove that the functor $\mathrm{Mod}_n:\mathrm{Mrt}_{E_n}(\mathcal{C})\to \mathrm{Mrt}_{E_{n-1}}(\mathrm{LMod}^{\mathrm{rep}}(\mathcal{C}))$ is an equivalence, relating the algebraic description of higher Morita theory to its realization in terms of module categories. In this formulation, the notion of a bi-bimodule arises naturally and provides a common framework for local and confined modules. Its explicit orientation data, together with the corresponding fusion rules, clarifies the relations among defects arising from condensation in topological orders.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-27T17:58:22Z
Max Blans
arXiv categories: math.AT, math.CT

We prove an $(\infty,2)$-categorical version of Koszul duality for operads and cooperads in spectra by showing that there is an equivalence between a Morita category of operads and bimodules and a dual Morita category of cooperads and bicomodules. This result subsumes various forms of operadic Koszul duality present in the literature.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-27T23:06:27Z
Jaime Herrera, Carmen Rovi
arXiv categories: math.GT, math.AT, math.CT

The category TFS of thin flat surfaces, introduced by Khovanov, Qi, and Rozansky, is a strict symmetric monoidal category whose morphisms are compact oriented surfaces with corners arising as neighbourhoods of immersed graphs in a strip. We prove two main results. First, a normal form theorem: every connected viewable tf-cobordism is equal, in TFS, to a canonical composite determined by its topological type. Second, a sufficiency theorem: we establish a list of relations in the TFS category which are sufficient, meaning that any two composites of generators representing the same tf-cobordism are related by a finite sequence of the listed relations. Together, these results give a complete generators-and-relations presentation of TFS.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-28T14:08:04Z
Viktoriya Ozornova, Martina Rovelli, Tashi Walde
arXiv categories: math.AT, math.CT

We study the marked simplicial set obtained as the Roberts-Street nerve of the walking coinductive equivalence. We show that it is a non-contractible saturated complicial set for which all of its finite truncations are contractible. When regarding saturated complicial sets as a model for right $(\infty,\infty)$-categories, it represents a concrete and explicit example of a right $(\infty,\infty)$-category that is itself non-contractible, but whose reflection to a left $(\infty,\infty)$-category is contractible.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-08-28T16:00:52Z
Perry Hart
arXiv categories: cs.LO, math.CT

We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We show that the proof may fail for adjunctions between wild categories and even produce a wild left adjoint that fails to preserve colimits. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, which we call 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor, as well as a generalization thereof, preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-24T09:54:18Z
Matthew de Brecht
arXiv categories: math.CT, cs.LO, math.LO

We construct the category of overt discrete quasi-Polish spaces and the category of compact Hausdorff quasi-Polish spaces (and some of their subcategories) as internal categories of the category of effective quasi-Polish spaces and computable maps. To demonstrate that the constructions are natural, we show that Stone duality is computable, in the sense that the dual contravariant functors and the natural transformations demonstrating their adjointness are computable.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-24T16:05:37Z
Peter Schneider, Claus Sorensen
arXiv categories: math.NT, math.CT, math.RT

Let $D(G)$ denote the derived category of smooth $G$-representations on $k$-vector spaces, where $G$ is a locally pro-$p$ group and $k$ is a field of characteristic $p$. In this paper we are primarily interested in the graded center of the subcategory of compact objects $Z^*(D(G)^c)$ and variants thereof. When $G$ is a $p$-adic Lie group, without proper open centralizers, we completely determine this center modulo locally nilpotent elements and give various applications.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-24T20:08:02Z
Marino Gran, George Janelidze
arXiv categories: math.CT, math.RA

We give an equivalent definition of a non-pointed torsion theory, also called a pretorsion theory in the literature. This uses a new, more general, notion of a near-torsion theory, and does not use non-pointed exactness. Furthermore, a general method of associating the `largest' (non-pointed) torsion theory to any given near-torsion theory is described. We also describe a near-torsion theory formed by the class of cokernel diagrams and the class of kernel diagrams in a pointed category with kernels and cokernels, and its associated torsion theory.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-24T22:13:59Z
Frank Murphy-Hernandez
arXiv categories: math.CT, math.GR

We study the cofree functor on the category of group actions and examine its categorical and combinatorial properties. Motivated by this construction, we introduce a family of functors associated with subgroups and develop their theory through a corresponding coreflective subcategory of group actions. Finally, we investigate the comonad in the category of sets induced by the cofree adjunction and prove that it classifies the groups.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-25T20:15:03Z
Dali Zangurashvili
arXiv categories: math.RA, math.CT

With the aid of the torsion-theoretical approach, several properties/characterizations of hereditary QF-$3^{+}$ rings are found. These characterizations are formulated in terms of the category of projective modules, the category of injective projective modules, and also in terms of the maximal left/right ring of quotients by Utumi. Moreover, it is shown that, for a hereditary QF-$3^{+}$ ring, the `largest stable submodule' radical (on the category of left/right modules) is permutable with injective envelopes. Besides, it is shown that there is a bimorphism (in the category of associative rings with identity) from such a ring to a semisimple left/right Artinian ring.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-26T10:23:23Z
Daniel Funck, Giacomo Gavelli
arXiv categories: math.CT, math.FA, math.NT

We construct a categorical framework in which we can view the direct integral as a functor taking as input objects in a certain category of Abstract Banach bundles and outputting a Banach space. We do this by constructing a quasi-abelian category of abstract Banach bundles, and we prove certain foundational and theoretical results about this category and its objects. As a consequence, we are able to define a notion of direct integral of sheaves.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-26T10:24:40Z
Richard Garner, Ross Street
arXiv categories: math.CT

In the context of enriched category theory, we give necessary and sufficient conditions for a module morphism $α\dd M \to \CC(F,Z)$ to exhibit a functor $Z\dd \CA\to \CC$ as an absolute $M$-weighted colimit of a functor ${F\dd \CB\to \CC}$. We also review, with short proofs, the various criteria for the weight $M$ itself to be absolute, in the sense that any $M$-weighted colimit is absolute. Finally, we prove that any absolute $M$-weighted colimit can be viewed as a colimit weighted by an absolute weight $M'$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-26T12:08:01Z
Morgan Rogers, Joshua Wrigley
arXiv categories: math.LO, math.CT

We give an example of a coherent theory, a topological space, and a continuous assignment of the (model-theoretic) types of the theory to the points of the space, such that there is no sheaf model of the theory over the space with the property that the fibre over a point, as a set-based model, realises the corresponding type; thus, we answer in the negative a problem posed by Kristóf Kanalas.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-26T13:51:46Z
Mark Lyttle
arXiv categories: math.CT, math.AC

There is an isomorphism between the frame of radical thick tensor ideals of an essentially small tt-category and the frame of open sets of the Hochster dual of its Balmer spectrum. This isomorphism allows us to compare topological properties of the latter with tt-geometric properties of the former. We use this to give an intrinsic definition of those tt-categories which satisfy a variant of the second De Morgan law, and furthermore give a construction for producing such tt-categories.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-26T17:49:10Z
Nesta van der Schaaf
arXiv categories: math.LO, math.CT

Esakia duality is the dual equivalence between Heyting algebras and Esakia spaces. However, the traditional proof uses the Prime Ideal Theorem to recover the algebra from its spectrum, a choice principle that is not constructively valid. We build on Townsend's localic Priestley duality to describe a fully constructive, localic Esakia duality. On the algebraic side, we use the recently introduced Heyting frames as the point-free version of Heyting algebras. On the spatial side, Esakia spaces are modeled by two point-free alternatives. First, Esakia locales are defined as a subclass of the ordered Stone locales introduced by Townsend, and it is shown directly that Townsend's equivalence restricts to a duality between Heyting frames and Esakia locales. Second, using the theory of conic frames, in which join-preserving closure operators on frames model localic preorders, we introduce Esakia frames as a frame-theoretic analogue of Esakia spaces. It is shown that Esakia frames are equivalent to Heyting frames and dually equivalent to Esakia locales, and that this factorises the restriction of Townsend's equivalence. This yields a fully constructive, localic Esakia duality.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-27T02:20:23Z
Xiaoyan Yang
arXiv categories: math.CT

This paper studies finitistic dimensions in triangulated categories with a compact silting generator. We unify several notions of (big) finitistic dimension appearing in the literature, show that they are essentially equivalent, and relate them to the abelian heart when the generator is tilting. This yields a new categorical perspective on the finitistic dimension conjecture. Furthermore, we establish explicit inequalities for (big) finitistic and global dimensions under recollements, demonstrating that finiteness in the middle category is equivalent to finiteness in the outer categories. These results generalize classical ring-theoretic theorems and apply to triangular matrix rings, exact contexts and trivial extensions.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-27T05:40:34Z
Lili Shen, Xiaojuan Zhao
arXiv categories: math.RA, math.CT

We establish a new bridge connecting quantales, semigroups and the theory of formal concept analysis. By introducing residuated relations whose domains are semigroups, we show that every quantale arises as the formal concept lattice induced by such a relation. Furthermore, this construction yields an equivalence between the category of quantales and a category of such residuated relations whose morphisms are multiplicative bonds.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-27T06:04:14Z
Jian He, Yu-Zhe Liu, Panyue Zhou
arXiv categories: math.RT, math.CT

Let $\mathcal C$ be an $(n+2)$-angulated category. Zhou proved that, when $n$ is odd, if the Auslander-Reiten $(n+2)$-angles generate the relations for the Grothendieck group of $\mathcal C$, then $\mathcal C$ is locally finite. Whether the corresponding statement remains valid for even $n$ is still open. In this paper, we give a partial affirmative answer to this problem by establishing a sufficient condition under which the same implication holds for even $n$. We further show that our sufficient condition is satisfied by a broad class of examples, thereby demonstrating that the result extends well beyond isolated cases.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-27T16:00:04Z
Haicun Wen, Jian He, Yu-Zhe Liu
arXiv categories: math.GR, math.CT

We show that power semigroups of groups, and more generally reduced finitary power monoids, arise naturally as convolution monoids in Kleisli categories of powerset monads: (1) for the non-empty powerset monad, the Kleisli Hom-space $\mathrm{Hom}_{\mathbf{Kl}(\mathscr P_+)}(1,G)$ is isomorphic to the power monoid $\mathcal P_+(G)$; (2) for the reduced finite powerset monad on pointed sets, the Kleisli Hom-space $\mathrm{Hom}_{\mathbf{Kl}(\mathscr P_{\mathrm{fin}})}$ $(\mathbb Z/2\mathbb Z,H)$ is isomorphic to the reduced finitary power monoid $\mathcal P_{\mathrm{fin},1}(H)$. This unifies several constructions in power semigroup theory: Kleisli convolution representations of semigroups, base change along surjective group homomorphisms, and rigidity of automorphism groups. As an application, we prove that for every proper numerical monoid $S$, the Kleisli Hom-monoid $\mathrm{Hom}_{\mathbf{Kl}(\mathscr P_{\mathrm{fin}})}(\mathbb Z/2\mathbb Z,S)$ is rigid, thereby giving an affirmative answer to the Tringali--Yan conjecture via the language of Kleisli categories.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-27T19:54:51Z
Daniel Almeida
arXiv categories: math.CT, math.LO

We describe a (combinatorial, monoidal, Cat-enriched) Quillen model structure on the category of Cartmell's generalized algebraic theories (gats); its homotopy bicategory consists essentially of Taylor's rooted display map categories. This allows us to compare two kinds of morphisms of gats: one where sort dependency and substitution are preserved strictly, thus directly matching the syntax, and one where the given structure is preserved up to isomorphism. We prove a strictification result for morphisms out of cofibrant theories, which are the retracts of theories without sort equality axioms. Along the way, we give a structural characterization of when a contextual category can be presented without sort equality axioms. Our results also imply that when restricted to cofibrant objects, the tensor product of gats has the expected semantic behaviour, namely, it corresponds to the tensor product of locally finitely presentable categories equipped with a cofibrantly generated weak factorization system. Strict and weak morphisms specialize, respectively, to two familiar concepts of model of a gat A: ones valued in iterated families of sets, with substitution interpreted as reindexing, and set-valued models of the contextual category C(A) viewed as a finite-limit sketch. We characterize strictifiability of a model of the latter kind via a loop freeness condition on a certain map of functors out of the category of context projections of A.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-27T21:55:23Z
Yuta Takashima
arXiv categories: math.AG, math.CT, math.RT

We study the singularity categories of simple singularities of the same dimension over an algebraically closed field of positive characteristic, and show that, as in characteristic zero, these categories are not equivalent as triangulated categories unless the underlying singularities are analytically isomorphic. In contrast to the characteristic zero case, simple singularities in positive characteristic cannot be distinguished solely from the Auslander-Reiten quivers of their singularity categories. To address this, we extend to positive characteristics a theorem by Hua and Keller, which asserts that the 0th Hochschild cohomology of the dg singularity category of an isolated hypersurface singularity in characteristic zero is isomorphic to the Tyurina algebra of the defining polynomial. Furthermore as an application, we determine the condition for the singularity category of a rational double point (i.e., a simple singularity of dimension two) to be standard. We prove that such a category is standard if and only if the defining polynomial is weighted homogeneous.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-08-28T10:47:18Z
Goncalo Tabuada
arXiv categories: math.AG, math.CT, math.RT

In this short note, making use of the theory of noncommutative motives, we prove that the Grothendieck classes of the twisted symplectic flag varieties are linearly independent and moreover homogeneous-quadratic independent in the Grothendieck ring of algebraic varieties.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-08-25T09:47:13Z
Aochu Dai, Mingsheng Ying
arXiv categories: cs.LO, quant-ph

We present QisMC, the first quantum model checker dedicated to debugging Qiskit programs. On the theoretical side, we introduce the notion of quantum-classical transition system and a quantum computation tree logic (qCTL) grounded in Birkhoff-von Neumann logic for modeling the behaviors and specifying the properties of Qiskit programs, respectively. On the implementation side, QisMC provides an end-to-end framework encompassing transition system generation, logical formula representation, and model checking algorithms, and it efficiently performs image computation based on decision diagrams. These methods and design principles give QisMC advantages over previous Qiskit program debuggers, including a unified property specification language, a fully automated and exhaustive verification process, and the ability to generate counterexamples. Extensive illustrative examples and benchmark evaluations demonstrate the practicality, efficiency, and scalability of QisMC in verifying realistic quantum programs.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-25T15:48:07Z
Agrima Regmi, Jenish Pant, Pratistha Sapkota, Sanskriti Khatiwada, Binod Sapkota
arXiv categories: cs.LO, cs.CL

Physical implementations of Turing Machines remain rare, and existing electromechanical demonstrators and mechanical logic games typically require manual operator intervention, either to trigger each computational step or to reconfigure the state table, or both. This restricts prior physical models to short, operator-paced demonstrations and prevents autonomous execution of extended computations. This paper addresses that gap with a hardware Turing Machine that enables autonomous multi-step execution and reprogrammable optical input without manual intervention between programs. The system integrates an Arduino Mega for state-transition logic, dual NEMA 17 stepper motors for bidirectional tape actuation, infrared reflectance sensors for symbol detection, and an ESP32-CAM-based optical punched-card reader for automated state-table loading. Hole detection under non-uniform illumination used a Breadth-First Search flood-fill algorithm with local adaptive thresholding rather than fixed global thresholding, driven by the memory and library constraints of the ESP32-CAM's microcontroller environment; this improved card-decoding accuracy from 75% to 90% (100% with mechanical card flattening) on a 20-card test set. Mechanical evaluation showed fabrication accuracy of +/-0.15 mm, rack-and-pinion positional error below 0.3 mm across 50 trials, and voltage supply stability within +/-0.2 V under full system load. End-to-end computation was validated against a parallel software simulator (tlang), with all hardware outputs matching the simulated reference exactly across multiple test programs. The system advances prior physical Turing Machine demonstrations through autonomous execution, reprogrammable optical input, and quantitative evaluation of its mechanical, optical, and computational performance.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-27T05:34:40Z
George Barmpalias, Su Gao, Jialiang He, Takayuki Kihara, Andre Nies, David Schrittesser, Theodore Slaman, Chieu-Minh Tran, Daniel Turetsky, Philip Welch, Liang Yu, Hang Zhang
arXiv categories: math.LO

These open problems were presented in the Problem Sessions held during the Tianyuan Workshop on Definability and Computation, June 22-26, 2026. The problems are organized into sections named after their contributors, in the order of their presentations during the workshop. Notes were taken and compiled by Wei Dai, Xiangxi Hu, Yingying Jiang, Ruiwen Li, Tianhao Wang, Xu Wang, and Jie Zou.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-08-27T10:07:40Z
Gurjeet Sangra Singh, Frantzeska Lavda, Alexandros Kalousis
arXiv categories: stat.AP, cs.CV, cs.LO

Deep generative models such as flow matching and diffusion models have shown potential for learning complex dynamical systems, but typically act as black boxes that neglect underlying physical structure, while physics-based models governed by partial differential equations are often incomplete due to missing source terms, or uncertain parametrisations. We present Climate Physics Dynamic Matching (ClimPhyDM), a variational simulation-free dynamics informed framework for weather forecasting that combines an advection-type physics prior with data-driven components in a variational framework. % to capture the stochasticity and multi-modality of unresolved atmospheric dynamics. On the ERA5 benchmark at hourly (42-hour) and monthly (5-month) resolutions, ClimPhyDM outperforms ClimODE, and GB-DM, keeping the lower error at extended horizon, indicating improved temporal stability and resistance to error accumulation, while its simulation-free paradigm also enables training on a single modest 12 GB consumer GPU.

arXiv abstract · PDF