跳到正文
研踪PaperTrail

论文库

检索计算机领域论文，按研究方向、作者或关键词筛选。

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

全站更新概况

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

arXiv 最近完成扫描：2026-11-15 00:32 · 全站最近入库：2026-11-14 15:09各信源进度 →

统计口径与数据新鲜度

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

最近完成检查：2026-11-15 00:32最近发现新增版本：2026-11-14 15:09库内论文最新更新时间：2026-11-13 02:59

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

23,348 已收录论文19,580 AI 相关6,729 有修订112 HF 社区发现

浏览论文库

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

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

找到 259 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-15 00:30（北京时间）
新论文 · v1arXiv:2611.17127

分级交集类型

Graded Intersection Types

Rémy Cerda, Ugo Dal Lago

AI 速读 基于摘要

作者提出分级交集类型，用半环系数标记箭头域的多重集，统一幂等与非幂等交集类型，并给出保持归约与展开的代数条件。

cs.LO · cs.PL

arXiv ↗PDF ↗
查看原文摘要

We introduce graded intersection types, in which arrow domains are multisets of types with coefficients in a semiring. Boolean and natural number grades recover idempotent and non-idempotent intersection types. We give algebraic conditions on the semiring for subject reduction and expansion in finite systems and in locally finite systems with guarded infinite types. We construct a lifting to multisets of grades corresponding, in this general setting, to lifting the idempotent system to the non-idempotent one. We recall the main existing operational characterisations from the literature, and show some general extensions.

新论文 · v1arXiv:2611.17106

对称编程与推理的数学基础

Mathematical foundations for symmetric programming and reasoning

Ohad Kammar, Matija Pretnar

AI 速读 基于摘要

该文基于数学中“不失一般性”（w.l.o.g.）的证明原则，提出一种统一利用对称性的数学抽象，用于编程与推理。

cs.PL · cs.LO · math.CT · math.GR · math.LO

arXiv ↗PDF ↗
查看原文摘要

