Vibe Coding an LLM-powered Theorem Prover

Isabellm ist ein brandneuer, von großen Sprachmodellen unterstützter Theorem-Prover für Isabelle/HOL, der komplette Beweise automatisch erzeugt. Das System nutzt lokale LLMs über Ollama sowie APIs wie Gemini CLI und ist so optimiert, dass es auf handelsüblichen Computern läuft.

Die Funktionsweise kombiniert einen schrittweisen Beweiser, der mithilfe von LLMs Proof-Befehle vorschlägt und diese in einem begrenzten Suchraum von Isabelle validiert, mit einem höheren Planer, der strukturierte Isar-Gliederungen erstellt und fehlende Teile ergänzt. Zu den Kernkomponenten gehören Beam‑Search für Taktiken, ML‑ und RL‑basierte Taktik‑Ranglisten, Premise‑Auswahl mit kleinen Transformer‑Modellen, micro‑RAG für Isar‑Beweise aus der AFP-Bibliothek sowie ein counter‑example‑gesteuertes Reparaturverfahren.

In Experimenten konnte Isabellm Lemmas beweisen, die die Standard‑Automatisierung von Isabelle, etwa Sledgehammer, übertrifft. Gleichzeitig zeigen die Tests, dass selbst hochmoderne LLMs wie GPT‑5.2 Extended Thinking und Gemini 3 Pro Schwierigkeiten haben, die komplexen Fill‑and‑Repair‑Mechanismen zuverlässig umzusetzen – ein Hinweis auf grundlegende Grenzen in der Code‑Generierung und dem logischen Denken von LLMs.

Der komplette Code ist frei verfügbar unter https://github.com/zhehou/llm-isabelle und wurde mit GPT‑4.1 bis GPT‑5.2, Gemini 3 Pro und Claude 4.5 entwickelt.