Zuse Research Seminar: Graduate Series

Wed, 04.09.24 at 11:00

Ingo Meise ZIB / TU Berlin

A Comparison of Simple and Repeated Weighted Majority Voting

Abstract.

While weighted majority voting (WMV) is a popular method in ensemble learning for classification, more complex aggregation rules have recently been shown to have beneficial theoretical properties such as better convergence in the number of calls to a weak learning oracle and better PAC-bounds. After a brief discussion of the literature, this talk compares simple WMV to repeated WMV. In particular, a tight approximability analysis of 1) empirical error minimization, 2) regularization by sparsity and 3) sparsity maximization subject to zero training error is provided. It reveals that, under polynomial time transformations, the respective problems for simple WMV are equivalent to a hard version of Minimum Weighted Set Cover (MWSC) while they are equivalent to a simple version of MWSC for repeated WMV. This analysis of approximability implies two lower bounds on convergence in the number of calls to a weak learning oracle until perfect fit for 1) simple WMV and 2) arbitrary aggregation rules which emphasizes the worse scalability of simple WMV. These theoretical results are complemented by experiments on medium-sized data sets from LIBSVM showing that repeated WMV needs fewer oracle calls compared to AdaBoost and XGBoost while having even or better test accuracy on average.

Zuse Research: GS

Wed, 14.08.24 at 11:00

ZIB Seminar Room

Hugo Abreu ZIB

Bell inequalities with classical communication via Frank-Wolfe algorithms

Abstract.

Bell's 1964 theorem established that the predictions of quantum theory cannot be explained by any local theory, making nonlocality a pivotal concept in the understanding of quantum mechanics. Quantifying the nonlocality of a quantum state in a given scenario is challenging, so we propose examining the amount of classical communication required to simulate the correlations obtained by a quantum state, and thereby indirectly characterizing its nonlocality. We explore Bell scenarios augmented with one or more bits of classical communication with Frank-Wolfe algorithms, and extend the BellPolytopes.jl Julia library to handle those scenarios. In this talk, I will introduce the theoretical framework, cover implementation details, and present some preliminary results.

Zuse Research: GS

Tue, 25.06.24 at 11:00

ZIB Seminar Room

Lídia Rodríguez ZIB / UPC

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.

Zuse Research: GS

Wed, 07.02.24 at 16:00

ZIB Lecture Hall

Etienne Jäckle ZIB / TU Berlin and Yves

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.

Zuse Research: GS

Wed, 07.02.24 at 16:00

ZIB Lecture Hall

Yves Etienne Jäckle ZIB / TU Berlin

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.

Zuse Research: GS

Wed, 06.12.23 at 14:00

ZIB Seminar Room

Deborah Hendrych ZIB / TU Berlin

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.

Zuse Research Seminar: Graduate Series 📅