基于 G"odel 逻辑的梯度优化：离散局部搜索

神经符号系统面临的根本挑战之一是将连续梯度优化应用于离散逻辑领域。虽然模糊松弛提供了可微性，但常常缺乏与经典逻辑的正式结构对齐。在本工作中，我们展示了 G"odel 语义通过一种将其连续解释映射到布尔值的同态映射解决了这一限制，使得在保持完全可微性的同时对离散变量进行编码。基于这一基础，我们进一步表明，针对 G"odel 逻辑的梯度优化在布尔满意性问题中实例化为离散局部搜索。我们的形式化分析证明，每一步优化都识别并修改一个不满足的子句中的单个变量，从而精确地模拟了离散求解器的步骤。我们识别局部最优点是此类动态的主要限制，并引入 G"odel 诀窍，这是一种旨在改善解空间探索的随机重参数化技术。我们进一步展示了该方法与概率推理以及 Gumbel-Max 诀窍之间存在形式化联系。在 SAT 基准测试和 Visual Sudoku 任务上的实验结果验证了我们的理论发现，表明该方法有效地导航了复杂的组合景观，为可微分离散搜索提供了坚实的基础。