公开(公告)号：CN118709756A

公开(公告)日：2024-09-27

申请号：CN202410836124.7

申请日：2024-06-26

Applicant: 中国人民解放军军事科学院系统工程研究院

Inventor： 张龙 ,  郑兴建 ,  樊瑜

IPC: G06N5/01 ,  G06N3/0499 ,  G06N3/08 ,  G06N5/04 ,  G06F40/242 ,  G06F40/126 ,  G06F40/284

Abstract: 本发明公开了一种基于大模型的形式化定理证明生成方法及系统，属于人工智能技术领域。本方法获取第一训练数据，第一训练数据为包括形式化定理命题、证明该形式化定理命题的全部证明步骤的文本数据；获取第二训练数据，第二训练数据为包括数学领域知识的数据；基于第二训练数据对大模型进行预训练，得到预训练完毕的大模型；基于第一训练数据对预训练完毕的大模型进行参数调整，得到调整后的大模型；将待生成定理证明步骤的形式化定理命题作为输入数据输入所述调整后的大模型，生成所述待生成定理证明步骤的形式化定理的证明步骤；本方法可以大大降低自动生成定理证明的复杂度，还可以显著提高模型推理期间的硬件利用率。