Premise selection is crucial for large theory reasoning with automated theorem provers as the sheer size of the problems quickly leads to resource exhaustion. This paper proposes a premise selection method inspired by the machine learning domain of image captioning, where language models automatically generate a suitable caption for a given image. Likewise, we attempt to generate the sequence of axioms required to construct the proof of a given conjecture. In our axiom captioning approach, a pre-trained graph neural network is combined with a language model via transfer learning to encapsulate both the inter-axiom and conjecture-axiom relationships. We evaluate different configurations of our method and experience a 14% improvement in the number of solved problems over a baseline.

Contains fulltext : 310648.pdf (Publisher’s version ) (Open Access)

This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. [1] . The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lacks several essential features. ESBMC v7.6 further enhanced this foundation by adding and extending features based on the Clang AST, such as exception handling, extended memory management and memory safety verification, including dangling pointers, duplicate deallocation, memory leaks and rvalue references and new operational models for STL updating the outdated C++ operational models. Our extensive experiments demonstrate that ESBMC v7.6 can handle a significantly broader range of C++ features introduced in recent versions of the C++ standard.

Abstract Symbolic Machine Learning Prover (SMLP)is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system based on this data by taking a grey-box approach: SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system’s response. SMLP has been applied in industrial setting at Intel for analyzing and optimizing hardware designs at the analog level. SMLP is a general purpose tool and can be applied to any system that can be sampled and modeled by machine learning models.

We introduce Virtual Integer-Real Arithmetic Substitution (Viras), a quantifier elim- ination procedure for deciding quantified linear mixed integer-real arithmetic problems. Viras combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that Viras gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

Abstract ESBMC implements many state-of-the-art techniques that combine abstract interpretation and model checking. Here, we report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC now employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, and forward-backward contractors. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.

Abstract Scientific discovery in biology is difficult due to the complexity of the systems involved and the expense of obtaining high quality experimental data. Automated techniques are a promising way to make scientific discoveries at the scale and pace required to model large biological systems. A key problem for 21st century biology is to build a computational model of the eukaryotic cell. The yeast Saccharomyces cerevisiae is the best understood eukaryote, and genome-scale metabolic models (GEMs) are rich sources of background knowledge that we can use as a basis for automated inference and investigation. We present LGEM+, a system for automated abductive improvement of GEMs consisting of: a compartmentalised first-order logic framework for describing biochemical pathways (using curated GEMs as the expert knowledge source); and a two-stage hypothesis abduction procedure. We demonstrate that deductive inference on logical theories created using LGEM+, using the automated theorem prover iProver, can predict growth/no-growth of S. cerevisiae strains in minimal media. LGEM+ proposed 2094 unique candidate hypotheses for model improvement. We assess the value of the generated hypotheses using two criteria: (a) genome-wide single-gene essentiality prediction, and (b) constraint of flux-balance analysis (FBA) simulations. For (b) we developed an algorithm to integrate FBA with the logic model. We rank and filter the hypotheses using these assessments. We intend to test these hypotheses using the robot scientist Genesis, which is based around chemostat cultivation and high-throughput metabolomics.

Automated reasoning with theories and quantifiers is a common demand in formal methods. A major challenge that arises in this respect comes with rewriting/simplifying terms that are equal with respect to a background first-order theory T , as equality reasoning in this context requires unification modulo T . We introduce a refined algorithm for unification with abstraction in T , allowing for a fine-grained control of equality constraints and substitutions introduced by standard unification with abstraction approaches. We experimentally show the benefit of our approach within first-order linear rational arithmetic.

In this work we extend an instantiation-based theorem prover iProver with machine learning (ML) guidance based on graph neural networks. For this we implement an interactive mode in iProver, which allows communication with an external agent via network sockets. The external (ML-based) agent guides the proof search by scoring generated clauses in the given clause loop. Our evaluation on a large set of Mizar problems shows that the ML guidance outperforms iProver’s standard human-programmed priority queues, solving more than twice as many problems in the same time. To our knowledge, this is the first time the performance of a state-of-the-art instantiation-based system is doubled by ML guidance.

Abstract Automated reasoning is routinely used in the rigorous construction and analysis of complex systems. Among different theories, arithmetic stands out as one of the most frequently used and at the same time one of the most challenging in the presence of quantifiers and uninterpreted function symbols. First-order theorem provers perform very well on quantified problems due to the efficient superposition calculus, but support for arithmetic reasoning is limited to heuristic axioms. In this paper, we introduce the $$\textsc {Alasca}$$ A L A S C A calculus that lifts superposition reasoning to the linear arithmetic domain. We show that $$\textsc {Alasca}$$ A L A S C A is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated $$\textsc {Alasca}$$ A L A S C A using the Vampire theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.

