arXiv weekly literature review

Lean Proof Assistant Applications · primary corpus · published 2026-10-26T15:22:15Z
Zihua She, Xiao Wang
arXiv categories: stat.CO, cs.AI, cs.LO

Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organizes language model agents, run by Claude Code, to translate the proofs of a LaTeX paper into the proof assistant Lean 4 with its library Mathlib and check them there, result by result. Each numbered result receives one of four verdicts: verified unconditionally; verified conditionally, with every cited or unproved input stated as a named hypothesis; issue recorded, with its place in the paper and the side at fault; or unfinished, with the reason. The kit follows the paper's own proof step by step, rather than finding a new one. Separate agents write and review, each statement is compared with the paper before it is proved and fingerprinted afterwards, and every verdict rests on evidence that can be rerun without a language model. The kit runs unattended for hours, waits out usage limits, re-checks only what a revision changed and reports its cost by role, model and result. We describe the design, walk through a complete run, and apply the kit to four example papers with answer keys and to three published statistical papers, checked blind in their versions from before public corrections. In all three, the kit found the published error at the step that the correction names, together with further problems that we confirmed by hand. Given the same papers directly, the same language model working with Lean classified fewer results correctly on the longest paper and reported some statements narrower than the paper's as proved; no verdict of the kit claimed more than its Lean evidence showed.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-26T19:34:36Z
Johannes K. Fichte, Stefan Szeider
arXiv categories: cs.LO, cs.AI

We present count-catcher, a tool that turns a CPOG certificate of a count by the exact model counter d4 into a Lean theorem that a CNF formula defined in Lean has exactly N models over V variables. With an encoding lemma, this theorem becomes a theorem about the number of combinatorial objects. A CPOG certificate consists of a Boolean circuit equivalent to the formula and a proof of equivalence. count-catcher checks in Lean that the formula implies the circuit (forward check) and the circuit implies the formula (reverse check). For the forward check, lrat-catcher streams a refutation through the LRAT checker of Lean's standard library. The reverse check and the validity check of the circuit are computations proved correct in Lean. Lean runs all three checks as compiled code, so the theorem depends on Lean's kernel, compiler and runtime, as does CPOG's verified checker. We combine the theorem with results from Mathlib, for instance with Burnside's lemma to count graphs up to isomorphism. We prove the number of Latin squares of order 8 as a weighted sum of hundreds of certified counts from about eight terabytes of certificates. We turn about half of the 2022 Model Counting Competition formulas into theorems, with the three checks taking about a quarter of the time of CPOG's verified checker. We found that CPOG's unverified checker reported wrong counts, and removed its verified checker's dependence on two unproved lemmas. End to end, a theorem costs about the same as a checked count.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-26T22:09:19Z
Colin T. Jones, Tyler R. Josephson
arXiv categories: cs.LO

The genetic code exhibits redundancy, meaning that multiple distinct nucleotide sequences can encode the same amino acid sequence, a property mathematically characterized as non-injectivity. While this phenomenon is well studied in molecular biology, its rigorous verification within a computational framework remains limited. In this work, we present a machine-verified model of the central dogma of molecular biology using the Lean 4 interactive theorem prover. We formalize nucleic acid bases and amino acids as inductive types and define transcription and translation as functions mapping DNA sequences to RNA and subsequently to polypeptides. Within this framework, we prove key properties of these biological processes, including the redundancy of the genetic code, injectivity of transcription, and the non-injectivity of translation. Additionally, we formalize auxiliary processes such as DNA replication and mutation, and verify properties such as length conservation under transcription and point mutations. Finally, we demonstrate how Lean 4 helps prevent semantic errors in our code, showing its effectiveness as a tool for advancing reliable, bug-free scientific computing, particularly within the life sciences.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-27T01:52:21Z
Lucy Horowitz
arXiv categories: cs.LO, cs.CY

We present Alaska's ranked-choice elections as a case study in Formally Verified Democracy, a program to establish election results through formally checked proofs. We formalize an interpretation of Alaska's tabulation rules in Lean, verify its implementation, and prove election-specific results. Across 115 ranked-choice contests in Alaska since 2022, we identify 75 ballot records across 10 contests that were counted differently from this interpretation by a program reproducing the published results, without changing any winners. We trace these differences to overvotes and duplicate rankings and examine their legal justification, showing how formal verification can expose consequential choices in translating election law into software.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-27T02:47:56Z
Florian Hellwig
arXiv categories: math.NT, cs.LO

We study completely normal elements of $\mathbb{F}_{q^n}$ over $\mathbb{F}_q$, that is, elements that are normal over every intermediate field, through partial Lagrange resolvents. In these coordinates, complete normality splits into independent components, in a way closely related to Hachenberger's decomposition theory. Our main tool is a structure theorem for the components; together with a finite computation, it shows that every component has weight (the sum of the probabilities that its conditions fail) at most $3/4$, uniformly in $n$. Combined with the classical character-sum method, this gives an explicit sufficient criterion for the existence of a primitive completely normal element. We verify the criterion for all $n>q$ except $70$ pairs $(q,n)$, which we settle with explicit elements found by computer. Since the case $n\le q$ is due to Garefalakis and Kapetanakis, this confirms the conjecture of Morgan and Mullen (1996) that every $\mathbb{F}_{q^n}$ contains a primitive element that is completely normal over $\mathbb{F}_q$. The same estimates give two further results. First, Hachenberger's conjectured lower bound $(q-1)^{n'}q^{(p^a-1)n'}$ for the number of completely normal elements, where $p$ is the characteristic and $n=p^an'$ with $p\nmid n'$, holds for all pairs $(q,n)$; it was known for regular pairs. Second, primitivity and complete normality are asymptotically independent: as $q^n\to\infty$, the number of primitive completely normal elements is $(1+o(1))\,\varphi(q^n-1)/(q^n-1)$ times the number of completely normal elements (for fixed $n$ this was known). Our arguments for $n>q$ and for both further results, including every computer-assisted step, are formalised in Lean 4 with Mathlib; the formalisation takes the case $n\le q$ and an explicit bound of Rosser and Schoenfeld as axioms and relies on Lean's compiler and interpreter for the large computations.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-28T10:36:36Z
Denis Firsov
arXiv categories: cs.LO, cs.DS

Order maintenance asks for a data structure that keeps a sequence of elements under insertions and deletions and tells which of two elements comes first. We give an algorithm, assembled from published components, that performs each operation in worst-case constant time, and verify it in Lean 4. The algorithm is a program for a random-access machine deeply embedded in Lean, whose interpreter counts every instruction. We prove that the program answers every query as a simple reference specification does, that each operation takes at most a fixed number of steps, independent of the number of elements and of the history, and that after $t$ operations no value it has computed has more than $O(\log t)$ bits, so it runs unchanged on a machine with words of that size. A verified translation that preserves step counts exactly connects the high-level proofs to the machine program, so the interpreter is the only cost model to trust. An unverified native implementation shows the algorithm's practical cost.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-29T04:47:50Z
Ignacio Vega-P\'aez
arXiv categories: cs.SC, cs.LO

We examine whether the integers admit a topology whose connected subsets are precisely the sets of consecutive integers. The main result gives a construction for every integer lattice {\mathbb{Z}}^{n}, n>0; the answer for Z is then obtained as a corollary. We prove that the neighborhoods determined by the parity of the sum of the coordinates form a basis and that topological connectedness agrees exactly with accessibility by finite paths of unit lattice steps. We also present a deductive audit and the correspondence between this argument and a verification in Lean 4 and Mathlib, including the empty set and the independent formal characterization of integer intervals. The construction and mathematical result originate in Problem 5712, proposed by Dan Marcus and solved in 1970 by the Cleveland State University group; the present article contributes a detailed exposition and a report on formal verification.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-29T15:49:40Z
Jonas Bodingbauer, Laura Kov\'acs
arXiv categories: cs.LO, cs.AI

We present Vampire-Hammer, a hammer for the Lean interactive theorem prover that discharges goals using the Vampire automated theorem prover and reconstructs proofs checked by the Lean kernel. Vampire-Hammer uses the Lean-auto framework to process goals and premises before dispatching them to Vampire for proof search. Doing so, we rely on standard TPTP problem formats and annotated TSTP proofs that support proof reconstruction. With a 10-second budget on 196,083 eligible Mathlib theorems, Vampire-Hammer solves 21,158 problems not solved by other evaluated tools within the same budget.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-29T17:35:21Z
Mike He, Dexin Zhang, Aarti Gupta
arXiv categories: cs.LO, cs.PL

Lean's rich expressiveness supports higher-order functions, inductive datatypes, and user-defined abstractions, making it challenging to translate proof obligations into first-order Satisfiability Modulo Theory (SMT) queries and reconstruct kernel checked proofs. We present crush, an extensible SMT-backed proof automation framework for Lean. To bridge the gap between Lean's higher-order constructs and the solver's first-order logic, crush uses defunctionalization to encode function values and their applications. We formalize this translation for a supported higher-order fragment and prove its soundness. Moreover, crush provides metaprogramming interfaces for extending both Lean-to-SMT translation and the reconstruction of Lean proofs from solver certificates without modifying the translation pipeline. We implement crush as both a tactic and a backend for other third-party automation systems. We show that across four such use cases that target verification and general proof automation, crush discharges more obligations than the competing backends and reconstructs more kernel-checked proofs than the baselines.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-29T17:40:57Z
Di Wu, Ling Liang, Haizhao Yang
arXiv categories: cs.AI, cs.LO

Automated computational science could accelerate discovery by selecting, adapting and developing numerical methods. This prospect requires mathematical knowledge that AI systems can interpret and reuse with explicit guarantees. Here we present FARMS, a faithful and efficient foundation that transforms computational mathematics into AI-ready computing knowledge. FARMS connects formal statements to source context, algorithmic meaning and quantitative guarantees through source preparation, reusable representations and semantic review. Across 171 targets in randomized numerical linear algebra and numerical partial differential equations, 157 were accepted by the pipeline, with mean estimated costs of US \$0.85-2.29 per target across sources. Lean-checked implications from explicit source premises connect selected statements to computational skills, illustrated by a heat-flow solve and wave-response compression. FARMS therefore supports an affordable, reusable knowledge foundation for trustworthy automated computational science.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-30T16:28:01Z
Jan Onderka, Armin Biere, Henrik B\"oving
arXiv categories: cs.LO, cs.PL

SMT-LIB is a standard input format for Satisfiability Modulo Theories (SMT) solvers. However, parsing the format is non-trivial and can become a bottleneck, e.g. when retrieving benchmark metadata or normalising the input for solvers. We introduce blazing-smtlib, a Rust parsing library for SMT-LIB, and BSmtLib, its port to Lean. We outline the library API we designed for composability and extensibility (including non-standard SMT-LIB commands), and discuss our implementation decisions for fast lexing and parsing. We proved that our lexing and parsing with Lean-specific optimisations match our formalised reading of the SMT-LIB syntax. We measured performance on a representative sample from the 2025 SMT-LIB corpus and found that blazing-smtlib is more than 6 times faster on the geometric mean than previous parsing libraries and BSmtLib is faster or comparable to them.

arXiv abstract · PDF

Lean Proof Assistant Applications · primary corpus · published 2026-10-31T23:55:48Z
Xujun Che, Depeng Xu, Jian Xiang, Taufiqua Khan
arXiv categories: cs.LO, cs.AI, cs.SE

The kernel of the Lean proof assistant checks that a proof establishes its statement. Whether the statement says what was intended is left to human reviewers. This is the old problem of validating a specification, and it grows more pressing as language models write formal statements in bulk and agents edit formal developments continuously. We present ProofPatch, a tool that helps reviewers judge Lean statements and keeps their judgments valid while the development changes. A reviewer can ask the kernel targeted questions about a statement, such as whether a hypothesis is needed or whether a counterexample exists. Each decision is stored with fingerprints of the statement as Lean elaborated it and of the definitions it depends on, and any declaration can be pinned so that a patch changing it is blocked, whether a person or an agent built on a large language model (LLM) wrote the patch. Working on elaborated terms rather than source text is the central design choice: notation and formatting changes leave a decision intact, and a changed definition reaches every theorem that uses it. On 229 pairs of consecutive revisions of Mathlib, Lean's mathematics library, ProofPatch sends 118 of 12,898 synthetic decisions back for review. Every text-based alternative misses at least 38 of these or sends back at least 13 times as many. On 1,527 labeled statements, kernel evidence flags unfaithful ones with precision 0.88 to 0.96, and in 344 runs of an LLM agent no change to a pinned statement got through.

arXiv abstract · PDF

Lean Proof Assistant Applications · cs.SE candidate · published 2026-11-01T09:43:09Z
Zihao Zhang, Zenan Li, Taolue Chen, Zhe Zhou, Tao Xie, Yuan Yao
arXiv categories: cs.SE

Software verification is typically more challenging than coding. Software developers routinely build on mature libraries and APIs, but turning successful verification solutions into reusable libraries still requires substantial expert effort. In this paper, we propose VeriBase, a framework for automatically constructing software-verification libraries by jointly generalizing code and its associated theorems from successful verification solutions. The key challenge is to generalize implementations together with the theorem statements and proofs that depend on these implementations, and reconcile overlapping components across verification tasks. To this end, VeriBase treats code and its associated theorems as declaration families, and designs a three-phase pipeline, which proves seed tasks, generalizes code and associated theorems, and harvests the resulting families into shared interfaces. VeriBase updates dependent declarations as interface change and uses Lean to check the resulting code and proofs. We evaluate VeriBase across four benchmarks with three backend LLMs. The results show that the general-purpose library built from independent 4,191 programs increases the average task success rate by up to 17.0% and meanwhile reduces the proof completion time by up to 21.4%. When VeriBase constructs a benchmark-specific library, further improvement can be observed.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-10-26T18:18:41Z
Rajan Maghera, Asher Tempest Arya, Aren A. Babikian, Marsha Chechik, Maryam Mehri Dehnavi
arXiv categories: cs.SE, cs.PL

Large language models (LLMs) are increasingly used for code generation, motivating techniques that guarantee the structural and semantic correctness of generated programs. Constrained decoding enforces correctness during generation by restricting token choices to those that admit at least one valid completion. While existing approaches can enforce syntactic constraints and selected semantic properties such as type safety, they either target specific properties or rely on operational pruning mechanisms that are difficult to generalize to data-dependent, inductive program properties. We present AGDecode, a programmable framework for semantic constrained decoding based on least-fixed-point semantics. AGDecode extends attribute grammars to partially constructed syntax trees, and reduces semantic constrained decoding to a realizability problem over such trees. The framework compiles semantic specifications into systems of relational constraints that are discharged by external verification oracles, such as SMT and CHC solvers, cleanly separating language semantics from constraint-solving machinery. We prove that our approach is sound and complete relative to an ideal verification oracle. In practice, solvers inevitably encounter uncertain queries; conservatively, our system can reject tokens for soundness or speculatively continue to generate until later queries resolve the entire generation. We mechanize the core metatheory in Rocq and evaluate the framework on semantic-constrained generation of C programs, enforcing path-sensitive safety properties including null-pointer safety, division-by-zero freedom, and initialized-variable usage. Our results demonstrate that solver-backed semantic constrained decoding can enforce rich semantic guarantees while incurring modest computational overhead at regular program boundaries.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-10-26T21:56:03Z
Aravind Mandiga, Guoming Li
arXiv categories: cs.AI, cs.LO, cs.SE

Benchmarks for verifiable code generation usually test a proof against one fixed implementation. We ask whether the same proof remains valid after a program refactoring that preserves behavior. We introduce RefactorProof, which derives 458 Lean-certified variants from the 185 VERINA tasks that compile in our pinned environment while holding the specification and evaluated proof fixed byte-for-byte. VERINA supplies reference proofs for 46 tasks, all from its basic split; the primary model-versus-reference comparisons further match on 21-25 short, non-recursive tasks. Structural refactorings expose substantial brittleness across proof sources: task-normalized structural PSR is 4.3% for the supplied references and 13.3-26.8% for the specialized provers. On the matched tasks, specialized prover proofs nevertheless have higher overall unchanged-proof survival than the supplied reference artifacts: +15.6 points for DeepSeek-Prover-V2-7B, +18.8 for Goedel-Prover-V2-32B, and +20.3 for Goedel-Prover-V2-8B; all three 95% CIs exclude zero. The ordering persists after excluding universally survived T1 variants, under family-balanced aggregation, and under alternative deployable valid-proof selection rules. However, unchanged-proof failure is not the same as high repair cost: predefined one-identifier edits repair 51/54 eligible reference structural failures and 58/85 eligible prover failures. RefactorProof therefore measures unchanged-proof stability under program refactoring, not the cost of maintaining a proof after it breaks.

arXiv abstract · PDF

Language Models for Formal Verification · cs.SE candidate · published 2026-10-27T10:06:26Z
S M Abdulla Al Mamun, Akif Islam, Mohd. Ruhul Ameen
arXiv categories: cs.SE, cs.AI

Can additional specialist language-model contexts improve software assurance when deterministic tool evidence is already available? We study this question through five experiments spanning authored Java warning controls, OWASP Benchmark assessment, Defects4J test generation, SV-COMP assertion verdicts, and deliberately misleading evidence packages. The evaluated systems use Qwen2.5-Coder-7B-Instruct, with a 1.5B sensitivity analysis, and complete 13,638 model requests. On eight related development warnings, increasing the context count from 1 to 50 increases token use 49-fold without improving unsafe clearance. On 160 OWASP cases, model configurations trade clearance against unresolved outcomes; the ten-context arm assesses only 96 cases. On 32 SV-COMP tasks, raw verifier feedback raises mean correct model verdicts from 12.7 to 22.0, but also raises incorrect verdicts from one to seven; a JBMC-plus-JVM validation baseline returns 26 correct verdicts and six unresolved outcomes. On two sets of 120 evidence packages, models reject 70-100% of applicable counterexamples, while construction-specific scope checks classify every package correctly. No target defect is discovered in three Defects4J bugs, one unsupported by the test adapter. These descriptive results support deterministic evidence admission for the tested settings, while exposing limits of verdict aggregation, feedback interpretation, and the available evaluation coverage.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-10-28T02:23:25Z
Debargha Ganguly, Divya Raghunathan, Dejan Jovanovi\'c, Vikash Singh, Soonho Kong, Aaron Tomb, Aman Goel, Ferhat Erata, Sam Bayless
arXiv categories: cs.CL, cs.AI, cs.LO, cs.SE

We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. The pipeline writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. It produces 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications. Unlike hand-written benchmarks, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-10-29T17:20:31Z
Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao
arXiv categories: cs.AI, cs.LO

AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-10-30T10:28:34Z
Zixuan Chen, Wenyuan Jiang, Junling Wang, Mrinmaya Sachan, Yinya Huang
arXiv categories: cs.LO, cs.CL, cs.LG

LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas, because retrieval skews toward popular foundational lemmas, leaving the right premises buried among hundreds of thousands of candidates. Existing neural selectors rank candidates by semantic similarity, with three intrinsic limitations: frequency-skewed retrieval, isolated pairwise ranking, and degradation on out-of-distribution queries such as competition problems and informal language. Given that mathematics is structured by dependencies rather than similarities, we restore this signal to both the training data and the model. We curate two underused dependency resources. We conduct the first systematic mining of 53 Lean Blueprint projects, a previously untapped corpus of 3,805 manually curated informal+formal nodes that capture rare, research-level premises absent from Mathlib4. We further pair it with the extraction of comprehensive, typed, multi-level Mathlib4 dependencies. We then introduce DAPS, a dependency-aware premise selector with a structural neighborhood encoder, a group-level contrastive objective, and a Mathlib-then-Blueprint adaptation procedure. DAPS reaches mean Recall@32 of 89.25 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer), and maintains this lead on two out-of-distribution benchmarks. Further experiments demonstrate that DAPS premises improve theorem proving on miniF2F and IMO-ProofBench. Project page: https://daps-eth.github.io/.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-10-30T19:14:32Z
Pedro Ribeiro, Martim Afonso, Andr\'e Vasconcelos, Jo\~ao F. Ferreira
arXiv categories: cs.SE, cs.AI, cs.LO, cs.PL

Concurrent software underpins critical infrastructure, including operating systems and databases, yet thread interactions can have bugs that bypass conventional testing. Verus extends Rust with formal verification capabilities, enabling developers to specify, implement and prove the correctness of concurrent code in the same language. Although coding agents have been explored for automated proof construction, existing Verus benchmarks offer limited coverage of concurrency-specific examples that connect atomic operations to abstract protocols. To address this gap, we introduce VerusWeave, the first benchmark dedicated to concurrent proof repair, derived from four open-source projects. It comprises 75 focused tasks and 17 full-module variants that exercise features used to verify low-level concurrent code. Tasks remove selected proof annotations and require agents to fill gaps, while preserving executable code and specifications. The evaluation harness validates repairs using Verus and a change checker, recording solutions, execution traces, and resource usage. An initial evaluation of four general-purpose coding-agent harnesses achieved 75-85% success on focused tasks and 29-47% on full-module variants, highlighting the challenge of autonomous module-wide repairs. VerusWeave provides a reusable foundation for evaluating automated proof construction for concurrent software.

arXiv abstract · PDF

Language Models for Formal Verification · cs.SE candidate · published 2026-10-30T20:16:19Z
Henry Shen, Xinling Liao, Adarsh Vatsa, William Eiers
arXiv categories: cs.SE

Agentic systems translate natural-language requests into executable artifacts while managing ambiguity and inference cost. We evaluate seven autoformalization workflows on SQL and first-order logic benchmarks for ambiguous inputs. Across five SQL workflows, the raw model leads with F1 of 53.35% on AMBROSIA and 60.85% on AmbiQT. On AmP, DRIFT gains 15.98 F1 points over the raw model at 2.03 times its token cost, whereas LoC uses 18.65 times the raw model's tokens with lower F1. Within AutoCedar, structured interpretation lowers F1 by 6.44-6.95 points and raises AMBROSIA token use 2.2-fold. Paired reviewer comparisons show modest Kimi K3 gains of 1.93 points on AMBROSIA and 2.04 on AmbiQT. Clear-ambiguous AMBROSIA analysis shows greater relative stability for AutoCedar, with a smaller F1 drop than the raw model (11.46 vs. 16.68 points), alongside lower aggregate F1 (50.16% vs. 53.35%). Autoformalization alone does not guarantee robustness to ambiguity: the tested additions offer no uniformly effective remedy, making accuracy, ambiguity handling, and inference cost joint design requirements.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-11-01T11:45:13Z
Sherzod Turaev, Mary John
arXiv categories: cs.FL, cs.CL, cs.LO

A rule written for people fixes its atomic conditions and connectives but leaves open how the connectives are bracketed, and each bracketing is a different logical reading that an autoformalizer must resolve or expose. We study the scope grammar, a deliberately ambiguous context-free grammar whose derivation trees are the readings of a connective skeleton and whose quotient by logical equivalence is what matters downstream. A skeleton with $k$ binary connectives has $C_k$ derivation trees, the $k$-th Catalan number, but far fewer logically distinct readings. For the positive, repetition-free fragment we make the gap exact: through the uniqueness of the read-once normal form we characterize the realizable normal forms by lowest common ancestors and count them with a two-label recurrence over the operator word, verified against exhaustive enumeration up to eleven atoms. The count is invariant under reversal and $\wedge/\vee$ duality; a skeleton is ambiguous if and only if it uses both $\wedge$ and $\vee$, a one-pass test; and the number of classes is at least $2^{\lfloor n/3\rfloor}$. Up to fifteen atoms the alternating pattern is the worst case; its count has a cubic generating function, is the 3-Schr\"oder sequence (OEIS A137842), and grows with base $\varphi^{5/2}\approx3.330$, below the Catalan base 4. We reduce maximality to an inequality on increments, verified to sixteen atoms, and explain why local exchange arguments cannot prove it. We also treat negation, exceptions, and background axioms, where normal-form uniqueness still decides equivalence but counting is open.