We develop a mathematical abstraction for uniformly exploiting symmetries in programming and reasoning based on the mathematical proof principle `without-loss-of-generality' (w.l.o.g.). Given: group actions that describe symmetries of the input and the output; and a canoniser, which captures how arbitrary inputs get sent to canonical ones, our construction extends any function from the canonical inputs to the whole domain. We characterise the conditions on the canonisers which guarantee that the construction gives the unique equivariant (i.e. symmetry-preserving) extension. Furthermore, we adapt the construction to a dependently-typed setting, where it captures traditional symmetric w.l.o.g. arguments via the Curry-Howard correspondence. Finally, we extend the construction to algebraic data types, where the symmetries of the constructors both uniquely determine the symmetries of the data type and pave the way for efficient execution.

新论文 · v1arXiv:2611.17084

Strategic disclosure and epistemic manipulation in extensive games

Sergei Artemov, Benjamin Prud'homme

原文摘要

In many strategic settings, agents can influence opponents by selectively disclosing truthful information about their own future actions. We introduce a game-theoretic framework to model this phenomenon. As a case study, we consider a two-player, alternating-move epistemic game in which Player A evaluates actions under a conservative maximin rule, while Player B-the manipulator-leverages this behavior by strategically revealing commitments. We prove that the manipulator can implement every inducible outcome using at most n disclosures in a binary game of depth 2n with n decisions per player. This establishes a sharp contrast between the game tree's exponential size and the linear amount of information required to control the outcome, highlighting a general mechanism by which limited information can exert disproportionate strategic influence.

cs.LO

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

The complexity of bisimilarity on pointmass processes

Martín Santiago Moroni, Pedro Sánchez Terraf

原文摘要

We assess the descriptive complexity of *bisimilarity* or "equality of behavior" on a family of Markov decision processes over uncountable standard Borel spaces, namely *nondeterministic labelled Markov processes* (NLMP). We show that bisimilarity is analytic for processes with a uniform assignment of finitely-supported measures to each state and label. More precisely, we obtain that bisimilarity on the space of countable Kripke frames (or labelled transition systems) is classifiable by countable structures. We show that bisimilarity of well-founded ("terminating") processes is Borel. We also provide a lower complexity bound by reducing the relation of eventual equality of binary sequences, $E_0$, to the former. As a consequence, there is no countable fragment of basic modal logic with denumerable conjunctions that characterizes bisimilarity for processes of small rank. We finally apply the previous Borel-definability to study the well-founded part of discrete uniform processes over continuous spaces.

cs.LO · math.LO

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

LLM-Assisted Verification in Dafny

Wieger Wesselink, Kees Huizing, Huub van de Wetering

原文摘要

Formal verification of complex algorithms requires expertise in program specification, invariant construction, mathematical proof, and the management of automated theorem provers. Although large language models (LLMs) can generate program code and proof fragments, reliably developing complete machine-checked verifications remains challenging: it requires an iterative process of constructing and validating specifications and invariants, building proofs, diagnosing solver failures, and optimizing verification performance. This paper presents a systematic ten-step workflow for LLM-assisted verification of scientific algorithms using the Dafny verification system. The workflow integrates algorithm formalization, contract development, empirical invariant validation, proof construction, bottleneck profiling, and resource-driven proof optimization. We applied the workflow using Antrhopic's Claude Opus 5 and Opus 5.5 models, combining LLM-driven development with automated testing and verification feedback, while retaining human oversight for correctness-critical decisions and strategic interventions. We evaluate the approach on 37 complex algorithms from graph theory and labelled transition systems. Notably, we verified the Hopfcroft-Tarjan triconnectivity test, demonstrating that even highly challenging algorithmic verification tasks can be carried out through a structured LLM-assisted workflow. Many of our machine-checked verifications were obtained within hours to a few days of interactive development. Our results suggest that LLM-assisted workflows can shift the role of the human verifier from detailed proof construction toward supervision, specification review, and strategic guidance.

cs.LO · cs.AI · cs.SE

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

Foundational Analysis Of The Solvability Complexity Index

Christopher Sorg

原文摘要

The Solvability Complexity Index (SCI) provides an extensional limit-height formalism for recovering a target map $Ξ$ from finite samples of an evaluation interface $Λ\subseteq\mathbb C^Ω$ by finite-height towers of pointwise limits. We first give a foundational analysis of what this extensional framework does and does not determine. In second place, we give a concrete non-trivial bridge result from a comparable SCI object to the well known limit rank of Weihrauch theory.

math.LO · cs.LO · math.SP

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

Selective Chaining of Parameterised Boolean Equation Systems

Jore J. Booy, Tim A. C. Willemse

原文摘要

Parameterised Boolean Equations Systems (PBESs) are used to verify properties of formal industrial models. We introduce a technique called selective chaining to simplify these PBESs by unfolding specific predicate variable instances when the unfolding results in a PBES that is likely to be simpler. For determining the latter we propose a set of heuristics. We show the formal correctness of the chaining operator and provide theoretical upper bounds using relevancy graphs on the size of the verification problem after chaining. Lastly, we study the effectiveness of our heuristics, showing that selective chaining can reduce memory usage and yield significant speed-ups solving PBESs that encode model checking problems for complex industrial systems.

cs.LO

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

Compact totally separated types

Martín Hötzel Escardó

原文摘要

Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The compact ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.

math.LO · cs.LO · math.GN

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

Propositional Dynamic Logic without tests does not have Craig Interpolation

Malvin Gattinger

原文摘要

It was shown recently by Borzechowski et al. (2026) that Propositional Dynamic Logic (PDL) has Craig Interpolation. Whether test-free PDL, i.e. PDL without the `?' operator, has interpolation remained open. Here we answer this question in the negative with a counterexample: a test-free PDL validity for which no test-free interpolant exists. The validity only uses one atomic program and the Kleene star, so it implies that the basic modal logic K extended with the reflexive transitive closure does not have interpolation, as previously shown by Studer (2009). The example was originally obtained using LLMs and Lean. We describe our methodology and provide links to all prompts, LLM output summaries as well as the Lean proof.

cs.LO · math.LO

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

Tracking relevance syntactically: A nested approach to weak relevant logic

Fabio De Martin Polo, Han Gao

