跳到正文
研踪PaperTrail

YOUR RESEARCH, IN SIGHT

让下一篇重要论文，不再错过。

覆盖计算机全学科，以 AI 为快捷入口。关注方向、作者和关键词，把发现变成持续的研究积累。

部分采集异常
正在读取账号与研究记录…

全站更新概况

+0新增论文
+0其中 AI 相关
+1已有论文修订
+100新增 AI 导读

arXiv 最近完成扫描：2026-11-08 22:53 · 全站最近入库：2026-11-08 06:02各信源进度 →

统计口径与数据新鲜度

统计 2026-11-07 23:10 — 2026-11-08 23:10（北京时间） · 点击数字查看对应简报；AI 相关包含在新增论文内。

最近完成检查：2026-11-08 22:53最近发现新增版本：2026-11-08 06:02库内论文最新更新时间：2026-11-06 02:59

每分钟刷新已保存的数据。空检查不代表采集异常；新收录可能包含历史论文。AI 导读按新增版本计数。

17,100 已收录论文14,661 AI 相关4,057 有修订112 HF 社区发现

浏览论文库

研究日报 / 周报 →按信源浏览 →

时间范围跟随排序：版本更新、本站收录或首次发表。最新收录可能包含历史论文。部分信源异常，查看状态 →

找到 181 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-08 22:48（北京时间）
版本更新 · v3arXiv:2603.04530

Complete Diagrammatic Axiomatisations of Relative Entropy

Ralph Sarkis, Fabio Zanasi

原文摘要

Relative entropy is a fundamental class of distances between probability distributions, with widespread applications in probability theory, statistics, and machine learning. In this work, we study relative entropy from a categorical perspective, viewing it as a quantitative enrichment of categories of stochastic matrices. We consider two natural monoidal structures on stochastic matrices, given by the Kronecker product and the direct sum. Our main results are complete axiomatisations of Kullback-Leibler divergence and, more generally, of Rényi divergences of arbitrary order, for each such structure. Our axiomatic theories are formulated within the framework of quantitative monoidal algebra, using a graphical language of string diagrams enriched with quantitative equations.

cs.LO · cs.IT · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2605.00812

Univalence without function extensionality

Evan Cavallo, Jonas Höfer

原文摘要

It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of the univalence axiom, asserting that the wild category formed by the universe is univalent, which we call categorical univalence. We show that categorical univalence does not imply function extensionality by an analysis of Von Glehn's polynomial model construction, which produces models of Martin-Löf type theory that always refute function extensionality. We find in particular that when the base model has a univalent universe, its polynomial model has a universe that is categorically univalent but lacks function extensionality.

cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2601.00312

Quantifier Elimination Meets Treewidth

Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan

原文摘要

In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth, a parameter that measures the graph's tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.

cs.LO · cs.CC · cs.SC

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2605.17112

A unification of graded and substructural logics

Peter Hanukaev, Harley Eades

原文摘要

Type systems which account for resource sensitive computations can generally be split into two styles: First, substructural logics such as Linear Logic which seek to restrict weakening and contraction and reintroduce them in a controlled manner; And second, graded systems which allow weakening and contraction by default, but track the use of variables quantitatively in some algebraic structure -- usually a semiring. We present GRASS (Graded and substructural), a type system which incorporates mechanisms from both of these approaches, thus allowing maximally flexible control over variable usage. Furthermore, GRASS allows grades from an arbitrary collection of grade algebras to coexist in the same system, thus allowing different variables to be controlled with respect to different notions of resource within the same program. We develop the categorical semantics of GRASS, and find that, on the level of categorical semantics, it subsumes multiple established systems such as LNL, Adjoint Logic, and mGL.

cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2610.03550

Counterexamples to the Strong Roberson Conjecture

Arnar Á. Kristjánsson

原文摘要

