Mgr. Josef Urban, Ph.D.

Specialist supervisor: Lasse Blaauwbroek, MSc.

Machine learning for interactive theorem proving is a topic with growing interest. Many individual learning projects exist which have seen considerable success in recent years. However, a lot still remains to be done to make machine learning viable in the wild. One roadblock is that most projects exist within their individual silo and cannot be directly compared to others. This is an issue that is already being solved in the wider domain of machine learning through initiatives such as the OpenML platform [1, 2] that allows one to create datasets and corresponding learning tasks and upload them to the platform. Once a dataset and task are uploaded, anyone can create and upload models that attempt to solve the task. The platform will then automatically evaluate and compare all submitted models, creating rich interactive visualizations that highlight the relative strengths and weaknesses of the models. Collaborative platforms bring considerable advantages, the most important one is the ability to easily compare different learning models through fair and consistent benchmarks that represent real-world conditions. Currently, every machine learning project develops their own evaluation technique, many of which do not represent real conditions. Additionally, human-computer research has shown that the "gamification" of difficult problems considerably helps with competitive engagement of a community [3]. Unfortunately, the data, evaluation methods and models associated to theorem proving are too complex to fit within the generic framework of initiatives like OpenML. As such, we will develop a dedicated platform for interactive theorem proving. Previous attempts at developing a central platform for theorem proving [4, 5, 14] have not gained much traction due to a lack of an interactive component. They provide a single, static dataset and code to perform an evaluation but lack the ability to automatically, fairly and interactively compare different models of the community. This work is on the intersection of multiple topics including machine learning, theorem proving, human-computer interaction, web technologies and engineering. Developing a successful platform involves multiple research angles and technical components.

More information:

• DocsGoogle

Specialist supervisor: Dr. Adam Pease

Train state-of-the-art language models to translate natural language statements such as "The cup is on the table" to formal logic statements. Those will be altimately used by today's automated theorem provers (ATPs) such as Vampire and E prover to derive conclusions from the statements. In this research we will use the SUMO (https://www.ontologyportal.org/) language and formal ontology. For example, the previous statement in SUMO will look as follows:

(exists (?X ?Y)
   (and
      (instance ?X Table)
      (instance ?Y Cup)
      (orientation ?Y ?X On)))

The language translation will be complemented by semantic tools such as SUMO's syntax and semantic checker. Data augmentation methods will be developed to increase the size of the training corpus for the NLP methods. This includes for example generating synthetic data by using SUMO's logic to language translator, direct translation to different natural languages, and transitive data generation via NLP-based methods such as Google Translate between different natural languages. The ultimate goal is to automatically enrich the SUMO knowledge base by a large amount of common-sense facts expressed in natural language. This will in turn allow automated reasoning about a growing number of everyday topics.

Specialist supervisor: RNDr. Martin Suda, Ph.D.

Automated theorem proving aims to fulfil the dream of automating mathematically precise deductive reasoning, with applications in formal verification of safety critical systems or the formalisation of math. Research on practical automated theorem provers combines development of logical calculi with their efficient implementation and empirical evaluation on relevant problem sets. Equally important role is played by effective heuristics which help to guide the search for the proof. Recent advances in AI, most notably machine learning and neural networks, allow for automated discovery of such heuristics, either from past prover experiences or in a reinforcement learning setup. The aim of the thesis will be to advance the state of the art in this area and to develop new methods for the automatic discovery of proof search heuristics.