原文摘要

The variable-sharing property (VSP) is regarded as a key feature of relevant logics, while the Craig interpolation property (CIP), formulated with respect to relevant implication, implies the VSP in constant-free propositional languages. However, to the best of our knowledge, no constant-free distributive relevant logic has previously been shown to enjoy the CIP. This absence of positive results has contributed to a widespread impression among relevant logicians that relevance and Craig interpolation are incompatible. In this work, we address this tension by proving that the negation-free fragment of base relevant logic B, denoted B+, enjoys both properties. Our proof is purely syntactic and is based on a novel nested sequent calculus featuring binary relevant blocks as primitive structural constructs. Unlike conventional nested sequent calculi, where unary nesting reflects the binary accessibility relation of Kripke semantics, our calculus employs a binary nesting operator that directly reflects the ternary relational structure of Routley-Meyer semantics for relevant logics. After establishing soundness and cut-free completeness of the calculus, we prove several meta-logical properties for the logic. Most notably, we provide the first syntactic proof of the VSP (along with a variety of its stronger variants) and the first proof of the CIP for B+, both derived directly from the cut-free system using a structural notion internalized within nested sequents.

cs.LO

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

ZFLean: a framework for set-level mathematics in Lean

Vincent Trélat, Matteo Pouillat

原文摘要

We present ZFLean, a Lean 4 library for doing core mathematics inside a model of ZFC with the ergonomics expected of typed Mathlib developments. Building on Mathlib's ZFC model, we contribute a relational calculus for sets with rewriting hints and small predictable tactics, canonical set-theoretic constructions -- Booleans, naturals, integers, sums/option -- and bridges between ZFC objects and Lean's native types enabling mixed set-level/typed proofs. The layer reduces boilerplate for extensional reasoning while remaining compatible with vanilla Mathlib. We discuss library organization and usage patterns that lower the friction of set-theoretic formalization in a dependently typed assistant. We demonstrate typical use of the framework with a case study exercising our constructions and relational calculus through a proof of an isomorphism theorem on curried functions.

cs.LO

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

Support is Search

Alexander V. Gheorghiu

原文摘要

For intuitionistic propositional logic, Sandqvist's base-extension semantics defines a support relation parametrised by atomic bases, with validity identified as support in every base. Sandqvist's completeness theorem answers the global question: which formulae are valid? This paper addresses the local question: given a fixed base, what does support in that base correspond to? We show that support in a fixed base coincides with proof-search in a hereditary Harrop logic program with a quantifier over atoms, via an encoding of formulae as logic programming goals. The encoding is a variant of the Russell-Prawitz translation of the connectives, with quantification restricted to atoms, and it is obtained by reading the semantic clauses in continuation-passing style. So read, the universal quantifiers over base extensions and atoms in those clauses need not range over a completed totality: they are eigenvariables under a standard freshness discipline. Base-extension semantics thereby acquires an explicit computational content: support is proof-search. The result complements Sandqvist's global theorem with a local correspondence and makes the constructive character of the framework explicit.

cs.LO · math.LO

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

Sound Automatic Lock Placement for Concurrent Programs with Pointers

Nicolas Waldburger, Florian Faissole, Ryo Okabe, Denis Cousineau

原文摘要

We propose a lightweight method for automatic lock placement in concurrent POSIX programs with explicit pointer manipulation, such as C programs. Given a program that lacks sufficient user-placed mutexes, or contains none at all, our method introduces new mutexes to prevent data races. The method is formally proven to guarantee the absence of data races and mainly consists of three steps. The first step performs lockset analysis and may-happen-in-parallel analysis. The second step conducts a concurrent points-to analysis derived from a Steensgaard-like procedural analysis, where per-thread points-to graphs are unified using a special completion rule. The final step places locks to prevent data races while respecting a lock ordering to avoid deadlocks. In addition, user-annotated critical sections are protected through insertion of dedicated locks. Since lock placement is a complex and error-prone task, our method aims at helping developers write correct concurrent programs.

cs.LO

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

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Tom de Jong, Nicolai Kraus, Axel Ljungström

