Project acronym AI4REASON
Project Artificial Intelligence for Large-Scale Computer-Assisted Reasoning
Researcher (PI) Josef Urban
Host Institution (HI) CESKE VYSOKE UCENI TECHNICKE V PRAZE
Call Details Consolidator Grant (CoG), PE6, ERC-2014-CoG
Summary 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 on which today's information society critically depends.
It seems extremely complex and unlikely to design an explicitly programmed solution to the problem. However, we have recently demonstrated that the performance of existing approaches can be multiplied by data-driven AI methods that learn reasoning guidance from large proof corpora. The breakthrough will be achieved by developing such novel AI methods. First, we will devise suitable Automated Reasoning and Machine Learning methods that learn reasoning knowledge and steer the reasoning processes at various levels of granularity. Second, we will combine them into autonomous self-improving AI systems that interleave deduction and learning in positive feedback loops. Third, we will develop 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.
The expected outcome is our ability to prove automatically at least 50% more theorems in high-assurance projects such as Flyspeck and seL4, bringing a major breakthrough in formal reasoning and verification. As an AI effort, the project offers a unique path to large-scale semantic AI. The formal corpora concentrate centuries of deep human thinking in a computer-understandable form on which deductive and inductive AI can be combined and co-evolved, providing new insights into how humans do mathematics and science.
Summary
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 on which today's information society critically depends.
It seems extremely complex and unlikely to design an explicitly programmed solution to the problem. However, we have recently demonstrated that the performance of existing approaches can be multiplied by data-driven AI methods that learn reasoning guidance from large proof corpora. The breakthrough will be achieved by developing such novel AI methods. First, we will devise suitable Automated Reasoning and Machine Learning methods that learn reasoning knowledge and steer the reasoning processes at various levels of granularity. Second, we will combine them into autonomous self-improving AI systems that interleave deduction and learning in positive feedback loops. Third, we will develop 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.
The expected outcome is our ability to prove automatically at least 50% more theorems in high-assurance projects such as Flyspeck and seL4, bringing a major breakthrough in formal reasoning and verification. As an AI effort, the project offers a unique path to large-scale semantic AI. The formal corpora concentrate centuries of deep human thinking in a computer-understandable form on which deductive and inductive AI can be combined and co-evolved, providing new insights into how humans do mathematics and science.
Max ERC Funding
1 499 500 €
Duration
Start date: 2015-09-01, End date: 2020-08-31
Project acronym CoCoSym
Project Symmetry in Computational Complexity
Researcher (PI) Libor BARTO
Host Institution (HI) UNIVERZITA KARLOVA
Call Details Consolidator Grant (CoG), PE6, ERC-2017-COG
Summary The last 20 years of rapid development in the computational-theoretic aspects of the fixed-language Constraint Satisfaction Problems (CSPs) has been fueled by a connection between the complexity and a certain concept capturing symmetry of computational problems in this class.
My vision is that this connection will eventually evolve into the organizing principle of computational complexity and will lead to solutions of fundamental problems such as the Unique Games Conjecture or even the P-versus-NP problem. In order to break through the current limits of this algebraic approach, I will concentrate on specific goals designed to
(A) discover suitable objects capturing symmetry that reflect the complexity in problem classes, where such an object is not known yet;
(B) make the natural ordering of symmetries coarser so that it reflects the complexity more faithfully;
(C) delineate the borderline between computationally hard and easy problems;
(D) strengthen characterizations of existing borderlines to increase their usefulness as tools for proving hardness and designing efficient algorithm; and
(E) design efficient algorithms based on direct and indirect uses of symmetries.
The specific goals concern the fixed-language CSP over finite relational structures and its generalizations to infinite domains (iCSP) and weighted relations (vCSP), in which the algebraic theory is highly developed and the limitations are clearly visible.
The approach is based on joining the forces of the universal algebraic methods in finite domains, model-theoretical and topological methods in the iCSP, and analytical and probabilistic methods in the vCSP. The starting point is to generalize and improve the Absorption Theory from finite domains.
Summary
The last 20 years of rapid development in the computational-theoretic aspects of the fixed-language Constraint Satisfaction Problems (CSPs) has been fueled by a connection between the complexity and a certain concept capturing symmetry of computational problems in this class.
My vision is that this connection will eventually evolve into the organizing principle of computational complexity and will lead to solutions of fundamental problems such as the Unique Games Conjecture or even the P-versus-NP problem. In order to break through the current limits of this algebraic approach, I will concentrate on specific goals designed to
(A) discover suitable objects capturing symmetry that reflect the complexity in problem classes, where such an object is not known yet;
(B) make the natural ordering of symmetries coarser so that it reflects the complexity more faithfully;
(C) delineate the borderline between computationally hard and easy problems;
(D) strengthen characterizations of existing borderlines to increase their usefulness as tools for proving hardness and designing efficient algorithm; and
(E) design efficient algorithms based on direct and indirect uses of symmetries.
The specific goals concern the fixed-language CSP over finite relational structures and its generalizations to infinite domains (iCSP) and weighted relations (vCSP), in which the algebraic theory is highly developed and the limitations are clearly visible.
The approach is based on joining the forces of the universal algebraic methods in finite domains, model-theoretical and topological methods in the iCSP, and analytical and probabilistic methods in the vCSP. The starting point is to generalize and improve the Absorption Theory from finite domains.
Max ERC Funding
1 211 375 €
Duration
Start date: 2018-02-01, End date: 2023-01-31
Project acronym LBCAD
Project Lower bounds for combinatorial algorithms and dynamic problems
Researcher (PI) Michal Koucky
Host Institution (HI) UNIVERZITA KARLOVA
Call Details Consolidator Grant (CoG), PE6, ERC-2013-CoG
Summary This project aims to establish the time complexity of algorithms for two classes of problems. The first class consists of problems related to Boolean matrix multiplication and matrix multiplication over various semirings. This class contains problems such as computing transitive closure of a graph and determining the minimum distance between all-pairs of nodes in a graph. Known combinatorial algorithms for these problems run in slightly sub-cubic time. By combinatorial algorithms we mean algorithms that do not rely on the fast matrix multiplication over rings. Our goal is to show that the known combinatorial algorithms for these problems are essentially optimal. This requires designing a model of combinatorial algorithms and proving almost cubic lower bounds in it.
The other class of problems that we will focus on contains dynamic data structure problems such as dynamic graph reachability and related problems. Known algorithms for these problems exhibit trade-off between the query time and the update time, where at least one of them is always polynomial. Our goal is to show that indeed any algorithm for these problems must have update time or query time at least polynomial.
The two classes of problems are closely associated with so called 3SUM problem which serves as a benchmark for uncomputability in sub-quadratic time. Our goal is to deepen and extend the known connections between 3SUM, the other two classes and problems like formula satisfiability (SAT).
Summary
This project aims to establish the time complexity of algorithms for two classes of problems. The first class consists of problems related to Boolean matrix multiplication and matrix multiplication over various semirings. This class contains problems such as computing transitive closure of a graph and determining the minimum distance between all-pairs of nodes in a graph. Known combinatorial algorithms for these problems run in slightly sub-cubic time. By combinatorial algorithms we mean algorithms that do not rely on the fast matrix multiplication over rings. Our goal is to show that the known combinatorial algorithms for these problems are essentially optimal. This requires designing a model of combinatorial algorithms and proving almost cubic lower bounds in it.
The other class of problems that we will focus on contains dynamic data structure problems such as dynamic graph reachability and related problems. Known algorithms for these problems exhibit trade-off between the query time and the update time, where at least one of them is always polynomial. Our goal is to show that indeed any algorithm for these problems must have update time or query time at least polynomial.
The two classes of problems are closely associated with so called 3SUM problem which serves as a benchmark for uncomputability in sub-quadratic time. Our goal is to deepen and extend the known connections between 3SUM, the other two classes and problems like formula satisfiability (SAT).
Max ERC Funding
900 200 €
Duration
Start date: 2014-02-01, End date: 2019-01-31
