Pith. sign in

REVIEW 4 major objections 5 minor 42 references

Certified Guidance for Planning with Deep Generative Models

T0 review · 4 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Pith's one-line read Certified guidance modifies a pre-trained generative model, with no retraining, into a new model whose sampled trajectories satisfy the given temporal-logic planning specification with probability 1.

desk verdict Neat and mostly sound idea—restrict the latent distribution to verified boxes for probability-1 STL satisfaction—but the verifier encoding is unspecified and the paper overclaims one result. read the letter →

arxiv 2501.12815 v1 pith:SDJCYER3 submitted 2025-01-22 cs.LG stat.ML

classification cs.LGstat.ML
keywords neuralnetworkverificationdeepgenerativemodelsguidedsamplingsafeplanningcertifiedsignaltemporallogicGANsdiffusion
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that a pre-trained generative model can be changed, without retraining, into a new model whose outputs satisfy a given Signal Temporal Logic (STL) planning specification with probability 1. STL is a formal language for requirements such as "always keep a safety distance and eventually reach the goal." Existing guidance methods use gradient ascent on a differentiable reward to steer sampling, but they can produce violating trajectories and offer no guarantee. The proposed certified guidance instead searches the model's latent space for boxes that a neural-network verifier certifies as always yielding satisfying trajectories, then restricts the latent distribution to those boxes. The result is a mixture of truncated Gaussians that samples efficiently and preserves the relative likelihood of latent points; if the verifier is sound, every sample satisfies the specification.

What carries the argument

The central object is the certified $\varphi$-satisfying hyper-rectangle: an axis-aligned box $B_i\subset\mathbb{R}^k$ in latent space such that every $z\in B_i$ produces a trajectory $G_\theta(z)$ satisfying $\varphi$. The algorithm finds candidate boxes by running gradient ascent on the quantitative STL robustness $R_\varphi$, starting from random latent points, then expands each box while a neural-network verifier returns the lower bound 1 on $\chi_\varphi(G_\theta(z))$ over the whole box. The certified model is defined by Eq. (10), a mixture of truncated standard normals over the verified boxes; this keeps the distribution analytically tractable and preserves relative likelihoods. The verifier's soundness is what transfers local bound computations into the global probability-1 guarantee.

What would settle it

Take any certified latent box produced on the paper's benchmarks and probe inside it with dense sampling (or with a complete verification pass), monitoring each generated trajectory against the temporal-logic formula; a single violating trajectory inside a certified box disproves the probability-1 claim.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that certified guidance reduces to a single set-search problem. For a deterministic generator $G_\theta$ and an STL formula $\varphi$, let $\chi_\varphi$ be the Boolean satisfaction signal and let $\mathcal{B}=\{z : \chi_\varphi(G_\theta(z))=1\}$ be the maximal $\varphi$-satisfying set. Any subset $B\subseteq\mathcal{B}$ gives a new latent distribution $p_\varphi(z)=p(z\mid z\in B)$, and Corollary 3.2 shows the satisfaction probability of the modified model is 1 while the likelihood ratio $p_\varphi(z_1)/p_\varphi(z_2)=p(z_1)/p(z_2)$ is preserved for all $z_1,z_2\in B$. The paper constructs $B$ as a union of disjoint axis-aligned hyper-rectangles, each certified by sound lower bounds on $\chi_\varphi\circ G_\theta$ from a neural-network verifier, and writes the resulting $p_\varphi$ as a mixture of truncated normal distributions with closed-form box probabilities. On four planning benchmarks the method certifies both GANs and diffusion models, achieving an acceptance ratio of 1.00 where the original model ranges from 0.08 to 0.47 and where gradient guidance often falls short.

Load-bearing premise

The probability-1 claim collapses if the verifier's lower bound on "all points in this latent box produce trajectories that satisfy the temporal-logic formula" is not genuinely sound, and the paper does not specify how the discrete satisfaction signal is encoded for the verifier; additionally, the guarantee is for one conditioning value at a time, not for all conditions.

Editorial extensions

