GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching¶

会议: NeurIPS 2026
arXiv: 2605.08243
领域: 优化/理论
关键词: 混合布尔算术 (MBA), 程序合成, GPU加速, 逆向反混淆, 无缓存枚举

一句话总结¶

针对定量位向量行为导致语言缓存无法扩展的根本瓶颈，本文提出首个无缓存GPU程序合成系统Simba，通过双射逆波兰枚举与局部一致编码避免内存爆炸与warp分支分歧，实现规模达16的高效MBA表达式精确合成。

研究背景与动机¶

混合布尔算术（Mixed-Boolean Arithmetic, MBA）将定宽位向量上的按位逻辑运算（与、或、异或、非）与代数算术运算（加法、减法、乘法）交织结合。在软件安全与编译器领域，MBA被广泛用作代码混淆的核心机制，将简单的语义变换为高度晦涩复杂的等价指令流；从输入输出示例中自动合成最小等价表达式，是逆向工程反混淆、二进制密码分析以及超优化编译器的关键刚需。然而，传统的CPU反混淆器面临严峻的可扩展性挑战：基于蒙特卡洛树搜索或随机局域搜索的随机合成系统（如Syntia、Xyntia、XSmir）缺乏完备性保证且对复杂实例求解乏力；基于符号代数分解的化简器（如MBA-Blast、SiMBA、GAMBA）仅局限于线性或特定代数子类；而基于SAT/SMT理论的求解器（如cvc5）在32位及以上宽位向量时搜索空间急剧膨胀，计算极其耗时。

近期，基于GPU的大规模自底向上枚举合成技术在定性场景（如正则语言推断与LTL时序逻辑学习）中展现出数个数量级的加速效果。然而，现有GPU合成器高度依赖基于“观测等价性”（observational equivalence）的语言缓存机制，即将所有中间候选表达式的行为缓存并去重。这一范式在定性领域运行良好，因为每个候选在测试追踪上的行为仅为布尔判定，64条追踪的行为向量可直接压缩为一个64位机器字；但在MBA等定量合成任务中，每个候选表达式在每个测试用例上输出一个 $w$ 位的数值向量。若给定 $n$ 个示例，$w=32$ 位宽，其行为空间大小达到 $2^{wn}$（例如 $n=10$ 时为 $2^{320}$）。超指数增长的候选空间导致内存哈希缓存发生剧烈溢出与去重失效，GPU显存往往在表达式规模极小时便彻底耗尽。

面对定量合成中显存墙与去重收益递减的核心矛盾，本文彻底抛弃了“维护观测等价缓存”的传统思路。核心 idea：放弃语言缓存，构建整数标识符与逆波兰MBA表达式之间的双向双射映射，利用预计算计数表在GPU线程本地寄存器中即时解码并按位验证，并通过局部一致性编码保证同一warp内线程共享公共子树以消除分支分歧。

方法详解¶

整体框架¶

Simba采用无缓存的自底向上按表达式规模逐层递增搜索架构。输入包含 $n$ 组 $k$ 元位向量输入输出对规范 $S = \{(\mathbf{x}_i, y_i)\}_{i=1}^n$ 及规模上界 $C$。CPU端首先离线递推生成一个各规模各算子的紧凑计数表并固化到GPU常量内存中；随后主循环按规模 $s=1,2,\dots,C$ 和8个运算符槽位分别调度GPU计算核心。每个GPU线程根据自身全局线程ID，完全在本地寄存器中瞬时反算解码出唯一的逆波兰（RPN）表达式，并直接对 $n$ 个示例执行栈求值校验；一旦匹配成功，通过原子写回全局解缓冲区并通知主机中断搜索。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["输入规范与参数<br/>S={x_i, y_i}, 变量数k, 规模界限C"] --> B["算子递归计数与常量表加载<br/>递推计算T[s][op]并写入GPU常量内存"]
    B --> C["外层规模与算子批次调度<br/>按规模s=1..C及8个运算符槽位分发Kernel"]
    C --> D["双射逆波兰解码<br/>线程ID在寄存器中瞬时映射为唯一RPN树"]
    D --> E["局部一致性保序求值<br/>Warp内共享左子树消除SIMT分支分歧"]
    E --> F["端到端即时验证与原子命中<br/>求值匹配则原子写回解缓冲区并返回结果"]

关键设计¶

1. 算子递推计数表与无缓存即时双射解码：彻底消除显存占用的解空间直接寻址

