arXiv:2502.13834v1 通知类型: 新 摘要: 大型语言模型（LLMs）可以通过在一个证明系统内生成证明步骤（即，策略）来正式证明数学定理。然而，可能的策略空间庞大而复杂，而可用于形式证明的训练数据有限，这为基于LLM的策略生成带来了重大挑战。为了解决这一问题，我们提出了一种神经符号策略生成器，将LLM学习到的数学直觉与符号方法编码的领域特定见解相结合。这种整合的关键方面在于识别哪些部分的数学推理最适合LLM，哪些最适合符号方法。尽管神经符号整合的基本理念适用于各种数学问题，但在本文中，我们专门关注奥林匹克不等式（图1）。我们分析了人类是如何解决这些问题的，并将这些技术提炼为两种类型的策略：（1）缩放，由符号方法处理；（2）重写，由LLM处理。此外，我们将符号工具与LLM结合使用，以修剪和排名证明目标，从而提高高效的证明搜索效率。我们在来自多个数学竞赛的161个具有挑战性的不等式上评估了我们的框架，实现了最先进的性能，并明显优于现有的基于LLM和符号的方法，而无需额外的训练数据。