Many applications in machine learning involve data represented as probability distributions. The emergence of such data requires radically novel techniques to design tractable gradient flows on probability distributions over this type of (infinite-dimensional) objects. For instance, being able to flow labeled datasets is a core task for applications ranging from domain adaptation to transfer learning or dataset distillation. In this setting, we propose to represent each class by the associated conditional distribution of features, and to model the dataset as a mixture distribution supported on these classes (which are themselves probability distributions), meaning that labeled datasets can be seen as probability distributions over probability distributions. We endow this space with a metric structure from optimal transport, namely the Wasserstein over Wasserstein (WoW) distance, derive a differential structure on this space, and define WoW gradient flows. The latter enables to design dynamics over this space that decrease a given objective functional. We apply our framework to transfer learning and dataset distillation tasks, leveraging our gradient flow construction as well as novel tractable functionals that take the form of Maximum Mean Discrepancies with Sliced-Wasserstein based kernels between probability distributions.

In this paper, we investigate the properties of the Sliced Wasserstein Distance (SW) when employed as an objective functional. The SW metric has gained significant interest in the optimal transport and machine learning literature, due to its ability to capture intricate geometric properties of probability distributions while remaining computationally tractable, making it a valuable tool for various applications, including generative modeling and domain adaptation. Our study aims to provide a rigorous analysis of the critical points arising from the optimization of the SW objective. By computing explicit perturbations, we establish that stable critical points of SW cannot concentrate on segments. This stability analysis is crucial for understanding the behaviour of optimization algorithms for models trained using the SW objective. Furthermore, we investigate the properties of the SW objective, shedding light on the existence and convergence behavior of critical points. We illustrate our theoretical results through numerical experiments.

Abstract Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called $$\textsf{QSMA}$$ QSMA (Quantified Satisfiability Modulo Assignment), for the satisfiability of an arbitrary quantified formula modulo a complete theory and an initial assignment. The algorithm is proved partially correct and terminating, so that its total correctness is established. An optimized variant called $$\textsf{OptiQSMA}$$ OptiQSMA is also described and shown to preserve both partial correctness and termination. $$\textsf{OptiQSMA}$$ OptiQSMA is implemented in the YicesQS solver. $$\textsf{OptiQSMA}$$ OptiQSMA enabled YicesQS to achieve top of the line results, especially in linear rational arithmetic, in the 2022, 2023, and 2024 editions of the International Satisfiability Modulo Theories Competition (SMT-COMP). A report on these results in four fragments of arithmetic ( $$\textsf{LRA}$$ LRA —Linear Rational Arithmetic, $$\textsf{LIA}$$ LIA —Linear Integer Arithmetic, $$\textsf{NRA}$$ NRA —Nonlinear Real Arithmetic, and $$\textsf{NIA}$$ NIA —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( $$\textsf{BV}$$ BV ) is included.

Abstract This paper presents and proves totally correct a new algorithm, called $$\textsf{QSMA}$$ QSMA , for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of $$\textsf{QSMA}$$ QSMA implemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the $$\textsf{LIA}$$ LIA , $$\textsf{NIA}$$ NIA , $$\textsf{LRA}$$ LRA , $$\textsf{NRA}$$ NRA , and $$\textsf{BV}$$ BV categories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all $$\textsf{LRA}$$ LRA instances, where it was about two orders of magnitude faster than the second best solver (Z3).