Neural Proposals, Symbolic Guarantees: Neuro-Symbolic Graph Generative Modeling¶

会议: NeurIPS 2026
arXiv: 2602.16954
OpenReview: https://openreview.net/forum?id=4Q6ThyZHec
论文: https://arxiv.org/abs/2602.16954
领域: 图学习
关键词: 神经符号生成, 图生成模型, SMT求解器, 分子图设计, 严格逻辑约束

一句话总结¶

提出了神经符号图生成框架 NSGGM，将分布学习解耦为自回归神经模型提议图元脚手架与 SMT 求解器执行离散拼装，在保持高质量分布拟合的同时为严格逻辑约束提供可验证的构造性保证。

研究背景与动机¶

深度图生成模型（涵盖自回归、图扩散与流模型等）在分子设计、药物发现和电子电路拓扑生成等领域取得了巨大成功，能够从海量无约束数据中捕获高维连续特征并采样出多样化的新颖图拓扑。然而，在以药物化学过滤（如 PAINS 警示结构过滤、生物等排体替换）和骨架跃迁为代表的高风险实际研发中，用户往往对生成产物施加由多重命题逻辑组合而成的硬性约束（如“必须包含指定骨架 A 且排除官能团 B，或在二选一互斥位点引入特定取代基”）。当这些复合逻辑规则在训练集中支持度极低甚至完全未出现（Zero-support）时，传统模型便陷入分布外（OOD）泛化困境。

现有图生成方法处理此类约束通常依赖隐式偏置（如潜在空间种子条件化）或离散扩散中的局部碎片修补（inpainting），而通用手段则是“生成后过滤”（generate-and-filter）。这种试错循环在约束空间极其稀疏时采样效率呈灾难性崩溃，耗尽百万级采样预算亦难以获得满足条件的合法样本；更致命的是，纯神经模型无法提供单样本级别的数学可验证凭证，并在目标不可满足时完全失去向用户报告不可行性原因（infeasibility proof）的能力。

针对分布拟合与硬逻辑推理之间的脱节，本文的切入角度是将生成机制显式解耦为“神经提议”与“符号保障”两个独立阶段，让轻量神经网络专注从数据中拟合子图拓扑先验，而将离散组合拼装与硬约束判定移交给具备严格理论完备性的符号推理层。本文的核心 idea 是：将图生成解耦为自回归 Transformer 提议图元及其附带神经连接偏置的蓝图，并由 SMT 求解器在包含化学与用户自定义命题逻辑的硬子句约束下执行离散化原子融合，使生成图在构造上具备严格的拓扑有效性与可审计的逻辑可满足性证明。

方法详解¶

整体框架¶

NSGGM 将分子图生成视作基于离散图元的组合装配任务。整个生成流水线包含预处理离散蓝图分解、神经蓝图自回归提议以及基于 SMT（Satisfiability Modulo Theories）的符号拼装三个阶段：首先从分子数据集中通过最小环基（Minimum Cycle Basis）和桥键 BFS 分解构建图元与槽位变体词表；随后神经模块由图变分自编码器（GNN-VAE）抽取图表征并利用因果 Transformer 与双向细化网络输出图元序列及连接指导；最后 Z3 求解器在硬拓扑约束和用户一阶逻辑规约下执行精确解算，并将神经连接偏置作为 Max-SMT 软子句以保留先验分布倾向。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["输入分子图 / 先验分布"] --> B["阶段1：图元分解与槽位词表构建<br/>提取环与无环Tile并记录端口特征"]
    B --> C["阶段2：神经提议生成<br/>自回归Transformer蓝图生成与双向引导"]
    C --> D["阶段3：SMT符号拼装与硬约束解算<br/>Z3求解器在原子价键与用户逻辑下装配"]
    D -->|SAT| E["输出验证合法分子图<br/>附带可满足性模型凭证"]
    D -->|UNSAT| F["不可行诊断与反例核心<br/>提取不可满足最小子句集合"]

关键设计¶

