-
Repulsive Score Distillation for Diverse Sampling of Diffusion Models
Authors:
Nicolas Zilberstein,
Morteza Mardani,
Santiago Segarra
Abstract:
Score distillation sampling has been pivotal for integrating diffusion models into generation of complex visuals. Despite impressive results it suffers from mode collapse and lack of diversity. To cope with this challenge, we leverage the gradient flow interpretation of score distillation to propose Repulsive Score Distillation (RSD). In particular, we propose a variational framework based on repu…
▽ More
Score distillation sampling has been pivotal for integrating diffusion models into generation of complex visuals. Despite impressive results it suffers from mode collapse and lack of diversity. To cope with this challenge, we leverage the gradient flow interpretation of score distillation to propose Repulsive Score Distillation (RSD). In particular, we propose a variational framework based on repulsion of an ensemble of particles that promotes diversity. Using a variational approximation that incorporates a coupling among particles, the repulsion appears as a simple regularization that allows interaction of particles based on their relative pairwise similarity, measured e.g., via radial basis kernels. We design RSD for both unconstrained and constrained sampling scenarios. For constrained sampling we focus on inverse problems in the latent space that leads to an augmented variational formulation, that strikes a good balance between compute, quality and diversity. Our extensive experiments for text-to-image generation, and inverse problems demonstrate that RSD achieves a superior trade-off between diversity and quality compared with state-of-the-art alternatives.
△ Less
Submitted 24 June, 2024;
originally announced June 2024.
-
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
Authors:
Linpeng Zhang,
Noam Zilberstein,
Benjamin Lucien Kaminski,
Alexandra Silva
Abstract:
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}.…
▽ More
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}. We thus (i)~obtain a weakest pre calculus for hyper Hoare logic and (ii)~enable reasoning about so-called \emph{hyperquantities} which include expected values but also quantities (e.g. variance) out of scope of previous work. As a byproduct, we obtain a novel strongest post for weighted programs that extends both existing strongest and strongest liberal post calculi. Our framework reveals novel dualities between forward and backward transformers, correctness and incorrectness, as well as nontermination and unreachability.
△ Less
Submitted 7 April, 2024;
originally announced April 2024.
-
A Relatively Complete Program Logic for Effectful Branching
Authors:
Noam Zilberstein
Abstract:
Starting with Hoare Logic over 50 years ago, numerous sound and relatively complete program logics have been devised to reason about the diverse programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice.
The recently i…
▽ More
Starting with Hoare Logic over 50 years ago, numerous sound and relatively complete program logics have been devised to reason about the diverse programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice.
The recently introduced Outcome Logic reimagines Hoare Logic with effects at its core, using an algebraic representation of choice to capture a variety of effects. In this paper, we give the first relatively complete proof system for Outcome Logic, handling general purpose loo** for the first time. We also show that this proof system applies to programs with various effects and that it facilitates the reuse of proof fragments across different kinds of specifications.
△ Less
Submitted 9 January, 2024;
originally announced January 2024.
-
Joint channel estimation and data detection in massive MIMO systems based on diffusion models
Authors:
Nicolas Zilberstein,
Ananthram Swami,
Santiago Segarra
Abstract:
We propose a joint channel estimation and data detection algorithm for massive multilple-input multiple-output systems based on diffusion models. Our proposed method solves the blind inverse problem by sampling from the joint posterior distribution of the symbols and channels and computing an approximate maximum a posteriori estimation. To achieve this, we construct a diffusion process that models…
▽ More
We propose a joint channel estimation and data detection algorithm for massive multilple-input multiple-output systems based on diffusion models. Our proposed method solves the blind inverse problem by sampling from the joint posterior distribution of the symbols and channels and computing an approximate maximum a posteriori estimation. To achieve this, we construct a diffusion process that models the joint distribution of the channels and symbols given noisy observations, and then run the reverse process to generate the samples. A unique contribution of the algorithm is to include the discrete prior distribution of the symbols and a learned prior for the channels. Indeed, this is key as it allows a more efficient exploration of the joint search space and, therefore, enhances the sampling process. Through numerical experiments, we demonstrate that our method yields a lower normalized mean squared error than competing approaches and reduces the pilot overhead.
△ Less
Submitted 16 November, 2023;
originally announced November 2023.
-
Solving Linear Inverse Problems using Higher-Order Annealed Langevin Diffusion
Authors:
Nicolas Zilberstein,
Ashutosh Sabharwal,
Santiago Segarra
Abstract:
We propose a solution for linear inverse problems based on higher-order Langevin diffusion. More precisely, we propose pre-conditioned second-order and third-order Langevin dynamics that provably sample from the posterior distribution of our unknown variables of interest while being computationally more efficient than their first-order counterpart and the non-conditioned versions of both dynamics.…
▽ More
We propose a solution for linear inverse problems based on higher-order Langevin diffusion. More precisely, we propose pre-conditioned second-order and third-order Langevin dynamics that provably sample from the posterior distribution of our unknown variables of interest while being computationally more efficient than their first-order counterpart and the non-conditioned versions of both dynamics. Moreover, we prove that both pre-conditioned dynamics are well-defined and have the same unique invariant distributions as the non-conditioned cases. We also incorporate an annealing procedure that has the double benefit of further accelerating the convergence of the algorithm and allowing us to accommodate the case where the unknown variables are discrete. Numerical experiments in two different tasks in communications (MIMO symbol detection and channel estimation) and in three tasks for images showcase the generality of our method and illustrate the high performance achieved relative to competing approaches (including learning-based ones) while having comparable or lower computational complexity.
△ Less
Submitted 6 December, 2023; v1 submitted 8 May, 2023;
originally announced May 2023.
-
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
Authors:
Noam Zilberstein,
Angelina Saliling,
Alexandra Silva
Abstract:
Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many programs display computational effects and, orthogonally, static analyzers must handle incorrectness too. We present Outcome Separation Logic (OSL), a program logic that is sound for both correctness and incorrectness reaso…
▽ More
Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many programs display computational effects and, orthogonally, static analyzers must handle incorrectness too. We present Outcome Separation Logic (OSL), a program logic that is sound for both correctness and incorrectness reasoning in programs with varying effects. OSL has a frame rule -- just like separation logic -- but uses different underlying assumptions that open up local reasoning to a larger class of properties than can be handled by any single existing logic.
Building on this foundational theory, we also define symbolic execution algorithms that use bi-abduction to derive specifications for programs with effects. This involves a new tri-abduction procedure to analyze programs whose execution branches due to effects such as nondeterministic or probabilistic choice. This work furthers the compositionality promised by separation logic by opening up the possibility for greater reuse of analysis tools across two dimensions: bug-finding vs verification in programs with varying effects.
△ Less
Submitted 13 March, 2024; v1 submitted 8 May, 2023;
originally announced May 2023.
-
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Authors:
Noam Zilberstein,
Derek Dreyer,
Alexandra Silva
Abstract:
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to captur…
▽ More
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL expresses true positive bugs, while retaining correctness reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in nondeterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.
△ Less
Submitted 10 March, 2023; v1 submitted 6 March, 2023;
originally announced March 2023.
-
Unsupervised Learning of Sampling Distributions for Particle Filters
Authors:
Fernando Gama,
Nicolas Zilberstein,
Martin Sevilla,
Richard Baraniuk,
Santiago Segarra
Abstract:
Accurate estimation of the states of a nonlinear dynamical system is crucial for their design, synthesis, and analysis. Particle filters are estimators constructed by simulating trajectories from a sampling distribution and averaging them based on their importance weight. For particle filters to be computationally tractable, it must be feasible to simulate the trajectories by drawing from the samp…
▽ More
Accurate estimation of the states of a nonlinear dynamical system is crucial for their design, synthesis, and analysis. Particle filters are estimators constructed by simulating trajectories from a sampling distribution and averaging them based on their importance weight. For particle filters to be computationally tractable, it must be feasible to simulate the trajectories by drawing from the sampling distribution. Simultaneously, these trajectories need to reflect the reality of the nonlinear dynamical system so that the resulting estimators are accurate. Thus, the crux of particle filters lies in designing sampling distributions that are both easy to sample from and lead to accurate estimators. In this work, we propose to learn the sampling distributions. We put forward four methods for learning sampling distributions from observed measurements. Three of the methods are parametric methods in which we learn the mean and covariance matrix of a multivariate Gaussian distribution; each methods exploits a different aspect of the data (generic, time structure, graph structure). The fourth method is a nonparametric alternative in which we directly learn a transform of a uniform random variable. All four methods are trained in an unsupervised manner by maximizing the likelihood that the states may have produced the observed measurements. Our computational experiments demonstrate that learned sampling distributions exhibit better performance than designed, minimum-degeneracy sampling distributions.
△ Less
Submitted 2 February, 2023;
originally announced February 2023.
-
Accelerated massive MIMO detector based on annealed underdamped Langevin dynamics
Authors:
Nicolas Zilberstein,
Chris Dick,
Rahman Doost-Mohammady,
Ashutosh Sabharwal,
Santiago Segarra
Abstract:
We propose a multiple-input multiple-output (MIMO) detector based on an annealed version of the \emph{underdamped} Langevin (stochastic) dynamic. Our detector achieves state-of-the-art performance in terms of symbol error rate (SER) while kee** the computational complexity in check. Indeed, our method can be easily tuned to strike the right balance between computational complexity and performanc…
▽ More
We propose a multiple-input multiple-output (MIMO) detector based on an annealed version of the \emph{underdamped} Langevin (stochastic) dynamic. Our detector achieves state-of-the-art performance in terms of symbol error rate (SER) while kee** the computational complexity in check. Indeed, our method can be easily tuned to strike the right balance between computational complexity and performance as required by the application at hand. This balance is achieved by tuning hyperparameters that control the length of the simulated Langevin dynamic. Through numerical experiments, we demonstrate that our detector yields lower SER than competing approaches (including learning-based ones) with a lower running time compared to a previously proposed \emph{overdamped} Langevin-based MIMO detector.
△ Less
Submitted 26 October, 2022;
originally announced October 2022.
-
Annealed Langevin Dynamics for Massive MIMO Detection
Authors:
Nicolas Zilberstein,
Chris Dick,
Rahman Doost-Mohammady,
Ashutosh Sabharwal,
Santiago Segarra
Abstract:
Solving the optimal symbol detection problem in multiple-input multiple-output (MIMO) systems is known to be NP-hard. Hence, the objective of any detector of practical relevance is to get reasonably close to the optimal solution while kee** the computational complexity in check. In this work, we propose a MIMO detector based on an annealed version of Langevin (stochastic) dynamics. More precisel…
▽ More
Solving the optimal symbol detection problem in multiple-input multiple-output (MIMO) systems is known to be NP-hard. Hence, the objective of any detector of practical relevance is to get reasonably close to the optimal solution while kee** the computational complexity in check. In this work, we propose a MIMO detector based on an annealed version of Langevin (stochastic) dynamics. More precisely, we define a stochastic dynamical process whose stationary distribution coincides with the posterior distribution of the symbols given our observations. In essence, this allows us to approximate the maximum a posteriori estimator of the transmitted symbols by sampling from the proposed Langevin dynamic. Furthermore, we carefully craft this stochastic dynamic by gradually adding a sequence of noise with decreasing variance to the trajectories, which ensures that the estimated symbols belong to a pre-specified discrete constellation. Based on the proposed MIMO detector, we also design a robust version of the method by unfolding and parameterizing one term -- the score of the likelihood -- by a neural network. Through numerical experiments in both synthetic and real-world data, we show that our proposed detector yields state-of-the-art symbol error rate performance and the robust version becomes noise-variance agnostic.
△ Less
Submitted 17 March, 2023; v1 submitted 11 May, 2022;
originally announced May 2022.
-
Detection by Sampling: Massive MIMO Detector based on Langevin Dynamics
Authors:
Nicolas Zilberstein,
Chris Dick,
Rahman Doost-Mohammady,
Ashutosh Sabharwal,
Santiago Segarra
Abstract:
Optimal symbol detection in multiple-input multiple-output (MIMO) systems is known to be an NP-hard problem. Hence, the objective of any detector of practical relevance is to get reasonably close to the optimal solution while kee** the computational complexity in check. In this work, we propose a MIMO detector based on an annealed version of Langevin (stochastic) dynamics. More precisely, we def…
▽ More
Optimal symbol detection in multiple-input multiple-output (MIMO) systems is known to be an NP-hard problem. Hence, the objective of any detector of practical relevance is to get reasonably close to the optimal solution while kee** the computational complexity in check. In this work, we propose a MIMO detector based on an annealed version of Langevin (stochastic) dynamics. More precisely, we define a stochastic dynamical process whose stationary distribution coincides with the posterior distribution of the symbols given our observations. In essence, this allows us to approximate the maximum a posteriori estimator of the transmitted symbols by sampling from the proposed Langevin dynamic. Furthermore, we carefully craft this stochastic dynamic by gradually adding a sequence of noise with decreasing variance to the trajectories, which ensures that the estimated symbols belong to a pre-specified discrete constellation. Through numerical experiments, we show that our proposed detector yields state-of-the-art symbol error rate performance.
△ Less
Submitted 24 February, 2022;
originally announced February 2022.
-
Robust MIMO Detection using Hypernetworks with Learned Regularizers
Authors:
Nicolas Zilberstein,
Chris Dick,
Rahman Doost-Mohammady,
Ashutosh Sabharwal,
Santiago Segarra
Abstract:
Optimal symbol detection in multiple-input multiple-output (MIMO) systems is known to be an NP-hard problem. Recently, there has been a growing interest to get reasonably close to the optimal solution using neural networks while kee** the computational complexity in check. However, existing work based on deep learning shows that it is difficult to design a generic network that works well for a v…
▽ More
Optimal symbol detection in multiple-input multiple-output (MIMO) systems is known to be an NP-hard problem. Recently, there has been a growing interest to get reasonably close to the optimal solution using neural networks while kee** the computational complexity in check. However, existing work based on deep learning shows that it is difficult to design a generic network that works well for a variety of channels. In this work, we propose a method that tries to strike a balance between symbol error rate (SER) performance and generality of channels. Our method is based on hypernetworks that generate the parameters of a neural network-based detector that works well on a specific channel. We propose a general framework by regularizing the training of the hypernetwork with some pre-trained instances of the channel-specific method. Through numerical experiments, we show that our proposed method yields high performance for a set of prespecified channel realizations while generalizing well to all channels drawn from a specific distribution.
△ Less
Submitted 13 October, 2021;
originally announced October 2021.
-
Unrolling Particles: Unsupervised Learning of Sampling Distributions
Authors:
Fernando Gama,
Nicolas Zilberstein,
Richard G. Baraniuk,
Santiago Segarra
Abstract:
Particle filtering is used to compute good nonlinear estimates of complex systems. It samples trajectories from a chosen distribution and computes the estimate as a weighted average. Easy-to-sample distributions often lead to degenerate samples where only one trajectory carries all the weight, negatively affecting the resulting performance of the estimate. While much research has been done on the…
▽ More
Particle filtering is used to compute good nonlinear estimates of complex systems. It samples trajectories from a chosen distribution and computes the estimate as a weighted average. Easy-to-sample distributions often lead to degenerate samples where only one trajectory carries all the weight, negatively affecting the resulting performance of the estimate. While much research has been done on the design of appropriate sampling distributions that would lead to controlled degeneracy, in this paper our objective is to \emph{learn} sampling distributions. Leveraging the framework of algorithm unrolling, we model the sampling distribution as a multivariate normal, and we use neural networks to learn both the mean and the covariance. We carry out unsupervised training of the model to minimize weight degeneracy, relying only on the observed measurements of the system. We show in simulations that the resulting particle filter yields good estimates in a wide range of scenarios.
△ Less
Submitted 6 October, 2021;
originally announced October 2021.
