软件学报:jos:7656 · 记录 #1

引理库驱动的线性数据结构算法定理自动证明

来源日期 2026-07-08

来源记录日期 2026-07-08

雷达观测 2026-11-05 00:19

摘要

尽管大语言模型(large language model, LLM)为算法定理自动证明领域提供了一条新的探索路径, 但现有方法未能充分提升自动定理证明器在证明中间命题时的能力. 当前在线性数据结构算法形式化定理证明方面所需的标签数据非常稀少, 将大语言模型用于预测时, 尤其具有挑战性. 为弥补这一不足, 构建一种新的面向线性数据结构算法的引理库驱动证明方法LDPM, 融合了大语言模型与形式化技术. 该方法通过构建一个由已被证明的新引理组成的引理库, 通过从引理库中调取相关引理, 可有效强化自动定理证明器对中间命题的证明效能. 引理库的构建遵循三阶段递进式策略: 首先通过联合请求机制生成多个候选引理陈述, 以丰富库内资源; 接着借助迭代证明策略逐个证明候选引理, 逐步提升引理库的可靠性; 最终引入引理反思机制, 借助LLM对引理进行修正与优化, 从而实现引理库的动态扩展与持续完善. 通过这一方法, 线性数据结构算法定理证明的性能得以显著提升, 与最先进的方法比较, 证明成功率从44.00%提高到82.00%. 消融实验进一步表明, 引理库在提升自动定理证明器证明中间命题的能力上发挥了关键作用, 使线性数据结构算法定理证明的成功率提高了38.00%.