arXiv abstract · PDF

Language Models for Formal Verification · primary corpus · published 2026-11-01T23:29:34Z
Jason Hickey
arXiv categories: cs.SE, cs.LO

When autonomous coding agents synthesize implementation code, formal specifications, and mechanical proofs simultaneously, the software engineering hierarchy inverts: the formal specification becomes the primary human-reviewed artifact, while source code and proof scripts become disposable build outputs. This paper presents an end-to-end architecture for agent-authored, formally verified software engineering. First, we establish a logic-agnostic foundation combining a spec-first stack inversion, a zero-code-review workflow gated by automated continuous integration (CI) checks, and a minimal Verification Intermediate Representation (VIR) lowered via a thin, verified translator. Second, we pair an extensional Computational Type Theory (CTT) specification layer with Higher-Order Abstract Syntax (HOAS) and linear resource typing in the VIR--eliminating rewrite friction for synthesis agents while defining an experiment, its protocol frozen before the first reader, to measure whether removing boundary coercions improves human specification readability. Third, we scale collaboration across multi-team organizations using Personal Spec-Copilots and a Shared Synthesis Fleet that detects cross-team Semantic Merge Conflicts and fuses modular contracts into zero-copy binaries. We illustrate this architecture on a zero-copy authenticated message router and distinguish our existing empirical baselines (salt, SaltBench, x86lean, and MetaPRL) from newly proposed components.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-10-26T02:20:45Z
Liyi Li, Zoukarneini Difaizi Tagba, Alex Potanin
arXiv categories: cs.LO, cs.PL

Verifying quantum programs today requires specialized proof systems built on interactive theorem provers such as Rocq, Lean, Isabelle, or Why3, and even modest quantum algorithms cost substantial human effort to verify. Because quantum programs cannot be effectively checked by runtime testing, formal verification is the only viable path to correctness, making the cost of these bespoke systems the chief barrier to scalable quantum software assurance. We show that verifying a quantum program should be no harder than verifying a classical array program, a paradigm commonly used in parallel programming: the Qafny quantum proof system translates into Hoare logic with array theory completely (every Qafny proof becomes a valid Hoare triple) and soundly (a valid translated triple certifies only true quantum specifications), and we mechanize the completeness direction in Rocq. The embedding determinizes quantum proof obligations and exposes the full machinery of classical automated verifiers (e.g. Dafny and SMT-based separation logic) to quantum code, removing the need for dedicated quantum proof system infrastructure. In particular, the embedding supplies the correctness argument that the existing compilation of Qafny into Dafny lacks.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-10-29T06:55:21Z
Min Lai, Yu-Fang Chen, Shih-Han Hung
arXiv categories: cs.PL, cs.LO, quant-ph

We present, to the best of our knowledge, the first fully automated verification framework for QSP-based Hamiltonian simulation. Our framework exploits the structure of the simulation algorithm: Hamiltonians are given as weighted sums of Pauli strings, embedded into larger unitaries through block encodings, and transformed into time-evolution operators by quantum signal processing (QSP). Using a symbolic Pauli-sum semantics for ancilla-indexed circuit blocks, our verifier proves that the distinguished all-zero ancilla block is proportional to the target Hamiltonian and infers the subnormalization factor automatically. It then verifies the QSP layer by extracting the implemented polynomial transformation and certifying its approximation error. This structure-aware abstraction is essential for scalability. Composing our verified block encoding and QSP wrapper yields an estimated macro-expanded size of about 1.52 million gates. The verifier certifies the block encoding once and checks the QSP layer through its abstract interface, without expanding the oracle calls. Our implementation verifies block encodings of structured Pauli-sum Hamiltonians with up to 256 system qubits and verifies QSP Hamiltonian-simulation instances by extracting their implemented polynomials and checking the resulting approximation bounds. These results show that fully automated verification can handle common Hamiltonian-simulation circuits at substantial scale when it exploits their algorithmic structure.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-10-29T17:44:20Z
Lorenzo Ciardo, Antoine Mottet
arXiv categories: quant-ph, cs.CC, cs.LO, math.CO, math.OA