We refute the Strong Roberson Conjecture, which asserts that adding any graph outside a graph class closed under minors and disjoint unions strictly increases the distinguishing power of homomorphism counts from that class. More precisely, we construct connected graphs $H$ for which homomorphism counts from graphs excluding $H$ as a minor determine the number of homomorphisms from $H$ to any target graph. We also refute the analogous conjecture with immersions in place of minors. The proof introduces a method for deriving exact homomorphism count dependence from modular equivalences. We obtain these modular equivalences for infinitely many primes using prime-order automorphisms and the corresponding orbit quotients. We complete the refutations by proving that suitable circulant graphs with two jump lengths and related cubic bipartite graphs exclude their corresponding orbit quotients as minors and immersions, respectively.

math.CO · cs.DM · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2603.14955

Convex algebras on an interval with semicontinuous monotone operations

Ana Sokolova, Harald Woracek

原文摘要

In a recent work of Matteo Mio on compact quantitative equational theories (here compact means that all its consequences are derivable by means of finite proofs) convex algebras on the carrier set [0,1] whose operations are monotone and satisfy certain semicontinuity properties occurred. We fully classify those algebraic structures by giving an explicit construction of all possible convex operations on [0,1] possessing the mentioned properties. Our result thus describes exactly the range of theories to which Mio's theorem applies.

cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.26778

An Exponential Succinctness Gap between Three-Variable Logic and the Calculus of Relations

Yuya Uezato, Yoshiki Nakamura

原文摘要

Three-variable first-order logic ($\mathrm{FO}^3$) and the calculus of relations (CoR) define the same binary queries, an equivalence that goes back to Tarski's work in the 1940s. The classical translation from $\mathrm{FO}^3$ to CoR is single-exponential, but it has remained open whether this blowup is necessary. We prove that it is, even over finite structures and even for circuits that share subterms. Our proof introduces a new technique: we modify a single finite structure in exponentially many local ways, each changing the answer of a short $\mathrm{FO}^3$ formula $\varphi$. In any CoR circuit $C$ equivalent to $\varphi$, only compositions of binary relations can notice these modifications, and each composition can notice at most two; thus, $C$ requires exponentially many compositions. The same technique gives an exponential succinctness gap between $\mathrm{FO}^3$ and $\mathrm{FO}^2$, and exponential lower bounds for matrix query languages over the Boolean and tropical semirings, where the analogous question was also open.

cs.LO · cs.CC

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.21009

Robustness Analysis via Horofunction Compactification

Harrison Bennett, Amin Farjudian

原文摘要

Robustness analysis plays a central role in the verification and design of computational and hybrid systems, particularly when system behaviour depends continuously on parameters subject to perturbation. Existing domain-theoretic frameworks provide a principled foundation for reasoning about such perturbations via monotone maps on lattices of closed sets. However, these frameworks face significant limitations when the underlying state space is not locally compact, as is the case for the infinite-dimensional spaces that arise in analysis, machine learning, and control theory (e.g., $\ell_p$ and $L_p$ spaces). In these settings, the lattice of closed subsets fails to be continuous, and classical compactifications either sacrifice precision or lack computable structure. We propose Gromov's horofunction compactification as a new tool for robustness analysis over a class of separable metric spaces of practical importance, including separable reflexive Banach spaces. Given a metric space $\mathbb{S}$, we show that its horofunction extension yields a compact metric space together with a Lipschitz embedding, which enables robust approximations of monotone maps via Scott-continuous maps on the compactified domain. For separable spaces, the horofunction compactification is metrizable, which provides a path toward effective domain-theoretic constructions.

cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.22551

The category of nominal sets is locally monoidal closed

Fahimeh Bayeh, Peng Fu, Peter Selinger

原文摘要

