arXiv:2504.04942v1 公告类型: 新 摘要: 自动猜想有用的、有趣的和新颖的引理将极大地改进自动推理工具，并降低在证明助手中形式化数学的门槛。然而，这对神经和符号方法来说都是一个非常具有挑战性的任务。我们提出了第一个实用的神经-符号引理猜想工具Lemmanaid，该工具结合了大型语言模型（LLMs）和符号方法，并将其在Isabelle证明助手的证明库上进行了评估。我们训练一个LLM生成描述引理形状的模板，并使用符号方法填充细节。我们将Lemmanaid与一个旨在生成完整引理陈述的LLM以及以前的全符号猜想方法进行了比较。我们的结果表明，神经技术和符号技术是互补的。通过利用符号和神经方法的最好部分，我们可以为广泛的输入领域生成有用的引理，从而促进计算机辅助的理论开发和形式化。