1. 图元分解与槽位变体词表构建：建立结构自同构与接口配位数的一致性抽象 传统以单原子或任意片段为单元的拼接极易破坏化学环系稳定性，而无类型约束的拼装又会导致巨大的搜索空间。为此，NSGGM 将分子图 $G=(V, E, \ell_V, \ell_E)$ 分解为图元多重集 $\mathcal{T}(G) = \{t_i\}_{i=1}^K$：环图元取自环边导出的最小环基，无环图元由桥键的深度受限广度优先搜索（BFS）生成。为支持精确拼装，每个图元 $t$ 中的外向连接端口被形式化为节点槽位 $\sigma_v^t$ 与边槽位 $\sigma_e^t$。节点槽位严格统计该原子在全图与该图元内部键型 $\tau$ 的差值： $$\sigma_v^t(\tau) = b_G(v)(\tau) - b_t(v)(\tau)$$ 接着，利用两阶段 Weisfeiler-Lehman（WL）散列分别计算图元拓扑散列 $h_{\mathrm{struct}}(t) = \mu$ 和附带槽位信息的元数据散列 $h_{\mathrm{meta}}(\tilde{t}) = \nu$。高频出现的组合被固化为词表 $\mathcal{V}$，将任意图紧凑映射为离散键序列构成的蓝图 $S_G = ((\mu_i, \nu_i))_{i=1}^K$。该设计在引理层面保证了分解可逆覆盖性，且大幅缩减了下游求解器必须枚举的候选对接对。

2. 神经引导蓝图提议网络：解耦宏观语义采样与微观几何决策 纯符号搜索缺乏数据分布先验，容易在巨大的离散解空间中生成符合规则但不符合真实药物分子分布的怪异构型。NSGGM 引入 GNN-VAE 与 Transformer 协同的神经提议网络：图编码器通过 GINE-Conv 聚合图元图拓扑特征输出高斯潜变量 $z \sim q_\phi(z \mid G)$；因果 Transformer 解码器在 $z$ 的条件化引导下自回归预测图元拓扑序列 $\mathcal{M} = (\mu_1, \dots, \mu_K, \texttt{<eos>})$；随后双向 Transformer 细化网络输出特征状态 $\mathbf{h}_i$，并接入三个并行的预测头：掩码预测图元槽位变体 $\nu_i \in \Omega(\mu_i)$、通过双线性注意力预测当前图元的父节点挂载索引 $\pi_i \in \{1, \dots, i-1\}$、以及通过 Sigmoid 预测融合模式 $\eta_i \in \{0, 1\}$（节点并合或共用边并合）。模型完全遵循 ELBO 目标端到端优化： $$\mathcal{L}(\theta, \phi) = \mathbb{E}_G \mathbb{E}_{z \sim q_\phi(z \mid G)} [\log p_\theta(y \mid z)] - \beta \, \mathrm{KL}(q_\phi(z \mid G) \,\|\, p(z))$$ 这保证了神经模块为后续符号求解提供高度贴合真实数据流形的结构模板，而不越俎代庖去处理严苛的离散一致性。

3. 基于 SMT/Max-SMT 的构造性符号装配：化学价键法则与任意命题逻辑的双层硬约束编译 在接收到蓝图提议 $\hat{S} = ((\mu_i, \nu_i))_{i=1}^K$ 后，符号装配器在布尔变量集合（包含候选并合变量 $m_{u,v}$、图元激活变量 $\mathrm{in\_mol}_i$ 和子结构指示变量 $p_u$）上构建 SMT 约束公式 $\Phi = \phi_{\mathrm{hard}} \wedge \phi_{\mathrm{user}}$。硬约束 $\phi_{\mathrm{hard}}$ 联合编译了元素一致性、并合传递闭包、图元内部原子单射性、全图连通性（基于深度受限 BFS 命题编码）、共享边标签一致性，以及最为关键的原子价键上限： $$B([u]) = \Bigl(\sum_{w \in [u]} \mathrm{iv}(w)\Bigr) - \Delta_{\mathrm{share}}([u]) \leq \mathrm{val}(u) \quad \forall u \in V^{\mathrm{slot}}$$ 对于用户自定义的高阶逻辑规范 $(U, \psi)$，系统将目标子结构 $u \in U$ 编译为指示布尔变量 $p_u$，直接将任意一阶逻辑公式 $\psi$ 嵌入求解器；同时将神经提议中的父节点索引 $\pi_i$ 与融合方式 $\eta_i$ 转化为 Max-SMT 的加权软子句（Soft Clauses）。求解器优先最大化神经软偏置权重，在硬约束冲突时自动退让，从而彻底消除了传统神经网络在规则外推上的死角。