The category Nom of nominal sets was proposed by Pitts and Gabbay as a setting for the semantics of abstract syntax with variable bindings. It is well-known that Nom is a topos, also known as the Schanuel topos, and in particular it follows that Nom is locally closed, i.e., every slice category Nom/X is cartesian-closed. In this paper, we show that Nom has a much stronger property: every monoidal (closed) structure on Nom induces a monoidal (closed) structure on all slice categories Nom/X. One monoidal closed structure of particular interest on Nom is the separated product A * B, whose right adjoint A -* B is called the separated function space. In particular, it follows that Nom is locally separatedly closed.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2603.18321

A Simple Categorical Calculus of Interacting Processes

Chad Nester, Niels Voorneveld

原文摘要

We present a calculus that models a simple sort of process interaction. Our calculus consists of a collection of terms together with a rewrite relation, parameterised by an arbitrary multicategory whose morphisms we understand as non-interactive processes. We show that our calculus is confluent and terminating, and that terms modulo the induced convertibility relation form a virtual double category. We relate our calculus to the free cornering of a monoidal category, which is a double-categorical model of process interaction that is similar in spirit to the calculus presented herein. Precisely, we construct a functor from the virtual double category given by our calculus into the underlying virtual double category of the free cornering of the free monoidal category on the multicategory of non-interacting processes. If we think of the terms of our calculus as programs and the rewriting system as an operational semantics for these programs, this functor gives a sound denotational semantics for our calculus in terms of the free cornering.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2603.16375

Monoidal categories graded by partial commutative monoids

Matthew Earnshaw, Chad Nester, Mario Román

原文摘要

Effectful categories have two classes of morphisms: pure morphisms, which form a monoidal category; and effectful morphisms, which can only be combined monoidally with central morphisms (such as the pure ones), forming a premonoidal category. This suggests seeing morphisms of an effectful category as carrying a grade that combines under the monoidal product in a partially defined manner. We axiomatize this idea with the notion of monoidal category graded by a partial commutative monoid (PCM). Monoidal categories arise as the special case of grading by the singleton PCM, and effectful categories arise from grading by a two-element PCM. Further examples include grading by powerset PCMs, modelling non-interfering parallelism for programs accessing shared resources, and grading by intervals, modelling bounded resource usage. We show that effectful categories form a coreflective subcategory of PCM-graded monoidal categories; introduce cartesian structure, recovering Freyd categories; and describe PCM-graded monoidal categories as monoids by viewing a PCM as a thin promonoidal category.

cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2610.10789

An explicit shuffle construction of the homotopy span model of differential linear logic

Paul-André Melliès, Federico Olimpieri, Lionel Vaux Auclair

原文摘要

We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of small categories equipped with its natural model structure. Following the principles of homotopy theory, the formulas and proofs of linear logic are interpreted in the model as small categories up to categorical equivalence, the notion of weak homotopy equivalence underlying the natural Quillen model structure on Cat. Here, we explain how the original interpretation of proofs as fibrant spans can be replaced by a more liberal interpretation of proofs as separately fibrant spans. This relaxation from fibrant spans to separately fibrant spans enables us to give a simple and intuitive description of the homotopy span model, where the axiom and cut links are interpreted as identity spans, and where the symmetries of the exponential modality are captured by a shuffle structure on the interpretation of proofs.

cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2610.13201

Compact Quantitative Equational Theories as Monad Restrictions

Matteo Mio, Colin Riba

原文摘要

Proofs in quantitative algebra are, generally, infinite objects due to the presence of infinitary rules in the deductive apparatus. A quantitative equational theory is called compact if all its consequences are derivable by means of finite proofs, that is, proofs not using any instances of the infinitary rules. This definition is purely logical. In this work we give an equivalent, but categorical, characterisation based on the notion of monad restriction.

cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.37815

Concurrent Strategies as Street Fibrations

Hugo Paquet, Glynn Winskel

原文摘要

