Research Seminar

Riemannian optimization refers to the optimization of functions defined over Riemannian manifolds. Such problems arise when the constraints of Euclidean optimization problems can be viewed as Riemannian manifolds, such as the symmetric positive-definite cone, the sphere, or the set of orthogonal linear layers for a neural network. This Riemannian formulation enables us to leverage the geometric structure of such problems by viewing them as unconstrained problems on a manifold. The convergence rates of Riemannian optimization algorithms often rely on geometric quantities depending on the sectional curvature and the distance between iterates and an optimizer. Numerous previous works bound the latter only by assumption, resulting in incomplete analysis and unquantified rates. In this talk, I will discuss how to remove this limitation for multiple algorithms and as a result quantify their rates of convergence.

Decision diagram is a data structure that has been used for a long time to represent logic functions. Recently, the development of quantum computers has become very active, and decision diagrams are used in quantum circuit simulation because it can represent quantum states (complex vectors) and quantum gates (complex unitary matrices) with less memory. In this presentation, I will explain a method for large-scale parallelization of quantum circuit simulations using decision diagrams in an HPC (High-Performance Computing) environment. I will also discuss the difference between quantum circuits that can be simulated quickly with decision diagrams and those that are slow, and discuss suitable applications.

In 1960 Kelley proposed a cutting plane method to minimize a continuous convex objective function over a compact set. This iterative method consists at each step in minimizing a polyhedral approximation of the objective function before improving the approximation by a valid affine cut. In generalized convexity, the affine functions giving the cuts are replaced by some family of base functions. This base functions are chosen so that the objective function is their supremum, making it abstract convex. In this framework, Kelley’s algorithm has been generalized to continuous abstract convex functions by Pallaschke and Rolewicz in 1997 and Rubinov in 2000. We continue the generalization of the cutting plane method by providing a convergence result that can be applied to lower semicontinuous objective functions. This convergence result is motivated by the Capra-convexity results in 2022 by Chancelier and De Lara on the l₀ pseudonorm, which is lower semicontinuous. As explicit formulas for the Capra-subdifferential of the l₀ pseudonorm have been calculated by Le Franc in 2024, we can now implement Capra-cutting plane methods for the sparse problem of minimizing l0 over a compact set.

The use of quantum computers in the simulation of dynamical systems promises many advantages. In order to achieve this objective, it is necessary to employ a unitary description of the dynamical system. One approach to this is the Koopman-von Neumann framework. However, adapting this framework for practical quantum computation requires special discretizations. This talk presents a novel approach to bridge this gap, enabling efficient quantum simulations of classical dynamical systems.

The Frank-Wolfe method is a classical first-order algorithm for constrained optimization that avoids projections by relying on linear minimization oracles. While extensively studied over polytopes, its behavior over strongly convex domains remains less understood, especially near the boundary. In this talk, we will explore the challenges of optimizing over such sets, with a particular focus on the difficulty of finding optima located on the boundary. Using the simple example of projections onto the L2-ball, we will provide geometric insights into convergence behavior of Frank-Wolfe. This example illustrates fundamental limitations of the method in boundary regimes and motivates further analysis of step size strategies and alternative update directions.

Reliable and detailed information on forest canopy height is essential for understanding the health and carbon dynamics of forests, which play a pivotal role in climate adaptation and mitigation strategies. Traditional methods of forest monitoring, while foundational, lack the global coverage and are often costly, hindering effective policymaking. Jan Pauls and colleagues have developed a novel framework using satellite data to estimate canopy height on a global scale. The approach combines cutting-edge data preprocessing techniques, a unique loss function to mitigate geolocation inaccuracies, and data filtering from the Shuttle Radar Topography Mission to enhance prediction reliability in mountainous areas. The framework significantly improves upon existing global-scale canopy height maps. By offering a high-resolution (10 m) global canopy height map, the produced map provides critical insights into forest dynamics, aiding in more effective forest management and climate change mitigation efforts. This talk will explore the methods and implications of this work, demonstrating how advancements in Earth observation and machine learning can revolutionize global forest assessments and ecological studies.

Entanglement is the core feature in the quantum world, which plays an important role in many quantum information processes. For low-dimensional and small systems, quantum entanglement can be detected by the positive partial transpose (PPT) criterion sufficiently and necessarily. However, it is tricky to detect entanglement for high-dimensional and/or large multipartite quantum systems, both theoretically and numerically. In this work, with the help of the Frank-Wolfe algorithms, or named conditional gradient algorithms, and their progress in recent years, we develop a high-precision numerical tool that can certify quantum entanglement and quantum separability at the same time. Our method can detect the entanglement of bipartite systems with local dimensions higher than 20. For multipartite systems, our method can characterize entanglement within not only a specific partition, but also the more general k-separability structure, which includes the genuine multipartite entanglement (GME) problem (i.e., 2-separability), up to 10 qubits. Moreover, the overall design of the tool is oriented towards experimentation, which can access the raw data and achieve an operational entanglement witness. Last but not least, our method supports the analysis of noise robustness for arbitrary noise types, not limited to conventional white noise.

We present a framework that transforms geometric and combinatorial problems into optimization tasks by designing loss functions that vanish precisely when the desired coloring properties are achieved. We employ neural networks trained through gradient descent to minimize these loss functions, allowing for efficient exploration of the solution space. We demonstrate the effectiveness of the method on variants of the Hadwiger-Nelson problem, which asks for plane colorings that avoid monochromatic unit-distance pairs and sketch how the approach can be applied to other problems.

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.

Quantum optimal control is a vital area of research enabling the precise manipulation of quantum systems to achieve desired objectives, including quantum state preparation, optimization of quantum gate operations and manipulation of chemical reactions. We will begin the talk by presenting the quantum optimal control problem, followed by a quick overview of various algorithms from the literature designed to address this problem. The discussion will conclude with an exploration of some practical applications.

Differential privacy is a concept that can be used to express the extent to which algorithms like database queries, statistics and machine learning procedures, preserve a certain notion of privacy of an input dataset. Prominent applications of the technique include the US census and user data aggregation procedures of multiple large tech companies. The correct implementation of such algorithms requires a substantial amount of care, which motivated the development of type systems tailored to verify the differential privacy properties of programs. We implemented a type checker for one such type system and integrated it with the julia programming language to enable not only verification but automatic inference of privacy parameters for a reasonable subset of julia code.

Cutting planes are a crucial tool in mixed-integer programming. When measuring the strength of a specific class of cutting planes, a key question is whether the corresponding cut closure is polyhedral, meaning that finitely many cuts are sufficient to obtain the closure. The vast amount of literature investigating polyhedrality for different kinds of cutting planes indicates that the field has not yet settled on a universal solution to this problem. In this talk, we will look at cutting plane generation through a unifying framework and establish conditions that ensure polyhedrality of cut closures. This enables us to prove polyhedrality for a broad range of cutting plane families more easily.

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