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

作     者：万亮亮 刘艳娇 龙海建 王昌晶 WAN Liangliang;LIU Yanjiao;LONG Haijian;WANG Changjing

作者机构：江西师范大学计算机信息工程学院江西南昌330022 

出 版 物：《江西师范大学学报(自然科学版)》 (Journal of Jiangxi Normal University(Natural Science Edition))

年 卷 期：2024年第48卷第5期

页      面：459-463页

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

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

摘      要：该文利用大语言模型(large language models,LLMs)与形式化验证技术实现线性数据结构定理的自动证明,并提出通过引入引理来提高线性数据结构定理证明效率的方法.首先,利用LLMs生成定理的非形式化证明及形式化证明草图;然后,基于非形式化证明构造相关引理进行形式化验证以确保引理的正确性;最后,通过引入引理,辅助定理形式化验证,降低现有自动定理证明工具在处理形式化证明草图时的难度,提高自动证明效率.实验结果显示线性数据结构定理的证明成功率从54.55%提升至68.18%,这充分表明引理在定理证明过程中发挥了关键作用.