If this is right

  • Under a sound verifier, the modified GAN or diffusion model has acceptance ratio 1.00 by construction: every sampled trajectory satisfies the STL specification, removing the need for rejection sampling at runtime.
  • The certified model preserves the relative likelihood of latent points, so it avoids the off-manifold drift that pure gradient guidance can cause.
  • Certification is demonstrated for both GANs and diffusion models, but diffusion verification is expensive and did not scale to the 3D City benchmark.
  • Runtime sampling from the certified model is much cheaper than running gradient guidance for each new sample, after the offline certification cost.
  • The method extends directly to VAEs, since a variational decoder plays the same role as the GAN generator.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: because the certified boxes are subsets of the maximal satisfying set, the truncated distribution may discard feasible latent regions; reporting the probability mass $p(B)$ of the certified set would quantify the coverage cost, which the paper does not do.
  • Beyond the paper: the per-conditioning-value guarantee means deployment on unseen conditions needs an additional verified bound over the conditioning input; the paper's conclusion acknowledges this as future work rather than a demonstrated capability.
  • Beyond the paper: certifying a positive margin of the quantitative STL robustness over each box, rather than the Boolean satisfaction signal, would give a smooth, transparent verification target and could yield tighter bounds; this is a natural testable variant the paper does not pursue.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper proposes certified guidance, a method that turns a pre-trained deep generative model (GAN or diffusion model) into a new model that satisfies a given Signal Temporal Logic specification with probability one, without retraining. The key idea is to find a union of hyper-rectangles B in the latent space such that every latent point in B generates a trajectory satisfying the STL property phi, and then redefine the latent distribution as the original latent distribution conditioned on B. Section 3 formalizes this reduction: Proposition 3.1 equates satisfaction probability with the probability mass of the maximal phi-satisfying set, and Corollary 3.2 states that conditioning on any certified subset yields probability-one satisfaction while preserving likelihood ratios. Section 4 describes a practical algorithm that uses gradient ascent on STL robustness to find pivot latent points, iteratively expands epsilon-boxes around them, and uses the Auto-LiRPA verifier to certify that each box is phi-satisfying. Experiments on four planning benchmarks (UMaze, Crossroad, Obstacles, City) with both GANs and diffusion models report acceptance ratios of 1.00 for the certified models and log-likelihood comparisons against original and guided sampling.

Significance. If the verification step is sound, the paper makes a useful conceptual contribution: it reduces certified planning with generative models to finding certified regions in latent space, a constructive reduction that does not fit free parameters to make the guarantee true. The derivation of the truncated-normal mixture distribution (Eq. 10) and the preservation of likelihood ratios are clear and correct. The paper also demonstrates an engineering effort in encoding GAN and diffusion models into a verification framework, and reports plausible empirical improvements over non-certified guidance. The main significance hinges on the soundness of the unspecified Boolean STL encoding inside Auto-LiRPA; because that encoding is not described or validated, the central probability-one claim is currently an assertion rather than a demonstrated result.

major comments (4)
  1. [§3.1 and §5.2.1] The central guarantee rests on the soundness of the lower bound b_phi_theta computed by the neural network verifier over the Boolean STL satisfaction function chi_phi composed with the generator. The paper does not specify how chi_phi is encoded in Auto-LiRPA: chi_phi is a discontinuous, piecewise-constant function built from comparisons (g(s)>0), min/max, conjunction/disjunction, and temporal until/globally/eventually operators over a finite time grid. Auto-LiRPA's linear-relaxation engine is designed for continuous piecewise-linear activations, and no formal encoding, soundness proof, or independent validation is provided. As written, Eq. (14) and Corollary 3.2 therefore assert rather than establish the probability-1 guarantee. A revision must either specify the exact computational graph used (e.g., how strict inequalities and temporal quantifiers are relaxed) or provide a soundness argument, and should validate the bounds against a ground-truth STL monitor on the certified boxes.
  2. [§3.1 and Algorithm 1] The notation and object of verification are inconsistent: §3.1 defines b_phi_theta := G_theta ∘ chi_phi, which is the wrong composition order (it should be chi_phi ∘ G_theta), and then says the verifier propagates the box through this function to obtain bounds on Boolean satisfaction values. Algorithm 1 (lines 8 and 11) calls NNVerification with r_theta(z) (the real-valued robustness reward) as the function being verified, while the comments claim bounds on Boolean satisfaction chi_phi. These are different functions, and the algorithm must be explicit about which one is passed to the verifier. This is not merely cosmetic: if robustness bounds are used as a proxy, only the implication 'robustness > 0 implies satisfaction' is available, which does not yield a sound Boolean lower bound of 1 unless the verifier also proves robustness > 0 over the whole box.
  3. [§3.1 and §5.1] The Boolean STL satisfaction function chi_phi is defined in §2.1 as a function of signal and time, chi_phi(s,t), but the certification procedure uses a single binary value for the entire trajectory without specifying the evaluation time. For a trajectory defined on a finite horizon, satisfaction is presumably evaluated at t=0, but this is never stated. If the verifier instead evaluates satisfaction at some other time or over a concatenated prefix, the guarantee in Eq. (8) would not apply to the intended planning semantics. Please state the evaluation time explicitly and carry it through Algorithm 1.
  4. [§5.3] Table 1 reports acceptance ratio 1.00 for certified models, but the paper does not specify how this ratio was measured. If the satisfying check uses the same chi_phi implementation that is embedded in the verifier, it does not independently validate soundness; a ground-truth STL monitor (e.g., an external STL library) should be used to count violations among samples from the certified distribution. This is especially important because the verifier encoding is not specified (see above); the empirical acceptance ratio is the only evidence that the encoding is correct.
