ABSTRACT. The talk will mainly discuss several recent AI/TP systems and experiments that combine reasoning with learning in positive feedbackloops. I will try to describe the settings, the datasets that may today contain millions of proofs, the interesting parts of the algorithms, and some of the practical challenges when building learning-guided systems that actually prove theorems in realtime. Time permitting, I will also discuss the outlook, interesting future directions and initial experiments related to them.

ABSTRACT. This paper introduces QuAPI, an easy to use library for enabling efficient assumption-based reasoning for arbitrary SAT or QBF solvers. The users of QuAPI only need access to an executable of these solvers. The only requirement on the solvers is to use standard C library functions, either wrapped or directly, for reading input files in the standard DIMACS or QDIMACS format. No source code or library access is necessary, also not for API-less solvers. Our library allows applications to benefit from assumptions and thus incremental solving matching the native support of a standard incremental interface such as IPASIR, but without the need to implement it. This feature is particularly valuable for applications of QBF solving as most state-of-the-art solvers do not support assumption-based reasoning, with some not providing any API at all. We present the architecture of QuAPI and discuss crucial implementation details in depth. Our extensive performance evaluation shows substantial speedup compared to using unmodified solver binaries on similar incremental reasoning tasks.

ABSTRACT. The two-watched literal scheme for propositional logic is a core component of any efficient CDCL (Conflict Driven Clause Learning) implementation. The family of SCL (Clause Learning from Simple Models) calculi also learns clauses with respect to a partial model assumption built by decisions and propagations similar to CDCL. We show that the well-known two-watched literal scheme can be lifted to SCL for first-order logic.

ABSTRACT. ableaux-based provers work well for certain classes of first-order formulas and are better suited for integration with machine learning techniques. However, the tableaux techniques developed so far perform way worse than saturation-based techniques on the first-order formulas with equality. In this paper, we present the first implementation of Lazy Paramodulation which allows applying the ordering constraints in connection tableaux proof search without exponential blowup of the number of clauses (characteristic for Brand's modifications). We implement the original Lazy Paramodulation calculus and propose a variant of the Brand's modification (called LP-modification), which is based on the same ideas as Lazy Paramodulation, avoids exponential blowup and is just a preprocessing step for the standard Connection Tableaux calculus. We demonstrate the impact of both the Lazy Paramodulation and LP-modification on the proof search on a benchmark of TPTP library problems.

ABSTRACT. Term orderings play a critical role in most modern automated theorem proving systems, in particular for systems dealing with equality. In this paper we report on a set of experiments with the superposition theorem prover E, comparing the performance of the system under Knuth-Bendix Ordering and Lexicographic Path Ordering with a number of different precedence and weight generation schemes. Results indicate that relative performance under a short time limit seems to be a good predictor for longer run times and that KBO generally outperforms LPO. Also, if other strategy elements (especially clause selection) are independent of the ordering, performance of a given ordering instance with one strategy is a decent predictor of performance with a different strategy.

ABSTRACT. The family of SCL (Clause Learning from Simple Models) calculi learns clauses with respect to a partial model assumption, similar to CDCL (Conflict Driven Clause Learning). The partial model always consists of ground first-order literals and is built by decisions and propagations. In contrast to propositional logic where propagation chains are limited, in first-order logic they can become infinite. Therefore, the SCL family does not require exhaustive propagation and the size of the partial model is always finitely bounded. Any partial model not leading to a conflict constitutes a model for the respective finitely bounded ground clause set. We show that all potential partial models can be explored as part of the SCL calculus for first-order logic without equality and that any overall model is an extension of a partial model considered.

ABSTRACT. SGGS (Semantically-Guided Goal-Sensitive reasoning) is a refutationally complete theorem-proving method that offers first-order conflict-driven reasoning and is model complete in the limit. This paper investigates the behavior of SGGS on Horn clauses, which are widely used in declarative programming, knowledge representation, and verification. We show that SGGS generates the least Herbrand model of a set of definite clauses, and that SGGS terminates on Horn clauses if and only if hyperresolution does. We report on experiments applying the SGGS prototype prover Koala to Horn problems, with promising performances especially on satisfiable inputs.

ABSTRACT. In recent years, the application of machine learning in program verification, and the embedding of programs to capture semantic information, has been recognized as an important problem by many research groups. Learning program semantics from the raw source code is challenging due to the complexity of real-world programming language syntax, and due to the difficulty to reconstruct long-distance relational information implicitly represented in programs using identifiers. Addressing the first point, we consider Constrained Horn Clauses (CHCs) as a standard representation of program verification problems, providing simple and programming language-independent syntax. For the second challenge, we explore graph representations of CHCs, and propose a new Relational Hypergraph Neural Network (R-HyGNN) architecture to learn program features.

We introduce two different graph representations of CHCs. One is called constraint graph, and emphasizes syntactic information of CHCs by translating the symbols and their relations in CHCs as typed nodes and binary edges, respectively, and constructing the constraints as abstract syntax trees. The second one is called control- and data-flow hypergraph (CDHG), and emphasizes semantic information of CHCs by constructing the control and data flow through ternary hyperedges.

We then propose a new GNN architecture, R-HyGNN, extending Relational Graph Convolutional Networks (by Schlichtkrull et al.), to handle hypergraphs. To evaluate the ability of R-HyGNN to extract semantic information from programs, we use R-HyGNN to train models on the two graph representations, and on five proxy tasks with increasing difficulty, using benchmarks from CHC-COMP 2021 as training data. The most difficult proxy task requires the model to predict the occurrence of clauses in counter-examples (CEs), which subsumes satisfiability of CHCs. CDHG achieves 90.59% accuracy in this task. Furthermore, R-HyGNN has perfect predictions on one of the graphs consisting of more than 290 clauses. Overall, our experiments indicate that R-HyGNN can capture intricate program features for guiding verification problems.

ABSTRACT. Parametrization of a theorem prover is critical for it to solve a problem. A specific parametrization is called a strategy and the best strategy usually differs from problem to problem. Strategy scheduling is trying multiple strategies within a time limit. veriT-schegen is a toolbox to work with strategy schedules. In its core is a simple tool that uses integer programming to generate optimal schedules automatically. Another tool translates the schedules into shell scripts. Hence, the toolbox can be used with any theorem prover. The generated schedules solve more problems then schedules generated in a greedy manner. While generating optimal schedules is NP hard, the generation time is short in practice.

ABSTRACT. We discuss practical aspects of automating inductive reasoning in the first-order superposition prover Vampire. We explore solutions for reasoning over inductively defined dataypes; generating, storing and applying induction schema instances; and directly integrating inductive reasoning into the saturation reasoning loop of Vampire. Our techniques significantly improve the performance of Vampire despite the inherent difficulty of automated induction. We expect our exposition to be useful when implementing induction in saturation-style provers, and to stimulate further discussion and advances in the area.

ABSTRACT. Automatic theorem provers may introduce fresh function or predicate symbols for various reasons. Sometimes, such symbols can be reused. We describe a simple form of symbol reuse in the first-order system Vampire, investigate its practical effect, and propose future schemes for more aggressive reuse.