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

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.