We confirm a conjecture of the first author [SODA'26] on a strong form of pseudo-telepathy for Khot's $d$-to-$1$ games: for every $d\geq 4$, every $\epsilon>0$, and every $k\in\mathbb N$, there is a $d$-to-$1$ label-cover game of classical value less than $\epsilon$ that admits a perfect quantum strategy using finite-dimensional shared entanglement with measurement contexts of radius at least $k$. As a consequence, there exist graphs whose quantum chromatic number $\chi_q$ is $3$ and whose classical chromatic number $\chi$ is arbitrarily large. This is the first improvement on the quantum chromatic gap since the work of Brassard, Cleve, and Tapp [Phys. Rev. Lett.'99], which produced graphs for which $\chi$ grows exponentially in $\chi_q$. To prove the conjecture, we proceed as follows. We start with a ``stretched'' version of the Mermin--Peres magic square, obtained by spacing out its equations and linking them with additional long equation wires. This operation increases the radius of the initial measurement contexts of a perfect quantum strategy for the game, while preserving classical unsatisfiability. We then apply parallel repetition to make the classical value small, and we turn the system into a pseudo-telepathic multi-layered Kneser hypergraph via a PCP construction of Dinur, Guruswami, Khot, and Regev [STOC'03]. Finally, we feed the resulting hypergraph into the reduction of Fei, Minzer, and Wang from hypergraph colouring to $4$-to-$1$ games, we establish quantum completeness of this reduction, and we show that it preserves context radius.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-10-29T18:01:52Z
Tomoaki Kawano (Kanagawa University)
arXiv categories: cs.LO

Quantum logic has developed in various directions since its inception. However, many existing logical approaches either focus only on pure states, or use Hilbert-space models in which the abstract relationship between pure states, mixed states, and probabilities is not made explicit. In this work, we introduce a model designed to handle quantum mixed states abstractly. Furthermore, we construct a proof system for the proposed logic and establish its completeness with respect to the intended semantics.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-10-29T18:02:11Z
Tomoaki Kawano (Kanagawa University), Ryo Kashima (Institute of Science Tokyo)
arXiv categories: cs.LO

Orthomodular logic has long been studied as a fundamental logical framework within quantum logic. In addition to its lattice-theoretic foundations, various formulations have been proposed that incorporate specialized implication connectives and more complex logical connectives. In this study, we reconstruct orthomodular logic by introducing a connective referred to as restricted negation, which has received comparatively little attention in the existing literature. We demonstrate that this connective provides a natural and expressive basis for formulating the core principles of orthomodular logic. Furthermore, as a main result, we construct a new proof system for orthomodular logic founded on this connective.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-10-31T10:52:11Z
Loan Le Maguet
arXiv categories: math.LO, quant-ph

We introduce logics of dependence and independence over polyteams (that is, databases with multiple relation schemes), in a similar way as in arXiv:1704.02158v3 [cs.LO]. On this basis, we develop a logical framework in which we can express (in formulas) relevant properties about the statistics of a repeated quantum experiment. In this framework, we formalize Bell's theorem, and the Kochen-Specker theorem as failure of logical entailments, as it was suggested in arXiv:2107.10817v3 [math.LO]. The key feature of polyteam logics in action here is their power to express both local and global properties, with respect to the set of possible measurements. The point of this is at least twofold. Firstly, as in arXiv:1102.0264v7 [quant-ph], it gives a high-level (information-theoretic) understanding of these physical phenomena, that is not intrinsic to the physical objects involved. Secondly, since logical entailment is often (partially) axiomatizable, this framework incites us to tackle the question of contextuality computationally. We also define semiring-weighted polyteams along with logics on them, and use them to recover the probabilistic versions of the contextuality theorems mentioned above.

arXiv abstract · PDF

Quantum Logic and Quantum Verification · primary corpus · published 2026-11-01T17:17:08Z
Mladen Pavicic
arXiv categories: quant-ph, math-ph, math.LO, math.MP, math.QA

Both quantum and classical logics have several mutually non-equivalent and non-isomorphic models as has repeatedly been proved in the literature. Yet, several authors have recently come with criticisms of this result. In this paper, we show that the criticisms are either unfounded or wrong.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-26T09:45:30Z
Hans van Ditmarsch, Djanira Gomes, Rojo Randrianomentsoa, Thomas Studer
arXiv categories: cs.LO

We present the directed simplicial complex: this is an extension of a simplicial complex with a direction on its faces. This enables us to model a local notion of belief in a three-valued semantics, in which formulas may be true, false, or undefined. Of particular interest is a class of directed simplicial complexes called cups, in which any maximal set of vertices of different colors is a facet. Cups permit a more concise relational representation. We give examples and applications of our logical semantics. We then provide a sound and complete axiomatization for the class of directed simplicial complexes and extend it to an axiomatization for the class of cups. We include a detailed technical comparison with other works on belief on complexes. Our work generalizes a prior axiomatization for knowledge on (undirected) impure simplicial complexes.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-27T12:06:41Z
Damiano Presa, Fabio Aurelio D'Asaro, Massimiliano Badino
arXiv categories: cs.LO

The logic KL$_1$ of Evans, Sergot and Stephenson formalizes Kant's rules as conditional imperatives $B \square\to C$ and permissives $B \diamond\to C$ over acts. Its consequence relation is operational: a rule follows from a set of rules when adjoining it leaves the set of outcomes unchanged for every input. The authors proved their calculus sound and conjectured that it is complete. We show that the conjecture fails: for distinct atoms $b,c,d$ the rules $\top \diamond\to b \lor d$, $b \diamond\to c$, $d \diamond\to c$ and $c \square\to b \lor d$ entail $\top \diamond\to c$, which is not derivable. Non-derivability is proved by an invariant that holds at every derivation depth and for arbitrary intermediate atoms. The obstruction is the side condition of may-trans, which requires each new act to bring with it a single intermediary act. Replacing it by a disjunctive side condition yields may-trans-disj, a strict generalization from which the original rule is derivable. Using a local characterization of entailment, we prove the repaired calculus sound for arbitrary sets of rules and complete for finite ones, and we show that, with finite inputs, completeness cannot be extended to infinite sets. The main results on KL$_1$ are formalized in Agda. For KL$_2$ we observe that the published reduction to KL$_1$ passes through infinite rule sets; re-establishing the decomposition for finite rule sets, we prove that KL$_2$ with the disjunctive rule is sound and complete for finite sets of rules. We close with remarks on KL$_3$ and on the significance of completeness for the relation between the operational and the inferential questions of Kant's logic.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-29T18:00:54Z
Ela Drozdowska, Pawel Pawlowski
arXiv categories: cs.LO

We introduce a uniform non-deterministic semantics for the hierarchy of paraconsistent systems mbC^n introduced by Ciuciura. The proposed construction generalizes Omori's three-valued semantics for mbC^1 to all systems of the hierarchy. We prove soundness and completeness of the semantics with respect to the corresponding axiomatizations and show that the consequence relations of the systems mbC^n cannot be characterized by finite deterministic matrices.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-29T18:01:13Z
Maciej A. Ha{\l}apacz (University of Wroc{\l}aw)
arXiv categories: cs.LO

Hamkins and Loewe described modal logic S4.2 through the notion of sets of independent buttons - statements that are possibly necessary - and switches - necessarily contingent statements. In this article we investigate logics intermediate between S4.2 and S4.3 that are defined through a different notion of independence. We provide an axiomatic description of such logics, state some basic facts and prove various completeness and decidability results.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-29T18:02:30Z
Muhammad Afaq Khan (CIDMA & Department of Mathematics, University of Aveiro Aveiro, Portugal), Manuel A. Martins (CIDMA & Department of Mathematics, University of Aveiro Aveiro, Portugal), Alexandre Madeira (CIDMA & Department of Mathematics, University of Aveiro Aveiro, Portugal), Babar Zaman (CIDMA & Department of Mathematics, University of Aveiro Aveiro, Portugal)
arXiv categories: cs.LO

In this paper, we propose fuzzy topological semantics for {\L}ukasiewicz valued modal logic, based on the standard {\L}ukasiewicz algebra. Within this setting, formulas are interpreted as fuzzy sets of truth values, while the modal operators are realized through fuzzy interior and closure operators. We define a Kripke-induced fuzzy Alexandroff topology and establish a precise correspondence between {\L}ukasiewicz fuzzy Kripke semantics and its topological counterpart. The proposed topological semantics validates the S4 modal axioms that include reflexivity, transitivity, monotonicity, normality, and the necessitation of truth.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-29T18:02:53Z
Manuel A. Martins (CIDMA & Dep. of Mathematics), Abilio Rodrigues (Federal University of Minas Gerais)
arXiv categories: cs.LO, cs.DB

A new approach to information-based logics using many-logic modal structures (MLMSs) was recently proposed by Martins et al. In such a setting, it is possible to have worlds with different underlying logics within the same frame, all anchored to a base lattice that contains the semantics of each logic as a down-complete sublattice. In this paper, we take the lattice L6, defined by the six-valued semantics of the logic of evidence and truth LET + K , as our base lattice. We also consider four-, three-, and two-valued formal systems associated with down-complete sublattices of L6. These logics are capable of representing paracomplete, paraconsistent, and classical contexts with six, four, three, and two informational scenarios, respectively. As applications of MLMSs, we will discuss the merging and temporal evolution of databases whose underlying logics are two-, three-, four-, and six-valued. We will also investigate inconsistency measures in this context.

arXiv abstract · PDF

Non-Classical Logics · primary corpus · published 2026-10-29T18:03:33Z
Pawel Pawlowski (Centre for Logic, Philosophy of Science Ghent University, Ghent, Belgium), Pietro Vigiani (Institute of Computer Science Czech Academy of Sciences, Prague, Czech Republic Centre for Logic, Philosophy of Science Ghent University, Ghent, Belgium)
arXiv categories: cs.LO

We study three paraclassical propositional logics with two negations, CLoaN, CLouN, and CLauN, obtained by pairwise combining the one-negation systems CLuN, CLaN, and CLoN. CLuN's negation is glut-tolerant and paraconsistent, CLaN's negationis gap-tolerant and paracomplete, and CLoN's negation is both paraconsistent and paracomplete. We provide sound and complete two-valued non-deterministic semantics for each of the two-negations systems. We then focus on CLauN, the system containing the primitive dual pair of CLaN and CLuN negations. In this setting, we show deductive relationships between different negations expressible in CLauN; we show two diferent ways to recapture classical logic by means of translations, locally and globally; and we show a duality results for the multiple conclusion consequence relation of the logic.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-26T16:33:20Z
Khashayar Irani
arXiv categories: cs.LO

This paper investigates the proof-theoretic foundations of the principle of reiteration (R) in natural deduction, arguing that its legitimacy originates in the structural preservation of formulae within sequent calculus rather than in an independent logical rule. By examining singlesuccedent and multisuccedent sequent calculus, we demonstrate how logical operations transform principal formulae while preserving unaffected antecedent and succedent contexts. We subsequently analyse the schematic formulation of reiteration and compare natural deduction derivations with corresponding sequent calculus derivations. This comparison identifies two fundamental functions of reiteration, namely the reuse of previously employed formulae and the restoration of previously derived conclusions. We conclude that reiteration introduces no independent inferential content but explicitly represents the structural continuity of inferential dependencies already included into sequent calculus.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-27T03:01:37Z
Oualid Merzouga
arXiv categories: cs.LO, math.LO

The fibrational framework of Licata, Shulman, and Riley gives a uniform account of substructural and modal logics for single-conclusion judgments. This thesis extends it to a multiple-output setting in which cartesian resources may be used freely, while linear resources occur exactly once on either side of the turnstile. Judgments are indexed by descriptors: directed acyclic graphs generalizing the tree-shaped expressions of the original framework. Descriptor $2$-cells encode structural transformations, and explicit gates provide weakening, contraction, coweakening, and cocontraction at linear modes. We define a sequent calculus generated by two connectives, $F$ and $U$. We prove identity, invertibility, and cut admissibility. The mode and type theories present linear-non-linear $2$-polycategories, and the projection is a local discrete fibration and a fibration, with opcartesian lifts for one-output base morphisms. Two adequacy results validate the framework: its cartesian fragment recovers the Licata--Shulman--Riley calculus, and its purely linear fragment presents classical multiplicative linear logic. Finally, we relate indexed and fibrational semantics. After developing representability correspondences for multicategories and polycategories, we establish an equivalence between multi-indexed categories over a fixed representable base and multicategorical opfibrations over it, together with its biclosed bifibrational version. We also give a one-way construction from planar poly-indexed data to a planar polycategory.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-27T19:27:12Z
Matthias Baaz, Mariami Gamsakhurdia
arXiv categories: cs.LO

Quantifier shifts are one of the oldest proof methods, but they are orthogonal to the cut free format: They can shorten proofs non-elementarily. (The proof is based on the sequence of proofs exhibiting a non-elementary difference between proofs with cuts and cut-free proofs by Orevkov). The cost is, however, that those proofs are globally sound but locally unsound. (Their subderivations might be unsound in contrast to the Hilbert concept of proof). In non-classical logics these calculi are only sound when all quantifier shifts are added. This characterizes all intermediate logics where Skolemization and the epsilon calculus is conservative (in contrast to the epsilon theorem which holds only for finite-valued Goedel logics).

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-28T20:42:06Z
Victor Barroso-Nascimento, Joaquim T. Waddington, Elaine Pimentel
arXiv categories: cs.LO, math.LO

We investigate the relationship between base-extension semantics, Beth semantics, and Prawitz's ecumenical logic. We first present a base-extension semantics for the propositional fragment of Prawitz's system and prove that it is sound and complete. The semantics interprets intuitionistic and classical operators directly within a common proof-theoretic framework, without reducing the classical operators to their intuitionistic counterparts by means of a translation. We then analyse the effect of incorporating Beth-style clauses into base-extension semantics. When arbitrary bases are admitted and $\bot$ is governed by atomic explosion, these clauses trivialise. By contrast, when $\bot$ is treated as a basic sentence and attention is restricted to consistent bases, the Beth-style clauses for atoms and disjunction characterise, respectively, classical atoms and classical disjunction in Prawitz's system. We also obtain equivalent, path-independent formulations of the classical clauses for atoms, disjunction, and implication. These results reveal that the consistency constraint is not merely a technical restriction: within base-extension semantics, it transforms clauses originally associated with intuitionistic semantics into semantic characterisations of classical operators.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-29T18:03:12Z
Satoru Niki (Kanagawa University)
arXiv categories: cs.LO

The constructive logic JP' is known to be the weakest logic between intuitionistic and minimal logic that satisfies Glivenko's theorem. In spite of this natural and desirable formal property, the motivation for its notion of negation remains rather elusive: it can be characterised by a restriction of Peirce's law or by the double negation of ex falso quodlibet, neither of which is very intuitive. In order to have an alternative perspective on this negation, we study in this paper a couple of natural deduction systems for JP'. We first present a system that is normalisable and satisfies a restricted form of the subformula property. Then a modification of this system is introduced, whose rules satisfy the separation of connectives and the full subformula property. Afterwards we turn our attention to a typed lambda-calculus, with respect to which our natural deduction enjoys the Curry-Howard correspondence, followed by a concluding discussion.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-29T18:03:52Z
Yaroslav Petrukhin (University of Lodz)
arXiv categories: cs.LO

In this paper, we present a natural deduction system for a strong Kleene-based neutral free logic with definite descriptions. The system combines a three-valued propositional basis with free quantification, identity, existence, and rules for definite descriptions. The main result is a normalisation theorem for a proof-theoretically equivalent restricted formulation of the system; we also establish a corresponding modified subformula property for its fragment.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-29T18:04:11Z
Pawe{\l} P{\l}aczek (WSB Merito University in Poznan, Poland), Cheng-Syuan Wan (Tallinn University of Technology, Estonia)
arXiv categories: cs.LO

Cyclic Linear Logic (CyMALL, CyBL) is a compromise between Commutative Linear Logic (MALL) and Noncommutative Linear Logic (Bilinear Logic, BL). We do not admit commutativity of the tensor, but we still admit only one De Morgan negation. MALL and its variants are natural extensions of Full Lambek Calculus (FL). Abrusci proved that CyBL is not a conservative extension of FL, if we admit additive constants in these logics. In this paper we show that Cyclic Nonassociative Bilinear Logic (CyNBL) with both additive constants is a strongly conservative extension of Full Nonassociative Lambek Calculus with only one additive constant - the upper bound - and that this holds even in the presence of an arbitrary set of nonlogical axioms.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-29T18:11:25Z
Kaito Ichikura (Tohoku University)
arXiv categories: cs.LO

This paper investigates the role of negation in arithmetic by analyzing subsystems based on subminimal logic. We introduce NA^PR, a system of subminimal arithmetic equipped with all primitive recursive functions, and answer the following four questions: (1) Can we develop reasonable arithmetic within NA^PR? (2) Can we characterize logical rules Absorption of Negation (An) and Ex Falso Quodlibet (ECQ) by arithmetical principles? (3) Are there strict differences in deductive power among NA^PR, MA^PR, and HA? (4) Do MA^PR and MA, and NA^PR and NA have a similar mutual interpretability relationship as HA? We show the following: First, Heyting Arithmetic (HA) is shown to be a conservative extension of NA^PR for positive formulas. Based on NA^PR, we prove that (ECQ) is equivalent to the definability of disjunction, and that (An) is equivalent to a variant of the least number principle. Furthermore, using the constant domain neighbourhood semantics, we show that the systems NA^PR, MA^PR (written as NA^PR+(An)) and HA (written as NA^PR+(An)+(ECQ)) form a strictly increasing hierarchy of strength. Finally, we demonstrate the essential role of primitive recursive functions in weak arithmetic using classical countermodels.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-29T18:12:12Z
Nils K\"urbis (University of {\L}\'od\'z)
arXiv categories: cs.LO

While Russell's theory of definite descriptions, expressions of the form 'the F', is almost incontrovertible in classical logic, in free logic matters stand differently. Several alternatives have been proposed. In Lambert's hierarchy, the weakest theory is his minimal free theory of definite descriptions (MFD), which only says that anything is the F iff it is the unique existing F, the strongest one is a chosen object theory in which all improper definite descriptions refer to the same object (FD2). Intermediate is Lambert's FD1, which adds ix(x = t) = t as an axiom to MFD. MFD is very weak. FD2 is very strong. One might hope to find intermediate systems in which ix(x = t) = t is provable from more fundamental principles. The present paper considers one avenue where one might hope to find them and closes it. Two theories, FDA and FDH, will be considered that are motivated by considerations from proof-theoretic semantics. The former turns out to be equivalent to FD2, the latter to have unreasonable consequences. A third theory, similarly motivated, is also not viable. The philosophical upshot of this is briefly discussed.

arXiv abstract · PDF

Proof Theory and Sequent Calculi · primary corpus · published 2026-10-31T20:21:08Z
Joost J. Joosten, Cosimo Perini Brogi
arXiv categories: math.LO

The reflection calculus with one modality is denoted by $\mathsf{RC}_1$ and its quantified generalization is known as $\mathsf{QRC}_1$. These decidable calculi are of interest since they generate the strictly positive fragments of the (quantified) provability logic for theories like Peano Arithmetic and Heyting Arithmetic. We introduce analytic cut-free calculi ${\mathrm{GRC1}}$ and ${\mathrm{GQRC1}}$ for $\mathsf{RC}_1$ and $\mathsf{QRC}_1$ respectively. The new calculi derive sequents of the form $A\Longrightarrow B$ with $A,B$ strictly positive formulas. In particular, the new calculi do not use (multi)sets nor nested sequents. For both ${\mathrm{GRC1}}$ and ${\mathrm{GQRC1}}$ it is shown that the cut-rule is admissible. As a consequence, it is proven that the calculi are deductively equivalent to $\mathsf{RC}_1$ and $\mathsf{QRC}_1$ respectively. The cutfree systems are used to prove uniform interpolation for the two reflection calculi. In addition, ${\mathrm{GRC1}}$ is used to give a syntactic proof of Dashkov's Theorem to the extent that $\mathsf{RC}_1$ is the strictly positive fragment of the provability logic ${\mathsf{GL}}$. The paper also introduces non-analytic calculi that are conceptually easier but proof-theoretically behave badly. It is shown that even those systems allow direct cut-elimination: the benefits of the strict positivity outweigh the draw-backs of a non-analytic calculus in these cases.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-10-26T17:13:05Z
Yoshiki Nakamura
arXiv categories: cs.LO, math.LO

The validity problem for first-order logic is a well-known undecidable problem. The undecidability also holds even for $\mathsf{FO}3$ and (equational formulas of) the calculus of relations. In this paper we tighten these undecidability results to the following: (1) $\mathsf{FO}3$ with just one binary relation is undecidable even without equality; and (2) the calculus of relations with just one character and with only composition, union, and complement is undecidable. Additionally we prove that the finite validity problem is also undecidable for the above two classes.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-10-28T22:09:20Z
Wilmari Morton, Claudette Robinson
arXiv categories: cs.LO

We adapt a construction by Comer (1983) for polygroups to define the wreath product of the dual frames of two distributive quasi relation algebras satisfying certain conditions and show that it is itself a frame. Frames play a role analogous to that of atom structures for relation algebras. After introducing the notion of a frame network, we establish a correspondence between frame networks satisfying certain conditions and representability of finite distributive quasi relation algebras. Next we describe a frame network for the wreath product of two finite representable distributive quasi relation algebras that satisfies the aforementioned conditions, as well as additional conditions, and use this to conclude that the complex algebra of the wreath product is a representable distributive quasi relation algebra. Thus, our construction provides a method for obtaining representable DqRAs from certain finite DqRAs that are already known to be representable.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-10-29T09:26:31Z
Mingkun Xiao, Yixuan Sun
arXiv categories: cs.FL, cs.LO

Higher-order recursion schemes (HORS) are finite, simply typed recursive programs that generate potentially infinite trees. Their monadic second-order model-checking problem is decidable. We prove that tree equivalence of deterministic HORS is undecidable and, more precisely, $\Pi^0_1$-complete under total computable many-one reductions. The lower bound holds for safe, productive schemes of order at most four over the fixed ranked alphabet $\Sigma_2=\{e:0,d:2\}$, consisting of one nullary and one binary symbol. Adapting the counter-guard witness of Boiret, Piorkowski, and Schmude, we generate all candidate executions of a two-counter machine by producing both continuations at every counter test. An integer weight is nonzero exactly on legal prefixes. Functions at fixed simple types represent the polynomial of growing degree. A shift recurrence updates them without storing a separate step counter, allowing the witness to be implemented by safe applicative HORS rules. At candidate halts, the intermediate schemes generate unary observation subtrees whose lengths encode the two natural-number components of the signed weight. Invalid candidates give matching observations; a legal halt produces a finite discrepancy. Fixed constructor contexts encode these intermediate trees over $\Sigma_2$. For the upper bound, a finite monotone semantics decides head convergence and supports an algorithm computing exact tree prefixes at any prescribed finite depth, including positions labelled $\bot$.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-10-29T10:13:46Z
Sofia Brenner, Jan Hubi\v{c}ka, Mat\v{e}j Kone\v{c}n\'y
arXiv categories: math.CO, cs.DM, math.LO

We prove that finite two-graphs have coherent EPPA and that neither graphs modulo global complementation nor two-graphs modulo global complementation have EPPA. This completes the classification of EPPA and coherent EPPA for the reducts of the random graph, answering a question and confirming a conjecture of Evans, Hubi\v{c}ka, Kone\v{c}n\'y and Ne\v{s}et\v{r}il.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-10-29T13:46:23Z
Bjarki Geir Benediktsson, Dugald Macpherson, Isolde Adler
arXiv categories: math.LO

A \emph{Johnson graph} $J(n,k)$ is a graph whose vertices are the $k$-element subsets of an underlying set of size $n$ where two vertices are adjacent if they intersect in a subset of size $k-1$. We extend the definition to allow infinite parameters and we study a natural limit theory $T_{\mathcal{J}}$ of Johnson graphs. We show that $T_{\mathcal{J}}$ is complete and we give an axiomatisation of $T_{\mathcal{J}}$, from which we obtain a complete description of the models of $T_{\mathcal{J}}$. We use this to show tameness properties of $T_{\mathcal{J}}$, namely that $T_{\mathcal{J}}$ is $\omega$-stable of Morley rank $\omega$, but not monadically dependent. In particular it follows that the class of all finite Johnson graphs is stable, and therefore dependent but not monadically dependent.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-10-30T16:24:22Z
Dibyayan Chakraborty, Sebastian Ordyniak, Sebastian Siebertz
arXiv categories: cs.LO

Monadic second-order logic yields powerful algorithmic meta-theorems, but cannot express that a vertex set induces a shortest path. We study metric extensions of counting monadic second-order logic and identify structural parameters supporting efficient model checking, optimization, and counting. We show that shortest paths and equidistance guarded by geodesic cycles are definable in ordinary vertex-set MSO on graph classes of bounded cycle-basis length. This yields fixed-parameter tractable model checking for the corresponding extensions of CMSO2, parameterized by formula length and bag-connected treewidth, and of CMSO1, parameterized by formula length and geodesic cliquewidth: the sum of cliquewidth and cycle-basis length. The translations preserve free variables, yielding additive optimization and counting. Applications include Minimum Geodetic Set and Strong Metric Dimension for geodesic cliquewidth, and Minimum Isometric Path Partition for bag-connected treewidth. We also introduce restricted packing-covering templates that allow numerical distance thresholds to remain outside the parameter. For each fixed template, feasibility, additive vertex-weight optimization, and counting are fixed-parameter tractable in bag-connected treewidth. Applications include Distance-r Dominating Set, d-Scattered Set, and Minimum Eccentricity Shortest Path. Finally, we characterize bounded bag-connected treewidth and bounded geodesic cliquewidth through monadic dependence for the corresponding guarded logics. Unguarded distance comparisons have stricter structural boundaries: first-order model checking is AW[*]-complete already on uncolored caterpillars, and model checking a fixed existential monadic sentence is NP-complete on this class.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-11-01T03:35:22Z
Derek R. Aoki
arXiv categories: math.LO, cs.LO

Order-invariant cluster first-order logic (CFO) and local-order-invariant first-order logic are two fragments of order-invariant first-order logic, both motivated by the study of invariant logics on classes of bounded degree. Our main result is that order-invariant CFO contains local-order-invariant FO on arbitrary classes of finite structures, settling the conjecture of Ghasemi and Grange that order-invariant CFO contains plain FO. By combining this with a collapse result of Ghasemi and Grange, we obtain the equivalence of FO, local-order-invariant FO, and order-invariant CFO on classes of finite colored graphs of bounded degree. The proof makes use of Gaifman normal form, which allows our translation from local-order-invariant FO to order-invariant CFO to be effective. Combined with the fixed-parameter tractability of model-checking for order-invariant CFO on bounded-degree colored graph classes, this shows that model-checking for local-order-invariant FO on bounded-degree colored graph classes is fixed-parameter tractable. To generalize our collapse and model-checking results beyond colored graphs, we use a method based on first-order interpretations which also yields a collapse of order-invariant FO to FO when restricted to graph classes of bounded shrub-depth. Finally, we give an application to the database-motivated frozen-witness logic of Abiteboul, Simon, and Vianu by showing that local-order-invariant FO contains deterministic frozen-witness FO, and thus that deterministic frozen-witness FO collapses to FO on classes of finite structures of bounded degree.

arXiv abstract · PDF

Decidability and Finite Model Theory · primary corpus · published 2026-11-01T22:10:22Z
Olivia Aubone, Eduardo Due\~nez, Jos\'e Iovino
arXiv categories: math.LO

For countable vocabularies, we extend the omitting types theorem for countable fragments of infinitary logic to Keisler's general real-valued structures by proving that the space of Henkin types of each such fragment is \v{C}ech-complete. The structures interpret function symbols arbitrarily and predicate symbols by bounded real-valued functions, while each formula carries a bound of its own. This extends the setting of Eagle's theorem from metric structures with a prescribed master metric to general structures whose vocabulary prescribes the sorts and bounds of the symbols. Following Keisler and Miller's treatment of logic without equality, we build models from closed terms. Morley's Baire category method then gives every satisfiable theory on a countable fragment a model with countable sorts omitting any countable family of types whose closed-term instances have empty interior in the space of Henkin types satisfying the theory.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-26T13:21:47Z
Vahagn Aslanyan
arXiv categories: math.CV, math.DS, math.LO, math.NT

We prove the Modular Existential Closedness conjecture for the modular $j$-function extended from the upper half-plane to $\mathbb{C} \setminus \mathbb{R}$ by Schwarz reflection. Specifically, we show that any system of equations involving the field operations and $j$ has solutions in the complex numbers unless it is overdetermined. Such a system is overdetermined if, roughly, there are more independent equations than variables, possibly after applying the transformation rules of the $j$-function under the linear fractional action of $\rm{PGL}_2(\mathbb{Q})$ on $\mathbb{C} \setminus \mathbb{R}$. In general, we do not expect overdetermined systems of equations to have solutions due to the algebraic and transcendental properties of the $j$-function captured by the modular analogue of Schanuel's conjecture. In geometric terms, Modular Existential Closedness states that given a broad and free irreducible algebraic variety $V \subseteq \mathbb{C}^n \times \mathbb{C}^n$ -- where broadness and freeness are geometric conditions guaranteeing that the system is not overdetermined -- there is a point of the form $(\tau_1, \ldots, \tau_n, j(\tau_1), \ldots, j(\tau_n)) \in V$ with $\tau_i \in \mathbb{C} \setminus \mathbb{R}$. The proof uses Ratner's theorems on the closure and equidistribution of the orbits of unipotent flows in powers of $\rm{PGL}_2(\mathbb{R})$ to describe the asymptotic behaviour of the orbits of certain analytic maps. This is then applied to approximate a relatively simple system of equations using the original system and the action of $\rm{PGL}_2(\mathbb{Z})$. The construction of the limiting system makes use of the Ax--Schanuel theorem and guarantees an isolated solution. Rouch\'e's theorem then establishes the existence of solutions for the original system of equations.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-27T16:52:24Z
Mira Tartarotti
arXiv categories: math.LO, math.CO

We prove Szemer\'edi-Trotter-type incidence bounds for algebraic relations in any field $F$ admitting a valuation with finite residue field. This includes $\mathbb F_q(t)$, $\mathbb F_q((t))$, and all finitely generated extensions of finite fields. Bays and Martin show that any algebraic $K_{d,s}$-free relation $E\subseteq F^k\times F^\ell$ admits a power-saving in the classical Zarankiewicz bound of K\H{o}v\'ari, S\'os, and Tur\'an. Answering a question of the authors, we show that this power-saving is uniform in $F$: There is some $\epsilon>0$ depending only on $d$ and the complexity of $E$ (and not on $F$) such that for $A\subseteq F^k$ and $B\subseteq F^\ell$, the number of edges $|E(A,B)|$ is at most $O(|A|^{1-\epsilon}|B|^{1-\frac{1-\epsilon}{d}}+|A|+|B|)$. For the case where $A$ is a set of points and $B$ is a set of lines in $F^2$ and $E$ is the incidence relation, we prove the explicit bound $O(|P|^{\frac{8}{9}}|L|^{\frac{5}{9}}+|P|+|L|)$. As the central ingredient of the proof, we introduce the model-theoretic notion of distality relative to a definable set. We begin developing this notion and prove that the theory of algebraically closed valued fields is distal relative to the residue field. An application of a result of Chernikov, Peterzil, and Starchenko, based on work of Chernikov, Galvin, and Starchenko, yields our incidence bounds.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-29T23:19:16Z
Leo Gitin
arXiv categories: math.LO, math.NT

Many explicit constructions in algebra are not first-order definable in classical finitary logic, but are, however, definable in infinitary logic. The aim of this paper is to show how infinitary logic can be used to lift model-theoretic results in arithmetic to a quantifier-sensitive form. We apply this idea to a deep result of Jahnke and Kartas on the model theory of perfectoid fields. Our main result is that a first-order sentence $\phi$ holds in the tilt $k^{\flat}$ of a perfectoid field $k$ if and only if a certain sentence $\phi^{\natural}$ holds in a non-principal ultrapower of $k$, where $\phi^{\natural}$ does not depend on $k$ and is only slightly more complicated than $\phi$ itself. In particular, tilting preserves the L\'evy hierarchy in a precise sense. To this end, we prove that the Standard Decomposition of a valued field at a constant $t$ is infinitarily interpretable by formulas of rank at most 1.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-30T08:36:06Z
Will Johnson, Jinhe Ye
arXiv categories: math.LO

Let $K$ be a field which is strongly stable, that is, stable and strongly dependent. Then $K$ is finite or algebraically closed. This answers a question of Shelah.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-30T14:59:33Z
Will Johnson
arXiv categories: math.NT, math.LO

Let $p$ be a prime number and let $K$ be a field such that $p$ is prime to the absolute Galois group $\operatorname{Gal}(K)$, in the sense that $p$ does not divide the degree of any finite Galois extension of $K$. We conjecture that $K$ is large in the sense of Pop: any smooth algebraic curve $C$ over $K$ with a $K$-rational point has infinitely many $K$-rational points. This conjecture would have some consequences in mathematical logic. For instance, it would imply the expected classification of stable fields of positive characteristic. We give some weak evidence for this conjecture. Specifically, suppose that $K$ is a perfect field and $\operatorname{Gal}(K)$ is prime to $p$. Then every abelian variety $A$ over $K$ has Zariski dense $K$-rational points, and if $C$ is a smooth curve of genus less than $7-p$ with at least one $K$-rational point, then $C$ has infinitely many $K$-rational points.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-31T16:43:55Z
C. Terry, J. Wolf
arXiv categories: math.CO, math.LO

In the setting of abelian groups, Haussler's packing lemma implies that any subset of bounded $\operatorname{VC}$-dimension can be approximated by one of a small number of representative translates. While this exact statement is provably false under the weaker hypothesis that $A$ has bounded $\operatorname{VC}_2$-dimension, we show that in $\mathbb{F}_p^n$ a similar statement does hold after localization to cosets of subspaces depending on the individual translates. More precisely, given $\epsilon>0$ and $A\subseteq \mathbb{F}_p^n$ with $\operatorname{VC}_2(A)<k$, we show that there exist $r\leq \epsilon^{-O_{k,p}(1)}$ and $g_1,\ldots, g_r\in \mathbb{F}_p^n$ with the property that for every $x\in \mathbb{F}_p^n$, there is a partition $\mathcal{C}_x$ of $\mathbb{F}_p^n$ into cosets of (possibly distinct) subgroups, each of index at most $\exp(\epsilon^{-O_{k,p}(1)})$, and a subcollection $\Omega_x\subseteq \mathcal{C}_x$ whose union has size at least $(1-\epsilon)|\mathbb{F}_p^n|$, such that on each $C\in \Omega_x$, the translate $A-x$ looks like one of $A-g_1,\ldots, A-g_r$, in the sense that $|((A-x)\Delta (A-g_{i_{x,C}}))\cap C|<\epsilon|C|$ for some $1\leq i_{x,C}\leq r$. We also prove a second version of this result in which each partition $\mathcal{C}_x$ is the set of cosets of a single subgroup $H_x$ of quasipolynomial index but where the bound on $r$ is a quadruple exponential.

arXiv abstract · PDF

Model Theory of Fields and Combinatorics · primary corpus · published 2026-10-31T18:58:10Z
H. Sheats, C. Terry
arXiv categories: math.CO, math.LO

This paper classifies hereditary properties of k-uniform hypergraphs according to bounds in the weak hypergraph regularity lemma first developed by Chung. Specifically, we prove the bounds must grow at a constant, polynomial, exponential, or tower rate. This generalizes work in the 3-uniform case by the second author.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-26T06:20:07Z
Monroe Eskew
arXiv categories: math.LO

We show that if $\kappa^{<\kappa} = \kappa$, then there is a $\kappa$-strategically closed, $\kappa^+$-c.c. partial order that forces $\square_\kappa$. We discuss consequences for generic large cardinals.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-26T08:36:31Z
Ruijun Wang
arXiv categories: math.LO, math.FA

We determine all Borel-reducibility comparisons within the family of benchmark equivalence relations in Gao's monograph, enlarged by the universal treeable relation $E_{\infty T}$ and its countable power $E_{\infty T}^\omega$. We prove $E_\infty^\omega\leq_B c_0$, $E_\infty\nleq_B\ell_p$ for $2<p<\infty$, $\ell_p\nleq_B{\equiv_m}$ for $2<p<\infty$, $c_0\nleq_B{\equiv_m}$, $c_0\nleq_B\ell_\infty^+$, and $\equiv_m\nleq_B\ell_\infty^+$. Together with the classical result, these give $\ell_p\leq_B{\equiv_m}$ exactly when $p\leq2$. The same methods show that $E_{\infty T}$ is incomparable with every $\ell_p$, $1\leq p<\infty$. The comparisons answer questions recorded in Gao's monograph and Kanovei's monograph. We also prove that unitary equivalence of all bounded linear operators is not Borel reducible to $\equiv_m$, answering a question of Ding and Gao. Equivalently, unitary equivalence of arbitrary representations of $F_\infty$ is strictly more complicated than that of arbitrary representations of $\mathbb Z$, answering a question of Thomas.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-26T20:40:31Z
M\'arton Elekes, M\'at\'e P\'alfy
arXiv categories: math.LO, math.GN

Universally Baire sets are a standard tool in modern set theory, where they are closely connected with forcing and absoluteness. In this paper we study universal Baireness instead as purely a regularity notion for subsets of Polish spaces. Our aim is not to develop the set-theoretic theory, but to place the notion on a systematic descriptive-set-theoretic footing and to clarify the several nonequivalent definitions that occur in the literature. A subset of a Polish space is called \emph{universally Baire} if all its continuous preimages possess the property of Baire. However, it is important to specify what the domain of these continuous functions can be. In fact, a plethora of definitions are used by various authors in the literature, the class of possible domains is sometimes the class of Polish spaces, compact metrizable spaces, all topological spaces, compact topological spaces, etc. We clarify this situation by demonstrating that the above four options are pairwise nonequivalent under the Continuum Hypothesis, we determine all the implications between these four notions that are provable in $ZFC$, and also show that all the notions used in the literature are equivalent to one of these four. Furthermore, we use Miller forcing to show that actually the cases of Polish and compact metrizable spaces are consistently equivalent. We show that numerous definitions using Borel isomorphisms, changes of topologies and Boolean algebras are all equivalent to the case of Polish domains. We present an argument that the notion using Polish domains is the natural dual to the notion of universally measurable sets. Finally, as a byproduct, we prove that the following statement is independent of $ZFC$: if a subset of a Polish space has the property of Baire relative to every nowhere dense Cantor subspace, then the subset has the property of Baire in the whole space.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-28T21:29:48Z
Armando Martino, Motiejus Valiunas
arXiv categories: math.LO, math.FA, math.GR

We show that, in ZF set theory, the existence of "coset correct means" on all groups is equivalent to the Hahn-Banach Theorem, as well as to the existence of invariant means on abelian groups.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-28T21:32:43Z
Tom Benhamou, Hannes Jakob
arXiv categories: math.LO

We give an example of a directed set whose Tukey spectrum is not closed under stationary limits. This is a counterexample to a theorem due to Isbell from the 60's. We isolate a combinatorial principle arising from our example, between stationary reflection and weak compactness.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-29T15:12:23Z
Wei Dai
arXiv categories: math.DS, math.LO

We study the density of ergodic subrelations in the canonical Polish space of subequivalence relations of a probability-measure-preserving countable Borel equivalence relation. Our main result establishes rich ergodicity for ergodic treeable equivalence relations. The proof combines a strongly increasing exhaustion with relative ergodic hyperfinite decomposition. As an application, for every $2\leq r<\infty$, we show that the product of the dyadic odometer action of $\mathbb{Z}$ with the Bernoulli action of $\mathbb{F}_r$ has a richly ergodic orbit relation, whereas the Bernoulli action of $\mathbb{Z}\times\mathbb{F}_r$ does not. Thus rich ergodicity of a free ergodic action is not determined by the acting group.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-29T16:56:30Z
Assaf Shani
arXiv categories: math.LO

Given a collection of mathematical objects and a natural notion of equivalence (such as isomorphism), we want to find a complete classification. This paper presents methods for proving anti-classification results, that is, when a complete classification is not possible using certain classifying invariants. The problem of using real numbers as classifying invariants is well understood. In this case, the obstruction to classifiability is ergodicity. We consider classifiability by higher rank objects, such as countable sets of real numbers, and present a simple ergodicity-like obstruction for classifiability. This method is particularly useful when applied in various models of ZF where even weak fragments of the axiom of choice fail.

arXiv abstract · PDF

Set Theory and Descriptive Set Theory · primary corpus · published 2026-10-30T15:15:55Z
Elliot Glazer, Toby Meadows
arXiv categories: math.LO

We prove that KP, with Full Set Induction, is neither solid nor tight. More generally, every consistent theory obtained from KPC by adding a quantifier bounded set of sentences has a model with a parameter-free definable class surjection from its natural numbers onto its universe. Using such enumerations to define generic extensions by relative interpretations, we show that theories with the stable definable ground property are not tight. Ground definability over MOST and continuum coding over ZFC^{\Pi_3} yield applications to weak inductive set theories with large cardinals and forcing axioms. Finally, solidity for quantifier bounded extensions of MOST with Full Set Induction implies a Ground Axiom formulated using a fixed finite level of genericity; under the same solidity hypothesis, the corresponding extension of full ZFC proves the ordinary Ground Axiom.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-10-27T10:34:25Z
Yudai Suzuki
arXiv categories: math.LO

In this paper, we consider conservation results for iterated $\beta_n$-model reflection principles. Using these principles, we characterize the $\Pi^1_{m+2}$-, $\Sigma^1_{m+2}$- and $\mathsf{B}(\Pi^1_{m+2})$-consequences of $\Sigma^1_{n+1}$-$\mathsf{DC}_0$ and $\Sigma^1_{n+1}$-$\mathsf{TDC}_0$ for $m \leq n$. Here, $\mathsf{B}(\Pi^1_{m+2})$ denotes the set of Boolean combinations of $\Pi^1_{m+2}$-formulas, and $\mathsf{TDC}$ stands for transfinite $\mathsf{DC}$. We also show that, in each case, the stronger theory has a super-exponential speed-up over the corresponding conservative subtheory.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-10-29T02:01:00Z
George Barmpalias, Lu Liu
arXiv categories: math.LO

Given a real $x\in 2^\omega$, how many reals are there that are simpler (or equally simple) to describe than $x$. With ``simpler to describe" characterized by $K$-complexity of initial segments (hence we call such $y$ with $y\leq_K x$ a solution to $x$), if $x$ is infinitely often $K$-trivial (hence i.o. $K$-trivial), then a simple counting argument shows that the number of solutions to $x$ is countable. If $x$ is non i.o. $K$-trivial, then must it admit uncountably many solutions? Motivated by this question, we show that: (1) There is a non i.o. $K$-trivial $x$ such that most of its solution is i.o. $K$-trivial. i.e., Only countably many solution to $x$ are non i.o. $K$-trivial. In particular, the cardinality of $K$-degree of $x$ is countable. (2) There is a minimal pair of K-degree (meaning their common solutions are all $K$-trivial) so that each of the pair is non i.o. $K$-trivial, generalizing a result of Csima and Montalb\'an (where the pair is not required to be non i.o. $K$-trivial but non $K$-trivial). (3) There is a non i.o. $K$-trivial $x$ whose $\Delta_K$ complexity grows arbitrarily slow (in a weak sense: $\inf_{m\geq n}\Delta_K(x\upharpoonright m)\leq h(n)$ with $h$ a given unbounded and nondecreasing function) such that $x$ admits uncountably many solutions. (4) An ample excess lemma holds for non i.o. $K$-trivial. Namely: $$ \sum_n 2^{-(K(x\upharpoonright n)- \log_2 n)}<\infty. $$ for all non i.o. $K$-trivial $x$. Actually, this even holds for non i.o. $b$-$K$-trivial with $b$ only depends on the universal prefix free machine. The same argument also gives a constant complexity return phenomenon for $K$-trivial where this constant only depends on the universal prefix free machine.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-10-29T02:03:24Z
George Barmpalias, Lu Liu
arXiv categories: math.LO

Can random real carry arbitrary information. In terms of (Turing) computability, Ku\v{c}era and G\'{a}cs addressed this question in affirmative. i.e., Every real $x\in 2^\omega$ is computable from some Martin-L\"of random real. This result motivated quantitative versions of coding into random reals. i.e., How many bits of the random oracle are needed to compute the first $n$ bits of $x$. Barmpalias and Lewis-Pye obtained a coding that uses $n+O(\log n)$ many bits. Is it possible for the coding to use $n$ bits exactly? This is equivalent to say, if every real is $rK$-reducible to a Martin-L\"of random real. In this paper, we prove that such a coding does not exist. i.e., There exists some real that is not $rK$-reducible to any Martin-L\"of random real.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-10-29T17:28:11Z
Ekin Arik\"ok, Christoforos Panagiotis, Nicholas Pischke, Thomas Powell
arXiv categories: math.PR, math.LO

We prove quantitative sub-ballisticity for the self-avoiding walk on the lattice $\mathbb{Z}^d$, $d\geq 2$. Namely, we obtain an explicit exponential rate of decay for the probability that a self-avoiding walk of length $n$ reaches distance at least $vn$, in terms of $v>0$. As a consequence, we show that the displacement of an $n$-step self-avoiding walk is at most $n/\exp(c\log^* n)$ with very high probability. Previously, only a non-quantitative $o(n)$ bound was known from the work of Duminil-Copin and Hammond. Along the way, we show that at criticality the partition function of bridges of length $n$ is on average bounded by $C/\log\log n$, which we believe to be of independent interest. Our approach is based on a quantitative analysis of the original nonconstructive proof of Duminil-Copin and Hammond using ideas from proof theory.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-10-31T10:59:30Z
Manlio Valenti
arXiv categories: math.LO, math.CO

We characterize the uniform computational strength of finding one-way Eulerian paths in countable graphs. For both directed and undirected graphs, this problem is Weihrauch-equivalent to $\mathsf{lim}\times\mathsf{C}_{\mathbb{N}}'$, where $\mathsf{C}_{\mathbb{N}}'$ is the jump of closed choice on the natural numbers. This refines the proof-theoretical strength of the existence of an Eulerian path given by the reverse mathematics framework. The $\mathsf{C}_{\mathbb{N}}'$ component comes entirely from the difficulty of choosing a starting vertex: with a valid start prescribed, the problem is equivalent to $\mathsf{lim}$. We also study the problem $\mathsf{OrientEP}$ of orienting an undirected graph while preserving the existence of a one-way Eulerian path. We prove $\mathsf{lim}_2<_{\mathrm{W}}\mathsf{OrientEP}<_{\mathrm{W}}\mathsf{C}_{2}'\sqcap\mathsf{Sort}_2$ and $\mathsf{OrientEP}\not\le_{\mathrm{W}}\mathsf{C}_{\mathbb{N}}$.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-11-01T02:02:52Z
Xuanheng Zhao
arXiv categories: math.LO

We investigate whether classical recursion-theoretic notions defined by function domination remain unchanged when success is required only on sets of prescribed asymptotic density. We establish robustness for many such notions and uncover unexpected connections between familiar degree properties by comparing upper and lower density. In contrast, pdomination, as defined by Chong, Hoi, Stephan and Turetsky, is not robust under density weakenings. We also answer a question of Kjos-Hanssen and Nies by characterizing superhighness as domination with a threshold boundedly limit recursive in the oracle. As an application, we introduce supermaximal sets, a strengthening of maximality whose degrees are exactly the superhigh r.e. degrees.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-11-01T02:03:07Z
Xuanheng Zhao
arXiv categories: math.LO

Every K-degree has an upper bound of effective Hausdorff dimension one and Kurtz random sequences are cofinal in the K-degrees.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-11-01T04:52:22Z
Patrizio Cintioli
arXiv categories: math.LO

This paper shows that the pairwise intersection principle ($2\mathrm{IP}$) implies, over $\mathsf{RCA}_0$, the existence of a Cohen $1$-generic real relative to every given set. Together with the known implications, this yields the equivalence over $\mathsf{RCA}_0$ of the finite intersection principle (FIP), $2\mathrm{IP}$, and $1$-GEN. In fact, FIP is equivalent to $n\mathrm{IP}$ for every fixed $n\geq 2$. These results give affirmative answers to Questions~1 and~2 of Cholak, Downey, and Igusa, and to Question~9.10.26 of Dzhafarov and Mummert. The proof uses cumulative, nested supports satisfying a finite Helly property and a decoding argument based on a least selected label. Neither $\Sigma^0_2$ induction nor $\Sigma^0_2$ bounding is required.

arXiv abstract · PDF

Computability and Reverse Mathematics · primary corpus · published 2026-11-01T04:57:32Z
Patrizio Cintioli
arXiv categories: math.LO

This paper shows that the problem of producing a Cohen $1$-generic real relative to a given oracle is not Weihrauch reducible to the finite intersection principle (FIP). More strongly, no nontrivial computable FIP instance admits a single Turing functional that produces an absolute $1$-generic real from every enumeration of every maximal centered set of indices. The argument combines a $1$-generic real that computes no perfect tree all of whose paths are $1$-generic with local constancy and a parametrization of maximal centered sets. This answers Question~9.10.25 of Dzhafarov and Mummert.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-10-29T01:41:18Z
S. Mahmoud Mousawi, Sandra Zilles
arXiv categories: cs.LO, cs.FL, cs.LG

Relational pattern languages generalize Angluin's pattern languages by requiring the strings substituted for repeated occurrences of a variable to stand in a given relation, rather than to be identical. We study erasing pattern languages under the equal-length relation, where all occurrences of a variable must be replaced by strings of the same length. Over alphabets with at least three letters, this class is known to be learnable in the limit from positive data. We show that over a binary alphabet it is not, which resolves an open question from earlier work. Our proof reveals that non-learnability already holds for the restricted subclass of languages generated by patterns that have exactly three maximal substrings of variables. We then show that patterns with at most two maximal substrings of variables are learnable in the limit from positive data for every alphabet of size at least two. If the target pattern is known to have at most one maximal substring of variables, this can even be achieved by an iterative learner, which updates its hypothesis using only the current example and its previous hypothesis.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-10-29T10:06:07Z
Kirill Osipov
arXiv categories: cs.LO, math.LO

We study finite-terminating, address-only step recursion on the nonnegative reals, from zero, unit successor and projections. For reduced positive rational strides $s=a/q$ and $t=b/v$, we prove $\mathcal{C}s\subseteq\mathcal{C}t$ if and only if $q$ divides $v$, for both the bounded and unbounded algebras $\mathcal{C}\in{\mathcal{B},\mathcal{U}}$. The bounded compiler preserves earlier global majorants on every auxiliary input. Mixed rational stride sets are classified by least common denominators and supernatural denominators. Primitive-recursive translated-coordinate grid codes characterize the unbounded algebras and yield $\mathcal{U}{1/q}\cap\mathcal{U}{1/v}=\mathcal{U}{1/\gcd(q,v)}$. For bounded intersections, we prove an exact reduction: all corresponding identities hold if and only if the single identity $\mathcal{B}{1/2}\cap\mathcal{B}_{1/3}=\mathcal{B}_1$ holds, equivalently if the Boolean parts of the integer successor and addition algebras under scalar bounded recursion coincide. A Boolean reconstruction reduces general functions to predicates; a clipped fine-grid simulation with a frozen global resource bound identifies the union of predicate precision classes with the addition level. These reductions do not decide the resulting predicate equality, so literal bounded intersections remain unresolved. We also prove that unbounded-program equality is $\Pi^0_1$-complete and extensional bounded-algebra membership is $\Sigma^0_2$-complete. The model has no free real arithmetic or Zeno limits; semantic majorant validity is distinguished from syntax transformation.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-10-29T10:23:38Z
Kirill Osipov
arXiv categories: cs.LO, math.LO

For a strictly increasing $G:\mathbb{N}\to\mathbb{N}$ with $G(0)\geq 1$, we study minimal-basis function algebras generated by recursion along generalized inverses of its iterates. Bounded recursion requires an earlier pointwise majorant; unbounded recursion has no such requirement. If the orbit $G^{[t]}(0)$ has no polynomial upper bound, we obtain exact fixed-function membership spectra, reverse-divisibility inclusion, and indexed intersections that need not be single-stride algebras. Every finite divisibility-downset is realized in both regimes, and mixed strides admit fixed functions expressing any finite monotone Boolean condition on their additive stride monoid. For every generator, the realized bounded spectra form a bounded meet-semilattice: a construction sharing a bounding input coordinate realizes finite intersections without an unrestricted selector. Polynomial orbit growth is equivalent to definability of each of ordinary predecessor, unary doubling, and addition in any fixed unbounded stride algebra. In this case the algebra is ordinary primitive recursion relative to its inverse map, giving full collapse for primitive-recursive $G$. Ordinary predecessor belongs to a bounded stride algebra exactly when the orbit is polynomially bounded and $G$ has bounded successive differences; equivalently, ordinary bounded recursion embeds. A locality obstruction explains the additional bounded requirement, and two primitive-recursive generators with quadratic orbits have opposite bounded collapse behavior.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-10-29T13:33:23Z
Olivier Bournez
arXiv categories: cs.CC, cs.LO, math.DS

We construct, for each deterministic Turing machine that halts on all inputs, one polynomial vector field with rational coefficients that performs the same logical computation at unit Euler step, at every smaller or variable step in $(0,1]$ with divergent sum, and along the flow. This unifies discrete-time and continuous-time computation by polynomial dynamics, which earlier characterizations treated separately. For a machine making $T$ transitions in space $H$, a logical scale $h=2^{-s}$ with $s=O(H)$ suffices, with physical time $O(s(T+s))$, drift disturbances up to $h^{2K}$ for a fixed exponent $K$, and $2Ks+3$ fractional bits at unit step. On a fixed compact domain, polynomial time and robust eventual decision characterize P and PSPACE, respectively, with polynomial scale thresholds and no supplied stabilization horizon in the space case. Without sign, floor or conditional primitives, margin amplification at bounded speed, overlapping polynomial gates and interval-product estimates give the common realization, from which we derive shared logical traces, fixed-field PSPACE-complete prediction and a robust safety family with polynomial certificates common to all Euler steps and the flow.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-10-30T03:03:24Z
Noah Bertram, Daniel Luckhardt, Alexandra Silva
arXiv categories: cs.FL, cs.LO

Weighted automata learning has been well-studied over (semi)rings which have a dimension theory. In this work, we investigate active learning for weighted automata over semirings that lack such a structure. We first show that the principal ideal domain variant of the L* algorithm also terminates for a larger class of semirings containing Noetherian semirings, commutative rings, and bounded distributed lattices. We then present a variant of this algorithm for learning deterministic weighted automata, and prove that this algorithm terminates for commutative semirings.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-10-30T07:19:13Z
T. Yokoyama
arXiv categories: cs.FL, cs.LO

A reversible Turing machine (RTM) is a Turing machine in which every instantaneous description has at most one predecessor. Writing URTM(m,n) for a universal RTM with m states and n symbols, we construct URTM(3,600), URTM(4,41), URTM(5,37), URTM(6,30), URTM(7,28), URTM(8,21), and URTM(85,2); each of them has fewer states or fewer symbols than each of the nine URTMs in Morita's book (2017). They come from improved versions of Morita's conversions to three states, to four states, and to two symbols; for example, the improved conversion to three states uses O(mn^2) symbols instead of O(m^2n^3). We also show that the halting problem of RTMs with at most two states is decidable for finite instantaneous descriptions, so that no RTM with at most two states is universal under any notion of universality that reduces the halting problem of Turing machines to it by a computable encoding into finite instantaneous descriptions; in particular, there is no URTM with at most two states in our formalization of Morita's definition. We also show that no three-state, two-symbol RTM is universal in that formalization.

arXiv abstract · PDF

Models of Computation and Learning Theory · primary corpus · published 2026-11-01T12:14:41Z
Damian Arellanes
arXiv categories: cs.LO

Boolean circuits abstract away from physical implementation details to capture the logical structure and computational behaviour of digital components. Despite their long history of study, their compositional foundations have received comparatively little attention. Building on the theoretical foundations of computons introduced in previous work, we develop a concrete and operationally defined model of computation for control-driven Boolean circuits. We introduce colimit-based operators for composing circuits into sequential, parallel, branching and iterative structures, supported by concrete operational semantics grounded in particular abstract computing devices. The framework refines the semantics of composition, establishes the algebraic properties of its operators and introduces atomic circuits to support more expressive computation units. We demonstrate the applicability of the proposed framework through examples from propositional logic, biomedicine and electronics, and establish an operational equivalence with respect to classical Boolean circuits through a systematic transformation that accommodates gates of arbitrary arity. By this equivalence, we show that control-driven Boolean circuits are at least as powerful as their classical counterpart. That is, they are capable of non-uniformly computing any Boolean function over inputs of arbitrary length. Implementations in Idris and Java demonstrate the practical realisability of the framework.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-26T18:53:17Z
Hoang-Loc Cao, Truong Thanh Hung Nguyen, Phuc Truong Loc Nguyen, Vo Thanh Khang Nguyen, Phuc Ho, Hung Nguyen, Duc Pham, Long Tran-Thanh, Hung Cao
arXiv categories: cs.MA, cs.AI, cs.LO

In multi-agent debates, matching reports can arise for two different reasons: agents may repeat the same evidence (replication), or they may provide separate evidential roots that support the same claim (corroboration). A judge must distinguish these two cases. Counting report occurrences gives extra weight to relays, paraphrases, alias resubmissions, and excerpt splits, while merging all matching content avoids this only by also removing genuine corroboration. We formalize this tension as a minimal judgment game in which acquiring new evidence is costly, but replication is cheap. We show that root replication invariance (RRI) is exactly threshold-uniform replication immunity. Under RRI, replication-only deviations cannot change the verdict, and positive-cost replication is strictly dominated, whereas occurrence-sensitive and content-keyed judges admit profitable deviations. We also establish an information boundary: if a judge's observation interface cannot distinguish a replica from a matched fresh root, no judge can both ignore the replica and respond strictly to the fresh root. To preserve this distinction, we introduce the lineage quotient, which removes wording, identity, occurrence multiplicity, and arbitrary root names while keeping distinct roots separate. On orbit-connected domains, it is the coarsest representation sufficient for every deterministic judge invariant to replication and root-label renaming. We further lift this construction to quantitative bipolar argumentation frameworks (QBAFs), characterize strict fresh-root response, prove its propagation along sign-consistent paths under DF-QuAD, and derive a tight closed-form response modulus. Exhaustive audits over 28,224 direct-star profiles, 2,052 multi-layer DAGs, with matched interventions on 277 AVeriTeC-derived profiles, show the predicted separation between replication and corroboration under a supplied partition.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-26T21:11:48Z
Ritika Poddar, Aidan Fennelly, Deirdre Murphy, Eric Wolos, Corre L. Steele, Michael Doyle
arXiv categories: cs.CR, cs.AI, cs.LG, cs.PL

Large Language Models (LLM) are increasingly applied to Reverse Engineering (RE) workflows. RE, however, differs from common LLM coding tasks as it requires models to reason about low-level program behavior. Furthermore, the deployment of tooling in resource-constrained sandboxed RE environments limits the ability to use frontier-scale solutions. We examine whether a targeted LLM training approach can transfer distinct RE skills to open models via inverse basic-block execution: given an x86-64 basic block and a desired output register state, the model predicts the input register values that produce it. Fine-tuning \texttt{Qwen3-1.7B} and \texttt{Nemotron-3-Nano} with Group Relative Policy Optimization (GRPO) raises knowable-register prediction accuracy from 73.2\% to 85.3\% and from 63.3\% to 95.2\%, respectively. Frontier models still score highest (up to 99.2\%), but our fine-tuned \texttt{Nemotron-3-Nano} comes within four points at a fraction of the parameter count. We release both fine-tuned models and the training dataset.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-27T07:59:05Z
Yong Wang, Zhiyan Wang, Hexiao Kang
arXiv categories: cs.LO, cs.AI

On the theoretic analyses on transforms, they mainly focus on the computability analysis, such the Turing-completeness of unbounded precision transformers, the advantage of parallelizability of unbounded precision transformers and the limitations of bounded precision transformers. This paper give transformers an algebra for reasoning, which relies heavily on the functional decomposition results of transformers. This algebra uses functional decompositions as atomic actions, includes sequential composition and parallel composition, recursion for feedback and abstraction for hidden layers. As we know, it is the first attempt to model transformers logically and can be used to verify the correctness of transformer based applications.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-28T05:04:04Z
Dimitrios Myrisiotis
arXiv categories: cs.CC, cs.LG, cs.LO

A depth lower bound for ReLU networks asserts that every sufficiently shallow network fails on some input. What does a proof of such a bound compute? We study this question for exact computation of the maximum of $n$ real inputs, with depth measured by the number of hidden layers. For every separately fixed prime $q$ and depth bound $K$, we give a uniform $\mathsf{TC}^0$ refuter for rational networks with at most $K$ hidden layers and more than $q^K$ inputs, provided that the reduced denominators of their nonbias weights are not divisible by $q$. Biases may be arbitrary rationals. The refuter finds a rational input on which the network fails, and its correctness is provable in $\mathbf{VTC}^0$, the bounded-arithmetic theory of uniform constant-depth threshold computation. The underlying numerical depth lower bound follows from Averkov, Hojny and Merkert (ICLR 2025), extending Haase, Hertrich and Loho (ICLR 2023); our contribution is an internal proof that makes its geometric argument into a feasible refuter. On the construction side, $\mathbf{VTC}^0$ verifies locally checkable certificates for the balanced integer-weight maximum network of depth $\lceil\log_2 n\rceil$. At $q=2$, the construction and refuter meet: for each fixed $K$, the theory verifies that integer-nonbias-weight networks with arbitrary rational biases can compute the maximum with at most $K$ hidden layers exactly when $n\le 2^K$. We also give certified rational constructions of polynomial encoding length and depth $O(\log n/\log\log n)$. These results instantiate a witnessing duality: bounded proofs of certified existence and of refutation correspond, respectively, to threshold-computable constructors and refuters whose guarantees the theory proves.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-29T00:47:03Z
Michael Benedikt, Chia-Hsuan Lu, Alex Perry, Tony Tan
arXiv categories: cs.LO, math.LO

We look at a two-variable logic over finite graphs that allows Presburger quantifiers: linear arithmetic inequalities between the number of elements that satisfy subformulas. The prior literature shows that closing two-variable logic under Presburger quantification leads to undecidability, while closing under \emph{local quantification} -- the counts are always over neighbors of a given node -- preserves decidability. Here we show decidability of satisfiability for an intermediate logic that allows both local counts and global counts, but where the linear constraints do not mix the two. The proof requires a significant extension of the prior machinery developed for two-variable logic with counting. As a corollary we obtain decidability of satisfiability for an important family of Graph Neural Networks (GNNs). GNNs are a popular graph learning formalism. For example, in a variation of GNNs considered in the past literature, local aggregation is used in each layer to create modified values at each vertex of a graph, and then global aggregation is used in a final layer to obtain a single numerical value for the graph as a whole. Our logic is motivated by the fact that mixing of local counting and global aggregation in GNNs has been shown to lead to undecidability. Our results here show that if global and local aggregation are separated, one regains decidability. Decidability of other static analysis problems, like equivalence of GNNs, follows from the decidability of satisfiability.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-29T10:00:08Z
Marco Giunti, Fabrizia Giulia Garavaglia
arXiv categories: cs.AI, cs.CL, cs.LO

We develop a formal semantics for a general class of coordinated systems of parameterized transformations, taking the Transformer as a paradigmatic starting point but abstracting from its particular mathematical instantiation. Representational vectors receive both extensional reference and ordered intensional interpretations, while parameter structures acquire relative, second-level interpretations that determine how argument properties are preserved, replaced, or combined. This yields the notion of a transforming concept: a parameterized transformation whose numerical action is coordinated with a corresponding property-level map. We then distinguish the common algebraic-semantic core of these systems from their architecture-specific functional organization, allowing different mathematical instantiations and mechanical realizations of the same abstract system type. The framework is applied to attention heads and residual connections, providing semantic explanations that depend only on the shared algebraic-semantic core and their local functional organization and therefore generalize beyond the standard Transformer. These analyses also reveal the modularity of the framework: complex architectures can be decomposed into simpler semantically coordinated subsystems whose organization may recur across different abstract system types.

arXiv abstract · PDF

Neural Networks and Formal Semantics · primary corpus · published 2026-10-31T17:32:57Z
Sandro Preto, Marcelo Finger
arXiv categories: cs.LO

A logical twin of a neural network is a logical representation that mimics the computation of the network through logical formulas. We revisit two earlier proposals for constructing logical twins of feedforward neural networks in {\L}ukasiewicz logic, both of which are susceptible to exponential blow-up in running time and representation size. Building on ideas from both approaches, we present a new construction that directly yields logical twins in {\L}ukasiewicz logic. We show that this construction can be computed in polynomial time and produces polynomial-size logical twins. Finally, we report an empirical evaluation of the three methods, showing that the new proposal substantially outperforms the other two.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-27T05:40:52Z
E.G Plante III, Eric Paul, Cosmo Viola, G.A. Kavvos, Talia Ringer
arXiv categories: cs.PL

Maintaining formal proofs in response to breaking changes in their dependencies is a major challenge of proof engineering. Proof repair is a kind of proof automation that lessens the burden of this challenge by automatically adapting proofs in response to those changes. While proof repair is well understood through an algorithmic lens, it has, until now, been poorly understood through a theoretical lens. We address this gap by giving the first foundational treatment of proof repair, focusing in particular on type-theoretic proof repair in response to changes in datatypes. Our key insight is that the core component of a proof repair algorithm---a ``configuration''---is exactly an algebra isomorphism. We formalize and prove this insight, answering open questions from prior work. We then take this one step further and show that, by taking the dual of this representation, we obtain proof repair over coinductive types. All of our results are formalized in Agda.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-27T07:59:35Z
Jinhao Tan, Jam Kabeer Ali Khan, Bruno C. d. S. Oliveira
arXiv categories: cs.PL

First-class environments expose runtime environments as ordinary values and support a substitution-free, environment-based operational semantics. They also support applications such as first-class modules, dynamic composition of environment fragments, and sandboxing via local environments. Existing environment-based calculi, however, are mostly studied in a simply typed setting and stop short of System F and polymorphism. We present $F_E$, a polymorphic calculus with first-class environments that conservatively extends System F with a small-step environment semantics. $F_E$ eliminates all forms of substitution in System F. Term and type abstractions evaluate to closures, boxes run code under local environments, and box types expose the local typing assumptions of both. Manifest types, together with a two-sided type equivalence, play a dual role: they model type-level instantiation, and enable transparent type components in environments and modules. We prove type soundness, normalization, decidability, and standard properties of type equivalence, and conservativity over System F. The metatheory of $F_E$ is based on instantiation lemmas rather than substitution lemmas. This foundation supports polymorphic first-class modules with dynamic composition and sandboxing. We study $F_E$ in two forms. Our main presentation is an explicit, type-passing calculus that follows conventional System F. We also develop an implicitly-typed variant aligned with the semantics of polymorphic functional languages. All metatheory is mechanized in the Rocq theorem prover.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-27T12:06:50Z
Takuma Imamura
arXiv categories: math.LO, cs.LO

We study algebras for the $\mathbf{BM}$-, $\mathbf{BI}$-, and $\mathbf{BMI}$-fragments of combinatory logic, where $\mathbf{B} xyz \to_{w} x\left(yz\right)$, $\mathbf{M} x \to_{w} xx$ and $\mathbf{I} x \to_{w} x$. We prove that every finite $\mathbf{BM}$-algebra $\mathcal{A}$ contains an element $Y$ satisfying $Yx = x\left(Yx\right)$ for all $x\in A$. Moreover, a single closed $\mathbf{BM}$-term represents such an element in every finite $\mathbf{BM}$-algebra. On the other hand, we show that there exists an infinite $\mathbf{BMI}$-algebra with no such element. Consequently, the variety of $\mathbf{BM}$-algebras is not generated by finite $\mathbf{BM}$-algebras. We also characterise finite $\mathbf{BI}$-algebras as finite semigroups with two distinguished left units $B$ and $I$, and finite $\mathbf{BMI}$-algebras as finite idempotent semigroups with three distinguished left units $B$, $M$ and $I$.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-27T16:22:03Z
Sewon Park
arXiv categories: cs.LO

Diaconescu's theorem derives excluded middle from the axiom of choice, using propositional extensionality. We show that in dependent type theory without propositional extensionality, global choice alone does not imply excluded middle. We consider extensional Martin-L\"of type theory with an impredicative universe of propositions included in the universe of types, extended with a global choice operator. We construct a consistent model of this type theory and show that the model refutes excluded middle and propositional extensionality. The model is built from staged sets, sets whose elements appear at stages of a well-order. It further validates proof irrelevance, inductive families, quotients with soundness, and a cumulative hierarchy of universes, which together cover a large fragment of the type theory of the proof assistant Lean. Even together with these features, global choice does not imply excluded middle.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-29T08:35:34Z
El Mehdi Cherradi
arXiv categories: math.CT

We study the category $\mathbf{Dep_{aff}}$ of finite posets and opfibrations between them, and prove that it is a perfect operator category in the sense of Barwick. Based on its additional properties, we propose a definition for a dependent operator category, and formulate a notion of dependent affine operad in a fibered way. In the particular case of $\mathbf{Dep_{aff}}$, we investigate the basic theory of such operads, establishing that the category of algebras for an operad is monadic over a canonical presheaf topos of "dependent sets". We finally extend this theory to a setting where we allow variable duplication, which we refer to as general dependent operads.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-29T14:35:51Z
Pablo Barenbaum, Delia Kesner, Mariana Milicich
arXiv categories: cs.LO

In this work, we present the first semantic interpretation of useful call-by-value evaluation through a non-idempotent intersection type system called U. One first contribution of this paper is a characterisation of termination of useful call-by-value evaluation via U-typability. That is, a term is typable in system U if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system U provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of useful evaluation is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy. Our third contribution is a termination-equivalence result between standard call-by-value, which may perform erasing reductions, and useful call-by-value, which is non-erasing. To establish this result, we introduce a non-erasing restriction of standard call-by-value, a refinement that serves as an intermediate calculus bridging standard and useful call-by-value. We show that all three calculi have the same termination behaviour, and hence induce the same observational equivalence.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-30T15:52:06Z
Theadora Fields Collin, Gilbert Bernstein, Oded Stein, Saman Amarasinghe
arXiv categories: cs.PL, cs.MS

Scientists, engineers, and mathematicians often formulate algorithms using coordinate-independent linear algebra because its tools are composable and harder to misuse. For numerical processing, however, users must translate these ideas into coordinate-dependent array code. Most practitioners do so prematurely because tools such as NumPy lack coordinate-independent representations, while existing languages with such constructs do not model enough linear algebra for the situations where they matter. We propose Grassmann, a small language bridging coordinate-independent linear algebra and coordinate-dependent implementations. It uses dependent types, linear types, and partially (pseudo-)invertible computation to model situations arising in exterior algebra and differential geometry. It targets the linear algebra at a point on a manifold, a prerequisite for many specifications in scientific computing and computer graphics. A language for coordinates lets users move between these representations. We give a denotational semantics assigning meaning without coordinates and an operational semantics translating Grassmann to array code under a choice of coordinates. Our main metatheoretic result shows that operational evaluations agree with the denotational semantics under an arbitrary choice of coordinates. This models how practitioners translate linear algebra for computers and suggests an approach to algorithmic optimization at a high level of abstraction. Our optimized implementation generates code for exterior algebra operations with overheads no more than 10%.

arXiv abstract · PDF

Type Theory and Lambda Calculi · primary corpus · published 2026-10-30T16:00:25Z
Martin E. Bidlingmaier
arXiv categories: cs.LO, math.CT

We extend dependent type theory by type classifiers and construct an interpretation in the category of contextual categories with families. Type classifiers extend contexts by type variables, complementing the usual context extensions by term variables of specified types. This allows statements with arbitrary type parameters to be formulated without assuming a universe. We show that substituting isomorphic types induces isomorphisms between the resulting types even in extensional type theory, giving an analogue of the invariance supplied by the univalence axiom in homotopy type theory. Omitting function types from the theory, so that all type formers are covariant, extends this naturality to arbitrary, possibly noninvertible maps.

arXiv abstract · PDF

Termination and Term Rewriting · primary corpus · published 2026-10-26T14:41:52Z
Rongkang Li, Jiaxin Hu, Taolue Chen, Yong Li, Fu Song, Zhilin Wu
arXiv categories: cs.SE, cs.AI, cs.LO

Ranking functions are a fundamental technique for proving loop termination, but constructing them manually is challenging and requires substantial expertise. We propose RAINFALL, a neuro-symbolic framework which follows the generate-verify-refine paradigm and tightly integrates LLMs with symbolic verification. RAINFALL formulates ranking function synthesis as a code-completion task by inserting placeholders into the input program and constraining the LLM to fill four predefined slots for each loop. The completed program is then checked by a symbolic verifier. If verification succeeds, a valid ranking function is obtained; otherwise, the verifier's diagnostics are translated into natural-language feedback that guides iterative refinement of the LLM's output. We evaluate RAINFALL on two public benchmark suites comprising 358 terminating C programs. Using MiniMax V2.7, RAINFALL synthesizes verifiable ranking functions for 323 programs (90.22%), outperforming all promising baselines. In particular, it solves 12 more programs than PROTON 2.1, the best-performing baseline and winner of the SV-COMP 2026 Termination category. Furthermore, combining RAINFALL with PROTON 2.1 increases the success rate to 96.65% (346/358 programs). We also conduct ablation study confirming individual contributions of placeholder contracts, few-shot examples, symbolic verification, and diagnostic information feedback. Experiments across LLMs further confirm the effectiveness of RAINFALL. Our results suggest a generic, sound framework for ranking-function synthesis and, beyond termination, LLM-assisted synthesis of formally checkable liveness certificates, both of which represent new directions of software engineering research.

arXiv abstract · PDF

Termination and Term Rewriting · primary corpus · published 2026-10-28T10:08:51Z
Johannes Niederhauser, Aart Middeldorp
arXiv categories: cs.LO

Confluence is a fundamental property of computation which implies that the nondeterminism of a system does not affect its outcomes. A key concept of confluence research in rewriting theory is the notion of critical pairs which captures the potential local sources of non-confluence. In this paper, we lift the definition of higher-order critical pairs to a more expressive class of higher-order rewrite systems. Thereby, we facilitate confluence analysis of rewrite systems which can express complex one-step computations as well as program transformations from functional programming.

arXiv abstract · PDF

Termination and Term Rewriting · primary corpus · published 2026-10-29T07:36:07Z
Teppei Saito, Nao Hirokawa
arXiv categories: cs.LO

Monotonic semantic path orders (MSPOs) are powerful reduction orders, but their effective use in theorem proving and termination analysis raises three issues: efficient comparison of terms, ground totality, and a reduction-pair formulation. Inspired by weighted path orders (WPOs), we introduce generalized weighted path orders (GWPOs) which encompass both WPOs and MSPOs. GWPOs and MSPOs coincide as classes of reduction orders, thereby yielding efficient and ground-total subclasses of MSPOs. We further formulate the reduction-pair version of the GWPO for the dependency pair method, from which a reduction-pair version of the MSPO is obtained. In contrast to the reduction-order setting, the correspondence between GWPOs and MSPOs no longer fully carries over, establishing the GWPO as a framework of independent interest. Effectiveness of the resulting reduction pairs is assessed by standard termination benchmarks.

arXiv abstract · PDF

Termination and Term Rewriting · primary corpus · published 2026-10-29T16:22:50Z
Daria Goliasova, Toghrul Karimov
arXiv categories: cs.LO

Recently, Guilmant, Lefaucheux, Ouaknine, and Worrell [2] proved decidability of the termination problem for linear constraint loops over two real-valued variables, thus settling a wellknown open problem. Their algorithm is based on a theoretical result that such a loop does not terminate if and only if it has a witness of an infinite run of a specific shape. By analysing the structure of the witness carefully, we show that termination such loops can be decided in polynomial time, improving on the polynomial space bound argued by Guilmant et al. We also present an efficient implementation of the polynomial-time algorithm based on the satisfiability modulo theories (SMT) solver Z3.

arXiv abstract · PDF

Termination and Term Rewriting · primary corpus · published 2026-10-30T14:42:08Z
Bryan Ford
arXiv categories: math.LO, cs.LO, cs.PL

A grounded arithmetic counts a sentence as true only when a terminating process establishes it; a sentence no such process settles has no value. Such a logic can state that an event happens, but not that it never happens under unbounded choice. This paper extends such a logic so that it can. The base is Reflective Grounded Arithmetic (RGA) with Inductive Grounded Arithmetic (IGA)'s least-fixed-point reading and ground induction. It adds a separate greatest-fixed-point former $\nu$ with Park's coinduction rule, proves that one former cannot carry both ground induction and coinduction, and adds a dichotomy rule: the classical disjunction between a least-fixed-point atom and the greatest-fixed-point atom of its dual, under a derivable premise that the body's leaves are decided. The systems are sound for an explicit model reading every $\nu$-body at its greatest fixed point, hence consistent; they agree with the least model wherever it has a value and prove sentences it leaves without one. The dichotomy replaces the underivable hypothesis that an order is well-founded by the derivable one that its steps are decided; the change of model pays for the move. With ground induction the dichotomy derives the omniscience rule of the sibling arithmetic OGA, so the system has no semantics whose certificates for universals are its own proofs. The systems prove, as single sentences, that every decided tree is well-founded or has an infinite branch given by a term, total in the new model; that random assignment terminates while its divergent twin runs forever; that a fair loop terminates and the alternating-bit protocol delivers every message; that open games are determined; that the termination gap in Nakata and Uustalu's trace semantics closes; and that Cinderella wins the bucket game at capacity three. Isabelle/HOL checks every result.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-26T10:16:56Z
Rene Heinzl, Markus Nissl
arXiv categories: cs.CR, cs.AI, cs.LO

Host-based intrusion detectors order events, window audit streams and sequence attack stages by their timestamps. Every conclusion they draw therefore rests on assumptions about clocks, delivery, entity identity and the integrity of the evidence, and most of these assumptions go unstated. This Systematization of Knowledge (SoK) makes them explicit. Drawing on temporal databases, stream processing and runtime verification, we distill five components of a time model, together with a checklist of evidence assumptions and four levels of guarantee, and walk through a running campaign with them. A documented search yields fifteen families of detection and investigation. For papers selected by screening role and period, plus named systems and landmarks, we check the stated assumptions in the full texts, and we assess eleven temporal knowledge representation and reasoning (KRR) formalisms and a learned baseline on nine attack patterns. Some early alert correlators stated clock and delivery assumptions, and forensics measures clock error. Current provenance-based detectors state no clock bound. Four audited papers describe input-ordering conditions or conventions, but none specifies conditions for conclusion validity across a stated class of delivery failures. In the selected provenance-based systems, campaign composition uses system-specific procedures or objectives, learned state, causal graph queries or language models, and beyond CEP-based query systems, we found no temporal rule language or stream reasoner from KRR applied to host audit data. In 28 of 38 audited provenance-era detector papers, capture or stored evidence is trusted or its manipulation is placed out of scope, and none says which conclusions survive deleted, delayed or forged records. Five open challenges follow from these gaps.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-26T10:33:46Z
Valeria Fionda, Antonio Ielo, Francesco Ricca
arXiv categories: cs.LO, cs.AI

Linear Temporal Logic over Finite Traces (LTLf) is widely used in Artificial Intelligence to specify desired temporal behavior and determine whether finite traces satisfy or violate it. Explaining these outcomes is essential for debugging and trust. However, existing approaches typically capture either sufficient reasons or counterfactual causes, without clarifying their relationship. We introduce a native characterization of abductive (AXps) and contrastive (CXps) explanations directly over finite traces, based on locking and unlocking time-indexed events. We prove its equivalence to the classifier-based formulation, and show that CXps coincide with a recently proposed temporal causality semantics for LTLf. This characterization enables an efficient implementation based on the enumeration of minimal unsatisfiable cores and minimal correction sets of ASP programs. Experiments on real-world event logs demonstrate the effectiveness of the approach.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-27T16:53:25Z
Yigit Narter, Emily Zhao, Inigo Incer
arXiv categories: cs.LO, cs.SY, eess.SY

Assume-guarantee contracts provide a set of algebraic operations that enable the efficient compositional design and analysis of complex engineering systems. The explicit computation of these operations at component interfaces is currently supported only for some logics lacking a notion of time. This paper develops theory and algorithms to compute these operations when the contracts are expressed in the GR(1) modulo theory. The key challenge is the computation of two quantifier elimination problems for temporal formulas. We develop context-aided variable elimination procedures on GR(1)-modulo formulas, establish their soundness, characterize subproblem-wise optimal solutions within an admissible class of formulas, and use the procedures to compute contract operations, including composition and quotient. We implement the resulting framework in Pacti, automating compositional reasoning over GR(1) contracts. Finally, we demonstrate the framework on an automated emergency-braking case study, where we compute system-level contracts and expose compatibility conditions arising from the interaction of component specifications. Experiments on synthetic families show that the cost is governed by the number of eliminated variables and liveness conjuncts, and a comparison with exact automata-based elimination shows complementary scaling.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · cs.SE candidate · published 2026-10-27T17:59:30Z
Sebastian Pandolfi, Guzm\'an Llamb\'ias, Laura Gonz\'alez
arXiv categories: cs.SE

Transferring semantically typed tokens between heterogeneous blockchains (e.g. EVM and Cosmos ecosystems) raises two problems: semantic mixing, the loss of a token's domainspecific meaning in transit (e.g., CO2 removals issued under different methodologies), and atomicity despite divergent consensus and timing assumptions. We propose a bridge that addresses both. A deterministic indicator identity derived from cryptographic commitments, mirrored in class registries on both chains and checked at mint time, preventing semantic mixing by construction. For atomicity, we extend hash time-locked contracts (HTLCs) from two-party exchange to single-owner transfer with an automatic callback that burns the source escrow after a destination claim, and a protocol-minimum bounty that makes the fallback burn incentive-compatible even against adversarial senders. We machine-check the protocol's invariants with TLC (supply conservation fails without the rational-monitor assumption and holds with it) and validate a bidirectional prototype on Polygon and Neutron mainnets over Axelar GMP: fully automatic transfers with a median end-to-end latency of 97 s over 50 Polygon to Neutron transfers across 7 days (all completed by the on-chain automatic callback) and 93 s in the reverse direction, and semantic-validation overhead below 0.4% of messaging cost. We also document the integration failure modes of Cosmos originated messaging, whose dominant operational risk proves to be relay eligibility rather than latency.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-28T00:44:51Z
Aaron D. Ames, Joe Moeller, Massimiliano de Sa, Paulo Tabuada
arXiv categories: math.CT, cs.SY, eess.SY, math.OC

Layered control architectures provide a powerful paradigm for synthesizing controllers for complex systems. Yet, translating guarantees at each layer to system-level guarantees is challenging due to the interactions between layers. To address this problem, this paper presents a categorical perspective on layered control architectures. Individual systems are represented as control coalgebras, their interactions are specified as morphisms to mediators, and system-level behaviors are obtained via composition defined categorically as a pullback. To analyze the safety of these systems, we formulate control barrier morphisms (CBMs), the categorical generalization of control barrier functions. We prove that feedback controllers satisfying a CBM condition render the associated safe subobject forward invariant. It is through CBMs that we can establish the safety of layered systems: given a CBM at each layer subject to compatibility conditions, the universal property of the pullback implies the existence of a CBM for the composed system. Safety of a full-order model being safety filtered by a reduced-order model is recovered as a specialization of the categorical framework.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-29T10:26:15Z
\'Eric Goubault (X-DEP-INFO, LIX), Nuwan Herath Mudiyanselage (LIX), Sylvie Putot (LIX)
arXiv categories: cs.LO

Many problems in control can be expressed as quantified constraints, such as robust forward and backward reachability, synthesis of controllers, solutions to motion planning problems. In this paper, we develop a method for computing inner and outer approximations of global solutions to very general quantified constraints, generalizing widely the state of the art on similar problems, usually restricted to at most one alternation of quantifiers or to local solutions. By global solutions, we mean characterizing accurately the entire set of solutions, within some prescribed bounds. For this, our approach uses a set inversion technique relying on oracles for set inclusion using local solutions to related quantified reachability problems. We exemplify the approach throughout the paper on different examples related to control problems.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-29T13:40:33Z
Peter Dolog, Kim G. Larsen, Marius Miku\v{c}ionis, Frederik F. K. Rasmussen
arXiv categories: cs.SE, cs.AI, cs.LO

For more than three decades, UPPAAL has supported the modelling and analysis of real-time and cyber-physical systems. Yet building a suitable model, formalising the intended properties, choosing analysis techniques and interpreting counterexamples remain iterative tasks that demand substantial expertise. Large language models (LLMs) can offer plausible explanations and even solutions, but they are not necessarily correct. We present UPPAAI, an extension of UPPAAL in which users construct, explain, debug and specify models in dialogue with an LLM. The guiding principle is that the user requests, the LLM proposes, explains and orchestrates, and UPPAAL verifies. UPPAAI exposes the UPPAAL editor, queries and verifier through a Tools API. We report on seven case studies, from explaining to a newcomer to learning a controller, covering timed automata, stochastic hybrid automata and strategy learning. LLMs proved to be extremely helpful in not just generating solutions but also pro-actively suggesting relevant UPPAAL features it was not asked about.

arXiv abstract · PDF

Temporal Logic and Reactive Systems · primary corpus · published 2026-10-29T16:22:36Z
Rados{\l}aw Klimek
arXiv categories: cs.LO

Logic-based workflow patterns capture recurring behavioural structures together with reusable temporal specifications. Their composition raises distinct problems as workflow structures become richer, including instantiation, nesting, conditional execution, repeated occurrences, and traceability of generated formulae. This paper proposes a hierarchy of Pattern Composition ($\Pi C$) procedures, from $\Pi C_0$ to $\Pi C_4$, that organizes these requirements as progressively richer compositional capabilities. The hierarchy separates compositional complexity from the expressive power of the temporal-logic fragment, represented by $TL_j$, yielding a framework $\Pi C_i[TL_j]$ for developing logical workflow specifications. We develop activation-aware Pattern Composition ($\Pi C_2$), which distinguishes the structural presence of a nested pattern from its execution in a particular workflow context. We formalise its recursive procedure, analyse its properties, and define an evaluation protocol for conditional activation, conservativity under mandatory composition, and specification growth. The hierarchy also characterizes selective occurrence qualification for iterative patterns ($\Pi C_3$) and provenance for tracing generated formulae to their sources ($\Pi C_4$). Finally, we outline $\Pi C_{\mathrm{Assist}}$, an orthogonal mode in which AI proposes and refines pattern expressions subject to the hierarchy's compositional checks.

arXiv abstract · PDF

Probabilistic Program Verification · primary corpus · published 2026-10-26T12:12:22Z
Rapha\"el Faure, Alain Finkel, Lina Ye
arXiv categories: cs.LO, cs.FL

Decisiveness is central to reachability algorithms for infinite Markov chains, but is a qualitative notion: it guarantees that path-enumeration algorithms terminate, without an a priori bound on the horizon. We study decisiveness quantitatively of Markov chains, and apply our results to the approximate quantitative coverability problem for effective probabilistic well-structured transition systems (pWSTS). We introduce truncation sets, which represent the horizons sufficient to approximate the reachability probability within a precision $\varepsilon$. These sets reformulate decisiveness quantitatively, and their elements can be computed when it is decisive. To obtain such horizons, before any exploration, we introduce geometrically reachable sets, for which the probability of not reaching them within n steps decreases exponentially in n, up to a prefactor depending on the initial state. Horizons valid for all initial states exist iff this prefactor can be chosen uniformly for boundedly coarse chains. For such pWSTS, including probabilistic vector addition systems and Galton-Watson processes, we obtain a priori global horizons growing at most logarithmically in $1/\varepsilon$. In the non-uniform case, we give a drift condition ensuring the existence of a finite geometrically reachable set. Under this condition, we derive a priori horizons growing at most logarithmically in $1/\varepsilon$ and in the weight w(x) measuring the size of the initial state x. In both cases, we compute a horizon function whose evaluation on any initial state and precision requires only a constant number of elementary operations $(+, -, \times, / \text{ and } \log)$. For probabilistic lossy channel systems, this yields, to our knowledge, the first explicit a priori horizons from arbitrary initial states, and it extends to $\nu$-pLCS, a new infinitely branching variant with probabilistic emissions.

arXiv abstract · PDF

Probabilistic Program Verification · primary corpus · published 2026-10-27T05:18:33Z
Arthur Gall, Ichiro Hasuo, Thomas Seiller
arXiv categories: cs.LG, cs.LO

Optimizing expected rewards and reachability probabilities in parametric Markov chains (pMCs) is central to the analysis and synthesis of probabilistic systems with loops. While traditional symbolic synthesis approaches--such as parameter lifting and rational function generation--suffer from scalability bottlenecks, gradient-based optimization emerges as an effective alternative. However, existing gradient-based techniques still rely on symbolic gradient computation--such as solving large linear systems--over the global state space, inheriting scalability limits. Finite-horizon approximation is possible but introduces uncontrollable bias. In this paper, we introduce a scalable Monte Carlo gradient estimator based on a measure-theoretic generalization of the log-derivative trick. We prove that our estimator provides unbiased gradient estimates under almost-sure termination and standard regularity conditions. Crucially, our method avoids global state-space materialization and linear system solving entirely: it operates purely along sampled trajectories, requiring only black-box evaluations of local transition probabilities (or densities) and their derivatives. Unlike existing pMC techniques that are fundamentally restricted to finite discrete systems, our measure-theoretic framework naturally extends to continuous and general $\sigma$-finite state spaces. Empirical evaluations on synthetic discrete pMCs and continuous-state case studies demonstrate that our method scales to state spaces far beyond the reach of existing solvers, significantly reducing execution time without introducing bias.

arXiv abstract · PDF

Probabilistic Program Verification · cs.SE candidate · published 2026-10-27T22:50:48Z
Asher Tempest Arya, Rajan Maghera, Nicholas Wu Jiang, Federico Mora, Aren A. Babikian, Marsha Chechik
arXiv categories: cs.SE

Self-adaptive systems are designed to accommodate variants of their environment, which form a family of instances whose uncertainty is captured by probabilistic models, and must meet probabilistic requirements on each instance. Within such a family, changes in size and structure complicate the fundamental adaptation decision: whether to retain, reuse, or construct a new controller, since controllers are often synthesized for and specific to an instance. Large language models (LLMs) have recently been used to write reusable controllers, but existing approaches largely target deterministic domains, and probabilistic model checking of their output remains limited to preliminary single-instance studies. In this paper, we propose a verifier-guided framework for controller reuse with explicit support for families of environments. The framework introduces a novel combination of LLM-written controllers with probabilistic model checking to provide per-instance guarantees for probabilistic requirements. We evaluate our approach using three LLMs on three benchmarks, assessing its effectiveness and cost with respect to baseline implementations, the distribution of adaptation decisions, and the impact of individual framework components. On grid worlds, LLM-written rule lists are verified on about 90% of held-out instances, against at most 77% for the baselines, and verifying a stored rule list is 15 to 103 times faster than per-instance synthesis. Reuse serves most episodes at a small fraction of the cost of generation or per-instance synthesis, and model-checking feedback increases verified coverage over independent restarts.

arXiv abstract · PDF

Probabilistic Program Verification · primary corpus · published 2026-10-29T09:52:36Z
Sebastian K\"orner, Oliver Emil B{\o}ving, Christoph Matheja
arXiv categories: cs.PL, cs.LO

Weighted programming is a framework by Batz et al. for describing mathematical models or optimization problems as imperative programs parametrized over semirings and then analyzing them with program verification techniques like weakest precondition calculi. Applications include reasoning about expected outcomes of probabilistic programs and competitive analysis of online algorithms. We extend weighted programming with (1) countable nondeterminism and (2) user-defined additive rewards, where programs are parametrized over modules instead of semirings. The resulting framework enables reasoning about expected resource consumption of probabilistic programs and about optimal scores of combinatorial games. A technical challenge is that wp-calculi for weighted programs with (1) and (2) over arbitrary modules can be unsound, because it is well-known that continuity properties commonly used in program semantics break in the presence of countable nondeterminism. We study conditions under which a wp-style transformer for reasoning about weighted programs is sound with respect to an operational ground truth defined in terms of weighted decision processes (WDPs) - transition systems that generalize Markov decision processes by drawing transition weights and state rewards from a module. Based on those conditions, we show that a range of concrete instances of the weighted programming framework enjoy sound weakest precondition reasoning. We demonstrate the usefulness of our wp-semantics through case studies for different modules. We mechanized our extended weighted programming framework and our main soundness results in the interactive theorem prover Lean. Instantiating these results for probabilistic programming yields, to the best of our knowledge, the first mechanized proof of a fixed point characterization of minimal expected rewards in Markov decision processes with countable nondeterminism.

arXiv abstract · PDF

Probabilistic Program Verification · primary corpus · published 2026-10-31T18:41:17Z
Jack Stanek, Adithya Murali
arXiv categories: cs.PL

What does my data look like? We study the problem of representing and learning summaries of datasets that account for both their structural and statistical properties. This problem is widely useful across many application domains that involve large datasets and analysis/modeling of data, and is of particular interest to Programming Languages. In particular, in this work we focus on the problem of learning these "stochastic summaries" for tree-like data composed of inductive datatypes and argue that probabilistic programs over inductive datatypes can effectively represent the desired summaries. We present Tali, a Probabilistic Programming Language over inductive datatypes, and study the problem of learning such programs from data samples. We identify a semantic property, called Observation-Bounded Compilability, which identifies a set of recursive probabilistic programs which admit exact inference, and can represent many useful and complex probabilistic structures. We then propose an algorithm for learning Tali programs satisfying the OBC property from observations using a combination of program synthesis (stochastic search) and maximum likelihood inference. We implement our learning framework, evaluate it on a diverse benchmark suite, and record our observations on the merits of our approach. We demonstrate the utility of learning stochastic summaries as symbolically-represented priors for downstream learning tasks. We also showcase another utility by using our technique to learn operational profiles of real-world datasets.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · primary corpus · published 2026-10-27T01:57:08Z
Zexin Li, Weibo Zhang, Linyi Li, Arvind Easwaran, Simin Chen
arXiv categories: cs.SE, cs.AI, cs.PL

We present \tool, a query-efficient framework for black-box probabilistic verification. Given a fixed, sampleable input distribution and a binary property oracle, \tool assesses the property's violation probability $p$ against a threshold $\theta$. Under independent sampling and stateless oracle behavior, acceptance asserts $p\le\theta$, rejection asserts $p>\theta+\eta$ for a user-specified separation margin, and an inconclusive verdict indicates insufficient evidence for either conclusion. The probability of each type of erroneous verdict is bounded by its specified error budget. To support this three-valued contract efficiently, \tool uses a single sequential test, eliminating the interval family required by the baseline. The test accounts for repeated sampling checks through either corrected exact binomial confidence intervals or an anytime-valid confidence sequence. We apply \tool to probabilistic local model semantic consistency, where the property oracle detects decision-level inconsistencies between reference and compiled executions under a specified perturbation distribution. Our evaluation covers 24 tasks across TorchInductor and TensorRT and examines sampling efficiency, conclusiveness, and diagnostic behavior. For sampling efficiency, we use paired one-model clean-label radius searches: the baseline requires 3.6-4.2 times as many unique samples under matched numerical parameters while providing a weaker decision contract. For model semantic consistency, checks at $\theta=10^{-3}$ yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections across 840 input--backend instances from 21 tasks. Case studies of two documented compiler faults further demonstrate what these local verdicts can diagnose.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · primary corpus · published 2026-10-27T10:50:14Z
Marco Campion, Isabella Mastroeni, Michele Pasqua, Caterina Urban
arXiv categories: cs.PL

We introduce Abstract Lipschitz Continuity (ALC), an extensional property of functions, in particular of program semantics, requiring that bounded differences between properties of two inputs yield proportionally bounded differences between properties of the corresponding outputs. ALC explicitly discerns between two complementary forms of approximation: property-based (or qualitative) approximations, which retain a property of the data and are formalized by upper closure operators as in abstract interpretation, and quantitative approximations, which measure the closeness of data and are formalized by pre-metrics, a weakening of metrics that covers the distances arising in program analysis. Keeping the two forms of approximation explicit has two main benefits. First, it allows us to precisely relate ALC to established extensional properties: ALC is a sufficient condition for partial completeness in abstract interpretation, for partial abstract non-interference in language-based security and, with a null Lipschitz constant, for abstract robustness in machine learning. Second, it supports reasoning about ALC of program semantics by induction on the syntax of programs: we present a sound deductive system, parametric in the property-based approximations and in the pre-metric of interest, that reduces a proof of ALC for a program to proofs for its basic commands and to some explicit side conditions, which isolate what makes ALC compositional across sequential composition, non-deterministic choice and iteration.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · cs.SE candidate · published 2026-10-28T01:07:37Z
Erfan Arvan, Michael D. Ernst, Martin Kellogg
arXiv categories: cs.SE

A dynamic invariant detector proposes invariants, such as method pre- and postconditions, and rules out those that do not hold at run time. Traditional detectors propose invariants from a fixed library of templates, which limits their expressiveness. A large language model (LLM) can propose invariants instead of, or in addition to, template-derived ones. With the right prompt and context choices, we found that this idea can both improve the invariants' expressiveness and reduce the cost of inferring the invariants. Greater expressiveness brings complications: an LLM-proposed invariant can execute arbitrary code during invariant evaluation, causing side effects or infinite loops. Our novel instrumentation strategies mitigate these problems. We wrap each candidate and evaluate only one invariant per thread at a time, so nested invariant evaluations cannot trigger one another indefinitely. To recover from non-nested hangs, we monitor each run for stalls and retry it under a growing time budget. Because we cannot prove a candidate side-effect-free in advance, we use delta debugging over the invariants evaluated during a failing test to isolate and disable a side-effecting candidate without discarding the rest of the run. We compared our implementation, Oca, to the popular template-based Daikon invariant detector on real open-source Java projects. Oca produces more expressive invariants: on average, 28% of its held invariants call a project-specific method, which Daikon's templates cannot express. Its invariants are more often valid, with a false-positive rate of 18% in a manual inspection, vs. 76% for Daikon, and more useful: as properties for property-based testing, they exposed 9 of 25 real bugs, compared with 4 for Daikon. Oca also costs less, using 566 minutes and 27 GB of disk, compared with 2,817 minutes and 827 GB for Daikon.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · cs.SE candidate · published 2026-10-28T06:36:57Z
Simantika Bhattacharjee Dristi, Matthew B. Dwyer
arXiv categories: cs.SE

A range of software engineering tasks, such as optimization and refactoring, seek to preserve the behavior of software components and require methods to assess functional similarity. Research has explored formal approaches to prove functional equivalence and used machine learning methods to approximate it, but the former does not scale and does not quantify the extent of similarity and the latter struggles when subtle semantic differences are present. Differential fuzzing offers a scalable approach for differencing programs semantically, but applying it often requires substantial manual effort to construct input generators that are well-suited to a target pair of programs. To address this challenge, we introduce DIFUZZI, which incorporates an LLM-based generator synthesis step that is iteratively validated and repaired. By automating this step, DIFUZZI paves the way for broader applicability of differential fuzzing. We release DIFUZZI at https://github.com/Dristi123/difuzzi_tool, with a demonstration video at https://youtu.be/FlHNOHuo9WE

arXiv abstract · PDF

Program Analysis and Equivalence Checking · primary corpus · published 2026-10-28T22:08:49Z
Xinyi Shi
arXiv categories: cs.MS, cs.PL, cs.SE

Low-precision GPU kernels are commonly tested against a reference using hand-picked absolute and relative tolerances. Legitimate numerical error varies with the input, format and precision plan, so a fixed tolerance trades false alarms for missed faults. We present numoracle, which derives per-element acceptance regions from precision-annotated reference programs. Its calculus tracks shared rounding errors, provenance-ordered products, block-scaled quantizers and calibrated math-library errors. A rounding-interval check detects faulty stores that symmetric bounds can admit. Soundness is conditional on explicit rounding, hardware, domain and implementation assumptions; a fixed-input mode removes the zero-mean rounding assumption. We evaluate 13 Triton operators from Liger-Kernel, Unsloth and vLLM on two GPU generations. The main campaigns produce no false alarm on 33,960 correct-kernel and behavior-preserving-variant runs per GPU. Under input shift, the GPU campaigns record no false alarm while tuned tolerances flag up to 30% of correct runs; final-version reference checks identify inputs without complete finite-range certificates. On the RTX PRO 6000, numoracle kills 116 of 124 effective mutants, versus 59-83 for four fixed baselines. Among 400 tuned tolerance configurations, requiring at most 1% false alarms in every evaluated Liger input group permits at most 31 of 53 main-mutant kills, versus numoracle's 50. Historical replays expose accuracy faults in eight change pairs without rejecting their matched corrected controls; a ninth change concerns rounding parity.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · cs.SE candidate · published 2026-10-30T09:24:02Z
Zhihao Guo, Zonghan Wu, Yilei Shao, Haizhou Du, Nan Tang, Xiao Cheng, Huan Huo
arXiv categories: cs.SE

Large Language Models (LLMs) for Text-to-SQL frequently generate queries with syntax errors, invalid identifier references, or violations of SQL scoping and typing rules. Repairing these errors is a program correctness problem, yet existing approaches rely on Execution Feedback (EF), whose symptom-level, dialect-specific error messages force the LLM to speculate on root causes. We identify an Arbitration Paradox in this paradigm: the system relies on unverified models both to propose repairs and to make the final judgment on whether those repairs satisfy the required properties. We resolve this paradox by reformulating Text-to-SQL repair as property-guided program repair. Our framework, Post-SQLFix, canonicalizes SQL into a dialect-aware Canonical Query Structure (CQS) and validates it through a hierarchical static analyzer with three stratified property layers (Syntactic, Context-Free Structural, Context-Sensitive Semantic). The analyzer produces precise, schema-aware violation diagnostics to guide the LLM's repair proposals. A Verify-Before-Apply Temporal Monitor then accepts only repairs that reduce the violation count, do not reintroduce resolved violations, and satisfy the operator contracts. These runtime invariants are bounded by the declared rule family and operator contracts, while a finite retry budget ensures halting. On three established benchmarks (BIRD, Spider, Mini-Dev) spanning over 3,000 evaluation instances, three SQL dialects (SQLite, MySQL, PostgreSQL), and six model configurations, Post-SQLFix resolves 77.8% of the execution errors that EF leaves unrepaired, while requiring less than half as many repair iterations and 30% fewer tokens. Crucially, accepted transitions under the monitor introduce no statically detectable structural regressions in our evaluation, translating checked repair fidelity into absolute accuracy improvements of up to +11.6 percentage points.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · cs.SE candidate · published 2026-10-30T10:56:30Z
Omid Saghatchian, Ali Mahzoun, Khashayar Etemadi, Saeed Reza Kheradpisheh
arXiv categories: cs.SE, cs.CL

Understanding how code changes affect program semantics is a core aspect of code reasoning in language models. It is commonly evaluated by asking whether two programs are semantically equivalent, but a yes/no answer does not reveal whether a model knows which code change caused a semantic difference, or which sequence of code changes produced the modified program. We study two tasks that ask these questions directly, diagnosing semantic change and reconstructing sequences of code changes, alongside detecting semantic equivalence. We build SCRBench, 67,658 Python program pairs generated by applying sequences of code changes that preserve or alter program semantics, and evaluate five language models on a stratified subset of 4,500 pairs. Detecting semantic equivalence exposes weaker models, whose accuracy declines as changes accumulate, but the strongest models remain near the ceiling. Diagnosing semantic change reveals weaknesses that equivalence accuracy hides: a model with 94.71% equivalence accuracy diagnoses only 54.44% of semantic changes. Reconstructing sequences of code changes is much harder: the best model reconstructs the exact sequence for only 39.27% of pairs, and no model exceeds 1.11% when five changes are applied. High equivalence accuracy therefore overestimates how well models reason about the semantic effects of code changes.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · cs.SE candidate · published 2026-10-30T11:56:19Z
Wonseok Oh, Michael Pradel, Hakjoo Oh
arXiv categories: cs.SE

Type annotations improve the maintainability and reliability of Python programs, but many real-world projects remain under-annotated because manual annotation is time-consuming and error-prone. Recent neural and LLM-based type inference systems can recover missing annotations, yet they often trade accuracy for efficiency. Existing approaches often fail to exploit project-wide type evidence, or do so inefficiently through unnecessary model calls and noisy prompts. We present SALT, an LLM-based type inference system guided by static analysis. SALT integrates static analysis with LLM inference to resolve types statically, prioritize LLM queries, and construct concise type-aware context. To demonstrate the effectiveness of SALT, we evaluated it on 12 real-world Python projects. SALT achieves the best accuracy among the evaluated systems and reduces estimated LLM cost by up to 78.5% compared with a strong coding-assistant baseline. It also shows similar cost savings with the frontier model GPT-5.5, demonstrating that SALT remains effective with strong LLMs.

arXiv abstract · PDF

Program Analysis and Equivalence Checking · primary corpus · published 2026-10-31T04:48:13Z
Ignacio Cano, Amir Saadat, Rishipal Singh Bhatia, Samuel Ginzburg, Patrick C. Toulme, Ioannis Zarkadas, Praveen Narayanan, Pratik Bhatu, Nicolas Basile, Alexander Dietm\"uller, Ruishan Wang, Jacob Wahlgren, Victor Barros, Subhankar Shah, Michael Kuperstein, Farzin Houshmand, Emma Sevastian, Peter Gavin, Karthik Srinivasa Murthy, Berkin Ilbeyi, Amit Sabne, Eli Bendersky
arXiv categories: cs.AI, cs.LG, cs.PL

Accelerating modern foundational models has pushed domain-specific compilers toward increasingly complex, multi-tiered optimization pipelines. However, this heavy optimization focus introduces delicate tradeoffs between peak execution performance and correctness. Subtle codegen defects can trigger numerical degradation and memory or buffer corruption, invalidating multi-million-dollar training runs and degrading live serving quality without raising obvious compiler errors. In this paper, we present a battle-tested methodology for verifying and triaging Google's XLA:TPU compiler at hyperscale. We leverage fuzzing techniques, combining synthetic program generation with real production traces, while orchestrating AI agent swarms to autonomously generate stress tests, reproduce failures, and draft fixes. To pinpoint root causes in full workloads, we pair this with a hierarchical differential pipeline that bisects large graphs down to individual failing operations inside fused kernels. Deployed in production, our framework has already driven the resolution of over 142 compiler bugs (with 103 additional findings under review), from which we distill pragmatic lessons learned.

arXiv abstract · PDF

Compiler Correctness and Systems Safety · primary corpus · published 2026-10-26T13:35:12Z
Zheyuan Xu, Xiaobei Zhang, Zihan Li, Zekai Nie, Guangtao Zhu, Zhuang Lu, Qianying Zhang, Shijun Zhao, Haibo Chen, Rui Hou
arXiv categories: cs.OS, cs.CR, cs.PL

Microkernels provide good features such as high security, safety, and flexibility, but their reliance on hardware-based isolation leads to heavy performance overhead, limiting their widespread adoption. Although constructing single-address-space microkernels based on safe language-based isolation is a promising approach to addressing the performance issue, this approach still faces challenges in maintaining the principle of minimality and enforcing capability-based, fine-grained access control over system resources. We propose safeL4, an approach to constructing microkernels based on safe languages. It guarantees minimality through low-level abstractions for unsafe operations, and implements a capability system based on the safe language's object capabilities to achieve fine-grained access control over all operations on system resources. We implement a prototype system in Rust, and our evaluation results show that the primitives provided by safeL4 are, on average, 1.9$\times$ faster than those of seL4.

arXiv abstract · PDF

Compiler Correctness and Systems Safety · primary corpus · published 2026-10-27T13:46:09Z
Carmine Abate, Kleio Liotati, Franti\v{s}ek Farka, Sebastian Ertel
arXiv categories: cs.PL

Program specifications in separation logic describe ownership of resources and serve as logical interfaces for local reasoning. Compiler correctness, expressed as semantics preservation, does not by itself supply such an interface for compiled code, because it does not explicitly relate source and target resources and assertions. We investigate WP-preserving compilation: when a compiler translates a source program, the weakest preconditions that the program satisfies in a separation logic carry over to the compiled program. Our proof technique consists of a resource-aware simulation over interaction trees: it relates the resources required by corresponding source and target events, and tracks ownership through target operations, such as register accesses, that have no source counterpart. We apply the approach to a compiler from a structured imperative language to an assembly-like language, first for closed programs and then extended with modules and function calls. In the extended setting, each module can be verified in the source logic and compiled separately; its specifications carry over to the compiled module and are preserved when compiled modules are linked. All results are mechanized in Rocq.

arXiv abstract · PDF

Compiler Correctness and Systems Safety · primary corpus · published 2026-10-28T06:29:02Z
Byonggon Chun
arXiv categories: cs.LG, cs.AI, cs.AR, cs.PL

Frontier large language models write correct CUDA kernels for most single-operator benchmark tasks, yet their accuracy collapses on accelerators whose architecture and programming language they have rarely seen. We present a case study of an LLM agent loop built for such accelerators. Our example is the FuriosaAI RNGD NPU, programmed in a recent, sparsely documented Rust DSL, where the loop optimized three Gemma-4-12B decode kernels over 12 days on a shared, scarce device. The loop builds its own target knowledge: it writes and checks a summary of the DSL documentation, measures the chip with microbenchmarks, records compiler-derived legality rules, and revisits this knowledge when the toolchain changes, rechecking rules and measurements where it can. A role-based search over per-kernel Design Trees explores whole-kernel designs and accumulates small accepted changes in the best version of each kernel. Because device time is scarce and readings are noisy, cheap checks screen new designs before any device run, and late in the run a change was accepted only after repeated comparisons with the best kernel on the device. The final kernels reach a 9.293x geomean speedup over the official baseline, each within 1.25x of the cycles needed just to move its weights. Our prompts, profiler and acceptance test are available at https://github.com/bgchun-fs/multi-agent-kernel-gen-loop.

arXiv abstract · PDF

Compiler Correctness and Systems Safety · primary corpus · published 2026-10-28T18:55:42Z
Elizabeth Gilbert, Chris Fallin, Heather Miller, Ben L. Titzer
arXiv categories: cs.SE, cs.PL

Monitoring and debugging deployed software is crucial for scalability, performance, and robustness. Cross-cutting concerns are pervasive across software ecosystems, yet engineers must address them with a fragmented toolbox. While high-level frameworks exist to offer application-level types and semantics, they often lock a solution into specific languages, runtimes, or hardware architectures. Portability often forces engineers to choose lower-level instrumentation mechanisms. For example, in-language frameworks can trace a request across processes, but multi-language contexts require instrumentation at the boundary, for example using eBPF. While these frameworks provide powerful capabilities, they often result in 1) a tradeoff between application-level types or low-level bytes and packets, 2) non-composable domain-specific tools, 3) feature fragmentation across frameworks, and 4) tools that often run with unrestricted access to the program and its environment. We address these problems with Splicer, a WebAssembly component interposition framework that 1) provides semantically rich application-level types, 2) enables pluggable tooling with powerful capabilities, 3) reduces ecosystem fragmentation through porting across languages and hardware, and 4) confines each tool to a sandbox with explicitly granted permissions. We evaluate Splicer on a suite of benchmarks demonstrating the pluggability of non-trivial tooling written in multiple source languages and their performance.