minor comments (5)
  1. [§1] The first sentence reads 'Deep generative models (DMG)' but the intended abbreviation is DGM (deep generative models).
  2. [Author affiliations] The affiliation 'King's Colledge London' contains a typo; it should be 'King's College London'.
  3. [§3] In Problem 1, 'finding a new latent distribution p_phi(phi)' should be p_phi(z); additionally, the conditional extension should state explicitly that the guarantee is per fixed conditioning value y, as the conclusion later acknowledges.
  4. [§5.2.1] The sentence 'Add times for DIFF.' is an incomplete editorial note that should be removed or replaced with the actual timing data.
  5. [§5.2] The symbol M is used both as the number of mixture components/hyper-rectangles and as the number of expansion cycles; the experimental settings paragraph equates M with cycles while Algorithm 1 uses M as an output count, which is confusing.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the probability-1 guarantee is a constructive definition, the certified-set search is the actual contribution, and the load-bearing verification step is an external soundness assumption, not a self-referential derivation.

full rationale

The derivation chain is not circular. Corollary 3.2 follows directly from the definition of a phi-satisfying set and the conditional distribution p_phi(z)=p(z|z in B): if B is a set on which chi_phi(G_theta(z))=1 everywhere, then conditioning on B makes satisfaction probability 1 by construction. The paper explicitly acknowledges this ('which is instead achieved by construction by our certified DGM'), so it does not present a fitted parameter as a prediction. The substantive claim is that such sets B can be found algorithmically by sound neural-network verification; that step depends on Auto-LiRPA's lower bounds on the composed function G_theta o chi_phi, which is an external tool and an independent soundness condition. Section 5.2.1 states that the Boolean STL semantics is 'integrated into the computational graph' of Auto-LiRPA but gives no formal encoding or proof of bound soundness; this is a correctness/rigor gap, not a circularity, because the result is conditional on that external property rather than assumed into existence by the paper's own definitions. The self-citations (e.g., [5] for iterative expansion) are not load-bearing: the heterogeneous-increment scheme from [5] is mentioned but the experiments report only homogeneous increments ('we report results only for the homogeneous increment version'). No load-bearing self-citation chain forces the outcome. The acknowledged limitation that guarantees are per conditioning value y is an honest boundary of the claim, not a circular step.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The central guarantee rests on standard STL semantics, the soundness of the NN verifier for the unstated Boolean STL encoding, and the assumption of a fixed deterministic generator with a standard normal latent distribution. No new physical entities are postulated. The hand-chosen expansion parameters affect how much of the latent space is certified but not the validity of the guarantee.

free parameters (4)
  • epsilon_0 = 0.01
    Initial perturbation radius in Algorithm 1. Hand-chosen, affects how many boxes can be certified and their volume, but does not affect the validity of the guarantee.
  • Delta_epsilon = 0.005
    Incremental expansion step in Algorithm 1. Hand-chosen, affects the granularity of box expansion, not the soundness of the certification.
  • L = 20 for GAN, 5 for DIFF
    Number of gradient-ascent pivot points in Algorithm 1. Hand-chosen, affects coverage of the latent space and the total number of certified boxes, not the correctness of each certified box.
  • alpha = not reported
    Ad-hoc constant for heterogeneous epsilon increments in Section 4. The authors report that heterogeneous increments were less effective and do not use them in the final results.