Concurrent games and strategies based on event structures are an established and expressive model of interactive computation. In this paper we revisit the problem of equipping this model with symmetry. Symmetry is essential for many applications, but it is also a source of mathematical complexity, not least because strategies with symmetry can be compared up to several distinct notions of equivalence. Our first contribution is a complete characterization of two classes of strategies for which composition admits an identity. For these two classes the identity laws hold, respectively, up to a "weak" and a "strong" notion of equivalence. The main result is that the weak class of strategies corresponds precisely to those inducing Street fibrations over the game. We also show how the established "thin" approach to symmetry also fits in this general framework. A second contribution is a formal connection between games and setoid-valued profunctors. This follows a long tradition of relating games and relational models, but here additionally includes a very general model of symmetries. Our characterization of strategies as Street fibrations makes the connection to profunctors significantly easier to establish.

cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2511.02386

Monadic Second-Order Logic of Permutations

Vít Jelínek, Michal Opler

原文摘要

Permutations can be viewed as pairs of linear orders, or more formally as models over a signature consisting of two binary relation symbols. This approach was adopted by Albert, Bouvel and Féray, who studied the expressibility of first-order logic in this setting. We focus our attention on monadic second-order logic. Our results go in two directions. First, we investigate the expressive power of monadic second-order logic. We exhibit natural properties of permutations that can be expressed in monadic second-order logic but not in first-order logic. Additionally, we show that the property of having a fixed point is inexpressible even in monadic second-order logic. Secondly, we focus on the complexity of monadic second-order model checking. We show that there is an algorithm deciding if a permutation $π$ satisfies a given monadic second-order sentence $\varphi$ in time $f(|\varphi|, \operatorname{tw}(π)) \cdot n$ for some computable function $f$ where $n = |π|$ and $\operatorname{tw}(π)$ is the tree-width of $π$. On the other hand, we prove that the problem remains hard even when we restrict the permutation $π$ to a fixed hereditary class $\mathcal{C}$ with mild assumptions on $\mathcal{C}$.

math.CO · cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v7arXiv:2504.08509

The Complexity of Generalized HyperLTL with Stuttering and Contexts

Gaëtan Regaud, Martin Zimmermann

原文摘要

We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is $Σ_1^1$-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the $Σ_0^1$-complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.

cs.LO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.03174

Final coalgebras over R-modules

Oisín Flynn-Connolly, Henning Basold, Chase Ford

原文摘要

Final coalgebras and the coinduction principle for coalgebras over $R$-modules, where $R$ is a commutative ring, are essential in determining the denotational behaviour of various types of linear weighted automata. The goal of this paper is to provide lower and upper bounds on the ordinals that are needed to construct final coalgebras over $R$-modules as the limit of a transfinite sequence of functor iterations. We give an example of a binary intersection preserving finitary functor on the category of abelian groups, which is the category of modules over integers, that fails to converge in $ω\cdot 2$ steps, thus settling an open problem of Adámek, Milius, and Moss. Then we relate this to the failure of the Artinian property of the integers and show that all finitary functors on $R$-modules for a Noetherian ring $R$ with Krull dimension $n$, which preserve countable directed intersections and a generalised notion of monomorphism, converge in $ω\cdot (n + 2)$ steps. We also establish how the connection between Aczel-Mendler bisimulation and behavioural equivalence is mediated by the functor $\operatorname{Ext}^1$. These results show that homological algebra tools can play an important role in coalgebra.

cs.LO · math.AC · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2610.38281

A Witnessing Duality for ReLU Network Depth

Dimitrios Myrisiotis

原文摘要

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.

cs.CC · cs.LG · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v7arXiv:2412.04970

CMSO-transductions for tree-like graph decompositions

Rutger Campbell, Bruno Guillon, Mamadou Moustapha Kanté, Eun Jung Kim, Noleen Köhler

原文摘要