arXiv abstract · PDF

Compiler Correctness and Systems Safety · primary corpus · published 2026-10-29T05:04:48Z
Sixuan Dang, Quan Zhou, Kaiming Huang, Jianan Zhu, Anitha Gollamudi, Trent Jaeger, Danfeng Zhang
arXiv categories: cs.CR, cs.PL

Although decades of research have yielded sophisticated mechanisms for enforcing memory safety, speculative execution can subvert these protections through transient memory operations. Conversely, defenses designed specifically for speculative safety, such as Speculative Load Hardening (SLH), cannot enforce memory safety during non-speculative execution. A naive combination of defenses from both domains raises two fundamental challenges: (1) which combination of otherwise fragmented defenses can ensure dual memory safety under speculative and non-speculative executions? (2) whether such combinations introduce redundant protections that incur unnecessary performance overhead? We present DualGuard, a unified framework for dual memory protection under non-speculative and speculative executions. DualGuard systematically analyzes memory behaviors, classifying them into four categories, and further identifies the minimal composition requirements for dual memory safety, which allow us to strategically combine existing mitigations and design new ones to avoid redundant or excessive protections. We implement DualGuard through a combination of static analysis and runtime enforcement within the LLVM infrastructure. Our evaluation demonstrates that DualGuard reduces overhead by 3%-72% compared to naive compositions of fragmented defenses. In some cases, it even incurs lower overhead than approaches that guarantee memory safety solely under either non-speculative or speculative execution.

