神经提议、符号保证：基于硬约束的神经符号图生成

我们挑战黑箱纯深度神经方法在分子和图生成中的做法，这些方法在可控性方面受限且缺乏形式保证。我们引入神经符号图生成建模（NSGGM），一种神经符号框架，将分子生成重新表述为带符号装配的骨架和相互作用学习任务。自回归神经模型提出骨架并细化相互作用信号，CPU 高效的 SMT 求解器在强制化学有效性、结构规则及用户特定约束的同时构建完整图谱，生成正确且可解释可控的分子——纯神经方法无法提供。NSGGM 在无约束生成和受约束生成任务上均表现出色，证明神经符号建模能够匹配最新生成式方法的性能，同时提供显式可控性和保证。为评估更细致的可控性，我们还引入了逻辑约束分子基准测试，旨在测试严格的硬规则满足，适用于需要显式、可解释规范及可验证合规性的工作流程。