| 摘要: |
| 尽管大语言模型(large language model, LLM)为算法定理自动证明领域提供了一条新的探索路径, 但现有方法未能充分提升自动定理证明器在证明中间命题时的能力. 当前在线性数据结构算法形式化定理证明方面所需的标签数据非常稀少, 将大语言模型用于预测时, 尤其具有挑战性. 为弥补这一不足, 构建一种新的面向线性数据结构算法的引理库驱动证明方法LDPM, 融合了大语言模型与形式化技术. 该方法通过构建一个由已被证明的新引理组成的引理库, 通过从引理库中调取相关引理, 可有效强化自动定理证明器对中间命题的证明效能. 引理库的构建遵循三阶段递进式策略: 首先通过联合请求机制生成多个候选引理陈述, 以丰富库内资源; 接着借助迭代证明策略逐个证明候选引理, 逐步提升引理库的可靠性; 最终引入引理反思机制, 借助LLM对引理进行修正与优化, 从而实现引理库的动态扩展与持续完善. 通过这一方法, 线性数据结构算法定理证明的性能得以显著提升, 与最先进的方法比较, 证明成功率从44.00%提高到82.00%. 消融实验进一步表明, 引理库在提升自动定理证明器证明中间命题的能力上发挥了关键作用, 使线性数据结构算法定理证明的成功率提高了38.00%. |
| 关键词: 大语言模型 形式化技术 定理证明 引理库 Isabelle/HOL |
| DOI：10.13328/j.cnki.jos.007656 |
| 分类号: |
| 基金项目:国家自然科学基金(62462037, 62462036); 江西省主要学科学术与技术带头人培养项目(20232BCJ22013); 江西省自然科学基金重点项目(20242BAB26017) |
|
| Lemma-library-driven Automated Theorem Proving for Linear Data Structure Algorithms |
|
WANG Chang-Jing, WAN Liang-Liang, LIU Yan-Jiao, LONG Hai-Jian, ZUO Zheng-Kang
|
|
School of Artificial Intelligence, Jiangxi Normal University, Nanchang 330022, China
|
| Abstract: |
| Although large language models (LLMs) provide a new exploration path in the field of automated algorithmic theorem proving, existing methods fail to sufficiently improve the capability of automated theorem provers in proving intermediate propositions. Currently, labeled data for formal theorem proving in linear data structure algorithms is very scarce, which presents significant challenges when large language models are used for prediction. To address this issue, this study proposes a novel lemma-library-driven proof method, LDPM, for automated theorem proving of linear data structure algorithms, which integrates large language models with formalization techniques. The method constructs a lemma library composed of newly proven lemmas. By retrieving relevant lemmas from this library, the capability of the automated theorem prover in proving intermediate propositions can be effectively enhanced. The construction of the lemma library follows a three-stage progressive strategy. First, a joint request mechanism is adopted to generate multiple candidate lemma statements, thus enriching the library resources. Second, an iterative proof strategy is employed to prove the candidate lemmas one by one, gradually improving the reliability of the lemma library. Finally, a lemma reflection mechanism is introduced, leveraging LLMs to revise and optimize lemmas, achieving the dynamic expansion and continuous refinement of the lemma library. Through this method, the performance of theorem proving for linear data structure algorithms is significantly improved. Compared with the state-of-the-art methods, the success rate of theorem proving is increased from 44.00% to 82.00%. Ablation experiments further show that the lemma library plays a key role in improving the capability of automated theorem provers in proving intermediate propositions, increasing the success rate of theorem proving for linear data structure algorithms by 38.00%. |
| Key words: large language model (LLM) formalization technique theorem proving lemma library Isabelle/HOL |
