Neural Theorem Proving: Neuer Benchmark für Verifikation von Programmen

Die automatisierte Beweisführung von Verifikationsbedingungen (VCs) ist ein zentraler Bestandteil der Programmanalyse, doch bleibt sie einer der größten Engpässe in der Praxis. Oft stoßen bestehende automatisierte Theoremprover (ATPs) an ihre Grenzen, sodass Entwickler auf aufwändige manuelle Beweise zurückgreifen müssen.

Neural Theorem Proving (NTP) hat in mathematischen Wettbewerben beeindruckende Erfolge erzielt und zeigt, dass maschinelles Lernen formale Argumentation unterstützen kann. Bislang wurde NTP jedoch kaum auf die Beweisführung von VCs angewendet, und es fehlt ein speziell dafür entwickelter Testdatensatz.

Mit NTP4VC wird das erste real‑welt‑basierte Benchmark‑Set für die automatisierte Beweisführung von VCs vorgestellt. Es basiert auf echten Projekten wie dem Linux‑ und dem Contiki‑OS‑Kernel und nutzt industrielle Pipelines (Why3 und Frama‑C), um semantisch äquivalente Testfälle in den formalen Sprachen Isabelle, Lean und Rocq zu erzeugen.

Die Autoren haben große Sprachmodelle – sowohl generische als auch für Theoremproving feinabgestimmte Varianten – auf NTP4VC getestet. Die Ergebnisse zeigen, dass LLMs vielversprechende Fortschritte erzielen, gleichzeitig aber noch erhebliche Herausforderungen bestehen. Der Benchmark verdeutlicht damit einen großen Forschungsspielraum für die Weiterentwicklung von NTP in der Programmanalyse.