https://arxiv.org/api/BHFzKUsnw9M6yOZVrL1JOtBG+jw 2026-07-21T23:17:16Z 19781 150 15 http://arxiv.org/abs/2607.05483v1 2026-07-06T16:13:56Z

Agentic workflows often operate over shared, structured state. Because LLM context windows are limited, each model invocation is typically shown only the state fragment needed for the current workflow step, a pattern commonly known as progressive disclosure. Modern systems construct such model-facing views using grep-like keyword search, retrieval-augmented generation (RAG), abstract-syntax-tree (AST) queries, and task-specific agent skills. These methods make the read side manageable, but they do not define when a locally proposed rewrite is valid after it is applied back to the full state. The missing piece is a contract between local updates and global validity. We introduce PatchOptic, an optic-inspired interface for shared-state LLM workflows. Optics are compositional bidirectional accessors that describe how views of structured data are read and updated. PatchOptic borrows this view/update intuition and realizes it through projected reads and verified structured patches. Each workflow step declares a projected read view, an authorized write region, and a patch-source region. Beyond runtime enforcement, the same declaration yields a path-level footprint that supports delegation, sub-workflow composition, and static certificates for reordering independent steps within the same phase. We evaluate this design with PatchBench, a benchmark with 46 cases across domains. The results show that projected reads reduce reported leakage and token cost while preserving accepted-output quality under the strong actor. Runtime verification blocks declared workflow-contract violations before commit, and patch-read enforcement rejects compromised patch artifacts that use hidden sources.

2026-07-06T16:13:56Z 24 pages, 13 figures, including appendix Zhaoyu Bai Jiaqi Cai http://arxiv.org/abs/2607.05251v1 2026-07-06T15:59:17Z

Neural network verification and data privacy are inherently in tension: verification demands full access to model parameters and input data, yet both are increasingly restricted by privacy regulations and intellectual property constraints. This tension has left robustness verification impractical in privacy-sensitive domains. In this work, we address this gap with SecureCROWN, the first framework for privacy-preserving neural network robustness verification. Built upon secure two-party computation (2PC), our framework enables a model owner and a data owner to jointly compute certified robustness bounds -- revealing only the final result while provably protecting both parties' private data under the semi-honest security model. A key challenge is securely computing the conditional operations in Linear Bound Propagation, where the data-dependent branching is incompatible with standard secure computation protocols. We eliminate branching by formulating conditional logic as continuous arithmetic operations. Additionally, we introduce a Newton--Raphson refinement method to improve numerical stability. Extensive analysis and experiments show that SecureCROWN strictly matches plaintext verification results, while completing in 0.1--200s across varied model sizes and communication settings (LAN/WAN), demonstrating the feasibility of privacy-preserving neural network verification.

2026-07-06T15:59:17Z Accepted by UAI 2026 Nianyun Song Xiaokun Luan Yu Guo Rongfang Bie Meng Sun Xiyue Zhang http://arxiv.org/abs/2607.05168v1 2026-07-06T14:49:15Z

Why do intelligent systems need to perform explicit symbolic reasoning? Computer science has traditionally regarded symbolic reasoning as a defining component of intelligence. Yet the remarkable success of modern foundation models raises a fundamental question: if increasingly capable AI systems can operate with little explicit symbolic reasoning, what role do symbolic methods actually play? This article argues that explicit symbolic reasoning is not a fundamental property of intelligence, but a computational consequence of operating on simplified models of reality. We propose the Compression Principle: every computational model is a simplified representation of reality, and explicit symbolic reasoning compensates for information omitted during model construction. From this principle, we derive the Modeling--Reasoning Trade-off: as computational models preserve richer representations of the world, the need for explicit symbolic reasoning correspondingly decreases. This perspective provides a unified explanation for both the historical success of symbolic methods and the remarkable effectiveness of modern foundation models. Paradoxically, the same development makes symbolic methods increasingly important for humans. As intelligent systems become more capable and more opaque, symbolic representations increasingly serve as interfaces through which humans specify requirements, verify behavior, regulate autonomous systems, and establish trust. We therefore argue that the future of symbolic methods lies not primarily as the computational engine of intelligent systems, but as the symbolic interface between increasingly capable AI systems and the humans who build, govern, and depend upon them.

2026-07-06T14:49:15Z Jun Sun http://arxiv.org/abs/2607.05126v1 2026-07-06T14:13:45Z

We investigate quantifier-free interpolation properties for several fragments generalising the extensional theory of arrays. Our results include the (general) quantifier-free interpolation properties of combinatory array logic with iterated diffs and the uniform interpolation property of the simple flat array fragment. To our knowledge, these are the first positive quantifier-free interpolation results obtained for theories of arrays featuring expressive specifications over unbounded domains.

