HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

Sicherheitsmeldung mit Schweregrad noch nicht bewertet. Technische Details im Tab „Originaltext“; empfohlene Schritte in der Checkliste.

Originaltext der Quelle (nicht übersetzt) – die deutsche Zusammenfassung findest du im Tab „Kurzfassung".

arXiv:2505.15740v2 Announce Type: replace-cross Abstract: Formal methods play a crucial role in ensuring the reliability of critical systems through rigorous mathematical verification. However, their adoption remains limited due to the labor-intensive nature of manual proof construction. Recent advances in large language models (LLMs) have opened new opportunities for automated theorem proving. Two main paradigms have emerged: stepwise tactic-based generation and whole-proof synthesis. While both approaches have complementary strengths, existing work largely treats them in isolation. In this work, we propose HybridProver, a unified framework that integrates whole-proof synthesis and tactic-based generation through proof sketches as an intermediate representation. This design enables the reuse of partially correct proof structures while effectively combining high-level planning with fine-grained reasoning. We implement HybridProver in Isabelle/HOL and post-train two 7B-scale LLMs on our optimized Isabelle datasets. Experiments on the miniF2F Isabelle benchmark achieved a 73.8% success rate and improved upon the previous state of the art (61.9%), demonstrating that lightweight models, when combined with our approach, can effectively generate Isabelle/HOL proofs without relying on very large LLMs. Ablation studies further analyze the impact of dataset quality, training configurations, and sampling strategies on proof generation.

Vollständiger Originalartikel ↗

• Betroffenheit im eigenen Stack prüfen: Versionen/Komponenten abgleichen.
• Originalquelle / Hersteller-Advisory lesen: https://arxiv.org/abs/2505.15740
• Verfügbaren Patch oder Workaround einspielen und dokumentieren.