传统GPU合成框架之所以陷入显存枯竭（OOM），是因为它试图物化保存所有中间子树及其观测指纹。Simba通过代数计数实现了无状态的即时反求：预先在CPU上建立动态规划表 $\mathsf{T}[s][op]$，记录规模为 $s$、顶层算子为 $op$ 的有效逆波兰式总数。对包含 $k$ 个变量、2个一元算子（$\sim, -$）和6个二元算子（$\land, \lor, \oplus, +, -, \times$）的语法，其递推公式充分利用算子对称性剪枝： $$ \begin{aligned} \mathsf{T}[1][8] &= k, \ \mathsf{T}[s][op_{\text{unary}}] &= \mathsf{T}[s-1][8], \ \mathsf{T}[s][op_{\text{comm}}] &= \sum_{j=1}^{\lfloor(s-1)/2\rfloor} \mathsf{T}[j][8] \cdot \mathsf{T}[s-1-j][8], \ \mathsf{T}[s][op_{\text{sub}}] &= \sum_{j=1}^{s-2} \mathsf{T}[j][8] \cdot \mathsf{T}[s-1-j][8], \ \mathsf{T}[s][8] &= 2\,\mathsf{T}[s][op_{\text{unary}}] + 5\,\mathsf{T}[s][op_{\text{comm}}] + \mathsf{T}[s][op_{\text{sub}}] \end{aligned} $$ 在对交换算子（$\land, \lor, \oplus, +, \times$）计数时，显式约束左子树规模不超过右子树（$|L| \le |R|$），天然杜绝了镜像冗余。在GPU执行时，给定线程ID加上批次偏移量 $n$，解码函数 $\phi_s(n)$ 仅需查阅常量内存中极小的前缀累加和，通过除法与取模在 $O(s)$ 寄存器步骤内还原整棵逆波兰语法树，完全无需全局内存交互或跨线程通信。

2. 局部一致性编码：消减SIMT多线程分支分歧的高效对齐机制

在GPU的单指令多线程（SIMT）执行模型中，一个warp内的32个线程必须执行相同的机器指令；若线程间由于表达式语法结构各异而走向不同的条件分支，硬件将被迫串行化执行各分支路径，导致有效算力严重缩水。Simba在构造整数与表达式双射映射时引入了“局部一致性”设计原则：在规模为 $s$、左子树固定为 $j$ 的二元算子分块中，全局连续的线程ID $tid$ 将被解析为左子表达式 $\phi_j(\lfloor tid / \mathsf{T}[s-1-j][8] \rfloor)$ 和右子表达式 $\phi_{s-1-j}(tid \bmod \mathsf{T}[s-1-j][8])$。由于除数 $\mathsf{T}[s-1-j][8]$ 通常远大于warp大小32，同一个warp内的全部32个线程拥有完全一致的商，即强制绑定完全相同的左子树表达式。整个warp在解码并执行左子树栈操作时，控制流完全同步，毫无分支分歧；而在右子树部分，连续ID解码出的表达式拓扑结构高度重合，通常仅在最底层的变量叶子索引上存在偏移。这种让高维拓扑变化保持平缓、低维叶子变化主导相邻线程的排布方式，从底层硬件特性上保证了warp分支分歧降到极低。

3. 寄存器级栈解释与零开销即时验证：无同步开销的端到端匹配流

每个GPU线程在完成解码后，无需将表达式展开为堆内存中的AST对象，而是直接在线程私有寄存器中维护一个固定深度的微型算术栈。针对规范中的 $n=16$ 组32位输入向量，线程按序读取输入并原地执行64位位向量的模 $2^{32}$ 算术与位操作。由于规范在全线程间只读共享，输入数据可常驻纹理或常量缓存，内存命中率近乎100%。在验证过程中，一旦某个输入样例与期望输出 $y_i$ 不符，线程可以提前判定失败；只有当16个样例全部精确通过时，线程才调用原子操作 atomicCAS 抢占全局单输出槽，写入求解公式并置位完成标志。整套流水线将数据与控制全部限制在寄存器内部，消除了所有中间结果写回显存带来的总线争用。

实验关键数据¶

主实验¶

评估在配置双路Intel Xeon Platinum 8468 CPU与8张NVIDIA H100 SXM5（80GB）的服务器上进行。基准测试集包含覆盖规模 $s \in [5, 30]$、真实变量数 $k \in [2, 10]$ 的2340个困难MBA生成实例，统一在 $n=16$ 个随机32位测试例下进行精确合成（时间上限60秒）。对比基线包括引入GPU语言缓存的最新工作VFB（移植自Valizadeh等人CAV 2024成果）以及成熟的CPU SMT SyGuS求解器cvc5。

求解算法	求解规模覆盖范围	共同解决实例数	在重叠实例上的相对表现	超出基线能力的独占解决数
Simba (本文)	可解规模达 16	—	基准 (中位求解时间 0.67s)	634 (vs VFB) / 668 (vs cvc5)
VFB (GPU缓存法)	仅能求解规模 $\le 11$	615	Simba在90%实例上更快 (中位加速1.6×)	0 (超出规模11全军覆没)
cvc5 (CPU SMT)	仅能求解规模 $\le 11$	581	Simba在96%实例上在1秒内完成	0 (超出规模11全军覆没)

