SMT求解新突破！GradSAT用梯度归一化打破瓶颈，加速浮点约束求解
Accelerating Floating-Point Satisfiability Solving via Gradient Normalization
📖 AI 总结
本文针对无数量词浮点理论（QF_FP）的可满足性模理论（SMT）求解问题，提出了一种名为GradSAT的新框架。现有基于优化的SMT求解器虽已将梯度下降应用于逻辑公式的连续松弛，但普遍受困于"梯度支配"现象：少数困难子句会劫持优化轨迹，导致求解器陷入局部极小值，无法满足整体公式。GradSAT的核心思路是将每个SMT子句视为多任务学习中的独立任务，通过动态梯度归一化（GradNorm）在运行时主动平衡各子句的梯度幅度，抑制主导梯度、加速滞后子句，从而实现均匀收敛。在实现上，GradSAT采用两阶段混合流水线：第一阶段利用GPU加速的PyTorch后端，结合符号编译与算子融合，将连续松弛导航至高质量解域；第二阶段将候选赋值交由位精确局部搜索引擎，快速求解出严格精确的赋值。该工作通过稳定连续搜索动力学，缓解了以往梯度类求解器的脆弱性，为复杂约束求解提供了鲁棒且高度可并行化的架构，对软件验证、程序分析和编译器测试等领域具有实用意义。
🔑 关键词速览
| SMT | 可满足性模理论，一种用于检查逻辑公式在特定理论下可满足性的形式化验证技术。 |
| QF_FP | 无量词浮点理论，SMT 中处理浮点运算且不含量词的理论片段。 |
| 梯度支配 | 优化过程中少数困难子句的梯度主导整体梯度方向，导致求解器陷入局部最优的现象。 |
| GradNorm | 动态梯度归一化，一种多任务学习中平衡不同任务梯度幅度的方法。 |
| GradSAT | 本文提出的框架，将基于优化的 SMT 求解与多任务学习结合，通过梯度归一化加速浮点可满足性求解。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