基于大模型的引理辅助线性数据结构定理自动证明  

The Lemma-Assisted Automatic Proof of Linear Data Structure Theorems Based on Large Models

作　　者：万亮亮 刘艳娇 龙海建 王昌晶[1] WAN Liangliang;LIU Yanjiao;LONG Haijian;WANG Changjing(School of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022

出　　处：《江西师范大学学报(自然科学版)》2024年第5期459-463,共5页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(62462037);江西省主要学科学术与技术带头人培养课题(20232BCJ22013);江西省教育厅科学技术重点课题(GJJ2200302)资助项目.

摘　　要：该文利用大语言模型(large language models,LLMs)与形式化验证技术实现线性数据结构定理的自动证明,并提出通过引入引理来提高线性数据结构定理证明效率的方法.首先,利用LLMs生成定理的非形式化证明及形式化证明草图;然后,基于非形式化证明构造相关引理进行形式化验证以确保引理的正确性;最后,通过引入引理,辅助定理形式化验证,降低现有自动定理证明工具在处理形式化证明草图时的难度,提高自动证明效率.实验结果显示线性数据结构定理的证明成功率从54.55%提升至68.18%,这充分表明引理在定理证明过程中发挥了关键作用.In the paper,the use of large language models(LLMs)with formal verification techniques is explored to achieve automatic proof of linear data structure theorems,and the method is proposed to improve the efficiency of proving linear data structure theorems by introducing lemmas.Firstly,LLMs generate the informal proofs and formal proof sketches of the theorems.Then,relevant lemmas are constructed based on the informal proofs,and formal verification is performed to ensure the correctness of the lemmas.Finally,by introducing the lemmas to assist the formal verification of the theorems,the difficulty of existing automatic theorem proving tools in handling formal proof sketches is reduced and the efficiency of the automatic proofs is improved.The experimental results show that the success rate of proving the linear data structure theorem is improved from 54.55%to 68.18%,which fully demonstrates that lemma plays a key role in the theorem proving process.

关 键 词：大语言模型 提示工程 自动定理证明 Isabelle/HOL 形式化验证 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]