摘要
形式化验证虽能确保关键系统正确性，但构建大型证明脚本仍高度依赖人工。本文提出一种神经符号证明生成框架，通过最佳优先树搜索自动探索证明状态，并利用大语言模型（LLM）预测下一步证明策略。该方法结合神经网络微调与符号工具（如自动子目标消解、状态剪枝），在 seL4 基准测试中证明了 77.6% 的定理，显著超越现有 LLM 方法及独立 Sledgehammer 工具，展现了可扩展自动化软件验证的可行路径。
AI 推荐理由
论文核心利用 LLM 数学推理能力进行神经符号证明搜索，解决多步逻辑推导问题。
研究机构
南京大学 novel software technology state key laboratory, 中国
南京大学计算机科学学院, 中国
南京大学novel software technology state key laboratory, 中国
苏黎世联邦理工学院计算机科学系, 瑞士
伦敦大学学院计算机科学系, 英国
论文信息