基于大语言模型的交互式定理证明系统及方法

本发明公开了一种基于大语言模型的交互式定理证明系统及方法，所述系统包括：策略建议模块，用于基于LLM分析待证明目标的若干候选策略；证明搜索模块，用于在待证明目标为需要多步策略组合证明的复杂定理时，基于规则库和若干候选策略进行深度推理，确定完整证明路径；前提选择模块，用于在待证明目标的证明过程需要引用前提时，基于相似度计算确定待证明目标对应的前提序列，基于用户在前提序列中所选的前提进行定理证明；本发明能够利用大语言模型动态生成推理策略，智能引导复杂定理的证明过程，显著减少人工干预，提升自动化水平；根据定理目标上下文动态调整推理路径，灵活应对数学特殊情况及跨领域证明任务，提高证明成功率和效率。