Generierung von Korrektheitsbeweisen mit neuronalen Netzwerken

Die Fundamentaler Verifikation ermöglicht es Programmierern, Software zu entwickeln, die empirisch nachgewiesen hat, eine hohe Sicherheitsgarantie in einer Vielzahl wichtiger Bereiche zu bieten. Allerdings bleibt der Aufwand zur Erstellung fundiert verifizierter Software für die meisten Projekte weiterhin prohibitiv hoch, da er erhebliche manuelle Anstrengungen durch hochqualifizierte Experten erfordert. In diesem Paper stellen wir Proverbot9001 vor, ein Beweissuchsystem, das maschinelles Lernen nutzt, um Beweise für die Korrektheit von Software in interaktiven Theorembeweisern zu generieren. Wir demonstrieren Proverbot9001 anhand der Beweisverpflichtungen eines großen praktischen Verifikationsprojekts, des CompCert-Compiler, eines verifizierten C-Compilers, und zeigen, dass es effektiv bisher manuelle Beweise automatisieren kann: In Kombination mit solverbasierten Werkzeugen erzeugt es automatisch Beweise für 27,5 % der Theoremsätze in unserer Testdatenmenge. Ohne zusätzliche Solver erreicht unser Ansatz eine Beweisabgeschlossenheitsrate, die eine Vervierfachung gegenüber der vorherigen State-of-the-Art-Maschinenlernmethode zur Beweisgenerierung in Coq darstellt.