ksmt is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this article we investigate properties of the ksmt calculus and show that it is a δ-complete decision procedure for bounded problems. For that purpose we provide concrete algorithms computing linearisations based on either uniform or local moduli of continuity of non-linear functions. The latter method is called local linearisation and is shown to have desirable properties sufficient for termination and which also allow for more efficient treatment of non-linear constraints. Our methods for constructing linearisations are based on computable analysis, in particular we introduce the Cauchy-compatible compact representation of reals and prove its names to be locally compact, allowing for more efficient computation of local linearisations while maintaining δ-completeness.

Application domains of Bayesian optimization include optimizing black-box functions or very complex functions. The functions we are interested in describe complex real-world systems applied in industrial settings. Even though they do have explicit representations, standard optimization techniques fail to provide validated solutions and correctness guarantees for them. In this paper we present a combination of Bayesian optimization and SMT-based constraint solving to achieve safe and stable solutions with optimality guarantees.

This paper presents ESBMC-CHERI -- the first bounded model checker capable of formally verifying C programs for CHERI-enabled platforms. CHERI provides run-time protection for the memory-unsafe programming languages such as C/C++ at the hardware level. At the same time, it introduces new semantics to C programs, making some safe C programs cause hardware exceptions on CHERI-extended platforms. Hence, it is crucial to detect memory safety violations and compatibility issues ahead of compilation. However, there are no current verification tools for reasoning over CHERI-C programs. We demonstrate the work undertaken towards implementing support for CHERI-C in our state-of-the-art bounded model checker ESBMC and the plans for future work and extensive evaluation of ESBMC-CHERI. The ESBMC-CHERI demonstration and the source code are available at https://github.com/esbmc/esbmc/tree/cheri-clang.

Abstract is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the calculus and show that it is a $$\delta $$ δ -complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.

Combining machine learning with constraint solving and formal methods is an interesting new direction in research with a wide range of safety critical applications.Our focus in this work is on analyzing Neural Networks with Rectified Linear Activation Function (NN-ReLU).The existing, very recent research works in this direction describe multiple approaches to satisfiability checking for constraints on NN-ReLU output.Here we extend this line of work in two orthogonal directions: We propose an algorithm for finding configurations of NN-ReLU that are (1) safe and (2) stable.We assume that the inputs of the NN-ReLU are divided into existentially and universally quantified variables, where the former represent the parameters for configuring the NN-ReLU and the latter represent (possibly constrained) free inputs.We are looking for (1) values of the configuration parameters for which the NN-ReLU output satisfies a given constraint for any legal values of the input variables (the safety requirement); and (2) such that the entire family of configurations with configuration variable values close to a safe configuration is also safe (the stability requirement).To our knowledge this is the first work that proposes SMT-based algorithms for searching safe and stable configuration parameters for systems modelled using neural networks.We experimentally evaluate our algorithm on NN-ReLUs trained on a set of real-life datasets originating from an industrial CAD application at Intel.

We show the NP-completeness of the existential theory of term algebras with the Knuth--Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth--Bendix ordering constraints.

We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by proposition tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision provides for an approximate consistency test, and the instance generation inference system is a means of successively refining the approximation.

Orientability of systems of equalities is the following problem: given a system of equalities s/sub 1/ /spl sime/ t/sub 1/, . . . , s/sub n/ /spl sime/ t/sub n/, does there exist a simplification ordering > which orients the system, that is for every i /spl isin/ {1, ..., n}, either s/sub i/ > t/sub i/ or t/sub i/ > s/sub i/. This problem can be used in rewriting for finding a canonical rewrite system for a system of equalities and in theorem proving for adjusting simplification orderings during completion. We prove that (rather surprisingly) the problem can be solved in polynomial time when we restrict ourselves to the Knuth-Bendix orderings.

The authors show the decidability of the existential theory of term algebras with any Knuth-Bendix ordering. They achieve this by giving a procedure for solving Knuth-Bendix ordering constraints. As for complexity, NP-hardness of the set of satisfiable quantifier-free formulas can be shown in the same way as by R. Nieuwenhuis (1993). The algorithm presented does not give an NP upper bound; we point out parts of our algorithm that may cause nonpolynomial behavior.