arXiv abstract · PDF

Compiler Correctness and Systems Safety · primary corpus · published 2026-10-30T03:25:12Z
Darius Foo, Viet-Anh Nguyen, Wei-Ngan Chin
arXiv categories: cs.PL

Today, semantic models of languages with concurrency and higher-order state are constructed using step-indexed predicates over resources and higher-order ghost state. There are two main lines of work for constructing such models. On the one hand, Iris provides these in full generality, at the cost of a large body of mechanised domain theory that is difficult to learn and port to new proof assistants. On the other hand, Indirection Theory is much simpler through the use of ordinary dependent types, but its foundation in separation algebra limits the expressiveness of its resource model compared to Iris-style higher-order ghost state. We resolve this conundrum by showing that Indirection Theory can be as expressive as Iris. To that end, we give a lightweight mechanisation of Indirection Theory in Lean, generalised so knots contain resources from an Iris-style resource algebra functor. We then reconstruct the Iris base logic on top of it. The advantage of this approach is in the elementary metatheory: a user can follow the whole construction without domain theory. We conduct two case studies to show that the base logic is expressive and faithful to Iris: a biorthogonal logical relation for higher-order state, and an Iris-style program logic with invariants and user-definable ghost state, complete enough to verify concurrent and higher-order programs.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-26T21:37:42Z
Tobias Dyckerhoff, Till Heine, Simon Schneider
arXiv categories: math.AG, math.AT, math.CT

