Graphics Processing Units (GPUs) are the work-horses of high-performance computing. The acceleration they provide to applications compatible with their programming paradigm can surpass CPU performance by several orders of magnitude, as notably evidenced by the advancements in deep learning. A significant spectrum of applications, especially within automated reasoning—like SAT/SMT solvers—has yet to reap the benefits of GPU acceleration. In this talk we discuss recent work that successfully implemented program synthesis on GPUs and used it to accelerate learning of logical specifications from examples. We conclude by mapping out a research programme to move more formal verification workloads to GPUs.

Modal logics have been extensively studied, as they are able to express non-trivial problems ranging from domains in Mathematics and Philosophy to representation of computational systems. The implementation of reasoning engines for those logics is, therefore, highly desirable. However, the satisfiability problem for even the most basic of the multimodal logics, the modal logic Kn, is not tractable: local and global reasoning in the multiagent set are PSPACE-complete and EXPTime-complete, respectively. We are, thus, interested in calculi that can be effectively employed for reasoning within those logics in an efficient way. In this talk we will discuss two different resolution-based calculi for the multimodal Kn with particular focus on the characteristics that have impact on theorem-proving. We will report on experimental results and the influence of proof strategies and processing techniques for both calculi. Finally we will discuss how both calculi can be extended to deal with other interesting modal logics, and how different techniques for achieving those extensions impact the efficiency of theorem-proving in practice.

We will take a closer look at the problem IMO-2009-6 (grasshopper on a minefield), and discuss what should be a suitable logic (ITP) and desirable automation (ATP) in order to solve it. We describe an automation based on a translation into SMT / QF_LIA capable of solving all 27 intermediate ("sledgehammer") problems in the ITP solution.

The formalization of mathematical theorems and their proofs stands as a cornerstone in modern mathematics and computer science. Manual formalization, although precise, is prone to errors and can consume significant time and effort. Learning-assisted autoformalization may offer a promising path to this challenge. It operates as a subset of machine translation tasks in which (large) language models (LMs/LLMs) have shown to have remarkable performance, albeit with the added complexity of adhering to rigid and intricate grammatical structures inherent in formal logic systems. In this recently started project, we experiment with the capabilities of LMs to tackle the autoformalization task. Specifically, our objective is to finetune the Phi-2 model on the task of translating LaTeX, a widely used typesetting system for mathematical documents, into Isabelle, a formal proof assistant. Furthermore we plan on exploring the benefits of building a feedback loop that adds type-checking and theorem proving to continuously improve the learner to the pipeline for more accurate use of the AFP.

We consider the fragment of Second-Order unification, referred to as Second-Order Ground Unification (SOGU), with the following properties: (i) only one second-order variable allowed, (ii) first-order variables do not occur. We show that Hilbert’s 10th problem is reducible to a necessary condition for SOGU unifiability if the signature contains a binary function symbol and two constants, thus proving undecidability. This generalizes known undecidability results, as either first-order variable occurrences or multiple second-order variables were required for the reductions. Furthermore, we show that adding the following restriction: (i) the second-order variable has arity 1, (ii) the signature is finite, and (iii) the problem has bounded congruence, results in a decidable fragment. The latter fragment is related to bounded second-order unification in the sense that the number of bound variable occurrences is a function of the problem structure. We conclude with a discussion concerning the removal of the bounded congruence restriction.

Automated tactics in Coq are numerous but often limited to some specific logical fragments. Pre-processing can help them to be efficient in more situations, but it is often specialized to one tactic. This is why we worked on a general pre-processing tool designed to compose predictable atomic compositional transformations, called Orchestrator. We applied this tool to SMTCoq, a plugin which allows the use of SMT solvers within Coq. This led to the creation of the "snipe" push-button tactic, which applies pre-processing transformations composed by the Orchestrator and calls an SMT solver at the end.

This talk will be a brief overview of my work on cellular automata in the past four years. We will talk about their connection to artificial life, how to classify their qualitative dynamics, identify phase transitions, and lastly, how to measure their computational capacity through algebraic methods.