损失函数 / 训练策略¶

模型监督目标包含图元拓扑标签、槽位变体、父指针与融合类型四个部分，整体重构似然形式化为： $$\log p_\theta(y \mid z) = \lambda_{\mathcal{M}} \log p_\theta(\mathcal{M} \mid z) + \lambda_{\nu} \log p_\theta(\nu_{1:K} \mid \mathcal{M}, z) + \lambda_{\pi} \log p_\theta(\pi_{2:K} \mid \mathcal{M}, z) + \lambda_{\eta} \log p_\theta(\eta_{2:K} \mid \mathcal{M}, z)$$ 训练采用 Adam 优化器，恒定学习率为 $10^{-4}$，梯度裁剪范数设为 1.0，批量大小为 1024。超参数权重设置为 $\lambda_{\mathcal{M}} = \lambda_{\nu} = \lambda_{\pi} = 2$，$\lambda_{\eta} = 1$。$\mathrm{KL}$ 正则化系数 $\beta$ 在前 1000 步从 0 线性预热至 0.5 并在后续训练中保持常数，最大训练轮数为 1500 轮（早停耐心值为 10）。

实验关键数据¶

主实验¶

论文分别在经典无约束生成基准（GuacaMol、MOSES、QM9）与评估严格逻辑满足率的全新基准 MolSAT 上进行了全方位验证。在 MolSAT 基准上，包含四大逻辑推理家族（I: 过滤级联；II: 析取选择/生物等排；III: 杂化复合条件；IV: 强耦合 XOR/IFF），并在三种训练支持度（High、Low、Zero）下评估命题满足率（Hit%）。基线模型 MoLeR 与 GenMol 赋予 $10^6$ 次采样预算。

任务家族	难度层级	MoLeR [21] (10⁶ 预算)	GenMol [15] (10⁶ 预算)	NSGGM (本文)	相对优势 / 评述
Family I (过滤级联)	High-support	14.1%	64.4%	98.9%	神经基线难兼顾多重过滤
Family I (过滤级联)	Low-support	7.1%	37.6%	99.9%	低频时基线采样命中率锐减
Family I (过滤级联)	Zero-support	0.0%	0.0%	79.7%	神经基线彻底崩溃，本文保持高命中
Family II (析取选择)	High-support	23.0%	51.0%	100.0%	本文达到 100% 构造性满足
Family II (析取选择)	Low-support	4.3%	48.6%	99.9%	显著超越最强扩散基线
Family II (析取选择)	Zero-support	0.0%	0.0%	84.1%	保持极强零样本符号泛化能力
Family III (杂化复合)	Low φ₁	10.9%	31.5%	99.7%	复合逻辑蕴含条件精确满足
Family III (杂化复合)	Low φ₂	5.9%	28.3%	96.0%	复杂多子句约束高稳定性
Family III (杂化复合)	Zero-support	0.0%	0.0%	63.9%	神经基线 10⁶ 预算无法生成单例
Family IV (耦合XOR/IFF)	High-support	12.5%	61.5%	99.6%	非局部逻辑绑定完全解析
Family IV (耦合XOR/IFF)	Zero-support	0.0%	0.0%	85.6%	零支持度下仍保持 85% 以上

在无约束分子生成基准 GuacaMol 上，NSGGM 同样保持了优异的分布逼近能力：

模型	有效性 Valid (%) ↑	唯一性 Unique (%) ↑	新颖性 Novel (%) ↑	分布拟合 FCD ↑	属性KL散度 KL ↑
MoLeR [21]	100.0	100.0	99.1	62.5	96.4
MiCaM [8]	100.0	99.4	98.6	73.1	98.9
DiGress [29]	85.2	100.0	99.9	68.0	92.9
DISCO-GT [32]	100.0	86.6	99.9	59.7	92.6
NSGGM (本文)	100.0±0.0	100.0±0.0	98.9±0.0	86.1±0.4	95.5±0.1

