Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts have to construct proofs manually by entering tactics into the proof assistant. In this paper, we study the problem of using machine learning to automate the interaction with proof assistants. We construct CoqGym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. We develop ASTactic, a deep learning-based model that generates tactics as programs in the form of abstract syntax trees (ASTs). Experiments show that ASTactic trained on CoqGym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. Code is available at this https URL.
FastSMT generates tactics to interact with the Z3 SMT solver @cite_0 , which determines the satisfiability of a certain class of logical formulas. Compared to our model, FastSMT uses substantially simpler tactics---all of them have only boolean and integer arguments, whereas tactics in Coq can have compound expressions as arguments. As a result, the approach of FastSMT does not output ASTs and is not directly applicable to our setting.
@cite_0
1480909796 1515930456 2963188972 1551250655
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications. The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (SMT), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems). In this paper, we focus on the case where the background theory is the combination T1∪T2 of two simpler theories. Many SMT procedures combine a boolean model enumeration with a decision procedure for T1∪T2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise). We propose a new approach for SMT(T1∪T2), called Delayed Theory Combination, which does not require a decision procedure for T1∪T2, but only individual decision procedures for T1 and T2, which are directly integrated into the boolean model enumerator. This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories. We show the effectiveness of the approach by a thorough experimental comparison. We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The decision procedure is proved correct and complete: correctness is established w.r.t. any model by formalising Kozen's initiality theorem; a counter-example is returned when the given equation does not hold. The correctness proof is challenging: it involves both a precise analysis of the underlying automata algorithms and a lot of algebraic reasoning. In particular, we have to formalise the theory of matrices over a Kleene algebra. We build on the recent addition of firstorder typeclasses in Coq in order to work efficiently with the involved algebraic structures. In this dissertation we show how conflict clause learning, a technique that has been very useful in improving the efficiency of Boolean logic satisfiability search, can be adapted to speed up dramatically the search for models of answer set programs. Answer set programming is a knowledge representation paradigm related to the areas of logic programming and nonmonotonic reasoning. Many of the applications of answer set programming come from the areas of artificial intelligence-related diagnosis and planning. The problem of finding an answer set for a normal or extended logic program is NP-hard. Current complete answer set solvers are patterned after the Davis-Putnam-Loveland-Logemann ( DPLL) algorithm for solving Boolean satisfiability (SAT) problems, but are adapted to the nonmonotonic semantics of answer set programming. Recent SAT solvers include improvements to the DPLL algorithm. Conflict clause learning has been particularly effective in this regard. A conflict clause represents a backtracking solver's analysis of why a conflict occurred. This analysis can be used to further prune the search space and to direct the search heuristic. The use of such clauses has improved significantly the efficiency of satisfiability solvers over the past few years, especially on structured problems arising from applications. In this dissertation we describe how we have adapted conflict clause techniques for use in the answer set solver Smodels. We experimentally compare the performance of the resulting program, Smodelscc, to that of the original Smodels program. Our tests show dramatic speedups for Smodelscc on a wide range of problems. We also compare the performance of Smodelscc with that of two other recent answer set solvers, ASSAT and Cmodels-2. ASSAT and Cmodels-2 directly call Boolean satisfiability solvers in order to search for answer sets. On so-called “non-tight” problems, Smodelscc showed substantially better performance than these solvers. The performance advantage that Smodels cc enjoys on non-tight problems is due to the unfounded set test that Smodelscc inherits from the Smodels solver, and the fact that this test is executed frequently throughout the program's search for answer sets.