We first demonstrate how the Naproche system transforms Euclid's theorem, formalized in readable controlled natural language, into first-order logic and into TPTP prover tasks exported to external ATPs. Naproche is able to handle some sophisticated undergraduate mathematics. On the other hand the system is still exploratory and difficult to use with brittle proof and type checking. We shall round off the present version and its associated library of formalizations for inclusion into Isabelle2023 and Isabelle2024. Finally we discuss whether to continue the Naproche project by expanding the current version, or by radically rewriting and modifying the system, or by interfacing Naproche's natural linguistics with "big systems" like Isabelle/HOL or Lean.

Improvements in theorem proving often rely on neural networks to guide their proof search. However, due to relatively slow evaluation of networks this can decrease the amount of exploration that can be done in the search. We propose a tradeoff between accuracy and speed that maintains nearly the full performance of the underlying prover, by rejecting the state information of the proof and only evaluating on the problem itself.

Differentiable Inductive Logic Programming is a method of constructing Logic Programs (Prolog code) using gradient descent. I am going to talk about my recent experiments trying to improve the performance of this method.

Ethereum Smart Contracts become a widely adopted technology to build Decentralized Financial Applications (DeFis) and as such, they already hold 200 billion USDs. Consequently, bugs in smart contracts can be exploited by malicious users and can lead to losses at the scale of millions or even billions of USDs. To prevent such situations from happening, there has been a growing interest in developing scalable formal verification techniques for this domain. In this talk, we will specifically focus on the architecture of the Certora VerificationTool, i.e. an industrial standard automated prover technology to verify smart contracts. Besides a brief overview of the overall tool architecture, we will focus mainly on the SMT-based subroutines, including features such as domain-specific CEGAR methodology, distributed solver-portfolio approach, or techniques to share and exploit information between individual SMT solvers.

A “Natural” proof assistant is one that aims for formalizations that are close to ordinary mathematical texts. I will briefly explain the motivations behind the natural proof assistant Naproche and then talk about its implementation and the overall status of the project. I will conclude with a demo of Naproche (plus answering questions), probably using my WIP formalization of Tarskian geometry.

In this talk, I will share what I learned during my 3-month-long internship at the statistical physics group in EPFL, Lausanne. I will introduce the belief propagation algorithm and explain how it can be used to analyze the dynamics of discrete systems. I will discuss how this relates to my main field of research: studying complexity of discrete systems.

We know that certain objects exist even though we can't provide a single example. One way we establish such knowledge is with the probabilistic method: we show that a randomly selected object has the desired property with non-zero probability. I'll present probabilistic proofs in group theory. I'll mostly talk about maps into finite groups that preserve certain properties (such as disjointness, non-membership, non-conjugacy).

Soft-typed, even without hard distinction between formulas and objects. Kept simple stupid, yet expressive and vertisile. Logic can mimic e.g. natural deduction-style, or skolemization & resolution. Core written in pure Python but extensible with external ATPs. We will discuss the logical foundations, design choices, future plans, and how / if they differ from existing ITPs.

We are building logic-based components of a hybrid system for natural language commonsense question answering with explanations: a commonsense knowledge base, a first order reasoner extended with confidences and default logic, a semantic parser for English. The main upcoming tasks are finding different ways to integrate machine learning into all components of the system. Learning to guide proof search is one of the targets, but machine learning could be also used for improving both the knowledge base and semantic parsing. The talk will give an overview of the current system, briefly describe other similar projects and outline several research questions and ideas for applying machine learning in this framework.

Program invariants play an important useful role in understanding programs as well as verifying properties about them. There are many ways to obtain program invariants--automatically, semi-automatically or they could be provided by a programmer as a part of a specification of the program or as annotations. The problem of determining whether a proposed formula is an invariant is undecidable. In this talk, methods are proposed to determine when in certain cases, formulas expressed in various logical theories can be determined to be invariant. If a formula is indeed an invariant, a saturation based procedure for strengthening the formula to generate inductive invariants are explored. This approach is contrasted with property directed reachability approach toward for program analysis.

TBA

I will talk about convolutional graph neural networks used for reinforcement learning with leanCoP.

In this talk, I briefly present various approaches how to represent a formula using neural networks. This includes representations where a formula is a sequence of symbols, a tree, and a part of a more involved graph structure.

In this talk, I will explain what is the BLEU (Bilingual Evaluation Understudy) rate used in machine translation evaluations and how it is useful for our informal2formal experiments.

