About

The goal of the AI4REASON project is a breakthrough in what is considered a very hard problem in AI and automation of reasoning, namely the problem of automatically proving theorems in large and complex theories.

Such complex formal theories arise in projects aimed at verification of today's advanced mathematics such as the Formal Proof of the Kepler Conjecture (Flyspeck), verification of software and hardware designs such as the seL4 operating system kernel, and verification of other advanced systems and technologies of today's information society.

It seems extremely complex and unlikely to design an explicitly programmed solution to the problem. However, we have recently shown that the performance of existing approaches can be multiplied by data-driven AI methods that learn reasoning guidance from large proof corpora.

The AI4REASON project focuses on developing such novel AI methods:

• Devising suitable Automated Reasoning and Machine Learning methods that learn reasoning knowledge and steer the reasoning processes at various levels of granularity.
• Combining them into autonomous self-improving AI systems that interleave deduction and learning in positive feedback loops.
• Developing approaches that aggregate reasoning knowledge across many formal, semi-formal and informal corpora and deploy the methods as strong automation services for the formal proof community.