协同大语言模型与符号推理证明奥林匹克不等式

大语言模型（LLMs）可以通过在证明系统中生成证明步骤（\textit{即}策略）来形式化地证明数学定理。然而，可能策略的空间庞大且复杂，而形式证明的可用训练数据有限，这对基于 LLM 的策略生成构成了重大挑战。为解决此问题，我们引入了一种神经符号策略生成器，将 LLM 学习到的数学直觉与符号方法编码的特定领域见解相协同。这种整合的关键在于识别数学推理的哪些部分最适合 LLM，哪些部分最适合符号方法。尽管神经符号整合的高层思想广泛适用于各类数学问题，但在本文中，我们专门聚焦于奥林匹克不等式（图 1）。我们分析了人类如何解决这些问题，并将这些技巧提炼为两类策略：(1) 缩放，由符号方法处理；(2) 重写，由 LLM 处理。此外，我们将符号工具与 LLM 相结合，以修剪和排序证明目标，从而实现高效的证明搜索。我们在来自多项数学竞赛的 161 道具有挑战性的不等式上评估了我们的框架，实现了 SOTA 性能，并在无需额外训练数据的情况下显著优于现有的 LLM 和符号方法。