paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Automatic Proof Generation: Fine-tuning and RAG in Reasoner vs. Math LLMs

自动证明生成：Reasoner 与 Math LLM 中的微调与 RAG 对比
FSE Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering2025匹配度 6/10 · 该论文属于 AI→PL 中用 LLM 改进形式化验证/定理证明的方向，与用户关注的 LLM 与形式化验证交叉点相关；但核心是比较数学 LLM、推理 LLM 及混合模型在 Isabelle/HOL 上的微调/RAG 配置，未涉及静态分析、Agentic 程序、浮点程序分析或贝叶斯程序分析，方法层面也偏模型比较而非问题驱动的新分析技术。引用 0 inbox
Juan Carlos Recio Abad, Rubén Saborido, Francisco Chicano
定理证明与证明工程机器学习与程序语言
crossref: 2026-09-12

AI 速览

一句话：在 Isabelle/HOL 上比较数学 LLM、推理 LLM 及混合模型在基座、微调与 RAG 三种配置下的证明推断能力。

软件形式验证依赖 Isabelle/HOL 等证明助手来形式化并验证数学定理，但证明构造通常需要人类专家。本文研究大语言模型用于 Isabelle/HOL 证明推断的有效性，系统比较数学 LLM、推理型 LLM 以及混合数学-推理 LLM，并在三种配置下评估：未经领域特定训练的基座模型、面向形式证明领域微调的变体，以及基于检索增强生成（RAG）的系统。该比较不仅具有理论意义，也有望指导利用各类方法互补优势的混合系统开发，从而推动形式验证中自动证明生成的研究。

问题
使用 Isabelle/HOL 进行形式验证时，定理证明过程往往依赖人类专家，能否用大语言模型自动推断证明、以及不同类型 LLM 与训练配置的效果差异尚不明确。
方法
比较数学 LLM、推理型 LLM 与混合数学-推理 LLM 在 Isabelle/HOL 证明推断中的表现，并覆盖基座模型、领域微调变体与基于 RAG 的系统三种配置。
评估
在 Isabelle/HOL 证明推断任务上评估各模型与配置的能力，分析不同类型模型及训练/检索增强策略的互补优势。
原文摘要（Abstract）

Software formal verification is an important and challenging tool to ensure software correctness. It requires tools to formulate and verify mathematical theorems. One example of such a tool is Isabelle/HOL, a proof assistant that supports higher-order logic (HOL), enabling rigorous mathematical reasoning that could be useful for formal verification in software and hardware systems. However, the use of these tools requires a human expert on theorem proving in many cases. With the advent of LLMs (Large Language Models) a research line emerged to use them for proof inference. This paper investigates the effectiveness of math LLMs, reasoner LLMs, and hybrid math-reasoner LLMs in Isabelle/HOL proof inference, evaluating their capabilities across three configurations: base models without domain-specific training, fine-tuned variants adapted to the formal proof domain, and systems based on Retrieval Augmented Generation (RAG). The significance of this comparison extends beyond theoretical interest, potentially informing the development of hybrid systems that leverage the complementary strengths of all approaches.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot9169,
  title = {Automatic Proof Generation: Fine-tuning and RAG in Reasoner vs. Math LLMs},
  author = {Juan Carlos Recio Abad and Rubén Saborido and Francisco Chicano},
  booktitle = {FSE},
  year = {2025},
  doi = {10.1145/3696630.3728705}
}