2026-07-06T14:13:45Z Rodrigo Raya Christophe Ringeissen http://arxiv.org/abs/2607.05062v1 2026-07-06T13:32:51Z

Often, the easiest way to learn something is to have to use it for a purpose. This purpose can be playful: In 'Tempus fugit', the player takes on the role of a magician who has to defeat enemies by casting spells. The applicability of spells and enemy attacks depends on the truth of formulas in linear temporal logic with past with respect to a trace that the player gradually builds. So, whoever wants to save the realm from monsters has to learn to read logic formulas. This paper describes the small browser game and explains our design choices. We expose how game mechanics connect to linear temporal logic with past over finite traces, and how this can help players approach a daunting topic like formal logic.

2026-07-06T13:32:51Z To be presented at TEAL 2026 @ FLoC 2026 Benjamin Bisping Tobias Loch Mustafa Mohsen Alessio Nicolo Perna Maximilian Lukas Stamm http://arxiv.org/abs/2606.28639v2 2026-07-06T12:56:49Z

We establish the mathematical limits of AGI safety in two forms: verifying a fixed system, and verifying that a certified safety property persists once the system self-modifies. In the static case, no algorithm can certify a highly expressive AGI's safe behaviour infallibly, completely and tractably, whether over unbounded input domains (blocked by Rice's and Godel's theorems) or over all finite hardware configurations (blocked by Trakhtenbrot's theorem, which splits into a PSPACE-hardness barrier and a co-RE-completeness barrier), forcing a Soundness-Completeness-Tractability Trilemma as a structural, not statistical, necessity. In the dynamic case, we formalise self-modification as a computable transition operator and prove that no algorithm can determine, from a system's current certified safety, whether safety survives its next self-modification step: a result that reduces to Rice's Theorem one level up, making the static and dynamic barriers two faces of one obstruction. This forces an exclusive dichotomy: persistent certification is attainable only for systems that have stopped evolving semantically, i.e. only for narrow, not general, systems. Nor can the obstruction be delegated: any supervisor adequate to audit a general AGI is itself a general AGI, so the supervisory regress never terminates. Three practical risks (finite test coverage, bounded deliberation time, restricted observation) are one phenomenon: every bounded scheme that does not reject correct evidence admits an evolution trace it certifies at every stage while the property is persistently violated. These results give formal content to the unverifiability of AI, showing it is not an engineering target deferred by current limits but a structural tension, an Expressivity Invariant governed by the same computational laws as the Halting Problem and Rice's Theorem.

2026-06-26T22:51:16Z v2: substantially expanded and retitled. Adds unpublished results on the dynamic (self-modifying) case, deriving the persistence barrier from Rice's Theorem one level up; a supervisory-regress theorem linking the results to scalable oversight and Yampolskiy's verifier theory; and a unified treatment of all four barriers as one obstruction, the Expressivity Invariant Jose Pascual Gumbau Mezquita 10.5281/zenodo.20764007 http://arxiv.org/abs/2607.04958v1 2026-07-06T11:42:26Z

Look-ahead bias (using information from after a decision epoch to make the decision at that epoch) is the dominant way a backtest or a machine-learning evaluation flatters a system that will disappoint in deployment. The field manages it with construct-specific recipes and empirical detectors, which are sound only channel by channel and certify nothing by their silence. We show that look-ahead-freedom is a formal property in disguise: fixing an epoch, the demand that the future not influence the present is temporal non-interference over a time-indexed information lattice. From this identification we develop a pipeline calculus separating a datum's availability from its reference time, and settle the problem's boundary. Where availability may depend on data values, look-ahead-freedom is undecidable (indeed Pi-0-1-hard): leakage is recursively enumerable but freedom is not. On the value-independent fragment (covering windowing, resampling, joins, point-in-time and vintage reads, and agentic retrieval) we give a type-and-effect system that is sound and decidable in linear time. An artifact confirms the theory: the check scales linearly, an independent oracle witnesses no leak in any accepted pipeline, and the checker catches every planted leak that differential and tiling detectors miss.

2026-07-06T11:42:26Z Submitted to ACM Transactions on Software Engineering and Methodology Xavier Fonseca http://arxiv.org/abs/2209.10517v19 2026-07-06T08:56:56Z

