Research Seminar

For almost two decades, mixed integer programming (MIP) solvers have used graph-based conflict analysis to learn from local infeasibilities during branch-and-bound search. In this talk, we discuss improvements for MIP conflict analysis by instead using reasoning based on cuts, inspired by the development of conflict-driven solvers for pseudo-Boolean optimization. Phrased in MIP terminology, this type of conflict analysis can be understood as a sequence of linear combinations, integer roundings, and cut generation. We leverage this MIP perspective to design a new conflict analysis algorithm based on mixed integer rounding cuts, which theoretically dominates the state-of-the-art method in pseudo-Boolean optimization using Chvátal-Gomory cuts. Furthermore, we discuss how to extend this cut-based conflict analysis from pure binary programs to mixed binary programs and-in limited form-to general MIP with also integer-valued variables. Our experimental results indicate that the new algorithm improves the default performance of SCIP in terms of running time, number of nodes in the search tree, and the number of instances solved.

Over the past decade, an enormous amount of satellite data has become freely available, unlocking countless opportunities for researchers to address a wide range of monitoring challenges. These include tasks like greenhouse gas estimation, ground displacement detection, soil moisture analysis, and many more. Despite this abundance of data, significant challenges remain when it comes to developing truly operational satellite analytics products—especially when scaling to create diverse solutions for various use cases. In this talk, I will explore these challenges from both a research and commercial perspective, highlighting the practical hurdles faced in turning satellite data into actionable products. I will also discuss how recent advancements in geospatial foundation models are beginning to emerge as a versatile, “Swiss Army knife” solution for building scalable and efficient satellite analytics tools.

How can we trust the correctness of a learned model on a specific input of interest? This work introduces Self-Proving Models—models that can prove the correctness of their outputs via an interactive proof system. These models offer high-probability correctness for most outputs, with a verification algorithm that reliably detects any incorrect ones. The framework, rooted in theoretical guarantees, is demonstrated through experiments using transformers trained for arithmetic tasks such as computing the greatest common divisor (GCD).

Faster algorithms for optimization problems are among the main potential applications for future quantum computers. There has been interesting progress in this area in recent years, for instance improved quantum algorithms for gradient descent and for solving linear and semidefinite programs. In this talk I will survey what we know about quantum speed-ups both for discrete and for continuous optimization, with a bit more detail about two speed-ups I worked on recently: for regularized linear regression and for Principal Component Analysis. I’ll also discuss some issues with this line of work, in particular that quadratic or subquadratic quantum speed-ups will only kick in for very large instance sizes and that many of these algorithms require some kind of quantum RAM.

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.

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.

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.

This talk will begin with a brief introduction to classical Ramsey theory (whose main idea is that complete disorder is impossible) and a discussion of a few well-known results. No specialized background knowledge in combinatorics is required for this talk. Then joint work with Will Smith from University of South Carolina (formerly Davidson) on a Ramsey theory problem based on the integer grid will be presented. Specifically, the L-theorem (an easy corollary of the Gallai-Witt theorem) states that for any integer k, there exists some n such that a k-colored n by n grid must contain a monochromatic "L" (a series of points of the form (i, j), (i, j+t), and (i+t, j+t) for some positive integer t. In this talk, we will investigate the upper bound for the smallest integer n such that a 3-colored n by n integer grid is guaranteed to contain a monochromatic L. We use various methods, such as counting intervals on the main diagonal, to improve the upper bound from 2593 to 493. For the lower bound, we match the lower bound of 21 generated by Canacki et al. (2023) and discuss possible improvements.

Many recent advances in the field of AI, including tools such as ChatGPT, rely on the training of foundation models. Foundation models are fine-tuned to avoid unsafe or otherwise problematic behavior, so that, for example, they refuse to comply with requests for help with committing crimes, or with producing racist text. One approach to fine-tuning, called reinforcement learning from human feedback, learns from humans’ expressed preferences over multiple outputs. Another approach is constitutional AI, in which the input from humans is a list of high-level principles. But which humans get to provide the feedback or principles? And how is their potentially diverging input aggregated into consistent data about “collective” preferences or otherwise used to make collective choices about model behavior? In this talk, I argue that the field of social choice is well positioned to address these questions, and discuss ways forward for this agenda, drawing on discussions in a recent workshop on Social Choice for AI Ethics and Safety held in Berkeley, CA, USA in December 2023.

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.

The simplex method is a very efficient algorithm. In this talk we see a few of the state-of-the-art theories for explaining this observation. We will discuss what it takes for a mathematical model to explain an algorithm’s qualities, and whether existing theories meet this bar. Following this, we will question what the simplex method is and if the theoretician’s simplex method is the same algorithm as the practitioner’s simplex method.

In light of the ongoing developments in the climate crisis, it is necessary to consider factors beyond the sole economic perspective in energy supply network planning. This gives rise to a classical multiobjective optimization problem involving conflicting objective functions. The presence of choices in the model, coupled with the consideration of stationary flow equations, results in an opti mization problem with a mixed-integer nonlinear structure. Following a short introduction of some model-specific details and arising challenges, we present a novel method for computing an enclosure of the nondominated set of such prob lems. We prove finite convergence and demonstrate its effectiveness through numerical experiments. We conclude by offering a preview of ongoing extensions of this work.

Sparsity of matrices can be exploited, in particular, to speed up algorithms in various applications, e.g., in linear system solvers or second-order optimization schemes. This motivates to consider the matrix sparsification problem, in which we seek an equivalent (column-space preserving) representation of a given matrix with as few nonzero entries as possible. We derive sequential solution approaches based on bilinear and linear mixed-integer programs, respectively, and point out connections to certain machine learning tasks. One particular problem appears as a subproblem or special case in both these approaches: Finding a sparsest nonzero vector in the nullspace of a matrix. We will outline how a dedicated branch-and-cut method for this problem can be utilized in the envisioned matrix sparsification algorithms, and touch upon some open questions and challenges of our ongoing work