原文摘要

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We show that all higher coherences can be stated and derived if simplicial type theory is taken to be homotopy type theory with a postulated interval type. In technical terms, this means that if a type has unique fillers for $(2,1)$-horns, it has unique fillers for all inner $(n,k)$-horns. This generalizes a result of Riehl and Shulman for the case $n = 3, k \in \{1, 2\}$. Our main technical tool is the Leibniz adjunction: the pushout-product is left adjoint to the pullback-hom in the wild category of types. While this adjunction is well known for ordinary categories, it is much more involved for higher categories, and the fact that it can be proved for the wild category of types (a higher category without stated higher coherences) is non-trivial. We make profitable use of the equivalence between the wild category of maps and that of families. We have formalized the results in Cubical Agda.

math.CT · cs.LO · math.LO

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

Strong Lyndon Interpolation for Multi-Modal Logics with Converses: A Constructive Approach with Tree Sequents

Tim S. Lyon

原文摘要

Grammar logics with converses are multi-modal logics that generalize tense logics and whose frame conditions are determined by context-free production rules. We study the strong Lyndon interpolation property (strong LIP) for these logics, which requires interpolants to respect both the polarities of propositional atoms and the indices of modalities. We show that the strong LIP properly strengthens the Lyndon interpolation property over grammar logics, since it fails for certain grammar logics with bridge axioms, i.e., path axioms relating modalities with distinct indices. We then prove that every bridge-free grammar logic, possibly extended with seriality axioms, has the strong LIP. This class includes the multi-modal tense logics obtained by imposing any combination of seriality, reflexivity, transitivity, symmetry, and Euclideanity on each pair of converse modalities. Our proof is constructive and purely syntactic, and is based on tree sequent calculi. Because standard methods for computing interpolants with tree and nested sequents may introduce modalities whose indices are not common to both sides of an implication, we introduce a novel tripartite partition method. It sorts the labels of a proof into common labels and labels private to the left or right component, and only lets relational atoms pointing to common labels contribute modalities to interpolants. Given a proof of an implication, our method computes a strong Lyndon interpolant together with proofs of its correctness.

cs.LO · math.LO

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

The Tiglath Pileser principle and models of persuasion

Willem Conradie, Krishna Manoorkar, Alessandra Palmigiano, Apostolos Tzimoulis, Nachoem Wijnberg

原文摘要

This paper develops a formal framework for analysing how agents extract reliable information from narratives and communicative interactions involving strategic deception. Building on Rubinstein and Glazer's models of persuasion, we introduce Tiglath-Pileser relations, a generalization of codex-based guidance relations, to formalize Baruch Halpern's Tiglath-Pileser principle: despite systematic bias, reported claims must retain a connection to the truth. We analyse these relations set-theoretically and axiomatically, identifying conditions for their successful application in persuasion. Our dynamic approach examines how such relations are formed, revised, and strategically manipulated, extending existing models beyond one-shot interactions. Two case studies, including a formal reconstruction of Halpern's interpretation of the biblical account of King David, illustrate the framework's application to historiographical reasoning. Combining logic, epistemic reasoning, and game theory, the paper provides an account of belief formation and truth approximation under partial information and strategic manipulation.

cs.LO

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

Does a Self-Learning Migration Agent Learn? An Audited Evaluation of Evidence-Graded Experience Memory for Oracle-to-PostgreSQL Migration

Oleg Grynets, Vasyl Lyashkevych, Valeriia Oliferuk, Vladyslav Babenko, Danylo Kovalchuk, Dmytro Kostetskyi

原文摘要

