Technische Samenvatting: ProofWala

Probleemstelling

Geautomatiseerd bewijsbewijs via neurale methoden vereist een robuuste infrastructuur om te interageren met Interactieve Stellingbewijzers (ITP's), gestructureerde bewijsgegevens te extraheren en bewijszoeking op schaal uit te voeren. Bestaande tooling is vaak gefragmenteerd, assistent-specifiek en gericht op interactieve, bestand-niveau uitvoering via REPL-interfaces (Read-Eval-Print Loop). Deze architectuur brengt significante beperkingen met zich mee:

• Schaalbaarheid: Het belemmert analyse op repository-schaal en parallel experimenteren.
• Data-extractie: Het biedt beperkte toegang tot declaratie-niveau metadata (bijv. inductieve definities, constanten, namespaces) en maakt het constructeren van repository-brede afhankelijkheidsgrafieken moeilijk of zelfs onmogelijk.
• Cross-Assistent Gaten: Het gebrek aan verenigde tooling maakt het uitdagend om potentiële cross-linguale en cross-domein winsten te exploiteren door te trainen op meertalige formele corpora (bijv. Lean en Rocq).

Methodologie

De auteurs presenteren ProofWala, een meertalig proof engineering framework ontworpen om interactie, data-extractie, training en zoekopdrachten te verenigen over verschillende ITP's. Het framework is gebouwd rond drie kerncomponenten:

1. De Interface Module (itp-interface)

Dit is een herbruikbare bibliotheek voor programmatische interactie met ITP's, die een verenigde abstractie biedt voor Lean 4 en Rocq (meerdere versies).

• Lean 4 Backend: In plaats van te vertrouwen op een REPL-gebaseerde architectuur, hebben de auteurs meta-programma's geïmplementeerd die direct binnen de Lean-elaborator worden uitgevoerd. Dit maakt mogelijk:
  • Semantisch getrouwe tactic-level tracing.
  • Extractie van declaratie-niveau metadata en de constructie van repository-brede afhankelijkheidsgrafieken.
  • Verbeterde afhandeling van geneste tactic-constructen (bijv. have-blokken).
  • Environment Cloning: De mogelijkheid om bewijsomgevingen te klonen voor parallelle uitvoering, wat moeilijk is met standaard REPL-workflows.
  • Versie-robuustheid: Een dunne compatibiliteitslaag zorgt voor voorwaartse compatibiliteit over Lean 4-versies vanaf 4.15.0.
• Rocq Backend: Gebouwd op coq_serapy, waarbij het is uitgebreid om systematische extractie van bewijsstaten en tactic-traces te ondersteunen, waarbij deze worden gemapt naar hetzelfde verenigde formaat dat voor Lean wordt gebruikt.
• Verenigd State Model: Beide assistenten worden gemapt naar een gestandaardiseerd state-transition systeem waarbij een bewijsstaat een verzameling verplichtingen (doelen en hypothesen) is, en tactics deze staten transformeren.

2. Data en Model Module

• Data-extractie: Het framework extraheert bewijsstaat–tactic paren uit belangrijke repositories (CompCert, MathComp, GeoCoq, Mathlib, CategoryTheory) door tactic-scripts binnen de assistent-kernel af te spelen.
• Verenigd Formaat: Geëxtraheerde data wordt opgeslagen in een verenigd JSON-formaat dat abstraheert over assistent-specifieke details terwijl semantische informatie behouden blijft. Het prompt-formaat voor training is identiek voor zowel Lean als Rocq, waarbij assistent-specifieke tokens worden weggelaten om cross-assistent training te faciliteren.
• Training: De auteurs hebben een CodeT5-Base model (220M parameters) gefinetuned op drie configuraties:
  1. ProofWala-Rocq: Getraind op Rocq-repositories.
  2. ProofWala-Lean: Getraind op Lean-repositories.
  3. ProofWala-Multilingual: Gezamenlijk getraind op beide assistenten.

3. Parallel Bewijszoekingsmodule

• Environment Pooling: Een belangrijke innovatie is de environment pool, die meerdere geklonde bewijsomgevingen bijhoudt die geïnitialiseerd zijn tot identieke frontier-staten.
• Parallelle Executie: Kandidaat-tactics worden gelijktijdig uitgevoerd over deze geklonde instanties. Deze pool integreert met Ray voor gedistribueerde uitvoering, wat schaalbare bewijszoeking en grootschalige annotatie mogelijk maakt.
• Zoekalgoritmen: De module ondersteunt geparallelliseerde best-first en beam search. Het houdt een geannoteerde bewijstree bij die alleen geldige, compileerbare staatsovergangen registreert, wat fijnmazige analyse van de zoekdynamiek mogelijk maakt.

Belangrijkste Bijdragen

1. Gestandaardiseerd Framework en Engineering Library: ProofWala biedt een verenigd framework voor het extraheren en organiseren van tactic-niveau data en het ondersteunen van toolontwikkeling. Het introduceert een meta-geprogrammeerde instrumentatie-pipeline voor Lean die dependency-bewuste repository-traversal en environment cloning ondersteunt, capaciteiten die voorheen moeilijk te bereiken waren via REPL.
2. Ondersteuning voor Parallelle Bewijsvoltooiing: Het framework is het eerste open-source systeem dat parallel bewijs zoeken biedt door expliciet geklonde bewijsomgevingen en gelijktijdige tactic-evaluatie te ondersteunen binnen een verenigde multi-ITP interface.
3. Meertalige Datasets en Modellen: De auteurs brengen een meertalige dataset vrij (~450K datapunten, 270M tokens) en getrainde modellen (Lean, Rocq, en Multilingual) die end-to-end bewijszoeking faciliteren.

Resultaten

De auteurs hebben de modellen geëvalueerd op testsplits van CompCert, MathComp, GeoCoq, CategoryTheory, en Lean/Mathlib, evenals op de MiniF2F benchmark.

• Cross-Linguale Transfer: Het ProofWala-Multilingual model komt over het algemeen overeen met of verbetert het monolinguale baselines.
  • Statistisch Significante Verbeteringen: Waargenomen op de grootste benchmark (Lean/Mathlib) en in de CategoryTheory domeinadaptatie-setting (waar het meertalige model werd gefinetuned op CategoryTheory data).
  • Trends: Andere datasets vertoonden consistente maar niet statistisch significante trends die gunstig waren voor meertalige training.
• Domeinadaptatie: In het CategoryTheory domein behaalde het meertalige model aanzienlijk hogere pass-at-k scores na finetuning vergeleken met de Rocq-only baseline, wat suggereert dat pretraining op gemengde-taal data helpt bij adaptatie, zelfs wanneer het doel-domein slechts in één assistent wordt gerepresenteerd.
• Zoekdynamiek: Analyse van bewijsbomen onthulde dat meertalige modellen vaak grotere bomen produceren met hogere branching factors, wat aangeeft dat ze een groter aantal geldige tactics per staat voorstellen.
• Schaalbaarheid: Parallelle executie via environment pools verbeterde de throughput aanzienlijk. Het verhogen van het aantal CPU-workers van 8 naar 20 verbeterde de pass@5 op MiniF2F van 22.54% naar 26.23%, terwijl de gemiddelde bewijstijd werd verkort.

Betekenis en Claims

De paper claimt dat ProofWala een verschuiving vertegenwoordigt van gefragmenteerde, assistent-specifieke tooling naar een verenigde, schaalbare infrastructuur voor neurale stellingbewijzing.

• Architecturale Unificatie: Door uitvoering, dataverzameling, afhankelijkheidsanalyse en zoekopdrachten te verenigen, maakt het framework systematische, reproduceerbare en fijnmazige analyse van neurale bewijszoeking over meerdere ITP's mogelijk.
• Bewijs van Transfer: Het werk levert empirisch bewijs dat meertalige training positieve cross-linguale en cross-domein transfer oplevert in formeel redeneren, met name in high-data regimes en domeinadaptatie scenario's.
• Onderzoeksfundament: De auteurs positioneren ProofWala niet enkel als een bewijszoekingssysteem, maar als een onderzoeksframework dat bewijszoeking transformeert van een "black-box" evaluatie naar een analyseerbare pipeline. Dit stelt onderzoekers in staat om structurele transfer, boomgrootte, branching factors en executie-latentie te bestuderen op manieren die voorheen moeilijk te verkrijgen waren.

De auteurs merken op dat hoewel grotere modellen en aanvullende infrastructuur (bijv. retrieval, verifiers) waarschijnlijk nodig zijn voor state-of-the-art prestaties op benchmarks, hun primaire bijdrage het framework zelf is, dat de effecten van meertalige training en parallelle zoekstrategieën isoleert. Zij beschouwen de uitbreiding naar document-georiënteerde assistenten (zoals Isabelle) als een engineering uitdaging in plaats van een conceptuele beperking, en laten dit over aan toekomstig werk.