In this paper, we define the notion of a {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity perspective. Specifically, we obtain the following important new results: (1) We first discuss the expressiveness of the logics PCTL, PCTL$^*$, $ω$-${\rm PCTL}$, and $ω$-${\rm PCTL}^*$ and study how Büchi conditions of probabilistic $ω$-pushdown systems influence $ω$-PCTL formulas. We then investigate the model-checking problem for {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (as defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}). By constructing $ω$-PCTL formulas that encode the {\em Post Correspondence Problem}, we show that this model-checking problem is generally undecidable. (2) We then study under which conditions there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-PCTL-like logic. In particular, we show that the model-checking problem for {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable and $\mathit{NP}$-hard. Currently, there is no known lower bound for this problem that is better than ours. (3) Finally, we investigate an upper bound for the model-checking problem for {\em stateless probabilistic $ω$-pushdown systems} against $ω$-bounded probabilistic computational tree logic ($ω$-bPCTL). We propose a potential approach to solving it by establishing a conditional upper bound and analyze the challenges of this method.

2022-09-21T17:33:48Z [v19] Incorporating answers to anonymous readers' all comments; comments are welcome Deren Lin Tianrong Lin http://arxiv.org/abs/2601.20735v2 2026-07-06T08:47:45Z

We develop a computational approach to Metric Answer Set Programming (ASP) to allow for expressing quantitative temporal constraints, like durations and deadlines. A central challenge is to maintain scalability when dealing with fine-grained timing constraints, which can significantly exacerbate ASP's grounding bottleneck. To address this issue, we leverage extensions of ASP with difference constraints, a simplified form of linear constraints, to handle time-related aspects externally. Our approach effectively decouples metric ASP from the granularity of time, resulting in a solution that is unaffected by time precision.

2026-01-28T16:07:54Z Under consideration in Theory and Practice of Logic Programming (TPLP) Arvid Becker Pedro Cabalar Martin Diéguez Susana Hahn Javier Romero Torsten Schaub http://arxiv.org/abs/2607.04685v1 2026-07-06T05:21:46Z

In their 2018 paper, Agotnes, van Ditmarsch, and Wang extended the notions of success and self-refutation in public announcements to true lies, impossible lies, and $σ$-validity in general, where $σ$ is a finite or infinite sequence of $0$s and $1$s. For example, successful formulas and self-refuting formulas are $11$-valid and $10$-valid, respectively. They then posed a conjecture on the classification of such sequences in terms of $σ$-validity. In this paper, we disprove the conjecture and give corrected classifications for multi-agent K45, single-agent KD45, and multi-agent S5 after reformulating the statement more explicitly. We leave the multi-agent KD45 case with more than one agent open. The results indicate that there is an asymmetry between truthful announcements and false announcements: the former are stable while the latter are unstable. In particular, successful formulas remain true forever while impossible lies can be true at some point when repeatedly announced. Also, although self-refuting formulas can become true again after following the truth pattern $10$, $100$-valid formulas are destructive in the sense that they remain false forever once they become false. On the other hand, true lies are fragile in the sense that truths created by lying can become false again.

2026-07-06T05:21:46Z 21 pages, 4 figures Eiji Yamada http://arxiv.org/abs/2603.26286v3 2026-07-06T04:29:11Z

We propose a new parameter called proofdoor in an attempt to explain the efficiency of CDCL SAT solvers over a certain class of formulas derived from circuit (esp., arithmetic) verification applications. Informally, given an unsatisfiable CNF formula F over n variables, a proofdoor decomposition consists of a chunking of the clauses into A_1, ..., A_k together with a sequence of interpolants connecting these chunks. Intuitively, a proofdoor captures the idea that an unsatisfiable formula can be refuted by reasoning chunk by chunk, while maintaining only a summary of the information (i.e., interpolants) gained so far for subsequent reasoning steps. We prove several theorems in support of the proposition that proofdoors can explain the efficiency of CDCL solvers for some class of circuit verification problems. First, we show that formulas with small proofdoors (i.e., where each interpolant is O(n) sized, each chunk A_i has small pathwidth, and each interpolant clause has at most O(log n) backward dependency on the previous interpolant) have short resolution (Res) proofs, and a certain configuration of CDCL solvers can compute such proofs in time polynomial in n. Second, we show that commutativity (miter) formulas over floating-point addition have small proofdoors and hence short Res proofs, even though they have large pathwidth. Third, we identify limits of the proofdoor framework: we show that a poor decomposition of arithmetic miter instances can force exponentially large interpolants, and hence our framework derives exponentially large Res refutations from such a decomposition, even when a different decomposition (i.e., a small proofdoor) yields short proofs. As a byproduct, these interpolant lower bounds imply new lower bounds for the partially ordered resolution proof system.

2026-03-27T10:53:23Z version 2.1 Sunidhi Singh Vincent Liew Marc Vinyals Vijay Ganesh http://arxiv.org/abs/2607.04321v1 2026-07-05T14:10:20Z

We present LogicProof, an interactive web-based theorem prover designed for educational use. The system supports natural deduction and sequent calculus for propositional and first-order logic in both classical and constructive variants. It emphasizes a modern user experience through real-time feedback and interactive visualization of proof trees. We evaluated LogicProof in a study involving 35 students. The results suggest that the system improves understanding of formal proof construction and supports student engagement with logical concepts. Compared to traditional pen-and-paper approaches, students reported faster iteration, easier error correction, and greater confidence in the correctness of their solutions. These findings indicate that LogicProof can serve as a practical supplement to existing teaching methods, particularly in supporting the learning process and reducing barriers associated with formal proof construction.

2026-07-05T14:10:20Z 13 pages, 5 figures. Accepted for the TEAL 2026 Workshop (Tools for Educational Activities in Logic), part of FLoC 2026 Ján Perháč Vasyl Khashcha Samuel Novotný http://arxiv.org/abs/2604.26976v2 2026-07-05T11:04:25Z

We study the problem of fitting a description logic (DL) ontology to a given set of positive and negative examples that take the form of an ABox and a Boolean query. While previous work has investigated this problem for the expressive DLs ALC and ALCI, we here focus on the Horn DLs EL and ELI, as well as their extensions with the bottom concept. As the query language, we consider atomic queries (AQs), conjunctive queries (CQs), and unions thereof (UCQs). We provide characterization of the existence of a fitting ontology based on simulations, use them to develop decision procedures, and clarify the exact computational complexity. For AQs, the problem is in PTime for both EL and ELI. For CQs and UCQs, it is $Σ_2^P$-complete for EL and ExpTime-complete for ELI. Adding the bottom concept does not change any of these complexities. Interestingly, moving from ALC and ALCI to EL and ELI introduces additional technical challenges rather than simplifying the matter.

2026-04-28T08:53:15Z Accepted by the 23rd International Conference on Principles of Knowledge Representation and Reasoning (KR2026) Marvin Grosser Carsten Lutz http://arxiv.org/abs/2604.03844v3 2026-07-05T10:01:18Z

Tokenized assets increasingly operate across heterogeneous blockchain networks and off-chain ledgers, where a regulatory action (a freeze, a seizure, a confiscation) must take effect atomically and consistently across every domain holding the asset. We mechanize, in Isabelle/HOL, cross-domain state preservation as a functor: state machines are objects, structure-preserving synchronization maps are morphisms, and the category laws (identity, composition, associativity) hold as theorems. On this base we establish four results. Safety: a regulatory transition on one domain is faithfully reflected across all connected domains, with bidirectional roundtrip preservation, N-domain consistency, per-asset isolation, and terminal states preserved. Liveness: under f < n/3 Byzantine nodes, deterministic conflict resolution and starvation freedom under a fair-leader assumption, with the threshold n >= 3f+1 shown to make that assumption inhabitable rather than vacuous. Convergence: from an arbitrary unlocked configuration, with no initial cross-chain consistency assumed, synchronization reaches a valid state in a bounded number of steps along a terminal-faithful recovery path. Hierarchy: a tower of synchronization-degree functors connected by natural transformations closed under composition, with a genuinely one-directional degree monotonicity. We couple the functor to Lochbihler and Maric's authenticated data structure at the global-state level, instantiated on a recursive model of the Canton transaction tree with a declared consensus-scope limit. The synchronization model is atomic; its lift to a partially synchronous network is future work. The application is a regulatory state transition model distilled from the RCP framework (arXiv:2603.29278). All ten Isabelle/HOL theory files build without sorry or oops and are submitted to the Archive of Formal Proofs.

2026-04-04T19:50:31Z 30 pages, 12 figures, 5 tables. v3: promoted to a functorial theory. The two v2 properties (safety, liveness) become four results, adding guarded bounded convergence and a synchronization-degree functor tower over a cross-domain state-preservation functor. Deadlock freedom demoted to a scope note; regulatory state/action model clarified as distilled from RCP. Four to ten theory files Jinwook Kim for the Oraclizer Core Team http://arxiv.org/abs/2607.04142v1 2026-07-05T07:02:03Z

Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors? The main contribution of this work is the development of an efficient and user-friendly tool, csb, that solves a bunch of problems around model counting and sampling on the theory of bit-vectors, namely exact and approximate projected and non-projected model counting, along with the almost-uniform and uniform-like sampling. In the case of exact counting, projected counting, and uniform sampling. Our tool csb converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. Our experiments demonstrate significant performance improvements over existing methods.

2026-07-05T07:02:03Z This is the authors' version of the article published in Acta Informatica Acta Informatica, Volume 63, article number 23 (2026) Arijit Shaw Kuldeep S. Meel 10.1007/s00236-026-00535-0