We show that several Dold-Kan type equivalences can be understood as a passage from constructible sheaves on symmetric products (i.e. spaces of polynomials) to polynomial sheaves in the sense of Goodwillie-Weiss calculus, by means of a natural analytic expansion functor. This geometric perspective provides access to standard tools from sheaf theory such as the six functor formalism and $t$-structures. For example, the equivalence between filtered objects and coherent chain complexes in a stable $\infty$-category receives a geometric incarnation as Verdier duality between $!$-sheaves and $*$-cosheaves on an $\infty$-dimensional simplex. As a main application, we obtain an intrinsic geometric explanation for the appearance of vanishing cycle data for perverse sheaves in a paracyclic variant of the Dold--Kan correspondence pioneered by Dwyer and Kan, at the same time lifting their equivalence to stable $\infty$-categories.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-28T19:01:30Z
Viktoriya Ozornova, Martina Rovelli, Tashi Walde
arXiv categories: math.AT, math.CT

We verify that saturated complicial sets model the right limit of the $\infty$-categories of $(\infty,n)$-categories, whereas the canonical comparison with the left limit is not an equivalence. By contrast the category of strict $\omega$-categories is equivalent to both the right and left limits of the categories of strict $n$-categories.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-28T21:34:12Z
Thorger Gei{\ss}
arXiv categories: math.AT, math.CT