In this informal lecture, I present latest developments of curriculum learning of theorem proving in the LeanCoP setting. I present a simple reinforcement learning system based on proximal policy optimization (PPO) that was trained to guide the proof search of LeanCoP ATP. We first trained the system on simple arithmetic formulae (in Robinson arithmetic), which successfully generalized from the proof of a single multiplication (1*1=1) to additions/multiplications with arbitrarily large numbers. We are working to extend these results to more complex arithmetic formulae and then - hopefully - to more complex problem domains as well.

Finite model finders represent a powerful tool for deciding problems with the finite model property, such as the Bernays-Schoenfinkel fragment (EPR). Further, finite model finders provide useful information for counter-satisfiable conjectures. In this talk, I will describe several novel techniques in a finite model-finder based on the translation to SAT, referred to as the MACE-style approach. The proposed approach is driven by counterexample abstraction refinement (CEGAR), which has proven to be a powerful tool in the context of quantifiers in satisfiability modulo theories (SMT) and quantified Boolean formulas (QBF). One weakness of CEGAR-based approaches is that certain amount of luck is required in order to guess the right model, because the solver always operates on incomplete information about the formula. To tackle this issue, the model finder is enhanced with a machine learning algorithm to improve the likelihood that the right model is encountered. The implemented prototype based on the presented ideas shows highly promising results.

CakeML is a functional programming language with a proven-correct compiler and runtime system. Ramana is one of the main developers of CakeML.

In this talk, I explain how computers control modern jet engines, and how they manage to keep them safe and reliable. I briefly explain how a jet engine works, before covering some basics about engine control hardware and software architecture. I then go on to talk about the software development processes that are typically employed.

The Common HOL project aims to facilitate porting source code and proofs between members of the HOL family of theorem provers. At the heart of the project is the Common HOL Platform, which defines a standard HOL theory and API that aims to be compatible with all HOL systems. So far, HOL Light and hol90 have been adapted for conformance, and HOL Zero was originally developed to conform. In this talk we provide motivation for a platform, give an overview of the Common HOL Platform's theory and API components, and show how to adapt legacy systems. We also report on the platform's successful application in the hand-translation of a few thousand lines of source code from HOL Light to HOL Zero.

A tautological clause is a clause which contains both a literal and its complement. While in the classical setting of propositional and first-order logic tautologies are harmless (in the sense that they are always vacuously satisfied and thus can be safely discarded), in the study of resolution-based calculi for quantified boolean formulas (QBF) we encounter tautologies which can be harmful (their generation is explicitly prohibited, because they would make the calculus unsound), but also useful (the long-distance resolution calculus gains exponential power over Q-resolution by allowing generation of certain tautologies). I will try to shed light on this discrepancy through the lens of the translation of QBF to first-order logic proposed by Seidl et al. (2012). This should also motivate a discussion about the currently missing local semantics of a clause within the context of QBF resolution-based calculi.

Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga provides a sophisticated infrastructure based on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivation trees as recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions. Our experience has demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics. To demonstrate Beluga's strength in this talk, we develop a weak normalization proof using logical relations.

In automated reasoning it is common that first-order formulas need to be translated into clausal normal form for proof search. The structure of this normal form can have a large impact on the performance of first-order theorem provers, influencing whether a proof can be found and how quickly. It is common folklore that translations should ideally minimise both the size of the generated clause set and extensions to the signature. This paper introduces a new top-down approach to clausal form generation for first-order formulas that aims to achieve this goal in a new way. The main advantage of this approach over existing bottom-up techniques is that more contextual information is available at points where decisions such as subformula-naming and skolemisation occur. Experimental results show that our implementation of the translation in Vampire can lead to clausal forms which are smaller and better suited to proof search.

We propose a method combining relational-logic representations with neural network learning. A general lifted architecture, possibly reflecting some background domain knowledge, is described through relational rules which may be handcrafted or learned. The relational rule-set serves as a template for unfolding possibly deep neural networks whose structures also reflect the structures of given training or testing relational examples. Different networks corresponding to different examples share their weights, which co-evolve during training by stochastic gradient descent algorithm. The framework allows for hierarchical relational modeling constructs and learning of latent relational concepts through shared hidden layers weights corresponding to the rules. Discovery of notable relational concepts and experiments on 78 relational learning benchmarks demonstrate favorable performance of the method.

