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 CHOBOTIX
Project Chemical Processing by Swarm Robotics
Researcher (PI) Frantisek Stepanek
Host Institution (HI) VYSOKA SKOLA CHEMICKO-TECHNOLOGICKA V PRAZE
Call Details Starting Grant (StG), PE6, ERC-2007-StG
Summary The aim of the project is to develop chemical processing systems based on the principle of swarm robotics. The inspiration for swarm robotics comes from the behaviour of collective organisms – such as bees or ants – that can perform complex tasks by the combined actions of a large number of relatively simple, identical agents. The main scientific challenge of the project will be the design and synthesis of chemical swarm robots (“chobots”), which we envisage as internally structured particulate entities in the 10-100 µm size range that can move in their environment, selectively exchange molecules with their surrounding in response to a local change in temperature or concentration, chemically process those molecules and either accumulate or release the product. Such chemically active autonomous entities can be viewed as very simple pre-biotic life forms, although without the ability to self-replicate or evolve. In the course of the project, the following topics will be explored in detail: (i) the synthesis of suitable shells for chemically active swarm robots, both soft (with a flexible membrane) and hard (porous solid shells); (ii) the mechanisms of molecular transport into and out of such shells and means of its active control; (iii) chemical reaction kinetics in spatially complex compartmental structures within the shells; (iv) collective behaviour of chemical swarm robots and their response to external stimuli. The project will be carried out by a multi-disciplinary team of enthusiastic young researchers and the concepts and technologies developed in course of the project, as well as the advancements in the fundamental understanding of the behaviour of “chemical robots” and their functional sub-systems, will open up new opportunities in diverse areas including next-generation distributed chemical processing, synthesis and delivery of personalised medicines, recovery of valuable chemicals from dilute resources, environmental clean-up, and others.
Summary
The aim of the project is to develop chemical processing systems based on the principle of swarm robotics. The inspiration for swarm robotics comes from the behaviour of collective organisms – such as bees or ants – that can perform complex tasks by the combined actions of a large number of relatively simple, identical agents. The main scientific challenge of the project will be the design and synthesis of chemical swarm robots (“chobots”), which we envisage as internally structured particulate entities in the 10-100 µm size range that can move in their environment, selectively exchange molecules with their surrounding in response to a local change in temperature or concentration, chemically process those molecules and either accumulate or release the product. Such chemically active autonomous entities can be viewed as very simple pre-biotic life forms, although without the ability to self-replicate or evolve. In the course of the project, the following topics will be explored in detail: (i) the synthesis of suitable shells for chemically active swarm robots, both soft (with a flexible membrane) and hard (porous solid shells); (ii) the mechanisms of molecular transport into and out of such shells and means of its active control; (iii) chemical reaction kinetics in spatially complex compartmental structures within the shells; (iv) collective behaviour of chemical swarm robots and their response to external stimuli. The project will be carried out by a multi-disciplinary team of enthusiastic young researchers and the concepts and technologies developed in course of the project, as well as the advancements in the fundamental understanding of the behaviour of “chemical robots” and their functional sub-systems, will open up new opportunities in diverse areas including next-generation distributed chemical processing, synthesis and delivery of personalised medicines, recovery of valuable chemicals from dilute resources, environmental clean-up, and others.
Max ERC Funding
1 644 000 €
Duration
Start date: 2008-06-01, End date: 2013-05-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 ELE
Project Evolving Language Ecosystems
Researcher (PI) Jan VITEK
Host Institution (HI) CESKE VYSOKE UCENI TECHNICKE V PRAZE
Call Details Advanced Grant (AdG), PE6, ERC-2015-AdG
Summary The ELE project will study the foundational principles of programming language evolution and develop practical tools and technologies for supporting the evolution of complete ecosystems. If successful, ELE will drastically decrease the cost of evolution and avoid the need to invent completely new languages every time there is a shift in hardware trends or in programming methodology. Instead, ELE will allow evolution of languages and will support migration of code and knowledge bases. The project proceeds along two major axes. The first axis is language dynamics where new features and new capabilities are added to a preexisting language. This requires changing, at the same time, the language's specification, it's semantics, and the language's implementation, the compiler and interpreter that runs code written in the language as well the runtime libraries that provide basic capabilities. The second axis for evolution is language statics where new rules are added to enforce novel programming disciplines and where existing code artifacts are adapted to new semantics. These axes are not entirely disjoint, as static restrictions, such as a new type system, can feedback into the implementation by providing behavioral information that can be exploited by a compiler.
Summary
The ELE project will study the foundational principles of programming language evolution and develop practical tools and technologies for supporting the evolution of complete ecosystems. If successful, ELE will drastically decrease the cost of evolution and avoid the need to invent completely new languages every time there is a shift in hardware trends or in programming methodology. Instead, ELE will allow evolution of languages and will support migration of code and knowledge bases. The project proceeds along two major axes. The first axis is language dynamics where new features and new capabilities are added to a preexisting language. This requires changing, at the same time, the language's specification, it's semantics, and the language's implementation, the compiler and interpreter that runs code written in the language as well the runtime libraries that provide basic capabilities. The second axis for evolution is language statics where new rules are added to enforce novel programming disciplines and where existing code artifacts are adapted to new semantics. These axes are not entirely disjoint, as static restrictions, such as a new type system, can feedback into the implementation by providing behavioral information that can be exploited by a compiler.
Max ERC Funding
3 234 000 €
Duration
Start date: 2016-10-01, End date: 2021-09-30
Project acronym FEALORA
Project "Feasibility, logic and randomness in computational complexity"
Researcher (PI) Pavel Pudlák
Host Institution (HI) MATEMATICKY USTAV AV CR V.V.I.
Call Details Advanced Grant (AdG), PE6, ERC-2013-ADG
Summary "We will study fundamental problems in complexity theory using means developed in logic, specifically, in the filed of proof complexity. Since these problems seem extremely difficult and little progress has been achieved in solving them, we will prove results that will explain why they are so difficult and in which direction theory should be developed.
Our aim is to develop a system of conjectures based on the concepts of feasible incompleteness and pseudorandomness. Feasible incompleteness refers to conjectures about unprovability of statements concerning low complexity computations and about lengths of proofs of finite consistency statements. Essentially, they say that incompleteness in the finite domain behaves in a similar way as in the infinite. Several conjectures of this kind have been already stated. They have strong consequences concerning separation of complexity classes, but only a few special cases have been proved. We want to develop a unified system which will also include conjectures connecting feasible incompleteness with pseudorandomness. A major part of our work will concern proving special cases and relativized versions of these conjectures in order to provide evidence for their truth. We believe that the essence of the fundamental problems in complexity theory is logical, and thus developing theory in the way described above will eventually lead to their solution."
Summary
"We will study fundamental problems in complexity theory using means developed in logic, specifically, in the filed of proof complexity. Since these problems seem extremely difficult and little progress has been achieved in solving them, we will prove results that will explain why they are so difficult and in which direction theory should be developed.
Our aim is to develop a system of conjectures based on the concepts of feasible incompleteness and pseudorandomness. Feasible incompleteness refers to conjectures about unprovability of statements concerning low complexity computations and about lengths of proofs of finite consistency statements. Essentially, they say that incompleteness in the finite domain behaves in a similar way as in the infinite. Several conjectures of this kind have been already stated. They have strong consequences concerning separation of complexity classes, but only a few special cases have been proved. We want to develop a unified system which will also include conjectures connecting feasible incompleteness with pseudorandomness. A major part of our work will concern proving special cases and relativized versions of these conjectures in order to provide evidence for their truth. We believe that the essence of the fundamental problems in complexity theory is logical, and thus developing theory in the way described above will eventually lead to their solution."
Max ERC Funding
1 259 596 €
Duration
Start date: 2014-01-01, End date: 2018-12-31
Project acronym LaDIST
Project Large Discrete Structures
Researcher (PI) Daniel Kral
Host Institution (HI) Masarykova univerzita
Call Details Consolidator Grant (CoG), PE1, ERC-2014-CoG
Summary The proposed project seeks to introduce novel methods to analyze and approximate large graphs and other discrete structures and to apply the developed methods to solve specific open problems. A need for such methods comes from computer science where the sizes of input structures are often enormous. Specifically, the project will advance the recently emerged theory of combinatorial limits by developing new insights in the structure of limit objects and by proposing a robust theory bridging the sparse and dense cases. The analytic methods from the theory of combinatorial limits will be used to analyze possible asymptotic behavior of large graphs and they will be applied in conjunction with structural arguments to provide solutions to specific problems in extremal combinatorics. The obtained insights will also be combined with methods from discrete optimization and logic to provide new algorithmic frameworks.
Summary
The proposed project seeks to introduce novel methods to analyze and approximate large graphs and other discrete structures and to apply the developed methods to solve specific open problems. A need for such methods comes from computer science where the sizes of input structures are often enormous. Specifically, the project will advance the recently emerged theory of combinatorial limits by developing new insights in the structure of limit objects and by proposing a robust theory bridging the sparse and dense cases. The analytic methods from the theory of combinatorial limits will be used to analyze possible asymptotic behavior of large graphs and they will be applied in conjunction with structural arguments to provide solutions to specific problems in extremal combinatorics. The obtained insights will also be combined with methods from discrete optimization and logic to provide new algorithmic frameworks.
Max ERC Funding
1 386 859 €
Duration
Start date: 2015-12-01, End date: 2020-11-30
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
Project acronym MATHEF
Project Mathematical Thermodynamics of Fluids
Researcher (PI) Eduard Feireisl
Host Institution (HI) MATEMATICKY USTAV AV CR V.V.I.
Call Details Advanced Grant (AdG), PE1, ERC-2012-ADG_20120216
Summary "The main goal of the present research proposal is to build up a general mathematical theory describing the motion of a compressible, viscous, and heat conductive fluid. Our approach is based on the concept of generalized (weak) solutions satisfying the basic physical principles of balance of mass, momentum, and energy. The energy balance is expressed in terms of a variant of entropy inequality supplemented with an integral identity for the total energy balance.
We propose to identify a class of suitable weak solutions, where admissibility is based on a direct application of the principle of maximal entropy production compatible with Second law of thermodynamics. Stability of the solution family will be investigated by the method of relative entropies constructed on the basis of certain thermodynamics potentials as ballistic free energy.
The new solution framework will be applied to multiscale problems, where several characteristic scales become small or extremely large. We focus on mutual interaction of scales during this process and identify the asymptotic behavior of the quantities that are filtered out in the singular limits. We also propose to study the influence of the geometry of the underlying physical space that may change in the course of the limit process. In particular, problems arising in homogenization and optimal shape design in combination with various singular limits are taken into account.
The abstract approximate scheme used in the existence theory will be adapted in order to develop adequate numerical methods. We study stability and convergence of these methods using the tools developed in the abstract part, in particular, the relative entropies."
Summary
"The main goal of the present research proposal is to build up a general mathematical theory describing the motion of a compressible, viscous, and heat conductive fluid. Our approach is based on the concept of generalized (weak) solutions satisfying the basic physical principles of balance of mass, momentum, and energy. The energy balance is expressed in terms of a variant of entropy inequality supplemented with an integral identity for the total energy balance.
We propose to identify a class of suitable weak solutions, where admissibility is based on a direct application of the principle of maximal entropy production compatible with Second law of thermodynamics. Stability of the solution family will be investigated by the method of relative entropies constructed on the basis of certain thermodynamics potentials as ballistic free energy.
The new solution framework will be applied to multiscale problems, where several characteristic scales become small or extremely large. We focus on mutual interaction of scales during this process and identify the asymptotic behavior of the quantities that are filtered out in the singular limits. We also propose to study the influence of the geometry of the underlying physical space that may change in the course of the limit process. In particular, problems arising in homogenization and optimal shape design in combination with various singular limits are taken into account.
The abstract approximate scheme used in the existence theory will be adapted in order to develop adequate numerical methods. We study stability and convergence of these methods using the tools developed in the abstract part, in particular, the relative entropies."
Max ERC Funding
726 320 €
Duration
Start date: 2013-05-01, End date: 2018-04-30
Project acronym ToMeTuM
Project Towards the Understanding a Metal-Tumour-Metabolism
Researcher (PI) Vojtech Adam
Host Institution (HI) VYSOKE UCENI TECHNICKE V BRNE
Call Details Starting Grant (StG), LS7, ERC-2017-STG
Summary A tumour cell uses both genetic and protein weapons in its development. Gaining a greater understanding of these lethal mechanisms is a key step towards developing novel and more effective treatments. Because the metal ion metabolism of a tumour cell is not fully understood, we will address the challenge of explaining the mechanisms of how a tumour cell copes both with essential metal ions and platinum based drugs. The metal-based mechanisms help a tumour to grow on one side and to protect itself against commonly used metal-based drugs. On the other side, the exact description of these mechanisms, which are being associated with multi-drug resistance occurrence and failure of a treatment, still remains unclear. We will reveal the mechanism of the as yet not understood biochemical and molecularly-biological relationships and correlations between metal ions and proteins in a tumour development revealing the way how to suppress the growth and development of a tumour and to markedly enhance the effectiveness of a treatment.
To achieve this goal, we will focus on metallothionein and its interactions with essential metals and metal-containing anticancer drugs (cisplatin, carboplatin, and oxaliplatin). Their actions will be monitored both in vitro and in vivo. For this purpose, we will optimize electrochemical, mass spectrometric and immune-based methods. Based on processing of data obtained, new carcinogenetic pathways will be sought on cell level and proved by genetic modifications of target genes. The discovered processes and the pathways found will then be tested on two animal experimental models mice bearing breast tumours (MCF-7 and 4T1) and MeLiM minipigs bearing melanomas.
The precise description of the tumour related pathways coping with metal ions based on metallothioneins will direct new highly effective treatment strategies. Moreover, the discovery of new carcinogenetic pathways will open a window for understanding of cancer formation and development.
Summary
A tumour cell uses both genetic and protein weapons in its development. Gaining a greater understanding of these lethal mechanisms is a key step towards developing novel and more effective treatments. Because the metal ion metabolism of a tumour cell is not fully understood, we will address the challenge of explaining the mechanisms of how a tumour cell copes both with essential metal ions and platinum based drugs. The metal-based mechanisms help a tumour to grow on one side and to protect itself against commonly used metal-based drugs. On the other side, the exact description of these mechanisms, which are being associated with multi-drug resistance occurrence and failure of a treatment, still remains unclear. We will reveal the mechanism of the as yet not understood biochemical and molecularly-biological relationships and correlations between metal ions and proteins in a tumour development revealing the way how to suppress the growth and development of a tumour and to markedly enhance the effectiveness of a treatment.
To achieve this goal, we will focus on metallothionein and its interactions with essential metals and metal-containing anticancer drugs (cisplatin, carboplatin, and oxaliplatin). Their actions will be monitored both in vitro and in vivo. For this purpose, we will optimize electrochemical, mass spectrometric and immune-based methods. Based on processing of data obtained, new carcinogenetic pathways will be sought on cell level and proved by genetic modifications of target genes. The discovered processes and the pathways found will then be tested on two animal experimental models mice bearing breast tumours (MCF-7 and 4T1) and MeLiM minipigs bearing melanomas.
The precise description of the tumour related pathways coping with metal ions based on metallothioneins will direct new highly effective treatment strategies. Moreover, the discovery of new carcinogenetic pathways will open a window for understanding of cancer formation and development.
Max ERC Funding
1 377 495 €
Duration
Start date: 2018-01-01, End date: 2022-12-31