The Freudenthal Suspension Theorem states that the connectivity of the unit map $X\rightarrow\Omega\Sigma X$ of the suspension-loop adjunction for a pointed space $X$ is twice the connectivity of $X$ itself. We extend this theorem to $X$ being a pointed $(\infty,\infty)$-category, i.e. an oriented space in the sense of Gepner--Heine.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-29T14:53:13Z
Klaus Mattis, Timo Wei{\ss}
arXiv categories: math.AG, math.CT

Let $p$ be a prime. We construct a coherent formalism of geometric operations on Cartier modules with coefficients in ind-coherent sheaves on noetherian derived $\mathbb F_p$-schemes. For such a scheme $X$, we consider the stable presentable category $\mathrm{Cart}(X)$ of ind-coherent sheaves $M$ equipped with a structural morphism $F_{*,X}M \to M$, where $F_X$ denotes the Frobenius endomorphism. We construct pushforward functors for arbitrary morphisms and exceptional pullback functors for separated morphisms almost of finite type, together with coherent composition and base-change equivalences. We single out conditions under which these functors admit further adjoints. On derived schemes separated and almost of finite type over $\mathbb F_p$, we construct compatible closed symmetric monoidal structures given by shriek tensor products, and establish which functors are symmetric monoidal. The constructions arise from a general procedure for forming functor formalisms of Cartier objects, using their description as lax limits and the universal properties of span $2$-categories developed by Cnossen--Lenz--Linskens [arXiv:2505.19192].

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-29T15:50:35Z
Sinem Odabasi
arXiv categories: math.CT, math.KT

Let $(\V, \otimes, I,[-,-])$ be a closed symmetric monoidal category with finite (co)limits. Assume that $\V$ is weakly idempotent complete and additive. For a given small $\V$-category $\A$, we investigate sufficient conditions on $\A$ under which the ordinary category $[\A, \V]_0$ of $\V$-functors from $\A$ to $\V$, equipped with the exact structure $\mathcal{E}_{\textrm{lowt}}$, is a Frobenius exact category,and hence, induces a triangulated stable category. The exact structure $\mathcal{E}_{\textrm{lowt}}$ encompasses the degre-wise trivial exact structure on categories of $N$-chain complexes and $m$-periodic chain complexes, with terms in a variety of settings, including left $R$-modules, quasi-coherent sheaves on a scheme, and Banach spaces. We subsequently address the question of describing abstract left and right homotopy relations in $([\A, \V]_0;\mathcal{E}_{\textrm{lowt}})$ in terms of families of morphisms defined objectwise, as in the cases of chain-homotopy and relative homotopy relations. To this end, we introduce the notion of left/right-weak Serre $\V$-functors on $\A$, and investigate their relationships with the classical Serre functor relative to a commutative ring $k$.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-30T10:50:06Z
Mitchell Buckley, Richard Garner
arXiv categories: math.CT

Many kinds of generalised syntax, including internal categories, T-categories or polynomial monads, arise as monads in bicategories of a certain flavour: maps are some kind of span, and composition is some kind of pullback. We explain the pattern behind these similarities: each bicategory is stitched together from two simpler pieces by a distributive law, where the distributivity is governed by pullback. A key novelty is in the kind of distributive law we consider; where Rosebrugh and Wood considered distributive laws between categories, we instead consider pseudo-distributive laws between double categories. A key construction, drawing on work of Weber, obtains such a distributive law from a so-called co-crossed double category: one whose codomain functor is a fibration, and whose cartesian cells are stable under horizontal composition. We show the horizontal Kleisli double category of a monad T is co-crossed just when T is cartesian, and that the composite double category recovers T-spans; that the double category associated to an identity-on-objects functor is co-crossed just when that functor is a calibration in the sense of B\'enabou; and that Street's calibrated bicategories yield co-crossed double categories in a similar manner, recovering the double category of polynomials of Gambino--Kock.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-30T10:58:42Z
Li He
arXiv categories: math.KT, math.CT

In this paper, we formulate Land-Tamme's $\boxtimes$-construction and $\odot$-construction for continuous exact monads on dualizable stable $\infty$-categories, and establish the behaviour of localizing invariants on pushouts of left modules over continuous exact monads on dualizable stable $\infty$-categories. Combining the Land-Tamme theory of continuous exact monads with the theory of analytic functors in Goodwillie calculus, we show that the reduced K-theory on modules over free tensor algebras of dualizable t-categories is modified 1-coanalytic or modified 2-coanalytic, depending on the coconnectivity of the base algebras. In particular, this answers Efimov's question concerning coanalyticity in the affirmative.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-30T15:39:48Z
Fernando Abell\'an, Thomas Blom
arXiv categories: math.CT

We extend the theory of lax-idempotent monads to the setting of $(\infty,2)$-categories. In particular, we prove an analogue of Kock and Z\"oberlein's characterization of the category of algebras over a lax-idempotent monad. We then apply this theory to many examples that arise naturally in homotopy theory. For example, we show that $(\infty,1)$-toposes are monadic over presentable $(\infty,1)$-categories, with left adjoint given by the symmetric $(\infty,1)$-topos. We also show that $\infty$-operads are comonadic over symmetric monoidal $(\infty,1)$-categories through the monoidal envelope construction, obtaining along the way a new proof of Barkan-Steinebrunner's result that the envelope functor is a faithful inclusion. We furthermore use this theory to simplify Ramzi's proof that dualizable stable $(\infty,1)$-categories are comonadic over $\aleph_1$-compactly generated stable $(\infty,1)$-categories.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-10-31T10:52:11Z
Kunal Arora, Vivek Mohan Mallick
arXiv categories: math.AG, math.AT, math.CT

By introducing the notion of stable compatibility, we provide a framework in the model category theory which addresses the existence of a stable model structure on the category of modules over a monad. Exact version of such monads have been studied in the setting of triangulated categories, separately as separable monads a la Balmer in tensor triangular geometry and non-separable monads a la Dell'Ambrogio and Sanders in stable homotopy theory. By introducing stable compatibility, we explore their properties together and produce a non-separable monad in Algebraic geometry and more.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-11-01T07:02:51Z
Fernando Lucatelli Nunes
arXiv categories: math.CT, math.AG

We continue the programme developed in Pseudo-Kan extensions and descent theory by studying descent for augmented pseudocosimplicial objects. Let $\mathcal H$ be a $2$-category, and let $\operatorname{suc}=\mathsf{1}+(-)$ be the successor monad on the augmented simplex category. Precomposition with $\operatorname{suc}$ induces the d\'ecalage pseudomonad $\mathbb S$ on the $2$-category of augmented pseudocosimplicial objects with values in $\mathcal H$. We prove that every successor contraction makes the corresponding augmented pseudocosimplicial object effective for descent. This structure is preserved by postcomposition with every pseudofunctor. Consequently, the resulting descent object is an absolute bilimit. A first application concerns split epimorphisms. We recover the Janelidze--Tholen characterization of absolute effective descent morphisms given in Facets of Descent II. Moreover, we prove that one direction holds for every pseudofunctor $A\colon C^{\mathrm{op}}\to\mathcal H$, where $\mathcal H$ is an arbitrary $2$-category. Consequently, every $\mathbb S$-pseudoalgebra is of absolute descent. In particular, this holds for every free $\mathbb S$-pseudoalgebra, and hence for every one-sided d\'ecalage. This makes the shift-effectiveness hypothesis in the B\'enabou--Roubaud theorem of Pseudo-Kan extensions and descent theory automatic. Thus, under the adjointness and Beck--Chevalley hypotheses, the descent and Eilenberg--Moore factorizations are equivalent whenever they exist. We thus obtain a stronger version of the B\'enabou--Roubaud theorem for arbitrary augmented pseudocosimplicial objects, which we call the formal B\'enabou--Roubaud theorem. Applied to indexed \v{C}ech objects associated with pseudofunctors $A\colon C^{\mathrm{op}}\to\mathcal H$, this theorem extends the classical B\'enabou--Roubaud theorem to an arbitrary $2$-category $\mathcal H$.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-11-01T13:57:47Z
Rune Haugseng
arXiv categories: math.CT, math.AT

We show that a closed symmetric monoidal V-enriched $\infty$-category can be described by a lax symmetric monoidal functor to V from its underlying $\infty$-category.

arXiv abstract · PDF

Higher Category Theory · primary corpus · published 2026-11-01T15:30:51Z
Rune Haugseng, Thomas Nikolaus
arXiv categories: math.AT, math.CT, math.KT

We prove Lurie's proposed description of left rigid symmetric monoidal $(\infty,n)$-categories in terms of purely $\infty$-categorical data. More precisely, unfolding gives an equivalence between left rigid symmetric monoidal $(\infty,n)$-categories and complete categorical chain complexes of rigid symmetric monoidal $\infty$-categories. More generally, unfolding identifies skeletal sequences with categorical chain complexes without the completeness condition. We extend these equivalences to $(\infty,\infty)$-categories and, stably, obtain an equivalence between complete unbounded categorical chain complexes and left rigid categorical spectra. We also analyze their groupoid completion and express the homotopy groups of the associated spaces and spectra in terms of categorical cycles and boundaries. As examples, we construct the categorical chain complexes associated to geometric and algebraic bordism categories, including their equivariant variants, and to iterated span categories. Their localizations recover classical bordism and $L$-groups, while the span examples are related to algebraic $K$-theory.

arXiv abstract · PDF

Monoidal Categories and Fusion Categories · primary corpus · published 2026-10-27T10:54:09Z
Thibault D. D\'ecoppet, Mateusz Stroi\'nski, Tony Zorman
arXiv categories: math.CT, math.QA

