Lemmanaid：面向神经符号化的引理猜想生成
人工智能
2026-01-13 v5 计算机科学中的逻辑
摘要
数学家和计算机科学家正越来越多地使用形式化证明助手来形式化和验证复杂证明的正确性。这本身是一个不 trivial 的任务，还对人类专业知识提出了高要求。我们能否通过自动化猜想有帮助、有趣且新颖的引理来降低门槛？本文提出了首个神经符号化引理猜想工具——LEMMANAID，旨在通过在数学理论之间进行类比来发现猜想。LEMMANAID使用微调后的大语言模型（LLM）生成引理模板以描述引理的结构，符号方法用于填充细节。我们将LEMMANAID与同一LLM微调后生成完整引理语句的纯神经方法，以及完全符号化的猜想方法进行比较。实验表明，LEMMANAID在Isabelle的HOL库及其形式化证明档案（AFP）中的测试集上 consistently 优于神经和符号方法。使用DeepSeek-coder-6.7B作为后端，LEMMANAID发现了HOL和AFP中金标准参考引理的50%和28%，分别比对应的纯神经方法高出8-13%。采用不同的提示策略组合两个LEMMANAID版本后，性能提升至55%和34%。在Octonions形式化的案例研究中，LEMMANAID发现了79%的金标准引理，远超神经方法的62%和领先符号工具的23%。我们的研究表明，LEMMANAID能够在涵盖数学和计算机科学中复杂概念的广泛领域内，发现大量有意义的引理，超越标准基准（如miniF2F、PutnamBench和ProofNet）中基本概念的探索。
引用
@article{arxiv.2504.04942,
title = {Lemmanaid: Neuro-Symbolic Lemma Conjecturing},
author = {Yousef Alhessi and Sólrún Halla Einarsdóttir and George Granberry and Emily First and Moa Johansson and Sorin Lerner and Nicholas Smallbone},
journal= {arXiv preprint arXiv:2504.04942},
year = {2026}
}