Zuse Research Seminar: Graduate Series   📅

Institute
ZIB
Organizer
Tim Conrad and Christoph Spiegel
Description
Complementing the Zuse Research Seminar, the Graduate Series offers a more intimate setting for graduate students and early PhDs to discuss their recent research. This series has a flexible format, but talks generally are under 30 minutes and take place in the institute's seminar room as they are aimed at a smaller, more specialized audience.
Usual venue
seminarroom@zib
Number of talks
4
Tue, 25.06.24 at 11:00
A Formal Proof of the Sensitivity Conjecture
Abstract. The use of proof assistants has been on the rise these past few years thanks to their ability to detect small flaws in mathematical proofs. The integration of AI has also made the use of these kind of tools easier and it has opened a lot of possible advancements for the future. In this talk we will focus on the ITP Lean, with an emphasis on some results in the hypercube graph. The center of these results will be the Sensitivity Conjecture, which had already been formalized previously. Our additions to this problem are the formalization of two extremal examples to prove the tightness of the two inequalities in the conjecture. These new results involved a few challenges, such as having to implement a proof of the inclusion-exclusion principle. Additionally, they highlighted the importance of selecting a good way to express our statement, especially as a number of definitions had to be made and the different data representations came with different lemmas available.
Wed, 07.02.24 at 16:00
Formal Theorem Provers and Formal Proofs from THE BOOK
Abstract. This talk introduces and illustrates the ITP Lean, that allows the user to write mathematical statements and their proofs in a way that can be mechanically checked for correctness by a computer. Lean has gained increased attention in the past few years, due to hosting formalization projects of two Fields medalists, and due to the rise of automated theorem proving via AI models as a field of research. In this talk, we will exemplify how Lean is used by discussing our Master thesis project and the experiences we gained from it. We will also survey some large and completed formalization projects and give an insight into existing AI models surrounding Lean.
Wed, 07.02.24 at 16:00
Formal Theorem Provers and Formal Proofs from THE BOOK
Abstract. This talk introduces and illustrates the ITP Lean, that allows the user to write mathematical statements and their proofs in a way that can be mechanically checked for correctness by a computer. Lean has gained increased attention in the past few years, due to hosting formalization projects of two Fields medalists, and due to the rise of automated theorem proving via AI models as a field of research. In this talk, we will exemplify how Lean is used by discussing our Master thesis project and the experiences we gained from it. We will also survey some large and completed formalization projects and give an insight into existing AI models surrounding Lean.
Wed, 06.12.23 at 14:00
Solving the Optimal Experiment Design Problems with Mixed-Integer Frank-Wolfe-based methods
Abstract. We tackle the Optimal Experiment Design Problem, which consists in choosing experiments to run or observations to select from a finite set to estimate the parameters of a system. The objective is to maximize some measure of information gained on the system from the observations, leading to a convex integer optimization problem. We leverage Boscia, a recent algorithmic framework, which is based on a nonlinear branch-and-bound with node relaxations solved to approximate optimality using Frank-Wolfe algorithms. One particular advantage of the method is its efficient utilization of the polytope formed by the original constraints which remains preserved by the method, unlike in those relying on epigraph-based formulations. We assess our method against both generic and specialized convex mixed-integer approaches. Computational results highlight the performance of the proposed method, especially on large and challenging instances.