We propose a definition of a finite linear 2-category, as a 2-categorical analogue of the notion of a finite abelian category of Etingof-Ostrik. We go on to prove that finite linear 2-categories with adjunctible projectives are precisely the Morita 2-categories of (all) algebras in a finite multitensor category. Thus, finite linear 2-categories with adjunctible projectives can be viewed as `non-semisimple' generalizations of the finite semisimple 2-categories of Douglas-Reutter. Secondly, we study finite multitensor 2-categories, that is, finite linear 2-categories equipped with a monoidal structure for which every objects has duals. We extend several results about fusion 2-categories to our present setting. In particular, we investigate the properties of the 2-category of bimodules over a rigid algebra $\mathcal{A}$ in a finite tensor 2-category $\mathfrak{C}$. We show that, if $\mathfrak{C}$ has adjunctible projectives, then the 2-category of $\mathcal{A}$-$\mathcal{A}$-bimodules in $\mathfrak{C}$ is a finite multitensor 2-category. This construction provides many examples of finite tensor 2-categories. For instance, the Drinfeld center of a finite tensor 2-category with adjunctible projectives is a finite tensor 2-category.

arXiv abstract · PDF

Monoidal Categories and Fusion Categories · primary corpus · published 2026-10-28T08:37:15Z
Vanessa Miemietz, Fiona Torzewska
arXiv categories: math.RT, math.CT, math.QA

In this paper we define comonoidal structures on additive $\Bbbk$-linear $2$-categories which guarantee the existence of a monoidal structure on the corresponding $2$-categories of $2$-representations.

arXiv abstract · PDF

Monoidal Categories and Fusion Categories · primary corpus · published 2026-10-29T04:02:54Z
Zhiqiang Yu
arXiv categories: math.QA, math.CT

Let $p>5$ be a prime. In this paper, we show that a pre-modular fusion category of global dimension $2p$ is either pointed or tensor equivalent to $\text{Rep}(D_{2p})$.

arXiv abstract · PDF

Monoidal Categories and Fusion Categories · primary corpus · published 2026-10-29T06:28:06Z
Hadi Salmasian, Alistair Savage, Yaolong Shen
arXiv categories: math.RT, math.CT, math.QA

We relate affinizations of braided monoidal categories to braided module categories, allowing a twist by a braided monoidal automorphism. Our main theorem establishes a bijection between twisted braided structures on a right module category and extensions of its action to the corresponding twisted affinization. We also show that the twisted affinization is the free twisted braided module category on one object. We give explicit presentations of twisted affinizations, both as monoidal categories and as module categories, using invertible dots and reflection relations. We also describe the relation to cylinder twists and tensor-pair cylinder twists, including the naturality condition needed to obtain a braided module structure. As applications, we obtain module-category presentations of the affine Kauffman and affine oriented skein categories and an orientation-reversing twisted version of the latter. We realize the disoriented skein category as a quotient of this twisted affinization by a single additional relation.

arXiv abstract · PDF

Monoidal Categories and Fusion Categories · primary corpus · published 2026-10-29T13:40:16Z
Zixuan Feng, Zhengwei Liu
arXiv categories: math.QA, math-ph, math.CT, math.GT, math.MP, math.OA

For a discrete group $G$, we construct an $(n+1)$-dimensional $G$-equivariant Alterfold topological quantum field theory from a $G$-equivariant $S^n$-algebra satisfying strong semisimplicity, complete finiteness, and Morita invariance. We use state sum on triangulation to define a partition function and prove that it is invariant under local surgery relations and is invariant under gauge transformations relative to the boundary. If the input is given a reflection-positive structure, the theory is unitary. For $n=2$ and input reconstructed from a strict faithful spherical $G$-fusion category, the restriction to ordinary $G$-cobordisms is naturally isomorphic to the Turaev--Virelizier state-sum HQFT \cite{turaev20123}. A Tambara-Yamagami example recovers the Quon language \cite{liu2017quon} as a $\mathbb{Z}_2$-equivariant Alterfold TQFT.

arXiv abstract · PDF

Monoidal Categories and Fusion Categories · primary corpus · published 2026-10-29T16:59:13Z
Matt Wilson, James Hefford, Timoth\'ee Hoffreumon
arXiv categories: quant-ph, math.CT

We extend the process-matrix framework for defining indefinite causal orders to a broad class of generalised physical theories. We give a simple re-axiomatisation of spacetime contexts in terms of naturality over classical probes, which precisely captures non-contextual assignment together with compatibility with convexity and coarse-graining within local laboratories. Using this compositional perspective, we give a clean characterisation of theories in which abstract spacetime contexts admit a process-matrix representation, and we pin down the precise conditions (satisfied by classical theory, quantum theory, and a Boxworld-like theory) under which the supermap and process-matrix perspectives on higher-order processes coincide.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-26T11:21:01Z
Javier D\'iaz Cabrera, Fernando Muro
arXiv categories: math.CT, math.KT, math.RT

We introduce a new secondary cohomology operation, the naturality defect product, associated with a graded natural transformation between the cohomology functors of two differential graded functors, and study its main properties. We then prove that a pretriangulated category satisfies the octahedral axiom if and only if the naturality defect product associated with the natural isomorphism given by a theorem of Heller vanishes on the homotopy category of acyclic complexes over it. This characterization extends immediately to n-angulated categories. As an application, we exhibit non-vanishing instances for the recently found examples of pretriangulated categories which are not triangulated. Finally, we show that horizontal composition of these natural isomorphisms preserves n-angulated structures, and we use it to obtain, from each of these examples and for every r >= 1, a pre-3r-angulated category which is not 3r-angulated.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-26T18:27:35Z
Daniil Mamaev
arXiv categories: math.SG, math.AG, math.CT

Given a compact surface $S$ admitting a Liouville form, a finite set $Q \subset S$, a line field on $S$, and a local system of dg-categories on $S \setminus Q$ together with a section of the monodromy functor around each interior $q \in Q$, we construct a Fukaya category. We give examples where such Fukaya categories are quasi-equivalent to derived categories of projective completions of line bundles and of iterated blow-ups of the affine plane; and to wrapped Fukaya categories of cotangent bundles of spheres. We define two versions of the Fukaya category, a topological, which is constructed combinatorially from a full arc system, and a geometric, which includes all Lagrangian branes supported on immersed curves. We prove that the topological category embeds into the geometric category in an essentially unique way. To define Lagrangian branes we develop a generalisation of the Chekanov--Eliashberg algebra incorporating dg-coefficients and wrapping along the boundary.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-27T10:21:57Z
Anastasios Slaftsos
arXiv categories: math.RT, math.CT

Compact generation allows large triangulated categories to be studied through suitably small objects. For homotopy categories arising from exact model structures, a natural question is how this intrinsic notion of smallness relates to finite presentation in the underlying exact category. In this paper, we investigate this relation for hereditary projective model structures generated by finitely presented Gorenstein projective objects. We establish compact generation and study the stronger requirement that every compact object admits a finitely presented cofibrant representative. We call objects with such representatives perfect. Under local coherence and the existence of enough projectives among the finitely presented objects, the finitely presented cofibrant objects form a Frobenius category whose stable category describes the perfect objects and whose idempotent completion recovers all compact objects. The relative $Q$-shaped setting, for suitable small categories $Q$, makes explicit how these finiteness properties depend on the choice of exact structure. The pure exact structure yields a compactly generated homotopy category, called the $Q$-shaped pure derived category. On the other hand, the split exact structure yields the $Q$-shaped homotopy category, which is compactly generated only in the pure semisimple case, analogously to the classical homotopy category of complexes. Finally, for acyclic $Q$ and for left artinian rings, we show that every compact object admits a strictly perfect representative. In particular, we establish that compact and perfect objects coincide, proving the conjecture of Holm and Jorgensen under these hypotheses.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-28T23:08:35Z
Cyril Matou\v{s}ek
arXiv categories: math.RT, math.AG, math.CT

Neeman's metric on a triangulated category assigns lengths to morphisms and allows us to construct triangulated metric completions of the category. We prove that the metric completion of a triangulated category with respect to a constant metric is always a subcategory of the Verdier quotient by the thick subcategory generated by cones of zero-length morphisms, and we provide a sufficient criterion for equality. To that end, we define continuous functors between completions which induce triangulated functors between completions. Moreover, we give two applications. First, we show that the additive equivalence discovered by Cummings and Gratz between the Paquette-Yildirim completion and a specific metric completion of an Igusa-Todorov discrete cluster category is, in fact, a triangulated equivalence. Second, we fully classify metric completions of bounded derived categories of coherent sheaves over weighted projective lines of domestic or tubular type.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-29T17:52:14Z
Juan Omar G\'omez, Sam K. Miller
arXiv categories: math.RT, math.AG, math.AT, math.CT

In this paper, we introduce a `reduced' form of permutation twisted cohomology as introduced by Balmer--Gallauer and further developed by Miller. This ring is bigraded by a well-chosen choice of endotrivial complex, rather than multigraded by a family of endotrivial complexes. The Balmer spectrum of the small derived category of permutation modules openly immerses into the homogeneous spectrum of this ring. We also show that for $p$-groups, Miller's `remixed' twisted cohomology ring also admits the Balmer spectrum as an open subspace, and confirm in both cases it can be upgraded to have Dirac scheme structure; furthermore, we prove that the two open covers witnessing this are in general different.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-29T18:02:09Z
Jean Paul Schemeil, Fraser Sparks
arXiv categories: math.AG, math.AT, math.CT, math.KT

We compute the Balmer spectra of geometric Tate and Artin--Tate motives with $\mathbb{F}_p$-coefficients over any field whose characteristic differs from $p$. For Tate motives, we find the bigraded comparison map to be a homeomorphism to the homogeneous spectrum of the motivic cohomology of the base field. For Artin--Tate motives, we describe the spectrum as a gluing of the spectrum of Artin motives computed by Balmer--Gallauer with the punctured Tate spectrum. We determine all specialisations between these pieces and the resulting topology. Under the hypothesis that the spectrum of rational Tate motives is a singleton, we also compute the integral Tate spectrum after inverting the exponential characteristic of the base field. As a consequence of our results, we identify the punctured Tate spectrum as an open subspace of the spectrum of the category of geometric Voevodsky motives, and draw some conclusions concerning the latter. Finally, we include an appendix where we define generalised periodicity in the context of tensor-triangular geometry, and explore its applications in motivic settings.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-10-31T14:09:14Z
Yiyu Cheng
arXiv categories: math.CO, math.CT, math.RT

The lattice of wide subcategories of a tube is isomorphic to the lattice of noncrossing partitions of type B. We prove that through this categorification of noncrossing partitions, Kreweras complement is taking left perpendicular categories. With the help of this categorification and weighted projective lines, we obtain an inclusion from the lattice of noncrossing partitions of type B_n to a lattice of affine type A_n which preserves Kreweras complement.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-11-01T03:41:29Z
Andrei Konovalov
arXiv categories: math.AG, math.AT, math.CT, math.KT

We extend the definition of cdh-sheafified Hochschild homology from varieties to stable categories linear over a field of characteristic zero, thereby proving its Morita-invariance. The dimensions of its homology groups give meaningful numerical invariants of a category; we combine them with invariants coming from topological K-theory and Poincar\'e duality to prove equality of mixed Hodge numbers for singular complex projective Fourier--Mukai partners in several classes in dimensions two, three, and four, including normal surfaces and threefolds with rational singularities and equal irregularity. Beyond these applications, we construct Du Bois versions of topological cyclic homology of stable categories together with appropriate multiplicative structures, prove a Geller--Weibel-type result for the variants of negative cyclic homology we introduce, and give categorical characterizations of cohomological purity of proper varieties and the $\mathbb{Q}$-factoriality defect of complex projective threefolds with rational singularities.

arXiv abstract · PDF

Triangulated Categories and Derived Geometry · primary corpus · published 2026-11-01T17:37:13Z
Yuan Gao, Zhen Gao
arXiv categories: math.KT, math.CT, math.RT

We study how Koszul duality relates two kinds of boundary constructions associated with a smooth category and a proper category. For a smooth category with a proper Koszul-dualizing subcategory, we construct a fully faithful functor from its categorical neighborhood of infinity to the singularity category associated to the proper category. We prove that this functor is an equivalence precisely when the smooth category is reflexive, meaning that it can be reconstructed from its finite-dimensional module theory. Under a Gorenstein condition, satisfied in the Calabi--Yau setting, the functor is induced by restriction of modules. We give algebraic criteria that ensure equivalence and obtain an identification of Hochschild cohomology.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-27T18:52:50Z
Carles Card\'{o}, Keith A. Kearnes, \'{A}gnes Szendrei
arXiv categories: math.RA, math.LO, math.PR

We classify the finite algebras $\mathbf{A}$ for which there is no value $p$ satisfying $\frac{1}{|A|}<p<1$ in the equational probability spectrum of $\mathbf{A}$. We will use the classification to determine which finite algebras have minimal equational probability spectrum. In our final section, we explore the relationship, for finite algebras, between the properties of (i)~having a finite equational probability spectrum and (ii)~being an abelian algebra.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-27T20:30:10Z
Fiona Blackett, Vikraman Choudhury, Rin Liu
arXiv categories: math.CT, cs.LO

Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-27T20:43:20Z
Andrea Cappelletti, Andrea Montoli
arXiv categories: math.CT

Generalizing a known result in the context of homological categories, we show that, in a regular protomodular category $\mathcal{C}$ equipped with a posetal, monocoreflective subcategory whose coreflector inverts monomorphisms, every torsion theory, in a non-pointed sense, satisfying suitable properties gives rise to a torsion theory in the category $\operatorname{Arr}(\mathcal{C})$ of arrows in $\mathcal{C}$. Moreover, we show that the induced torsion theory in $\operatorname{Arr}(\mathcal{C})$ satisfies the same good properties of the original one in $\mathcal{C}$, allowing to iterate the process. Examples of this situation can be found in protomodular varieties of universal algebras with more than one constant or in duals of elementary toposes.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-28T01:26:31Z
Nizar El Idrissi
arXiv categories: math.CT

There are many types of equivalence relations in mathematics, each one enjoying its own defnition, but many of them can also be defined by transformations of morphisms: Green's relations, orbit relations, conjugacy, equality of orbit closures, equivalence of Cauchy sequences, stable isomorphism. We unify them through the comparison category of a comparison datum, read at levels $-1,0,1,2,\dots$ (comparisons in both directions, connected components, homotopy groups). Its normal form is a full subcategory of a Grothendieck construction $\int_VH$ cut out by a map $s$; the classical relations are traced back to it by restriction along $s$, enrichment by a cost (limit relations) and filtered colimits (stabilization). If the map $\sigma$ transporting morphisms into a $2$-category is arbitrary, every relation occurs, so the constraint is the regularity of $\sigma$. We grade data along seven regularity classes. The rigid and diagonal classes are classified completely (on finite groups, by the double coset relations); completely functorial data contain conjugacy and obey a dichotomy on nil monoids. Whether every relation on a monoid is level $0$ of a completely functorial datum is open.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-29T23:31:50Z
Thomas Br\"ustle, Justin Desrochers, Samuel Leblanc
arXiv categories: math.CT, math.RT

Let $\mathcal{C}$ be a small category. We characterize the full initial subcategories of $\mathcal{C}$ as precisely those whose representables give a free presentation of the constant functor $\Delta_{\mathcal{C}}\mathbb{K}:\mathcal{C}\to\mathrm{Vect}$. Such a presentation yields a formula for the limit of any functor $\mathcal{C} \to \mathrm{Vect}$ as the kernel of a morphism between products of evaluations. When the linearized endomorphism ring of every object is local, we show that a minimal free presentation, whenever one exists, determines the unique minimal full initial subcategory, up to equivalence. Bass's characterization of perfect rings gives a sufficient condition for the existence of such presentations. In particular, every finite category with no nonidentity endomorphisms, such as a finite poset, contains a unique minimal initial full subcategory. In the poset case, our results recover the minimal initial subposet constructed in [BDL27] and [DL26]. When $\mathcal{C}$ is the free category on a finite quiver, we give an explicit construction of its minimal initial full subcategories, show that every such subcategory arises from this construction, and provide algorithms with time-complexity bounds.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-30T20:40:24Z
Jes\'us \'Avila, Fabi\'an Molina
arXiv categories: math.CT, math.GN, math.GR

We present some theoretical aspects of the categories of global and partial group actions of topological groups on topological spaces, denoted by G-ActTop and G-pActTop, respectively. We construct topological partial actions on products and disjoint unions of topological spaces, and G-pinvariant subspaces. Furthermore, we provide an adequate definition of congruence (G-pcongruence), which enables the construction of quotient objects in the category of topological partial actions. In addition, we associate a special G-pcongruence to each pair of strong G-pmorphisms. Then, we study products, co-products, equalizers, co-equalizers, pullbacks, and pushouts in the category G-pActTop. We find that the category of topological partial actions is finitely complete and contains a co-complete subcategory. Finally, we show that the relationship between a topological partial action and its enveloping action is functorial. As a consequence, we obtain that the categorical product in G-ActTop coincides with the categorical product in G-pActTop. Moreover, the envelope of a co-product in G-pActTop is given by the co-product of the respective envelopes.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-10-31T18:34:03Z
Maria Manuel Clementino, Fernando Lucatelli Nunes
arXiv categories: math.CT, cs.PL, math.LO

For a finitely complete category X, we prove that the lax comma category Cat//X is cartesian closed if and only if its free coproduct completion Fam(X) is cartesian closed. The proof uses a change-of-base theorem: postcomposition with a functor induces a left adjoint between lax comma categories precisely when that functor is a left multiadjoint. We describe the exponentials and derive examples from known results on family categories.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-11-01T18:12:07Z
Manuel Mancini
arXiv categories: math.CT, math.RA

We study the representability of actions in varieties of algebras with $n \geq 1$ not necessarily associative bilinear multiplications. We first prove that, for homogeneous varieties, action accessibility is equivalent to being an Orzech category of interest. For an action accessible, operadic variety we then construct the external weak actor $\mathcal{E}(X)$ of an algebra $X$, an algebra with $n$ bilinear partial operations together with a natural monomorphism encoding the actions on $X$. We characterise the algebras admitting an actor in terms of $\mathcal{E}(X)$, and we deduce an obstruction to action representability: if, for some algebra $X$ with trivial multiplications, $\mathcal{E}(X)$ does not satisfy a multilinear identity of the variety, then the variety is not action representable. Computing the external weak actor explicitly, we obtain that associative and matching dialgebras are weakly action representable but not action representable, and that Poisson algebras, left-right non-commutative Poisson algebras and matching Lie algebras are not action representable. Finally, we introduce the reduced type $(p,q)$ of such a variety and prove that, over a field of characteristic different from $2$, an operadic variety of reduced type $(p,0)$, $(0,q)$ or $(1,1)$ is action representable if and only if it is term equivalent to the variety of Lie algebras or to that of abelian algebras. For the reduced types $(p,0)$ and $(0,q)$, the arguments require no assumption on the cardinality of the field, whereas the case $(1,1)$ requires the field to be infinite.

arXiv abstract · PDF

Categorical Algebra and Universal Constructions · primary corpus · published 2026-11-01T19:21:54Z
Ana Sokolova, Harald Woracek
arXiv categories: cs.LO

Convex semilattices form an equational class that combines convex algebras and semilattices by a distributive law. For a set $I$ let $\mathcal FI$ be the free convex semilattice with basis $I$. A product $\mathcal FI\times\mathcal FJ$ is generated by $I\times J$, but is not free. Hence, not every map from $I\times J$ into an arbitrary convex semilattice $X$ extends uniquely to a homomorphism from $\mathcal FI\times\mathcal FJ$ to $X$. We investigate a condition on a map $\varphi$ of $I\times J$ into some convex semilattice $X$ that is always necessary and often sufficient for $\varphi$ to have such an extension to a homomorphism $\Phi$ of $\mathcal FI\times\mathcal FJ$ into $X$.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-26T11:39:55Z
F\'elix Cabello S\'anchez, Jes\'us M. F. Castillo, Ra\'ul Mart\'inez-Boh\'orquez, Jos\'e Navarro Garmendia
arXiv categories: math.FA, math.CT

We determine the Serre closure of Banach spaces in the category of quasi-Banach spaces, that is, the smallest class of quasi-Banach spaces that contains all Banach spaces and is stable under subspaces, quotients, and extensions. Precisely, a quasi-Banach space $X$ belongs to this closure if and only if there exist constants $M$ and $k\in\mathbb N$ such that $$ \frac{\|x_1+\dots+x_n\|}{\|x_1\|+\dots+\|x_n\|}\leq M\log^k n $$ for every $n\geq 2$ and every $x_1,\dots,x_n\in X$; equivalently, $X$ is a quotient of an Orlicz sequence space $\ell(I,f_l)$, where $I$ is an index set and $f_l(t)$ is equivalent to $t\log^l(1/t)$ near zero. The proof combines geometrical estimates for quasi-Banach spaces and quasilinear maps with the study of higher order derived spaces associated to complex interpolation between $\ell_{2/3}$ and $\ell_2$. We provide examples of spaces in the Serre closure of Banach spaces that are not iterated extensions of Banach spaces and discuss some related problems.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-26T14:48:18Z
Mohamed Elhamdadi, Bryce Virgin
arXiv categories: math.GT, math-ph, math.CT, math.DG, math.MP

Lie quandles were defined by T. Fritz as a nonlinear generalization of Lie algebras, to serve as a nonlinear algebras of observables in generalized form of Hamiltonian mechanics. These objects were subsequently generalized in a prequel article to objects referred to as smooth Lie group families of smooth racks by the authors. In this article, we investigate a particular system of nonlinear functional differential equations whose solution in general provides a pathway to the classification of smooth Lie group families of smooth rack structures on any given smooth manifold. We then discuss a particularly practical ansatz for solving these equations, and use it to construct new families of examples, as well as prove a result on the sense in which the Bloch sphere is the unique Lie quandle structure on the sphere.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-28T20:35:54Z
Ilias Kaperonis, Konstantinos Golfis
arXiv categories: math.CT, math.RA

Accessibility results are established for (Cartan-Eilenberg) strongly FP-injective complexes, by first proving the accessibility of Strongly FP-injective modules and then utilizing the pseudopullback theorem. We also prove that every acyclic complex of weakly FP-projective modules has weakly FP-projective cycles over left $<\aleph_m$-coherent rings for a non-negative integer $m$. This is achieved by introducing the cotorsion pairs $\bigl(\mathcal{C}\aleph_mP\text{-}proj,\mathcal{C}\aleph_mP\text{-}inj\bigr)$, cogenerated by all $\aleph_m$-presentable weakly FP-projective modules, and proving that acyclic complexes of modules from the class $\mathcal{C}\aleph_mP\text{-}proj$ have weakly FP-projective cycles for every non-negative integer $m$.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-28T22:23:13Z
Pierre Clavier, Yannic Vargas
arXiv categories: math.CO, math.CT, math.QA

We introduce graftings and cograftings for vector species, modelled on the elementary operations of adjoining and deleting a root in a rooted forest. We relate these maps to operads, up and down operators, and obtain nontrivial balanced pairs, admitting pair of creation/annihilation operators with commuting relations. We establish universal properties for the species of rooted forests. Using Fock functors, we recover the classical Connes--Kreimer Hopf algebra, its noncommutative planar analogue, and Foissy's $q$-infinitesimal Hopf algebra.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-29T00:46:26Z
Eleanor March, James Owen Weatherall
arXiv categories: math-ph, math.AP, math.CT, math.DG, math.MP, physics.hist-ph

We consider symmetric hyperbolicity and well-posedness in the context of natural equations, which are closed subobjects of jet bundles over natural bundles. We show how non-natural equations can be "naturalized", and we discuss how a precise version of "minimal coupling" offers a (provably unique, up to isomorphism) method for constructing natural equations from certain equations defined on a single manifold. We discuss how to define symmetrizers, hyperbolizations, and constraints for minimally coupled natural equations, and we show how these can be used to recover standard existence and uniqueness results, relative to any choice of background structure (a metric, for minimally coupled systems). Additionally, we show that minimal coupling and naturality together imply that the causal cones associated with a (first order, quasilinear, minimally coupled) naturally symmetric hyperbolic natural equation must always coincide with the metric lightcones, and that a certain rank-2 tensor, associates with a natural hyperbolization, must always be divergence free relative to the associated Levi-Civita derivative operator.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-29T21:46:30Z
Fran\c{c}ois Huard, Nathan Dion Larivi\`ere
arXiv categories: math.GR, cs.FL, math.CO, math.CT, math.DS

Let $G$ be a group and let $n\in\mathbb N$. We consider one-dimensional cellular automata of length $n$ over the alphabet $G$, with periodic boundary conditions and with local rules $\phi$ given by words. We construct a functor $F$ from $\mathbf{Grp}$, the category of groups (or any similar algebraic structure), to the category of pointed digraphs, and show its faithfulness. We introduce the image category $\mathcal C_{n,\phi}$ of state transition graphs of all such group-alphabet cellular automata, and show $F$ is an equivalence onto this category. Consequently we investigate the translation of categorical structures in $\mathbf{Grp}$ in terms of automata, and give examples of how standard methods of homological algebra may now be applied to automata. Additionally, a graph-theoretical construction of the product in $\mathcal C_{n,\phi}$ is given, together with a formula for cycle lengths and multiplicities in this product. When $G$ is abelian, further structural properties of state transition graphs follow, and we contrast these results with non-abelian counterexamples.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-30T10:20:45Z
Bo Le, Bin Zhu
arXiv categories: math.RT, math.CT, math.RA

An Artin algebra is called a composition factor algebra if its indecomposable finitely generated modules are determined, up to isomorphism, by their composition factors. We prove that every composition factor algebra is representation-finite. This settles a conjecture of Auslander, Reiten and Smal\o. We also give criteria for comma categories and factorization categories to be of finite representation type.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-10-31T10:20:20Z
Yanga Bavuma, Martin Mijangos, Francesco G. Russo
arXiv categories: math.AT, math.CO, math.CT

We study persistence modules obtained from the $A$-fundamental groupoids of finite graphs. Moreover, we verify the categorical properties needed to form generalized persistence diagrams, and describe a quotient that identifies equivalent groupoids. A normalized linear presheaf construction places these modules in an essentially small abelian category, where Patel's Continuity Theorem gives a $1$-Lipschitz estimate in erosion distance. Explicit graph filtrations illustrate the groupoid-valued construction, and so we suggest a new approach to interpret persistence diagrams and large data sets in topological data analysis, based on recent works of A-homotopy theory of the last years.

arXiv abstract · PDF

Representation Theory and Geometric Applications · primary corpus · published 2026-11-01T16:42:53Z
Baoyu Zhang, Shengmin Zhang
arXiv categories: math.GR, math.AT, math.CT, math.RT

We prove the D\'iaz$\unicode[Arial]{x2013}$Park conjecture for sharpness of saturated fusion systems. More generally, for every saturated fusion system $\mathcal F$ over a finite $p$-group and every Mackey functor for $\mathcal F$ over the localisation $\mathbb{Z}_{(p)}$ of the integers at $p$, the higher limits of its contravariant part over the centric orbit category vanish in all positive degrees. In particular, the subgroup and normaliser decompositions of every $p$-local finite group $(S,\mathcal F,\mathcal L)$ over the $\mathcal F$-centric subgroups are sharp. This answers in the affirmative a question in the list of important open problems in [M. Aschbacher, R. Kessar and B. Oliver, Fusion Systems in Algebra and Topology, Cambridge Univ. Press (2011)], and proves the sharpness conjecture stated in [M. Aschbacher and B. Oliver, Fusion systems, Bull. Amer. Math. Soc. (2016)] and Conjecture 1.2 of [E. Yal\c{c}$\unicode[Arial]{x131}$n, Higher limits over the fusion orbit category, Adv. Math. (2022)]. The proof is algebraic and does not rely on the classification of finite simple groups.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-26T22:09:13Z
Jeff Shrager, Kent M. Pitman, Mia Golec
arXiv categories: cs.AI, cs.HC, cs.PL

Early AI programs were often also theories of how people think, and programs that wrote programs were, in part, theories of how people program. Here we report on the reanimation of two such programs that offer two seemingly different theories of programming and were developed for quite different purposes. The first, Herbert Simon's Heuristic Compiler (1961), was an experimental model of programming as problem-solving, applying the means-ends analysis methods of the General Problem Solver to investigate the nature of the programming task. The second, KBEmacs (1984), was a working prototype of an intelligent programming assistant developed by MIT's Programmer's Apprentice project, built on the view that expert programmers recognize and combine familiar patterns, or "cliches." It let a programmer build up programs by combining cliches through a stylized English command language. We approach both through the methodology of Executable Archaeology, the study of historical computational systems by running their original code, a process we call "reanimation." Our reanimation of the Heuristic Compiler reproduces the compiled code appearing in Simon's 1963 paper, and our reanimation of KBEmacs reproduces the SQRT sequence of its December 1984 self-test. Examined side by side, the two theories turn out to have much in common: the Heuristic Compiler also works by adapting existing routines, and Simon later argued that search alone requires a large body of programming knowledge. To highlight the reflexivity of this project, we deliberately used a modern AI-assisted programming tool, Anthropic's Claude Code (Opus 5.5), to carry out much of the detailed reanimation work, building on a significant base of existing software. The explicit, executable theories of programming that both systems embodied are largely absent from today's far more capable AI coding assistants.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-30T10:46:05Z
Peter Bartholomew, Luke Phillips
arXiv categories: cs.PL, cs.CE

Since the calculation engine of Excel was the subject of a major upgrade to accommodate Dynamic Arrays in 2018, there has been a series of seismic changes to the art of financial modelling. This paper will show the traditional financial modelling techniques for spreadsheets can be replaced by radically different approaches that have significant gains in readability, performance and flexibility. With so much power added to the Excel engine in recent years, it is the responsibility of financial modellers to ensure that they are building in the simplest and most auditable way possible going forward.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-30T14:49:59Z
Nicola Botta, Patrik Jansson, Tim Richter
arXiv categories: cs.LO

We argue that simple conceptual models of the relation between short-term efforts in climate mitigation and adaptation policies (STECM&AP) and possible climate damages can help understanding the difficulties of increasing public support for a transition towards sustainable, decarbonized economies. Specifically, we show that, under fairly general conditions, mistrust and pessimism tend to polarize support for either minimal ``business as usual'' policies or maximal ``all-in climate mitigation efforts'' choices. Under the same conditions, trust and optimism tend to de-polarize societies towards moderate climate mitigation and adaptation (CM&A) policies and promote social consensus. If the relation between short-term efforts and possible climate damages can be quantified via empirical or model data, Pareto climate economics can be applied to extend these conceptual models and support climate decision making with trustable computational methods.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-10-31T23:56:31Z
Reza Sameni
arXiv categories: cs.SE, cs.DL, cs.PL

The WFDB format is widely used to store and exchange physiological waveforms and annotations. However, existing software implementations are limited to C, Python, and MATLAB/Octave, can produce different results in corner cases and checksum calculations, and have defaults such as sampling frequency and gain, that can lead to silent misinterpretation of recordings. We developed WFDB-x, a cross-language, performance-optimized reimplementation of WFDB in seven programming languages, with extensive unit tests, to provide consistent WFDB processing across programming languages. We reimplemented the WFDB Software Package 10.7.0 natively in Python, C++, Rust, Julia, R, MATLAB/Octave, and Kotlin, using AI-assistance under human direction and review. Each implementation has library functions, a high-level interface, and command-line tools. We compared their outputs with those of the original C programs using 1098 conformance cases, 877 legacy-mode cases, unit tests, and differential fuzzing. Deliberate changes remove implicit waveform parameters, restrict file and network access, and prevent annotation loss. A legacy mode retains the original behavior. All seven implementations passed every conformance and legacy-mode case on the tested Linux platform, with matching outputs. The unit tests contain 9353 assertions. C++, Rust, and Julia read records 1.5-6.9 times faster than the original C library, while the Python implementation wrote records 9.2 times faster than the existing wfdb-python library in the benchmark. WFDB-x provides a tested, open-source basis for reading and writing physiological recordings consistently across seven languages, supporting reproducible research and software development without requiring a shared programming environment. We also share details of the AI-assisted development process and token utilization, which may be useful for other applications.

arXiv abstract · PDF

Miscellaneous · primary corpus · published 2026-11-01T01:50:46Z
Theadora Fields Collin, Oded Stein, Gilbert Bernstein, Saman Amarasinghe
arXiv categories: cs.MS, cs.GR, cs.PL

Finite element methods (FEMs) are a powerful and ubiquitous tool for solving engineering problems. Experimenting with different finite elements can improve the quality and efficiency of solutions. In some cases, the wrong (but nonetheless most common) choice of finite element will produce solutions which converge to the wrong answer regardless of mesh resolution. However, in practice, the choice of finite element is not explored due to the complexity of re-deriving and re-implementing finite element methods. Trying a new finite element is challenging because practitioners must manually deduce formulas to use these elements and implement them within a potentially complex system. We address this problem by introducing ElementForge, a finite element system that is parametric over the literate mathematical specification of a finite element in a domain-specific language (DSL). The ElementForge compiler reasons about tensor spaces, tensors, and tensor bases from first principles to derive implementations of finite elements. The ElementForge compiler is able to automatically derive implementations of finite elements previously only derived by hand. Further, ElementForge minimally couples several key mathematical concepts, mainly tensor fields, mesh topologies, sparse tensors, and assembled finite element operators, to produce a complete finite element system that is parametric over the choice of element. Consequently, the elements derived by the compiler can be applied parametrically to new meshes, PDEs, and boundary conditions. We evaluate our system by implementing several simulations with different finite elements, demonstrating that our system can explore tradeoffs in generality, accuracy, speed, and representational complexity. For example, we are able to implement the Morley, Bell, Argyris, and Hermite like elements with less than 50 lines of code and use them all in a single simulation.

arXiv abstract · PDF