Constraint Satisfied Sampling for Formal Verification in Geometric Deep Learning and Molecular Modelling

Analyzing the macroscopic traits of biologicalmolecules and protein complexes requires accu-rate and specific descriptions of statistical en-sembles. A notable challenge is the samplingfrom subspaces of a state-space, either becausewe have prior structural knowledge or only cer-tain subsets of the state-space are of interest. Weintroduce a method to samples from distributionsthat formally satisfy sets of geometric constraintsin Euclidean spaces. This is accomplished by in-corporating a constraint projection operator intothe well-established structure of Denoising Dif-fusion Probabilistic Models. In deep learning-based drug design, maintaining specific molecu-lar interactions is essential for achieving desiredtherapeutic effects and ensuring safety. Thisstarts a meaningful intersection between formalverification principles and machine learning inthe realm of biochemical studies of compoundsand generative modeling. It offers a way to for-mally verify the distributions from which sam-ples are drawn.