Next Generation Computer Assisted Reasoning

ongoing

Galileo said that mathematics is the language of science. It is used to solve arbitrary abstract problems, underpinning hard sciences, technology and engineering. Automation of complex mathematical reasoning, discovery and large-scale formal proofs is today one of the greatest challenges in the fields of Automated Reasoning (AR) and Artificial Intelligence (AI). Compared to human experts, today’s main automated reasoning and theorem proving paradigms are severely one-sided: they largely lack the capability to combine learning, reasoning and conjecturing in complex feedback loops. There is solid evidence that such combinations are the key to building the next generation of advanced reasoning systems for mathematics, computer-assisted proof and formal verification. The NextReason project will create one of the world’s strongest teams working on such combinations. We will jointly develop (i) logic-aware learning architectures and neuro-symbolic methods for a range of automated and interactive theorem proving paradigms, (ii) novel AI approaches for learning-guided automated decomposition of hard reasoning problems, (iii) methods for automated formalization of human-written mathematics by combining learning-based translation methods with semantic methods such as type-checking and theorem proving, (iv) neuro-symbolic methods for synthesis of interesting mathematical objects, conjectures and explanations, and (v) autonomous systems and positive feedback loops interleaving learning, theory exploration and efficiently guided proof search to attack hard and open problems. The expected overall outcome is a new generation of strong architectures for reasoning and theorem proving, and their transformative effect on large-scale computer-assisted proof, mathematics and formal verification.