Thomas Sturm Projects
Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition
EPSRC Project
EP/T015748/1 & EP/T015713/1
Consortium:
M. England (Coordinator, Coventry, UK)
R. Bradford (Bath, UK)
J. H. Davenport (Bath, UK)
Project Partners:
E. Ábráham (RWTH Aachen University, Germany)
S. McCallum (Macquarie University, Australia)
S. Forrest (Maplesoft, Canada)
J. Gerhard (Maplesoft, Canada)
C. Mulligan (University of Chicago, IL, USA)
T. Sturm (CNRS, France)
For statements in polynomials over real numbers there will always exist an equivalent formula without the quantification. However, actually obtaining the answer can be very costly in terms of computation, and those costs rise with the size of the problem. We call this the "doubly exponential wall" in reference to how fast they rise.
The doubly exponential wall cannot be broken completely: this rise in costs is inevitable. However, the aim of this project is to "push back the wall" so that lots more practical problems may be tackled by QE. The scale here means that pushing the wall even a small way offers enormous potential: e.g. 2^(2^4) is less than 66,000 while 2^(2^5) is over 4 billion! We will achieve this through the development of new algorithms, inspired by an existing process (cylindrical algebraic decomposition) but with substantial innovations.
Biologically relevant problems for our new methods occur in the context of the ANR/DFG project SYMBIONT.
SYMBIONT
Symbolic Methods for Biological Networks
ANR/DFG PRCI Project
№ ANR-17-CE40-0036
DFG Project Number 391322026
Consortium:
T. Sturm (Coordinator, Nancy, France)
F. Boulier (Lille, France)
F. Fages (Saclay, France)
D. Grigoriev (Lille, France)
O. Radulescu (Montpellier, France)
A. Schuppert (Aachen, Germany)
W. Seiler (Kassel, Germany)
S. Walcher (Aachen, Germany)
A. Weber †
SYMBIONT is an interdisciplinary project ranging from mathematics via computer science to systems biology and systems medicine. The project has a clear focus on fundamental research on mathematical methods, and prototypes in software, which are in turn benchmarked against models from computational biology databases.
The principal approach of SYMBIONT is to combine symbolic methods with model reduction methods for the analysis of biological networks. In order to cope more effectively with the parameter uncertainty problem we impose an entirely new paradigm replacing thinking about single instances with thinking about orders of magnitude.
Our computational methods are diverse and involve various branches of mathematics such as tropical geometry, real algebraic geometry, theories of singular perturbations, invariant manifolds and symmetries of differential systems.
Embedding Machine Learning within Quantifier Elimination Procedures
EPSRC Project EP/R019622/1
Consortium:
M. England (Coordinator, Coventry, UK)
Project Partners:
E. Ábráham (RWTH Aachen University, Germany)
A. Bigatti (University of Genoa, Italy)
J. Gerhard (Maplesoft, Canada)
T. Sturm (CNRS, France)
Quantifier elimination (QE) procedures have many options and choices about how they are run. Making the right choice is a critical, but understudied problem. At the moment QE procedures make such choices either under direct supervision of a human or based on crude human-made heuristics, such as rules of thumb based on intuition or experience but with limited scientific basis. The purpose of this project is to replace these by machine learning techniques.
Machine Learning (ML) is an overarching term for tools that allow computers to make decisions that are not explicitly programmed, usually involving the statistical analysis of large quantities of data. ML is quite at odds with the field of Symbolic Computation which studies QE, as the latter prizes exact correctness and so shuns the use of probabilistic tools making its application here very novel.
REDLOG
Reduce Logic System
Inria ADT-135 (Fast Track)
Consortium:
T. Sturm (Coordinator, Nancy, France)
S. Glondu (Nancy, France)
Redlog is integrated with the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation with more than 100 functions on first-order formulas. Redlog has been publicly available since 1995 and is systematically being improved and developed further. The name Redlog stands for Reduce Logic System.
SC-SQUARE
Satisfiability Checking and Symbolic Computation
EU H2020-FETOPEN-2015-CSA 712689
Consortium:
J. Davenport (Coordinator, Bath, UK)
E. Ábráham (Aachen, Germany)
A. Bigatti (Genova, Italy)
B. Buchberger (Linz, Austria)
A. Cimatti (Trento, Italy)
M. England (Coventry, UK)
P. Fontaine (Nancy, France)
S. Forrest (Jena, Germany)
D. Kröning (Oxford, UK)
W. Seiler (Kassel, Germany)
T. Sturm (Saarbrücken, Germany)
Symbolic Computation is concerned with the algorithmic determination of exact solutions to mathematical problems. Recent developments in the area of Satisfiability Checking tackle some similar problems, but with different algorithmic and technological approaches.
Corresponding software — computer algebra systems and SMT solvers, respectively — addresses some prevailing problems with a direct effect to our society. For instance, Satisfiability Checking is an essential backend for assuring the security and the safety of computer systems.
Bridges between the communities in the form of common platforms and roadmaps are necessary to foster an exchange, and to support and to direct their interaction. Our Coordination and Support Activity will initiate a wide range of corresponding activities, identify common challenges, offer global events and bilateral visits, and propose standards.
SMART
Satisfiability Modulo Arithmetic Theories
ANR/DFG Programme Blanc
№ ANR-13-IS02-0001
DFG Project Number 242816019
Consortium:
P. Fontaine (Coordinator, Nancy, France)
T. Sturm (Coordinator, Saarbrücken, Germany)
S. Merz (Nancy, France)
L. Voisin (SYSTEREL, France)
SMArT adapts state-of-the-art arithmetic decision procedures for use within an SMT context in order to support formal system verification.
SMT solvers, are successfully used, e.g., for program verification, bounded and parameterized model checking, or test generation. On the other hand, computer algebra systems allow reasoning in fragments of arithmetic, which is a fundamental requirement in verification.
We combine both approaches, which has several advantages: The arithmetic solver need not handle propositional operators; the SMT solver gets access to a sophisticated infrastructure for handling expressive arithmetic fragments; users benefit from the modular architecture of SMT solvers where arithmetic can be combined with other relevant theories.