assumptions (4)
  • standard math STL robustness sign is sound: R_phi(s,t) > 0 implies satisfaction and R_phi(s,t) < 0 implies violation.
    Invoked in Sections 2.1 and 3.1 to justify using the quantitative STL semantics as a differentiable reward and as a basis for certification.
  • domain assumption Auto-LiRPA/CROWN computes sound lower and upper bounds for the composite network G_theta composed with the Boolean STL semantics.
    The probability-1 guarantee depends entirely on this bound being a true lower bound on chi_phi over the box. The paper asserts this in Sections 3.1 and 5.2.1 but does not specify the encoding.
  • domain assumption The latent distribution is standard normal and the generator G_theta is deterministic, so the conditioned distribution is a mixture of truncated normals.
    Used to derive the analytical sampling distribution in Eq. (10). For diffusion models, determinism is obtained by setting DDIM sigma_tau = 0, which changes the generative process from the trained DDPM.
  • domain assumption The pre-trained generative model is fixed and is a reasonable approximation of the target trajectory distribution.
    The certification holds for the fixed model G_theta, not for the true physical system. If the model is inaccurate, the guarantee is about the model's outputs, not about real-world safety. This is implicit in Section 2.2.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Certified Guidance for Planning with Deep Generative Models." pith.science (2026). https://pith.science/paper/SDJCYER3

@misc{pith2026250112815,
  author       = {Pith},
  title        = {Pith review of: Certified Guidance for Planning with Deep Generative Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SDJCYER3}},
  note         = {Machine review of arXiv:2501.12815}
}
read the original abstract

Deep generative models, such as generative adversarial networks and diffusion models, have recently emerged as powerful tools for planning tasks and behavior synthesis in autonomous systems. Various guidance strategies have been introduced to steer the generative process toward outputs that are more likely to satisfy the planning objectives. These strategies avoid the need for model retraining but do not provide any guarantee that the generated outputs will satisfy the desired planning objectives. To address this limitation, we introduce certified guidance, an approach that modifies a generative model, without retraining it, into a new model guaranteed to satisfy a given specification with probability one. We focus on Signal Temporal Logic specifications, which are rich enough to describe nontrivial planning tasks. Our approach leverages neural network verification techniques to systematically explore the latent spaces of the generative models, identifying latent regions that are certifiably correct with respect to the STL property of interest. We evaluate the effectiveness of our method on four planning benchmarks using GANs and diffusion models. Our results confirm that certified guidance produces generative models that are always correct, unlike existing guidance methods that are not certified.

Figures

Figures reproduced from arXiv: 2501.12815 by the authors.

