19,989 papers in this slice of arXiv.
Zhe Ye, Hantao Lou, Yuechun Sun +8
AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.
Charles Koll, Houssam Abbas
We give the first theoretical characterization, and the first algorithm, for continuous monitoring of a distributed Cyber-Physical System (CPS) against a dense-time temporal logic specification. A distributed CPS is composed of multiple agents, each with a local clock; these clocks drift from each other, so there is no well-defined global time. When monitoring such a system's output signal against a temporal logic specification, it is not evident how to interpret the temporal constraints of the formula, and what satisfaction means. Yet CPS designers, like control engineers, typically think of their system's operation in terms of global time. Most existing techniques for monitoring distributed systems work with discrete-time specifications not suitable for CPS, and/or require an explicit mapping of temporal constraints to local clocks. We introduce an algorithm that addresses the above challenges for a fragment of Signal Temporal Logic (STL) that still includes all temporal operators. It relies on a novel extension of satisfaction signals to this partially synchronous setting (where clocks drift), and an analysis of the geometry of multi-dimensional partially synchronous time. The algorithm returns the set of all possible global moments that can satisfy the specification. Knowledge of these possible global moments is important for debugging distributed hybrid control systems such as fleets of drones and electrical grids. We derive the worst-case complexity of the algorithm, and implement a sound approximation of it that experimentally illustrates effective monitoring, even in scenarios of up to 50 agents.
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test (p=0.0625).
Radu Curticapean, Daniel Neuen, Amir Nikabadi +2
Two graphs G and H are homomorphism indistinguishable over a graph class F if they admit the same number of homomorphisms from every graph in F. A wide range of relaxations of graph isomorphism arise this way: isomorphism itself over the class of all graphs [Lovász, Acta Math. Hung. 1967], equivalence under the k-dimensional Weisfeiler-Leman algorithm over the graphs of treewidth ≤k [Dvořák, J. Graph Theory 2010], and quantum isomorphism over planar graphs [Mančinska-Roberson, FOCS 2020]. Since the class F is typically infinite, it is not clear a priori whether homomorphism indistinguishability over F is decidable; for planar graphs it is undecidable. Every class for which decidability was previously known is sparse. We give the first decidability results for dense graph classes: We introduce the dense Weisfeiler-Leman algorithm that decides homomorphism indistinguishability over the class of graphs of cliquewidth ≤k, the dense counterpart of treewidth. This relation was not previously known to be decidable. The algorithm colors k-tuples of vertex subsets rather than k-tuples of vertices. Beyond the class of all graphs of cliquewidth ≤k, we prove a general meta-theorem: homomorphism indistinguishability over every CMSO1-definable graph class of bounded cliquewidth is decidable, in randomized exponential time. For classes of bounded linear cliquewidth the bound improves to PSPACE, and we show this is tight by exhibiting such a class for which the problem is PSPACE-complete. These are the first general algorithms for homomorphism indistinguishability over dense graph classes.
Xiaohong Chen, Grigore Rosu
Basic matching logic is matching logic without definedness. Symbols are interpreted as set-valued operations, element variables denote singletons and are bound by ∃, and no connective uniformly internalizes totality. For basic matching logic without fixpoints over an arbitrary one-sorted finitary signature, we prove global completeness (Γ⊨φ iff Γ⊢φ, for arbitrary, possibly infinite Γ) and, as a corollary, conservativity of the definedness extension. The proof localizes Γ to a theory ΔΓ and reduces semantic consequence and derivability to the same local relation: Γ⊨φ iff ΔΓ⊨locφ iff Γ⊢φ. A double-cover construction establishes the semantic equivalence. Least fixpoints destroy effective axiomatizability. Over a signature with one unary and two binary symbols and no constants, validity is not recursively enumerable; hence no sound calculus with a recursively enumerable proof relation is even weakly complete, already for the empty theory and without definedness. The positive result is also sharp in the number of sorts. Global completeness fails with three sorts for a satisfiable Γ. Thus the completeness conjecture holds for one sort and fails in general. The negative results arise from sort flow, fixpoint effectivity, and, for hybrid logic, an obstruction to every well-founded calculus whose leaves are hypotheses or valid patterns and whose rules respect localization. This yields a matching-logic-independent dichotomy: the language with state variables bound by ∃ and ∀ over modalities of arbitrary arity is globally complete without nominals, while no calculus in that well-founded class is globally complete once nominals are added.
Lena Verscht, Hannah Mertens, Kevin Batz +3
Probabilistic programs with nondeterminism model planning problems in which a strategy resolves the nondeterminism to optimize an expected outcome. We study the multiobjective setting, optimizing several outcomes at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that randomize over non-probabilistic determinizations. We prove the transformer and synthesis rules sound against an operational MDP semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using various case studies.
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen +1
We present global and local algorithms for solving systems of equations over Noetherian posets with a bottom element, a general setting underlying many verification problems. Our algorithms compute the solution of a selected variable by restricting exploration to those parts of the system required to determine its value. We achieve this by computing variable dependencies by means of dependency oracles. Oracles guide the exploration of the system and provide sound termination criteria for local fixed-point computation. A key advantage of our approach is its flexibility: oracles can be customized, composed, or over-approximated, offering a principled way to trade precision for performance without compromising correctness. We evaluate our solution against existing algorithms from the literature and show that our prototype implementation is competitive and often outperforms specialized solutions, while remaining simple and adaptable across diverse application domains.
Logan Kenwright, Partha Roop, Sobhan Chatterjee +1
Signal Temporal Logic (STL) is a popular formalism for the temporal safety properties of cyber-physical systems, most often used for runtime verification. In the synchronous family of languages, safety properties are instead expressed as synchronous observers, modules composed with a program for static verification, which are also runnable specifications suitable for runtime verification, though this use is rarely explored. We present a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre. Unlike previous work, we allow arbitrary nesting of bounded SSTL properties via modular compilation, and admit a globally unbounded outer operator for online monitoring; the resulting observers serve both runtime verification and, as a by-product, static verification with the Kind2 model checker. We further contribute an interactive visualiser that renders a property's three-valued verdict over an editable trace, and evaluate on two case studies from the literature: a spring-mass system and a car-following cruise controller.
Pablo Barceló, Floris Geerts, Matthias Lanzinger +2
We prove that, on finite simple undirected graphs equipped with a single Boolean node feature, the Boolean queries expressible in Σ-MPLang, for any collection Σ of eventually constant activation functions and with arbitrary real coefficients, form a strict subclass of the Boolean queries expressible in ReLU-MPLang. We thereby settle a recently posed open problem: whether ReLU-MPLang is more powerful than trReLU-MPLang when it comes to Boolean queries. In particular, this implies that ReLU-GNNs are strictly more expressive than TrReLU,id-GNNs with respect to Boolean queries on Boolean-featured graphs.
Jakub Rydval
We study the amalgamation decision problem: given a universal first-order sentence Φ, decide whether the class fm(Φ) of its finite models has the amalgamation property. We call Φ semantic Horn if fm(Φ) is closed under binary direct products. By McKinsey's theorem, this is equivalent to Φ being logically equivalent to a universal Horn sentence; the distinction is one of input representation, since Φ itself need not be given in Horn form and conversion to an explicit Horn normal form can incur an exponential blow-up. We prove that the problem is decidable under this semantic promise. Moreover, it belongs to 2EXPTIME, and to EXPTIME for every fixed bound on the arity of the input signature. Thus the semantic Horn fragment admits an unconditional decision procedure for signatures of unbounded relational arity. Our proof starts from the inside-out correspondence, which we use as a black box for the semantic reduction to a finite completion problem. We encode finite completions as homomorphisms to a finite relational template and introduce a finite set-valued local-consistency certificate for completion problems whose template has bounded width. For semantic Horn inputs, the local completions over each fixed source chart are closed under relationwise intersection of the added relations, and these intersections are compatible with restriction maps. This yields a semilattice polymorphism of the completion template. Since the template is binary, the semilattice operation gives width 2, making the local-consistency certificate complete. The same construction gives a decision procedure whenever the associated completion template has bounded width.
Arend Rensink, Andrea Corradini
Nested conditions are used, among other things, as a graphical way to express first order formulas ruling the applicability of a graph transformation rule to a given match. In this paper, we first introduce several operators on conditions mimicking logical connectives. Next we propose an original notion of structural morphism among nested conditions, and we identify circumstances under which morphisms are consistent with the entailment of the corresponding conditions. Finally we frame the results in a categorical context, proving functoriality and universality properties of the various operations.
Steffen van Bakel, David Davies
We define call-by-name and call-by-value reduction and reduction strategies for the calculi slmu (symmetric lmu), lmmt, and Xs (X with implicit substitution). We establish a strong relation between these notions through defining a single interpretation from slmu to lmmt that respects normal reduction, as well as the call-by-name and call-by-value reduction in slmu within the their counterpart in lmmt; for the strategies, we will show similar, but weaker results. We also define a single mapping from lmmt to Xs, and show that this also respects all three notions. We then continue with studying the natural encoding of Xs into lmmt, and show that only full reduction is respected, but that reduction steps are needed to model substitution, so the CBN and CBV strategies cannot be respected. We conclude with studying the combination of our efforts and define an interpretation of slmu into Xs, and show that CBN and CBV reduction are respected. This result underlines that Xs and lmmt are similar, but different calculi, and that the nature of slmu makes that any encoding into either can never fully respect the strategies.
Manfred Droste, Guo-Qiang Zhang
We study the discrete point-based fragment of Ensemble Logic () over the natural numbers, a logic combining displacement φu, bounded metric modalities _t and _t with additive bounds, Boolean connectives, and first-order quantification over . Motivated by the need for a unified symbolic layer for biomedical knowledge with temporal, spatial, genomic, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of () over a finite proposition set P into first-order monadic Presburger arithmetic (,<,+;P). This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter machines with recurring control states proves that satisfiability is Σ11-complete and validity is dually Π11-complete. Expressively, () strictly extends the star-free ω-languages and is incomparable with the ω-regular languages: it defines the non-ω-regular counting language {ambmcmdm∣m≥1}⋅Σω, whereas a delimited parity language remains outside the logic by classical Presburger-arithmetic lower bounds. On the proof-theoretic side, we present a sound Hilbert system and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible.
Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh +7
Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models, which come with limited guarantees of accuracy. In addition, these methods typically only consider inputs that are known to be correct, and therefore do not assess whether the AF translates incorrect inputs faithfully. To address these limitations, we propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples. Our method is based on automatically generating perturbed reasoning steps that are designed to be invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. We apply our method to eight AF systems across four mathematical datasets, and observe pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements. The most validity-preserving fine-tuned AFs are also the most sycophantic, suggesting a tension between validity and invalidity preservation in current AF systems.
Tianjiao Nie, Ao Zhang, Yusen Tang +4
Large-scale formalization of advanced mathematics requires more than translating individual statements: it must reconstruct a coherent theory distributed across heterogeneous sources. This process raises four challenges: discovering implicit dependencies, correcting source defects, preserving semantic fidelity, and reconciling cross-source misalignments. We present FormaTheoria, an end-to-end, AI-assisted workflow that coordinates source acquisition, formalization, proof construction, recursive dependency discovery, independent review, and reconciliation, while preserving provenance and protecting approved declarations. A shared agent framework supports long-horizon execution through tool use, context compaction, review-gated termination, section-level source context, and dependency-aware batch parallelization. Applying FormaTheoria to major components of the Classification of Finite Simple Groups (CFSG), we construct a machine-checked Lean development extending through the Bender--Suzuki theorem and encompassing the Feit--Thompson Odd Order Theorem, Glauberman's Z∗ theorem, and the Brauer--Suzuki theorem. This development verifies an extensive body of deeply interdependent finite-group theory while providing a foundation for continuing the CFSG formalization. An empirical analysis of the code and recorded construction process supports the practical relevance of the identified challenges and illustrates the roles of the corresponding workflow components. Together, these results demonstrate how AI-assisted workflows can reconstruct mathematically significant formal theories from distributed literature by combining language-model agents with formal verification, structured review, and explicit dependency management.
Alessandro Bertagnon, Marco Gavanelli
The Traveling Salesperson Problem (TSP) is one of the best-known problems in computer science and arises in many engineering applications, such as smart vehicles and intelligent transportation systems. In the "Euclidean" case, each node is defined by its coordinates in the plane and distances are computed using the Euclidean metric. In the Constraint Programming (CP) literature, the Euclidean TSP is typically addressed by computing the full distance matrix and treating it as a general case; however this approach ignores the geometric information carried by the points' coordinates. In this work, we propose new filtering algorithms, implemented in Constraint Logic Programming (CLP), that exploit such geometric information to achieve stronger constraint propagation than existing approaches. Moreover, we show how this methodology can be extended to other Euclidean variants of the TSP, including the Euclidean Generalized Traveling Salesperson Problem (EGTSP), which is relevant in practical routing and logistics applications. Experimental results demonstrate the computational advantages of the proposed approach.
Jan Tóth, Qipeng Kuang, Kuncheng Zou +4
The Weighted First-Order Model Counting Problem (WFOMC) asks for the weighted sum of models of a first-order logical sentence over a domain. It is a fundamental problem in statistical relational learning, with applications extending to enumerative combinatorics and graph polynomials. Computing WFOMC for the three-variable fragment is #P1-hard, whereas polynomial-time algorithms exist for the two-variable fragment and its extensions by cardinality constraints and counting quantifiers. In this work, we explore computing WFOMC in polynomial time over linearly ordered domains, enabling tractable reasoning across inference scenarios and combinatorial problems involving sequences. Because encoding a linear order in standard first-order logic requires three variables, negating our polynomial-time aspirations, we add a linear order axiom directly to the language. This forces one predicate to impose a total ordering on domain elements. We first prove that WFOMC with the linear order axiom can be solved in time polynomial in the domain size. We then extend this result to ordered domains with access to successor relations. While this holds when successors are explicitly defined via the linear order, we demonstrate an alternative implicit approach where successor relations are part of the axiom. This implicit method exhibits significantly better performance on all tested instances, sometimes providing exponential runtime improvements. Finally, we analyze scenarios with two distinct linear orders. We show that WFOMC over the two-variable fragment with two linear orders is #P1-hard. However, we develop a polynomial-time algorithm for WFOMC with one linear order and a successor relation of another, pushing the intractability barrier further, yet still leaving the question of how close to a second full linear order one can get.
Jake Masters, Nobuko Yoshida
A precise (sound and complete) subtyping relation ≤ specifies that T′ is a subtype of T if and only if a program of type T′ can always safely replace a program of type T without compromising the safety of a larger program. This paper formulates and proves preciseness of subtyping for mixed choice multiparty session types with session delegation, creation, and interleaving. We prove soundness by developing the first general type system for a full mixed choice multiparty session π-calculus. To prove completeness, we introduce the three-party lock, which is a minimal and general form of liveness error for handling interleaved sessions, and we establish a new proof technique based on a construction of scheduler processes which enable exhaustive detection for all failures of the subtyping relation. We then extend the preciseness results to a family of mixed choice multiparty session types. Algorithms for checking (1) subtyping and (2) safety, deadlock-freedom, and liveness of typing contexts are fully implemented and optimised to run in quadratic time with respect to the size of the state space and typing context, and have been evaluated with (mixed choice) case studies from the literature.
Mario Piazza
We prove decidability of Simpson's intuitionistic modal logic IK by working directly with cut-free nested proofs. Once the end formula is fixed, only finitely many combinations of input and output formulae can occur at a node, although the modal tree itself remains unbounded. We order these nested sequents by rooted homeomorphic embedding: weakening may add input formulae, while transitivity allows a modal edge to be stretched into a non-empty path. Kruskal's theorem makes rooted homeomorphic embedding a well-quasi-order, but does not by itself make backward application of the rules effective: an inference may still occur inside an arbitrarily large context. The finite-support lemma shows that a minimal predecessor need retain only the positions used by the inference, the images of the chosen basis elements, and the branch points joining them. Together with an effective enumeration of bounded rule instances, this bound makes the minimal predecessors computable. Backward closure from the initial sequents gives an increasing sequence of finitely based upward-closed sets. The sequence eventually stabilises, and its stable value is the set of provable nested sequents. At that point, finitely many cut-free proofs suffice: every other provable nested sequent is obtained from one of them by weakening along an embedding. Their maximum height gives a uniform proof-height bound.
Jordan Peper, Krish Kapadia, James Gast +2
Symbolic model checking is an effective approach for verifying semantically rich temporal-logic properties of cyber-physical systems, but it hinges on discretizing continuous-state dynamics into a finite-state abstraction. To transfer verification guarantees from the abstract model to the concrete CPS, the abstraction must conservatively approximate the concrete state space and behaviors. Hence, model-builders must maintain this soundness while balancing pessimism with tractability. However, they face several common pitfalls such as under-approximating the state space, under-approximating transitions, unsound pruning of "degenerate" behaviors, and improper specification lifting. This tutorial presents a pragmatic, conservative-by-construction workflow for building discrete abstractions of closed-loop dynamical systems. The workflow consists of four modular steps with interchangeable subroutines: (i) state-space partition and abstraction-function design, (ii) conservative transition construction via axis-aligned bounding boxes, polytopes, or sampling with PAC coverage certificates, (iii) mitigation of spurious transitions and self-loops using certified erasure and counterexample-guided abstraction refinement, and (iv) sound lifting of LTL specifications using may-must semantics. We demonstrate the end-to-end pipeline on three case studies and report how these design choices affect abstraction structure, runtime, and verification outcomes.