在规模1至11的区间内，Simba求解了几乎100%的实例；而在规模12至16的较深层搜索空间中，VFB与cvc5的求解率断崖式跌落至0%，Simba成为唯一具备实际求解能力的工具。

消融实验与显存扩展性分析¶

为揭示缓存机制在定量合成中的失效机理，以及局部一致编码对GPU利用率的真实贡献，作者分别进行了显存瓶颈测试与线程乱序消融（Simba-RTid：使用MurmurHash3常数对线程ID进行伪随机双射打乱 $\pi(i)=(i \cdot 2246822507) \bmod n_{\text{threads}}$）。

表1：VFB语言缓存随表达式规模的显存膨胀与去重效率（变量数 $k=5$）

表达式规模 $s$	候选MBA总数	VFB缓存条目数	VFB占用显存	缓存留存率 (%)	VFB累计耗时 (s)
2	15	15	< 1 MB	100.0%	1.2
4	875	166	< 1 MB	19.0%	3.4
6	60,715	6,874	< 1 MB	11.3%	5.5
8	5,062,975	504,522	32.3 MB	10.0%	7.4
10	438,822,815	32,523,385	2.1 GB	7.4%	9.3
11	4,472,457,185	OOM	OOM	OOM	OOM

表2：编码布局消融（局部一致性 vs 随机排列 SIMD 分歧影响）

求解器变体	局部线程关联方式	Warp 分支分歧情况	相对求解速度	解决实例覆盖率
Simba (完整模型)	连续整数双射（共享左子树）	极低（控制流高度对齐）	4.0× (中位加速比)	全集覆盖 (达规模 16)
Simba-RTid	伪随机置换（MurmurHash3）	极高（同Warp内子树结构完全混乱）	1.0× (基线)	覆盖相同实例，但耗时增加4倍

关键发现¶

去重收益递减与显存爆炸是缓存法的致命死穴：当规模达到10时，VFB仅缓存了7.4%的候选式，却已吞噬2.1 GB显存；到规模11时候选暴增至44亿，VFB立即因显存耗尽崩溃（OOM）。相反，Simba显存开销恒定（仅受寄存器和KB级常量内存约束），从而平滑突破规模11的死线。
分支分歧对SIMT硬件吞吐具有毁灭性打击：消融实验证明，在没有改动任何搜索空间和算子逻辑的前提下，仅仅破坏线程ID与子树结构的局部一致性，就会导致程序运行速度直接暴跌至原本的四分之一（$4\times$ 减速）。
跨平台鲁棒性与确定性表现极高：在A100与H100上的5次重复实验表明，Simba的标准差极小（曲线置信区间几乎不可见），算法在不同架构GPU上表现高度稳定。

亮点与洞察¶

反直觉的算法权衡：程序分析界长期将“观测等价去重”视作底层枚举的金科玉律，但本文有力证明，在定量位向量领域，重新计算的算力开销远远低于在海量显存中维护与查找哈希表的开销，无缓存即时解法在吞吐上完胜缓存去重。
数论置换消融的精巧设计：作者利用乘法逆元与MurmurHash3素数常数构造了严格保全单射/满射的随机ID排列，在严格保证不漏算一个表达式的前提下，纯粹隔离了SIMD分支分歧的系统性损耗。
通用定量合成范式的可迁移性：该无缓存即时解码架构并不局限于MBA混淆，在浮点表达式反演、紧凑指令重构、量化电路逻辑拟合等任意具有超大输出值域空间的程序合成领域具有极强的复用价值。

局限与展望¶

作者承认的局限：方法强依赖GPU的大规模并发硬件体系，在纯CPU上无加速优势；搜索空间随规模超指数增长的内在复杂性依然存在，使得当前极限深度仍停留在规模16附近；目前不支持含有任意数值常数的MBA合成，且无法容忍带噪声的输入输出规范。
深层局限：纯黑盒输入输出驱动缺乏对目标算子代数特性的主动导引，在面对包含复杂多项式乘法或深度嵌套混淆时，依然会受到组合爆炸的强力压制。
改进方向：可考虑将符号代数化简器（如GAMBA的线性分量分解）作为前处理，将超大表达式剥离为若干规模较小的独立子表达式，再交由Simba并发合成，实现代数与穷举的协同扩充。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 颠覆了GPU合成必用语言缓存的思维定势，提出了基于计数表双射与局部一致性的全新无缓存合成范式。
实验充分度: ⭐⭐⭐⭐⭐ 构造了2340个大规模挑战实例，涵盖多硬件平台、详细的显存扩展分析以及隔离度极高的硬件分支消融。
写作质量: ⭐⭐⭐⭐⭐ 数学建模与递推形式严谨清晰，系统架构与GPU微架构适配机理解释深入透彻。
价值: ⭐⭐⭐⭐⭐ 为软件安全逆向反混淆、超优化编译器提供了极具实用价值的利器，并拓宽了GPU在定量程序合成中的应用边界。