Figure 1
Figure 1. Certified Robust Generation: gradient ascent strat [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Visualizations of GAN-generated paths using each [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. DIFF Certified paths in different benchmarks [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 23 canonical work pages

  1. [1]

    Anurag Ajay, Yilun Du, Abhi Gupta, Joshua Tenenbaum, Tommi Jaakkola, and Pulkit Agrawal. 2023. Is Conditional Generative Modeling all you need for Decision-Making? arXiv:2211.15657 [cs.LG] https://arxiv.org/abs/2211.15657

  2. [2]

    Michael Akintunde, Elena Botoeva, Panagiotis Kouvaros, and Alessio Lomuscio

  3. [3]

    Martin Arjovsky, Soumith Chintala, and Léon Bottou. 2017. Wasserstein gan. arXiv preprint arXiv:1701.07875 (2017)

  4. [4]

    Arpit Bansal, Hong-Min Chu, Avi Schwarzschild, Soumyadip Sengupta, Micah Goldblum, Jonas Geiping, and Tom Goldstein. 2023. Universal guidance for diffusion models. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition. 843–852

  5. [5]

    Ben Batten, Mehran Hosseini, and Alessio Lomuscio. 2024. Tight Verification of Probabilistic Robustness in Bayesian Neural Networks. In The 27th International Conference on Artificial Intelligence and Statistics, AISTATS , Vol. 238

  6. [6]

    Francesca Cairoli, Nicola Paoletti, and Luca Bortolussi. 2023. Conformal Quan- titative Predictive Monitoring of STL Requirements for Stochastic Processes. In International Conference on Hybrid Systems: Computation and Control, HSCC . ACM, 1:1–1:11

  7. [7]

    Zibin Dong, Jianye Hao, Yifu Yuan, Fei Ni, Yitian Wang, Pengyi Li, and Yan Zheng

  8. [8]

    Alexandre Donzé and Oded Maler. 2010. Robust satisfaction of temporal logic over real-valued signals. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 92–106

Show all 42 references
  1. [9]

    2016.Deep learning

    Ian Goodfellow, Yoshua Bengio, Aaron Courville, and Yoshua Bengio. 2016.Deep learning. Vol. 1. MIT press Cambridge

  2. [10]

    Ian Goodfellow, Jean Pouget-Abadie, Mehdi Mirza, Bing Xu, David Warde-Farley, Sherjil Ozair, Aaron Courville, and Yoshua Bengio. 2014. Generative adversarial nets. In Advances in neural information processing systems . 2672–2680

  3. [11]

    Ishaan Gulrajani, Faruk Ahmed, Martin Arjovsky, Vincent Dumoulin, and Aaron C Courville. 2017. Improved training of wasserstein gans. Advances in neural information processing systems 30 (2017)

  4. [12]

    Jonathan Ho, Ajay Jain, and P. Abbeel. 2020. Denoising Diffusion Probabilistic Models. ArXiv abs/2006.11239 (2020)

  5. [13]

    Mehran Hosseini and Alessio Lomuscio. 2023. Bounded and Unbounded Verifica- tion of RNN-Based Agents in Non-deterministic Environments. In International Conference on Autonomous Agents and Multiagent Systems, AAMAS . ACM, 2382– 2384

  6. [14]

    Michael Janner, Yilun Du, Joshua B Tenenbaum, and Sergey Levine. 2022. Plan- ning with diffusion for flexible behavior synthesis.arXiv preprint arXiv:2205.09991 (2022)

  7. [15]

    Tenenbaum, and Sergey Levine

    Michael Janner, Yilun Du, Joshua B. Tenenbaum, and Sergey Levine. 2022. Plan- ning with Diffusion for Flexible Behavior Synthesis. In International Conference on Machine Learning, ICML , Vol. 162. PMLR, 9902–9915

  8. [16]

    Katz, Anthony L

    Sydney M. Katz, Anthony L. Corso, Christopher A. Strong, and Mykel J. Kochen- derfer. 2022. Verification of Image-Based Neural Network Controllers Using Generative Models. J. Aerosp. Inf. Syst. 19, 9 (2022), 574–584

  9. [17]

    Kavraki, P

    L.E. Kavraki, P. Svestka, J.-C. Latombe, and M.H. Overmars. 1996. Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Transactions on Robotics and Automation 12, 4 (1996), 566–580. https://doi.org/ 10.1109/70.508439

  10. [18]

    Tom Kuipers, Renukanandan Tumu, Shuo Yang, Milad Kazemi, Rahul Mang- haram, and Nicola Paoletti. 2024. Conformal Off-Policy Prediction for Multi- Agent Systems. arXiv:2403.16871

  11. [19]

    Lars Lindemann, Matthew Cleaveland, Gihyun Shim, and George J. Pappas. 2023. Safe Planning in Dynamic Environments Using Conformal Prediction. IEEE Robotics Autom. Lett. 8, 8 (2023), 5116–5123

  12. [20]

    Liyuan Liu, Haoming Jiang, Pengcheng He, Weizhu Chen, Xiaodong Liu, Jianfeng Gao, and Jiawei Han. 2021. On the Variance of the Adaptive Learning Rate and Beyond. arXiv:1908.03265 [cs.LG] https://arxiv.org/abs/1908.03265

  13. [21]

    Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of con- tinuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152–166

  14. [22]

    Mehdi Mirza and Simon Osindero. 2014. Conditional generative adversarial nets. arXiv preprint arXiv:1411.1784 (2014)

  15. [23]

    Alex Nichol and Prafulla Dhariwal. 2021. Improved Denoising Diffusion Proba- bilistic Models. arXiv:2102.09672 [cs.LG] https://arxiv.org/abs/2102.09672

  16. [24]

    Andreas Orthey, Constantinos Chamzas, and Lydia E. Kavraki. 2024. Sampling- Based Motion Planning: A Comparative Review. Annu. Rev. Control. Robotics Auton. Syst. 7, 1 (2024)

  17. [25]

    Weiss, Niru Maheswaranathan, and Surya Ganguli

    Jascha Sohl-Dickstein, Eric A. Weiss, Niru Maheswaranathan, and Surya Ganguli

  18. [26]

    Jiaming Song, Chenlin Meng, and Stefano Ermon. 2022. Denoising Diffusion Implicit Models. arXiv:2010.02502 [cs.LG] https://arxiv.org/abs/2010.02502

  19. [27]

    Yang Song and Stefano Ermon. 2019. Generative modeling by estimating gradi- ents of the data distribution. Advances in neural information processing systems 32 (2019)

  20. [28]

    Yang Song and Stefano Ermon. 2020. Generative Modeling by Estimating Gradi- ents of the Data Distribution. arXiv:1907.05600 [cs.LG]

  21. [29]

    Yang Song and Stefano Ermon. 2020. Improved techniques for training score- based generative models. Advances in neural information processing systems 33 (2020), 12438–12448

  22. [30]

    Yang Song, Jascha Sohl-Dickstein, Diederik P Kingma, Abhishek Kumar, Stefano Ermon, and Ben Poole. 2020. Score-based generative modeling through stochastic differential equations. arXiv preprint arXiv:2011.13456 (2020)

  23. [31]

    Kochenderfer, and Mac Schwager

    Jiankai Sun, Yiqi Jiang, Jianing Qiu, Parth Nobel, Mykel J. Kochenderfer, and Mac Schwager. 2023. Conformal Prediction for Uncertainty-Aware Planning with Diffusion Dynamics Model. In Advances in Neural Information Processing Systems, NeurIPS, Vol. 36. Curran Associates, Inc.,...

  24. [32]

    Yusuke Tashiro, Jiaming Song, Yang Song, and Stefano Ermon. 2021. Csdi: Conditional score-based diffusion models for probabilistic time series imputation. Advances in Neural Information Processing Systems 34 (2021), 24804–24816

  25. [33]

    Cédric Villani. 2008. Optimal transport: old and new . Vol. 338. Springer Science & Business Media

  26. [34]

    Matthew Wicker, Luca Laurenti, Andrea Patane, and Marta Kwiatkowska. 2020. Probabilistic Safety for Bayesian Neural Networks. In Proceedings of the Thirty- Sixth Conference on Uncertainty in Artificial Intelligence, UAI

  27. [35]

    Matthew Wicker, Luca Laurenti, Andrea Patane, Nicola Paoletti, Alessandro Abate, and Marta Kwiatkowska. 2024. Probabilistic reach-avoid for Bayesian neural networks. Artif. Intell. 334 (2024), 104132

  28. [36]

    Wei Xiao, Tsun-Hsuan Wang, Chuang Gan, and Daniela Rus. 2023. SafeDiffuser: Safe Planning with Diffusion Probabilistic Models. arXiv:2306.00148

  29. [37]

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. 2020. Automatic pertur- bation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems 33 (2020), 1129–11...

  30. [41]

    This training objective can also be viewed as a weighted combination of denoising score matching used for training score-based generative models [27, 29, 30]

    (20) The denoising function 𝜖𝜃 estimates the noise vector 𝜖 that was added to its noisy input x𝜏 . This training objective can also be viewed as a weighted combination of denoising score matching used for training score-based generative models [27, 29, 30]. Once trained, we ca...

  31. [42]

    The computational burden and complexity of sampling from a trained DDPM can be reduced by resorting to their implicit formulation [26]

    (21) Implicit Denoising Diffusion Models. The computational burden and complexity of sampling from a trained DDPM can be reduced by resorting to their implicit formulation [26]. The so-called De- noising Diffusion Implicit Models (DDIM) were first introduced to speed up the sa...

  32. [2015]

    arXiv:1503.03585 [cs.LG]

    Deep Unsupervised Learning using Nonequilibrium Thermodynamics. arXiv:1503.03585 [cs.LG]

  33. [2022]

    Journal of Autonomous Agents and Multi-Agent Systems 36, 1 (2022)

    Formal Verification of Neural Agents in Non-deterministic Environments. Journal of Autonomous Agents and Multi-Agent Systems 36, 1 (2022)

  34. [2024]

    arXiv:2401.15443

    DiffuserLite: Towards Real-time Diffusion Planning. arXiv:2401.15443

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.