We give $\operatorname{CMSO}$-transductions that, given a graph $G$, output its modular decomposition, its split decomposition and its bi-join decomposition. This improves results by Courcelle [Logical Methods in Computer Science, 2006] who gave such transductions using order-invariant $\operatorname{MSO}$, a strictly more expressive logic than $\operatorname{CMSO}$. Our methods more generally yield $\operatorname{C}_2 \operatorname{MSO}$-transductions that output the canonical decompositions of weakly-partitive set systems and weakly-bipartitive systems of bipartitions.

cs.LO · cs.CC · cs.DM · cs.FL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2610.40025

One Polynomial Field for Every Euler Step and the Flow: Polynomial Dynamics for P and PSPACE

Olivier Bournez

原文摘要

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.

cs.CC · cs.LO · math.DS

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.02971

Propositional Dynamic Logic with Program Costs

Krishna Manoorkar, Wolfgang Poiger

原文摘要

We introduce $\mathbb{N}\mathtt{PDL}$, a resource-aware variant of Propositional Dynamic Logic ($\mathtt{PDL}$) capable of accounting for program costs measured by natural numbers (such as time or space in the sense of computability theory). In this framework, programs correspond to transition systems weighted by extended natural numbers, and the syntax of our logic includes formulas expressing which properties are reachable by program executions within specific cost constraints. First, we explain how the standard program constructs of non-deterministic choice, sequential composition, iteration, and tests are interpreted in this weighted setting and establish the validity of their corresponding reduction axioms. Using an appropriate adaptation of the (Fischer-Ladner) filtration technique, we proceed to prove decidability and completeness for $\mathbb{N}\mathtt{PDL}$ as our main results. We furthermore provide upper and lower complexity bounds for this logic using translations between standard $\mathtt{PDL}$ and $\mathbb{N}\mathtt{PDL}$.

cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2509.04192

Domain size asymptotics for Markov logic networks

Vera Koponen

原文摘要

A Markov logic network (MLN) $\mathbb{M}$ determines a probability distribution $\mathbb{P}_n^\mathbb{M}$ on the set $\mathbf{W}_n$ of structures, or ``possible worlds'', with domain $\{1, \ldots, n\}$. We study the properties of such distributions as $n$ tends to infinity. We show that with mild assumptions on an MLN $\mathbb{M}$ with one soft constraint with an arbitrary positive weight the distribution $\mathbb{P}_n^\mathbb{M}$ will behave quite differently from the uniform distribution $\mathbb{P}_n^{uni}$ on $\mathbf{W}_n$ for all sufficiently large $n$. For a language with only one relation symbol $R$ which has arity 1 we give an almost complete characterization of the possible asymptotic behaviours of $\mathbb{P}_n^\mathbb{M}$ as $n \to \infty$, where $\mathbb{M}$ may be any MLN for this language. The asymptotic behaviour depends on the soft constraints and weights of the MLN. This characterization is used to show that if the language under consideration contains at least one relation symbol of arity 1 then the following holds: (a) There is an MLN $\mathbb{M}$ such that for every lifted Bayesian network (LBN) $\mathbb{G}$ there are infinitely many $n$ such that $\mathbb{M}$ and $\mathbb{G}$ determine different distributions on $\mathbf{W}_n$. (b) There is an LBN $\mathbb{G}$ such that for every MLN $\mathbb{M}$ there are infinitely many $n$ such that $\mathbb{G}$ and $\mathbb{M}$ determine different distributions on $\mathbf{W}_n$. We also show that, in the limit, the weight dimension and the domain size dimension may behave completely differently.

cs.AI · cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.02849

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System

Qian Cheng, Ruize Tang, Saad Mohammad Rafid Pial, Zhizhen Cathy Cai, Yiming Su, Jackson Clark, Munim Thahmid, Mahdiya Rahman Sukanya 等 16 位作者

原文摘要

TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of complex system specifications requires discovering inductive invariants, reasoning about intricate state transitions, and decomposing proofs into tractable obligations. TLAPS-Bench provides a proof harness that supports iterative proof development atop the TLA+ Proof System (TLAPS), where agents are equipped with proof tools and libraries, with safeguards against reward hacking. Using the harness, we have employed AI agents to prove desired properties for important system specifications that were not proved before, spanning cache coherence, Byzantine consensus, and write-ahead logs. TLAPS-Bench contains 265 proof targets (each encodes a property to prove) from 95 TLA+ specifications of real-world systems. We evaluated frontier AI agents, represented by Codex with GPT models, on a subset of 70 proof targets across 12 specifications. The highest-scoring model, GPT-6.1 Sol (max), proved 31 (44.3%) proof targets. The results show challenges and opportunities in end-to-end proof development.

cs.AI · cs.DC · cs.LO · cs.SE

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.02843

Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations

Jiaxin Xie, Guowei Dou, Xiang Ji, Wensheng Yu

原文摘要

Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning. With the development of large language models (LLMs) and interactive theorem provers, intelligent agents offer a promising approach to automating the formalization of mathematical theories. This paper presents the Math Foundation Formalization Agent (MFF-Agent), a general-purpose intelligent agent designed to support formalization tasks across multiple mathematical domains. The agent integrates the reasoning capabilities of large language models with the formal verification capabilities of the Rocq proof assistant. It incorporates task classification, tool-assisted execution, verification feedback, and state-based task management to support the generation, refinement, and verification of formal proofs. Unlike an approach focused on a single mathematical theory, the agent is examined through case studies involving Morse--Kelley axiomatic set theory (MK), real numbers, propositional logic, and equivalences of the axiom of choice. These cases investigate its applicability across mathematical foundations and distinguish source-level completion, interactive verification, and reproducible compilation. The results demonstrate the feasibility of a unified operational framework for heterogeneous foundation-level tasks and clarify the gap between such a framework and a fully integrated mathematical foundation.

cs.LO · cs.AI

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.02840

Iterated Narrow Networks: Turing Completeness at Width 4 on Convex Input Spaces and the Complexity of Verification

Olivier Bournez, Johanne Cohen, Adrian Wurm

原文摘要

We study the iterates of a fixed ReLU network $N$ of width 4, that is, the discrete-time system $x_{k+1} = N(x_k)$ on $[0,1]^4$. Equivalently, $x_k$ is the output of a weight-tied network made of $k$ copies of $N$, or of a recurrent network with no external input, started at $x_0$. We prove that every deterministic Turing machine $M$ admits such a network $N_M$. The network can be constructed in polynomial time from $M$. Each iteration has depth $\mathrm{poly}(|M|)$. The iterates of $N_M$ simulate $M$ exactly on every encoded tape. The number of iterations is proportional to the running time of $M$. Moreover, the fourth coordinate irreversibly flags every point of the convex cube $[0,1]^4$ whose simulation reads an invalid digit. This flag is the certificate that makes hardness reductions sound on convex input regions, the regime of practical verifiers. Convex regions were previously inaccessible because of a continuity obstruction inherent to ReLU networks. The correspondence has three consequences. First, reachability for iterated width-4 ReLU networks spans the full complexity hierarchy along the single axis of the time bound: it is NP-complete for a unary bound, NEXP-complete for a binary bound and RE-complete (undecidable) with no bound. Second, two extra neurons of width suffice to extend the hardness to every common smooth activation: at width 6, the robust verification problem (a promise problem with $δ/2δ$ gap) is NP-complete for $\tanh$, sigmoid, GELU, Swish, ELU, and any polynomial-time-computable continuous non-polynomial activation with a polynomial-time-computable Lipschitz constant. Third, the whole spectrum transfers to discretized Neural ODEs in dimension 5.

cs.LG · cs.CC · cs.LO · cs.NE

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2603.25710

Stone Duality for Monads

Richard Garner, Alyssa Renata, Nicolas Wu

原文摘要