消融实验¶

在 GuacaMol 上针对神经引导信号进行消融研究（在诊断性设置下放宽硬连通性约束以量化拓扑碎片化程度）：

配置	分布拟合 FCD ↑	属性散度 KL ↑	碎片化率 Frag. (%) ↓	丢失Token比例 (%) ↓	说明
Full model	86.1	95.5	0.0	0.0	完整模型：强分布拟合且图拓扑完全连通
w/o 父节点预测 (parent pred.)	49.2	87.6	62.5	23.4	失去主连通引导，62.5% 生成图解离为碎块
w/o 融合类型预测 (merge-type)	63.0	88.3	22.8	8.4	缺乏边/节点融合类型偏置，产生次级断裂
w/o 蓝图槽位细化 (blueprint char.)	62.4	88.9	0.0	0.0	退化为选择最高频变体，FCD显著滑落但保持连通

关键发现¶

零支持度逻辑泛化的维度碾压：在训练集中出现频次为零（Zero-support）的严苛化学逻辑约束下，无论是基于自回归潜空间偏置的 MoLeR 还是基于离散扩散修复的 GenMol，在高达 $10^6$ 次生成尝试中均产生 0% 的满足率；而 NSGGM 在所有四大家族中均实现了 63.9% 至 85.6% 的超高零样本满足率。
求解器计算复杂度次二次受控：在单核 CPU 评测中，随着分子包含的图元数量 $k$ 和候选并合变量数 $v$ 增加，SMT 求解时间呈现经验公式 $\sim v^{1.4}$ 与 $\sim k^{2.7}$ 增长，整体中位求解延迟仅为 15.1 ms（95 分位 99.2 ms），大幅打破了理论最坏指数界限，证实图元级抽象与神经剪枝的卓越效率。
神经引导与符号保障不可偏废：消融表明，缺少父节点预测将导致 62.5% 的图产生拓扑断裂，而缺少符号硬约束则会丧失可满足性保证；双系统配合是实现“保真度与硬控制兼得”的唯一途径。

亮点与洞察¶

神经提议与符号求解的纯正解耦：将连续数据分布特征留给深度网络拟合，离散组合推理留给 Z3 SMT 求解器，从根源上消除了“靠模型自发记住硬规则”的不可靠幻想。
可审计与带反例证明的生成范式：SAT 产物输出具体的并合赋值作为满足证书，UNSAT 则返回不可行核心（Unsat Core）指出具体冲突子句，为药物研发等高风险领域提供了前所未有的可解释性和错误溯源凭据。
免微调的零开销控制：用户追加的复杂化学假说或骨架筛选条件无需重新训练或适配适配器网络，可直接翻译为命题逻辑硬子句在推理期注入求解，开创了图生成的新范式。

局限与展望¶

领域先验向布尔子句转译的建模壁垒：将药物化学家的经验直觉转化为严谨的无二义性一阶逻辑子句并非易事，过于生硬的硬规则可能导致求解器频繁判定 UNSAT，未来需探索从自然语言或弱监督示例中自动提炼谓词库的技术。
化学有效性层级仍局限在 2D 拓扑：当前 $\phi_{\mathrm{hard}}$ 的约束深度与 RDKit 拓扑有效性等价，尚未覆盖三维立体化学构象、电子轨道分布及手性异构体几何约束。
向连续理论求解器的延伸空间：目前模型仅处理 2D 分子图，未来将 SMT 求解机制扩展到实数理论（SMT modulo Real Arithmetic）并结合三维坐标与空间几何谓词，是实现全流程 3D 分子生成的重要演进路径。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次建立基于 SMT 与 Max-SMT 软硬解耦的神经符号图生成理论框架，设计极具开创性。
实验充分度: ⭐⭐⭐⭐⭐ 构建 MolSAT 四大家族系统性评测基准，单核 CPU 延迟和百万次采样对比全面透彻。
写作质量: ⭐⭐⭐⭐⭐ 形式化理论推导严谨，定义完备，引理证明与算法表述清晰。
价值: ⭐⭐⭐⭐⭐ 为高风险分子发现与可控图生成提供了兼具理论证明与工业级落地潜力的崭新基石。