Do large language model (LLM) migration agents learn from accumulated experience, or do apparent gains reflect retrieval and reference reuse? We evaluate an evidence-graded agent for Oracle-to-PostgreSQL migration across four studies. On 1,833 documentation-derived source-reference pairs, persistent memory improved reference conformity (RC) over a no-memory baseline by 0.015 [0.004, 0.025], while policy adaptation added no gain (-0.004 [-0.010, 0.001]). An audit found that 264 of 367 held-out units (72%) shared a PostgreSQL reference with training, and the memory effect on the 103 leak-free units fell to 0.002 [-0.008, 0.011]. A model-free nearest-target copy baseline scored RC 0.222, outperforming all LLM systems (at most 0.163). A reference-grouped split reduced copying to 0.119; a rerun on 374 units in 118 independent target groups found no statistically distinguishable memory effect (0.005 [-0.003, 0.017]) and no policy effect. A separate Oracle-grounded evaluation on 216-224 real PL/SQL units showed that 10-22% of PostgreSQL-accepted units were behaviorally incorrect; a human-gated fix cycle increased demonstrably correct units from 98/216 to 167/224. A write-back study showed a 54% decline in retrieval margin as the knowledge base grew from 12 to 1,200 entries. We derive six evaluation rules that distinguish cross-task learning from reference leakage, copying, metric artifacts, and unstable feedback.

cs.LO · cs.DB · cs.SE

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

The multiplicative complexity of the three-bit low-half multiplier

Bshara Alhodali, Gregory Morse

原文摘要

We prove that the multiplicative complexity of the three-bit low-half multiplier is six, giving a structural, enumeration-free lower-bound proof valid against unrestricted nonlinear reuse in Boolean XOR-AND circuits. The value was previously established by SAT searches of the second author. An explicit six-AND circuit supplies the upper bound. The lower bound combines derivatives, quadratic products, complementary minors, and extraction modulo a Boolean ideal. Independent finite checks accompany the arguments. $\mathrm{MC}(M_3)=6$ is fully formalized in Lean 4. The kernel-checked proof uses only the axioms propext, Classical.choice and Quot.sound.

cs.CC · cs.LO · math.CO

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

k-partite quantum homomorphisms

Amin Karamlou

原文摘要

$k$-partite XOR games and linear binary constraint system (BCS) games arise from systems of linear equations over $\mathbb{Z}_2$, providing distinct quantum relaxations of the same classical constraint satisfaction problem (CSP). Linear BCS games have been generalised to synchronous homomorphism games on arbitrary relational structures, with compositional semantics provided by the quantum monad. We introduce $k$-partite homomorphism games, extending $k$-XOR games from linear systems to arbitrary relational structures. This yields a framework for studying multipartite quantum CSPs and quantum homomorphisms. We characterise perfect strategies in both the tensor-product and commuting-operator models as Kleisli morphisms of suitable state-dependent graded quantum monads on a category of $k$-partite relational structures. We then study quantum advantage in the pseudotelepathic sense: the existence of a perfect quantum strategy without a perfect classical strategy. We show that synchronous and $k$-partite quantum advantage are incomparable at the level of CSP instances. The GHZ instance admits three-player quantum advantage but no synchronous commuting-operator advantage, whereas the magic-square instance admits synchronous quantum advantage but no $k$-partite commuting-operator advantage for any number of players or proper colouring. We also exhibit an explicit six-element template whose CSP is NP-complete and admits two-player quantum advantage. Finally, we prove that no bounded-width CSP template admits $k$-partite quantum advantage, even in the commuting-operator model.

quant-ph · cs.LO

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

Bug Finding With Agentic Symbolic Execution

George Granberry, Wolfgang Ahrendt, Andy Gordon, Moa Johansson

原文摘要

Symbolic execution, in tools such as CrossHair for Python, is a powerful technique for finding bugs, but two barriers hinder its adoption: the human effort of annotating code with assertions, and the need to model the execution environment outside Python, such as an external database. To overcome both, we design an agentic harness that orchestrates the symbolic execution tool CrossHair together with an AI coding agent. Without human intervention, it instruments a repository with assertions, synthesizes a constraint-aware symbolic environment for the database, runs symbolic execution, and constructs a concrete test as evidence for each bug it reports. We evaluate our harness on 1,156,044 lines of Python code over 11 popular open-source Python web applications (Zulip, NetBox, Apache Superset, and others). With the synthesized environment, CrossHair executes 81% of the 5,406 contracted functions, against 4.5% without it. Our pipeline finds 1,050 bugs, each reproduced by a test against the unmodified application, 221 of them by CrossHair, and 312 of them are missed by a baseline in which the same LLM inspects the code. The two find different kinds of bugs: CrossHair's are mostly crashes on input-domain corner cases that validation admits, such as empty strings, missing fields and unusual characters, while inspection's are mostly bugs that produce wrong output. Our framework thus lets symbolic execution supplement inspection-based bug finding.

