We demonstrate the benefit of computer assisted reasoning by proving correctness of some matching algorithms for regular expressions. We give a brief survey of the VeriFun system used for verification, illustrate the problem, discuss the computation and usage of derivatives, present the machine assisted proofs and report on the effort for creating them.
Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines or deterministic finite automata. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this article, we present SL^λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of membership queries required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We prove that SL^λ is guaranteed to learn an acceptor, in the form of a register automaton with n locations and t transitions, for a given data language of finite index, and that it can do so with at most O(t^2 (2n)^n + m t^2 m^m) membership queries and O(t) equivalence queries, where m is the length of the longest counterexample received during learning. We have implemented SL^λ as a new algorithm in RALib. We evaluate its performance by comparing it against SL^* , the current state-of-the-art RA learning algorithm. Experiments on a series of benchmarks show that it reduces the number of membership queries by up to an order of magnitude, and also shows substantial asymptotic improvements in bigger systems.
Non-degenerate conditions (NDGs) are essential prerequisites that ensure the validity of geometric theorems. While algebraic methods such as Wu’s method generate NDGs in polynomial form and provide geometric interpretations, these interpretations are often not expressed in terms of intuitive geometric quantities, such as lengths, angles, and areas, and instead remain peripheral annotations. Consequently, such NDGs are rarely integrated into the core geometric reasoning process. This paper proposes a methodology based on complex number identities to provide a unifying viewpoint for interpreting NDGs in the following settings. First, we systematically transform algebraic NDGs into expressions involving explicit geometric quantities, thereby incorporating them more directly into the reasoning chain. Second, by leveraging these geometric-quantity-based NDGs, we progressively connect the given conditions to the conclusion, ultimately deriving complex number identities that unify the original theorem, its converse, and quantitative extensions. Experimental evaluation on over 100 geometric problems, including classical theorems and Olympiad-level challenges, indicates that more than 90
We present a formalization in Lean4 of some multi-graded algebraic geometry constructions, focusing on the Brenner–Schröer Proj construction and algebraic dilatations of rings. Multi-graded Proj schemes, defined from rings graded by more general monoids than ℕ or ℤ , have recently attracted increasing attention and play an important role in several areas of modern algebraic geometry. Our work follows the algebraic approach developed in the literature and provides a formal implementation of multi-graded Proj within the Lean4 theorem prover. In addition, we formalize dilatations of rings, an operation in commutative algebra closely related to localization and to blowup constructions. This article gives a comprehensive account of the definitions, main results, and design choices underlying the formalization. It is intended both as documentation of the development and as a foundation for future extensions in formalized algebraic geometry. The corresponding code is made publicly available, supporting further developments in the formalization of advanced geometric structures.
We define a parameterized system for propositional Linear Logic which allows for a formalization in Rocq which can be instantiated to the specific needs of the user. Parameters control the use of the exchange and mix rules in particular. The induced Rocq library provides basic key properties of the system (and of some variants) such as cut admissibility, focusing, etc.
We formalise tableau procedures for the modal logics K, KT, and S4, and the modal fixpoint logic LTL, in the proof assistant Coq version 8.17.1. This involves encoding the algorithms, and formally proving their termination and their correctness, the latter boiling down to showing that they are both sound and complete with respect to the semantics of these logics. We give a quick overview of our account of S4 because most of the work had already been achieved by Wu and Goré then focus on LTL: we describe the rules of our tableau calculus and our approach to formally verify it in Coq. Unlike K and KT, these logics require checking for loops and need particular attention to build a satisfying model. Moreover, for LTL, we must also distinguish “good loops” from “bad loops” due to the presence of least and greatest fixpoint modalities. We show how we manage to implement loop-checks to ensure termination and how a model can be constructed from their tableau tree in order to prove soundness. We also demonstrate how the eventuality formulae of LTL are handled in the tableau rules and the various proofs. Such algorithms encoded in Coq can easily be modified to output a satisfying model in the case where the input is satisfiable. We use the program extraction feature of Coq to produce source code for the verified tableau procedures in OCaml and compile them to obtain actual executable programs. We then evaluate these verified programs on the standard benchmarks against other reasoners which are optimised but unverified. As expected, the results show a clear inferiority of our verified reasoners in terms of efficiency, however they still demonstrate that we can be optimistic regarding the usability of verified reasoners in practice. Wu, M., Goré, R.: Verified decision procedures for modal logics.
In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour. While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as preservation of typing. In this paper, we present an implementation of rewrite rules on top of the Rocq Prover, together with two modular criteria to ensure that the added rewrite rules preserve confluence and typing. These criteria, based on the triangle property for the former and bidirectional type checking for the latter, are formally expressed for PCUIC—the type theory of Rocq recently developed in the MetaRocq project.
Motivated by the need to develop trust in the use of machine learning (ML) systems, but also of artificial intelligence (AI) systems in general there has been massive interest in explaining the predictions of ML models. Logic-based formal explanations offer a rigorous alternative to existing non-formal explainability approaches. Recent work studied the computation of formal explanations for a growing range of classifiers. However, a number of additional explainability queries are of interest and have been studied in recent years. Two concrete examples are feature necessity and relevancy. Feature necessity asks whether a feature must occur in all explanations of a given prediction (FNP). In contrast, feature relevancy asks whether a feature occurs in some explanation of a given prediction (FRP). This paper investigates both the computational complexity of these problems, but also algorithms for their solution in practice. In terms of algorithms for feature relevancy, the paper studies algorithms for specific families of classifiers, but also general-purpose algorithms, which can be applied to families of classifiers used in most systems of AI and ML. The experimental results confirm that feature relevancy can be efficiently decided in practice, for a wide range of families of classifiers.
In the last decade, numerous algorithms for single-objective Boolean optimization have been proposed that rely on the iterative usage of a highly effective Propositional Satisfiability (SAT) solver. But the use of SAT solvers in Multi-Objective Combinatorial Optimization (MOCO) algorithms is scarce. Due to the shortage of efficient tools for MOCO, many real-world applications formulated as multi-objective are cast as single-objective, using either a linear combination or by setting a preference order among the objectives. In this paper, we extend the state of the art of MOCO solvers with three novel unsatisfiability-based algorithms. The first two are core-guided MOCO solvers. The third is a hitting set MOCO solver. Experimental results in several sets of benchmark instances show that our new unsatisfiability-based algorithms can outperform and complement other SAT-based, state-of-the-art algorithms for MOCO.
We present the first formal correctness proof of Edmonds' blossom shrinking algorithm for maximum cardinality matching in general graphs. We focus on formalising the mathematical structures and properties that allow the algorithm to run in worst-case polynomial running time. We formalise Berge's lemma, blossoms and their properties, and a mathematical model of the algorithm, showing that it is totally correct. We provide the first detailed proofs of many of the facts underlying the algorithm's correctness.
There exist several approaches to infer runtime or resource bounds for integer programs automatically. In this paper, we study the subclass of periodic rational solvable loops (prs-loops), where questions regarding the runtime and the size of variable values are decidable and where we can therefore obtain techniques that are complete for such subclasses. We show how to use these results for the complexity analysis of arbitrary general integer programs. To this end, we present a modular approach which computes local runtime and size bounds for subprograms which correspond to prs-loops. These local bounds are then lifted to global runtime and size bounds for the whole integer program. Furthermore, we introduce several techniques to transform larger programs into prs-loops to increase the scope of the approach. The power of the procedure is shown by our implementation in the complexity analysis tool KoAT.
The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems (knowledge compilation proof system), (model counting induction by claim extension), and (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. A fourth system, (circuit linear introduction proposition), is a very powerful proof system of theoretical interest. Prior to this paper, it was only known that simulates the three other systems. All the remaining relations between the systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the four systems, establishing that simulates both and , while and are exponentially incomparable. This implies that is strictly stronger than the other two systems.
We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows us to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.
This is the first part of an analysis of the interplay between multiple properties that are related to combination methodologies for theories in the field of satisfiability modulo theories. We here focus on Nelson-Oppen and polite theory combinations, leading to a total of five model-theoretic properties to be considered: stable infiniteness, smoothness, finite witnessability, strong finite witnessability, and convexity. Our first result is an improvement on polite theory combination, showing that it is possible when only assuming stable infiniteness and strong finite witnessability, and thus implying smoothness is not a prerequisite for this method. Second, we provide examples of Boolean combinations of the aforementioned 5 properties whenever they are possible (e.g., a theory that admits all the properties, a theory that admits none, etc.), sharp in the sense that no theories within simpler signatures may exhibit the exact same properties, and prove which combinations cannot occur. Among these examples, the most surprising one is that of a polite yet not strongly polite theory in one sort, a combination whose previous example in the literature was two-sorted.
This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light’s as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to break confidentiality. We introduce relative security, a general notion of information-flow security that models this type of vulnerability by contrasting the leaks that are possible in a “vanilla” semantics with those possible in a different semantics, often obtained from the vanilla semantics via some optimizations. We describe incremental proof methods, in the style of Goguen and Meseguer’s unwinding, both for proving and for disproving relative security, and deploy these to formally establish the relative (in)security of some standard Spectre examples. Both the abstract results and the case studies have been mechanized in the Isabelle/HOL theorem prover. This paper is an extension of an earlier conference paper that provides significantly more detail on the Isabelle formalization and the unwinding proof process.
We present an automated prover for coherent logic with function symbols which uses the power of SMT solvers through the recently proposed paradigm “theorem proving as constraint solving”. The open-source implementation of the prover supports export of proofs in natural language and to the proof assistants Coq, Isabelle, and Mizar, and has other additional features such as the support for completing premises, goals, partially given proofs, and the support for creating illustrated proofs.
The convergence rate of various first-order optimization algorithms is a pivotal concern within the numerical optimization community, as it directly reflects the efficiency of these algorithms across different optimization problems. Our goal is to make a significant step forward in the formal mathematical representation of optimization techniques using the Lean4 theorem prover. We first formalize the gradient for smooth functions and the subgradient for convex functions on a Hilbert space, laying the groundwork for the accurate formalization of algorithmic structures. Then, we extend our contribution by proving several properties of differentiable convex functions that have not yet been formalized in Lean’s mathematical library Mathlib. Finally, a comprehensive formalization of these algorithms is presented. These developments are not only noteworthy on their own but also serve as essential precursors to the formalization of a broader spectrum of numerical algorithms and their applications in machine learning as well as many other areas.
We give a simple proof of correctness of folding the regular heptagon with origami. Our proof avoids using complex geometry, only polynomials and basic algebraic geometry is required with simple rigidity considerations. We also exploit automated reasoning via efficient black-box computing of Gröbner bases. Our proof can be used in classrooms where learners are not familiar with complex numbers.
Benchmarking is crucial for developing new algorithms. This also applies to solvers for the propositional satisfiability (SAT) problem. Benchmark selection is about choosing representative problem instances that reliably discriminate solvers based on their runtime. In this paper, we present a dynamic benchmark selection approach based on active learning. Our approach estimates the rank of a new solver among its competitors, striving to minimize benchmarking runtime but maximize ranking accuracy. Instead of using real-valued solver runtimes, our approach works with discretized runtime labels, which yielded better solver rank predictions. We evaluated this approach on the Anniversary Track dataset from the SAT Competition 2022. Our benchmark selection approach can predict the rank of a new solver after approximately 10 % of the time it would take to run the solver on all instances of this dataset, with a prediction accuracy of approximately 92 %. Additionally, we discuss the importance of instance families in the selection process. In conclusion, our tool offers a reliable method for solver engineers to assess a new solver’s performance efficiently.