We introduce a contravariant idempotent adjunction between (i) the category of ranked monads on $\mathsf{Set}$; and (ii) the category of internal categories and internal retrofunctors in the category of locales. The left adjoint takes a monad $T$-viewed as a notion of computation, following Moggi-to its localic behaviour category $\mathsf{LB}T$. This behaviour category is understood as "the universal transition system" for interacting with $T$: its "objects" are states and the "morphisms" are transitions. On the other hand, the right adjoint takes a localic category $\mathsf{LC}$-similarly understood as a transition system-to the monad $Γ\mathsf{LC}$ where $(Γ\mathsf{LC})A$ is the set of $A$-indexed families of local sections to the source map which jointly partition the locale of objects. The fixed points of this adjunction consist of (i) hyperaffine-unary monads, i.e., those monads where term $t$ admits a read-only operation $\bar{t}$ predicting the output of $t$; and (ii) ample localic categories, i.e., whose source maps are local homeomorphisms and whose locale of objects are strongly zero-dimensional. The hyperaffine-unary monads arise in earlier works by Johnstone and Garner as a syntactic characterization of those monads with Cartesian closed Eilenberg-Moore categories. This equivalence is the Stone duality for monads; so-called because it further restricts to the classical Stone duality by viewing a Boolean algebra $B$ as a monad of $B$-partitions and the corresponding Stone space as a localic category with only identity morphisms.

cs.LO · cs.PL · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2607.11352

Cover Semantics for Intuitionistic Modalities

Nachiappan Valliappan

原文摘要

Intuitionistic modal logic (IML) has inspired several developments in programming languages including modal type systems for staging, computational effects and language-based security. IMLs are typically studied using Kripke-style relational semantics, which simplifies proofs of meta-theoretic properties, such as completeness and consistency, by making it easy to construct models. Kripke-style relational semantics, however, relies upon classical reasoning principles, which makes it unappealing from a computational perspective and unsuitable for formalization in a constructive type theory. Goldblatt provides an alternative semantics for IMLs by extending Beth-Kripke-Joyal-style "cover" semantics for intuitionistic propositional logic with relations to support modalities. Goldblatt's "relational cover" semantics overcomes classical reasoning but introduces a new limitation: it relies upon a "modal localization" condition that restricts the class of models and complicates model construction. Goldblatt bypasses this restriction by using intricate order-theoretic completion arguments to prove completeness. In this article, we present a conservative extension of relational cover semantics that alleviates this restriction and is amenable to simpler and standard model construction techniques. We formalize our semantics in Agda and prove completeness constructively in the style of Normalization by Evaluation for a variety of IMLs featuring independent box and diamond modalities.

cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.02285

Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale

Jason Hickey

原文摘要

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.

cs.SE · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2602.03550

Formal Evidence Generation for Assurance Cases for Robotic Software Models

Fang Yan, Simon Foster, Ana Cavalcanti, Ibrahim Habli, James Baxter

原文摘要

Robotics and Autonomous Systems are increasingly deployed in safety-critical domains, so that demonstrating their safety is essential. Assurance Cases (ACs) provide structured arguments supported by evidence, but generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve. We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow. The approach addresses three challenges: systematically deriving formal assertions from natural language requirements using templates, orchestrating multiple formal verification tools to handle diverse property types, and integrating formal evidence production into the workflow. Leveraging RoboChart, a domain-specific modelling language with formal semantics, we combine model checking and theorem proving in our approach. Structured requirements are automatically transformed into formal assertions using predefined templates, and verification results are automatically integrated as evidence. Case studies demonstrate the effectiveness of our approach.

cs.SE · cs.FL · cs.LO · cs.RO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.02142

Homomorphisms on a product of free convex semilattices

Ana Sokolova, Harald Woracek

原文摘要

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 $Φ$ of $\mathcal FI\times\mathcal FJ$ into $X$.

cs.LO

查看论文
arXiv ↗PDF ↗