cs.SE · cs.AI · cs.LO · cs.SC

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

Initial Algebras, Well-Founded Coalgebras, and Kőnig's Lemma

Henning Urbat, Thorsten Wißmann

原文摘要

Kőnig's lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig's lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor $H$, and from the base category of sets to a locally finitely presentable category $\mathbb{c}$, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig's lemma states that, under mild assumptions on $\mathbb{C}$ and $H$, every well-founded coalgebra for $H$ is the directed join of its well-founded subcoalgebras with finitely generated state space -- in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig's lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor $H$: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.

cs.LO

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

DAISY: Fault-Guided Assertion Inference for Dafny

Álvaro Silva, Alexandra Mendes, Ruben Martins

原文摘要

Formal verification with Dafny provides strong correctness guarantees, but verification failures often require users to determine where helper assertions are needed and to manually write the assertions necessary for verification to succeed. This proof-engineering burden is difficult, time-consuming, and a barrier to the adoption of verification-aware languages. We present DAISY (Dafny Assertion Inference SYstem), a tool for fault-guided assertion inference in Dafny. Given a Dafny program and a target method, DAISY localizes likely assertion sites using verifier diagnostics, LLM-based localization, or their combination. It then annotates the program with assertion placeholders, retrieves relevant in-context examples, generates candidate assertions with an LLM, and validates candidates by running the Dafny verifier. To evaluate DAISY, we extend DafnyBench with verification-failing variants created by removing helper assertions from verified programs. The resulting benchmark distinguishes between programs with one missing assertion, two missing assertions, and all assertions removed, allowing us to evaluate DAISY on increasingly difficult proof failures. On this benchmark, DAISY verifies 86\% of programs with a single missing assertion and 36\% of programs with two missing assertions. These results show that fault-guided LLM assertion inference can repair many Dafny verification failures. They also show that successful repairs often differ from the original assertions, reducing proof-engineering effort without reconstructing the original proof.

cs.SE · cs.AI · cs.LO · cs.PL

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

Coinduction in Grounded Arithmetic

Bryan Ford

原文摘要

A grounded arithmetic counts a sentence 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 $ν$ 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 $ν$-body at its greatest fixed point, hence consistent; they agree with the least model where it has a value and prove sentences it leaves without one. The dichotomy trades the underivable hypothesis that an order is well-founded for the derivable one that its steps are decided, at the price of a change of model. With ground induction the dichotomy derives the omniscience rule of the sibling system OGA, so the system has no semantics whose certificates for universals are its own proofs; without the dichotomy it has one, though unsound for the least model. 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.

math.LO · cs.LO · cs.PL

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

Internal Reasoning and Consistency in Reflective Grounded Arithmetic

Bryan Ford

原文摘要

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic allowing direct expression of any general-recursive computation. Every RGA term is a program and truth is grounded evaluation, with a proof certificate at each universal quantifier. This paper shows, in a machine-checked Isabelle/HOL development, that such a system is powerful enough to carry out its own metamathematics. A fuel-indexed decider of RGA's grounded semantics and checkers for RGA's proofs are compiled primitive-recursive RGA terms. RGA proves internally that its decider never affirms 0 = 1, and that every well-formed term it affirms has an RGA proof accepted by a transparent test. RGA proves that, for each valid RGA proof, its conclusion is true. RGA proves that each grounded-true well-formed term is provable. RGA proves that no proof in either of two decided classes of RGA proofs derives 0 = 1. RGA's truth predicate also serves as a medium for proof by reflection, of the kind that adds nothing to the system. RGA derives disquotation for quantifier-free formulas as rules in every context, at a free variable, and proves, as one sentence, that whenever its normalizer for polynomials in one variable gives two terms the same normal form, the equation between them is true at every value of the variable. Each such polynomial identity then follows from that sentence by closed evaluation and disquotation, with no reflection rule. A companion paper proves Gödel's incompleteness theorems for RGA and its extensions.

