PhD Students
Tim Hoffmann (PhD project: Model counting)
Model counting is an extension of SAT solving to the more complex problem of determining the number of satisfying solutions (#SAT). This problem has many applications, in particular in probabilistic reasoning. In the project we evaluate the strength of current reasoning methods for model counting and formalise and investigate proofs for #SAT solvers.Kaspar Kasche (PhD project: Proof Complexity)
Proof complexity of Quantified Boolean Formulas (QBF) investigates the size of proofs of QBFs in central proof proof systems, including various resolution calculi. Lower bound methods for these systems have deep connections to logic and circuit complexity. A particular focus of this project will be to investigate the relations to communication complexity. QBF proof complexity provides the main theoretical tool to assess the strength of modern and versatile QBF solvers and aims to guide their future developments.Andreas Kröpelin (associated, PhD project: Statistical Methods for Reconstruction of Continuous Movements from Cryo-EM Data)
Cryo-electron microscopy (EM) does not only determine biomolecular structures at high resolution, but shows also potential for unraveling the entire spectrum of conformational dynamics of macromolecular assemblies. Our project aims to develop new computational approaches to reconstruct deformable 3D models that capture all of the structural dynamics hidden in cryo-EM projection images. The additional information about the dynamics of proteins will lead to a deeper understanding of enzymatic mechanisms and provide new insights into medically relevant modes of inhibiting proteins by drugs and binders.Steffen Meier (PhD project: Sequent calculi)
Sequent calculi and tableaux methods are important proof systems to support automated reasoning. In the project we determine the strength of sequent calculi for propositional and quantified Boolean logic and compare these systems with other standard tools, in particular resolution.Niklas Merk (PhD project: Graphical Models and Tensor Diagrams)
Recently, a duality between graphical models and tensor networks has been established. By this duality, the operation of marginalization in graphical models translates into computing tensor contractions, and the operation of conditioning becomes restricting a tensor network to a slice. By duality, the junction tree algorithm, a message passing technique, can be used for computing tensor contractions and expectation values in matrix product state networks. The duality was also exploited in the other direction for determining tensor contraction orders is used for weighted model counting, which in turn can be used for serving probability of evidence inference queries. This seems to be a promising direction of research that we want to pursue further in this project. Especially, since the duality makes potentially available a vast literature on tensor networks in physics for inference in probabilistic models.Paul Gerhardt Rump (PhD project: Efficient Tensor Calculus)
Matrix calculus computes derivatives of linear algebra expressions in vectorized form. The derivative of such an expression with respect to matrix is a matrix expression and its Hessian is a fourth order tensor, which cannot be expressed in a vectorized linear algebra language. For analyzing Hessians of matrix dependent functions it is necessary to work with a more general language for tensor expressions. The project aims at computing succinct and easy to analyze expressions for derivatives of tensor dependent expressions.Brian Zahoransky (PhD project: Visualization and Exploration of Cryo-EM Data and Gaussian Mixture Models)
This project is mainly concerned with probabilistic machine learning and modeling, computational Bayesian statistics and the analysis of complex biological data. Our goal is to visualize Cyro-EM data and to develop interactive exploration tools. The project is a cooperation between the Visualization group under Kai Lawonn and the Microscopic Image Analysis group at the University Hospital Jena under Michael Habeck. The working group is mainly concerned with probabilistic machine learning and modeling, computational Bayesian statistics, and the analysis of complex biological data. Our goal is to visualize the Cyro-EM data provided by the research group and to develop interactive exploration tools.Faculty
Olaf Beyersdorff (computational logic)
Torsten Bosse (automatic differentiation)
Alexander Breuer (high-performance computing)
Martin Bücker (automatic differentiation and high-performance computing)
Wolfhart Feldmeier (scientific machine learning)
Joachim Giesen (artificial intelligence and algorithm engineering)
Michael Habeck (probabilistic inference and bio-physics)
Christian Höner zu Siederdissen (computational biology and algorithm engineering)
Kai Lawonn (visualization)
Coordination
Olia Blacher (project coordinator)
Silvia Blaser (administrative assistance)
Advisory Board
Anthony G Cohn (University of Leeds, UK)
Thomas Eiter (TU Wien, AT)
Vijay Ganesh (University of Waterloo, CA)
Angelika Kimmig (Katholieke Universiteit Leuven, BE)
Meena Mahajan (The Institute of Mathematical Sciences (IMSc) Chennai, IN)
Tom Minka (Microsoft Research, UK)
Peter Schuster (Universita degli Studi di Verona, IT)
