【AAAI2025教程】面向解算器的机器学习，

机器学习与求解器

机器学习（ML）和逻辑推理自人工智能（AI）诞生以来一直是其两个基础支柱，但只有在过去十年里，这两个领域之间的互动才变得日益突出。特别是，机器学习对SAT和SMT求解器产生了巨大影响，正如获奖的SATzilla、MapleSAT和Z3alpha求解器所示。本教程旨在通过弥合机器学习和逻辑推理研究社区之间的鸿沟，激发新的跨学科研究。我们将向更广泛的AI社区介绍已经应用于逻辑推理求解器中的机器学习技术，重点介绍那些成功且有前景的方法。我们还将举办一个小组讨论，探讨大型语言模型（LLMs）如何在未来塑造这一领域。 与纯粹的端到端学习不同，成功的机器学习方法往往与符号求解器紧密集成。我们教程的核心论点是，机器学习最有效的应用场景是用来对求解器实现的证明/重写规则进行排序、选择、初始化和配置，这一点得到了许多成功案例的支持。我们将重点介绍一个典型例子，即使用机器学习来学习分支启发式方法，既可以通过强化学习（RL）在线地为特定实例进行训练，也可以通过离线训练神经网络策略来处理来自特定应用的代表性实例。 本教程假设参与者具有基本的机器学习知识，并从逻辑求解器的基本背景知识开始。我们将探索主要的机器学习求解范式——算法选择、算法配置和启发式方法的强化学习，重点介绍每个领域中的成功应用。我们还将讨论为什么图神经网络（GNNs）是用神经网络建模逻辑公式的合适架构。教程部分最后，我们将通过实践编码演示，展示如何为特定应用配置参数化求解器，使用SMAC微调MapleSAT中的在线学习参数。鼓励参与者带上自己的求解器和应用程序，测试这种方法是否对他们的工作有效。 最后，我们将与领域内的专家进行小组讨论，探讨大型语言模型对逻辑推理的影响，这是AI社区中意见往往非常分歧的一个话题。小组将探讨大型语言模型在推理任务中的有效性，并反过来讨论如何将形式化的逻辑推理融入到大型语言模型中，从而增强其可信度。