math.LO · cs.LO · cs.PL

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

Typed Knowledge over Constructive Institutions: A Proof-Relevant Type Theory for Verified Science

Hans-Martin Will

原文摘要

Mathematical proof assistants such as Coq, Agda, and Lean 4 build proof irrelevance into definitional conversion ($p \equiv q$ for $p, q : P$ with $P : Prop$), erasing which derivation established a theorem. While natural for mathematics over fixed axioms, judgmental proof irrelevance is incompatible with verified scientific stores, which must inspect and compare independent derivations of the same claim to assess consilience and compute counterfactual retractions when an assay, reagent, or model is invalidated. Moreover, combining definitional proof irrelevance with subsingleton elimination breaks strong normalization and renders algorithmic conversion non-transitive. We present the type-theoretic and institutional foundations of Eigenius, a verified knowledge substrate for science. First, we formulate a dependent kernel with cumulative universes ($Prop, Set, Type_k$), impredicative $Prop$, inductive families with index-forced subsingleton elimination, and intensional identity types, where definitional equality $\equiv$ is untyped joinability under an orthogonal CRS and proof irrelevance is a witnessed propositional axiom ($irrel : ΠP{:}Prop.\,Πp,q{:}P.\,Id\,P\,p\,q$). Second, we unify universe cumulativity, codomain-covariant $Π$-subtyping, and ontology class inclusions in a coercion-free subsumption judgment whose bidirectional fragments ($\mathcal{K}_0, \mathcal{K}_1$) satisfy subject reduction and are sound and complete for declarative typing. Third, we organize external verifiers into a three-level institutional hierarchy with explicit axiom policies (Adopt, Discharge, Relativize), internalize a justification logic with Why-provenance semiring support $supp(j,P)$, and embed Cooper's Type Theory with Records (TTR) to type open-world knowledge graphs. Finally, we prove consistency in Grothendieck universes and mechanize the metatheory in Lean 4 with zero sorry axioms.

cs.LO · cs.AI · cs.CL

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

A Four-Valued Graph Model for Conflict Resolution: Core Framework and a Machine-Checked Formalization in Lean 4

Yukiko Kato

原文摘要

This note consolidates the core of the Quasi-Closed World Graph Model for Conflict Resolution (QCW-GMCR), which extends the standard Graph Model for Conflict Resolution with Belnap's four-valued logic to represent option-level epistemic ambiguity, and pairs the framework with a machine-checked Lean 4 formalization. QCW-GMCR combines: (1) FOUR-valued option assignments with compositional propagation to state-level feasibility; (2) graded reachability (definite, credible, possible) based on an FDE-inspired transition-warrant semantics, with definite reachability related to FDE consequence in the Boolean fragment; (3) axiomatized deterministic reductions from four-valued assessments to binary decisions, including four canonical operators reflecting distinct risk attitudes; and (4) catastrophe-avoiding equilibrium concepts with a quasi-closed-world safety invariant. A four-valued hypergame extension captures heterogeneous subjective assessments across decision makers. We state the core definitions and results and report the parts verified in Lean 4 with mathlib, including the classical GMCR stability hierarchy, algebraic and compositional properties of FOUR-valued conjunction, properties of the canonical reductions, and the graded reachability hierarchy. The formalization also helped identify and correct earlier claims, including a knowledge-monotonicity axiom replaced by truth monotonicity. This preprint provides a stable, citable record of the framework and its current formal verification status.

cs.LO

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

A Multi-Prover Interactive Protocol for Certification of Resolution Refutations

Philipp Czerner, Adrian Krauss, Josia Pietsch, Javier Esparza

原文摘要