Deterministic multiagent planning described by MASTRIPS formalism requires mixture of coordination and synthesis of local agents' plans. All agents' plans, as sequences of actions, can be implicitly described by an appropriate generative structure. Having all local plans of all participating agents described by such a structure and having a merged process of such structures, we can induce a global multiagent plan by successive elimination of unfeasible combinations of local agents' plans. In this paper, we propose use of Nondeterministic Finite StateMachines (NFSs) as the generative structure for the plans and use of well-known process of intersection of NFSs to prune the plan spaces towards globally feasible multiagent plan. Since the numbers of the plans can be large we use iterative process of building of the NFSs using a state-of-the-art classical planner interleaved with the NFS intersecting process. To show efficiency of the approach, we have evaluated the algorithm on extensive number of planning problems from Internation Planning Competition extended for multiagent planning.

Deterministic multiagent planning described by MASTRIPS formalism requires mixture of coordination and synthesis of local agents' plans. All agents' plans, as sequences of actions, can be implicitly described by an appropriate generative structure. Having all local plans of all participating agents described by such a structure and having a merged process of such structures, we can induce a global multiagent plan by successive elimination of unfeasible combinations of local agents' plans. In this paper, we propose use of Nondeterministic Finite StateMachines (NFSs) as the generative structure for the plans and use of well-known process of intersection of NFSs to prune the plan spaces towards globally feasible multiagent plan. Since the numbers of the plans can be large we use iterative process of building of the NFSs using a state-of-the-art classical planner interleaved with the NFS intersecting process. To show efficiency of the approach, we have evaluated the algorithm on extensive number of planning problems from Internation Planning Competition extended for multiagent planning.

Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statements is named and re-used in later proofs by formal mathematicians. In this work, we suggest and implement criteria defining the estimated usefulness of the HOL Light lemmas for proving further theorems. We use these criteria to mine the large inference graph of all lemmas in the core HOL Light library, adding thousands of the best lemmas to the pool of named statements that can be re-used in later proofs. The usefulness of the new lemmas is then evaluated by comparing the performance of automated proving of the core HOL Light theorems with and without such added lemmas.

We prove that the consequence relation in the Full Non-associative Lambek calculus is undecidable. An encoding of the halting problem for 2-tag systems using finitely many non-logical axioms in the language {⋅,∨} will be presented. Therefore already the consequence relation in this fragment is undecidable. Moreover, the construction works even when the structural rules of exchange and contraction are added.

HOL(y)Hammer is an AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system, in particular for the users of the large Flyspeck library. The service uses several automated reasoning systems combined with several premise selection methods trained on previous Flyspeck proofs, to attack a new conjecture that uses the concepts defined in the Flyspeck library. The public online incarnation of the service runs on a 48-CPU server, currently employing in parallel for each task 25 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also available for local installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise are discussed, and an initial account of using the system is given.

Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means term-constructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. Our extension includes new definitions of alpha-equivalence and establishes automatically the reasoning infrastructure for alphaequated terms. We also prove strong induction principles that have the usual variable convention already built in.

http://www.cs.miami.edu/~tptp/MizarTPTP/

We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa. The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa. The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

In Isabelle/HOL, code generation is understood as the transformation of a system of equational theorems into a program in a functional programming language with the same equational semantics. This guarantees partial correctness of generated programs. This generic framework is instantiated for SML, OCaml and Haskell. The meta-theory permits program and datatype refinement, i.e. the replacement of abstract algorithms and representations by efficient and executable programs and data structures . without endangering partial correctness. On top of this, the scope of executable specifications can be extended by providing tools which produce suitable equational specifications from theories. An example is a predicate compiler which turns inductive specifications into equational ones, thus opening the world of functional-logic programming for code generation. Additionally, we have provided Haskabelle which transforms a subset of Haskell to Isabelle/HOL theory text.

Over the years, proof systems for propositional satisfiability (SAT) have been extensively studied. Recently, proof systems for quantified Boolean formulas (QBFs) have also been gaining attention. Q-resolution is a calculus enabling producing proofs from DPLL-based QBF solvers. While DPLL has become a dominating technique for SAT, QBF has been tackled by other complementary and competitive approaches. One of these approaches is based on expanding variables until the formula contains only one type of quantifier; upon which a SAT solver is invoked. This approach motivates the theoretical analysis carried out in this paper. We focus on a two phase proof system, which expands the formula in the first phase and applies propositional resolution in the second. Fragments of this proof system are defined and compared to Q-resolution.

The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.