A resolution refutation of a SAT-formula $\varphi$ is an independently checkable certificate proving that $\varphi$ is unsatisfiable. However, the refutations of $\varphi$ can be exponentially larger than $\varphi$. So, a verifier needs worst-case exponential time in the size of $\varphi$ to check their correctness. We present ResCertify, an interactive probabilistic protocol in which the verifier interacts with multiple independent, untrusted provers (MIP) to check the refutation with very low probability of error. The verifier runs in linear time in the size of $\varphi$. The provers require time $\mathcal{O}(n \cdot |Φ|)$, where $Φ$ is the resolution refutation and $n$ is the number of variables of $\varphi$. If they can be trusted to act as a multilinear oracle on certain queries, a single prover suffices, and the runtime can be improved to $\mathcal{O}(|Φ|)$. Finally, while the focus of our work is theoretical, we also report on a proof-of-concept implementation of ResCertify.

cs.LO

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

Exploring 3-CNF Formulas Generated From Partial Steiner Triple Systems

Wyatt Olson, Jared Soundy, J. Z. Schroeder

原文摘要

Steiner triple systems (STS) and subsets of these known as partial STS (PSTS) are combinatorial objects that have received substantial interest from mathematicians since their introduction in 1847. Over the last three decades, (P)STS have found applications in diverse fields ranging from digital circuit testing to wireless transmission. Perhaps unsurprisingly, the triple in (P)STS allows for a mapping to 3-conjunctive normal form (3-CNF) formulas, the Boolean formula used as input to 3-SAT. Prompted by this ready conversion of (P)STS to 3-CNF formulas and numerous real-world applications of (P)STS, we explore the intersection of (P)STS with 3-SAT and its counting version \#3-SAT. We explain the properties of (P)STS-generated 3-CNF formulas in terms familiar to the SAT community and experimentally compare them against randomly-generated 3-CNF formulas. We find that PSTS-3-CNF formulas are statistically distinct from randomly generated 3-CNF formulas, in both probability of satisfiability and expected solution count.

cs.LO · cs.DM · math.CO

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

一个极小直觉主义公开宣告逻辑

A minimal intuitionistic public announcement logic

Philippe Balbiani, Hans van Ditmarsch, Cigdem Gencer, Clara Lerouvillois

AI 速读 基于摘要

作者提出不要求传统合流条件的直觉主义公开宣告逻辑 Lmin 与 Lequ，并报告其相对于相应双关系框架类的可靠性与完全性。

cs.LO

arXiv ↗PDF ↗
查看原文摘要

We introduce intuitionistic public announcement logics Lmin and Lequ determined by classes of birelational frames where the intuitionistic preorder and the modal accessibility relation do not need to satisfy the confluence conditions traditionally considered within the framework of IPAL. Our logics can be seen as generalisations of IPAL seeing that their language is based on a binary epistemic modality of "relativised knowledge" that allows us to define valid reduction axioms. Our main results are the soundness and completeness of Lmin with respect to the class of all birelational frames and the soundness and completeness of Lequ with respect to the class of all birelational frames where the modal accessibility relation is an equivalence relation.

新论文 · v1arXiv:2611.14094

Wave-Domain Semantic ISAC: Holographic Surfaces as Analog Semantic Encoders for Integrated TN-NTN

Shadi Danesh, Pooria Salami, Hesaam Zaravashan, Abdulkadir Köse, Ayhan Akbas, Chuan Heng Foh, Mohsen Khalily

原文摘要

Semantic communication, near-field operation, and integrated sensing and communication (ISAC) are often considered separately in terrestrial and non-terrestrial networks (TN--NTN). We show how a large electromagnetic aperture can connect them. \textcolor{black}{Nonlocal metasurfaces and holographic apertures act on the spatial spectrum of an incident field and can execute linear projections, which form an early stage of semantic feature extraction, directly in the wave domain before digitisation, thereby reducing the corresponding digital processing burden.} Near-field focusing also provides position-dependent sensing features, allowing the aperture to serve as an analog semantic-ISAC front end on resource-constrained aerial and satellite platforms. We describe the underlying physics, the co-design of constrained analog projections with lightweight digital decoders, and a case study in which a data-adaptive projection outperforms a fully digital baseline in the simulated energy-limited regime while transmitting four times fewer coefficients and using 11.4 times fewer decoder MACs. Finally, we identify relevant 3GPP, ITU-R, and ETSI activities and the remaining standardisation gaps.

cs.LO

查看论文
arXiv ↗PDF ↗