💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

Dit artikel introduceert ITPEval, de eerste benchmark en verenigde infrastructuur voor het evalueren van geautomatiseerde formele bewijsvertaling over vier belangrijke interactieve bewijsvoerders, waarbij wordt onthuld dat huidige grote taalmodellen aanzienlijk moeite hebben met bewijsvertaling vanwege mismatches in bibliotheken en dat native type-checking alleen vaak de semantische getrouwheid overschat.

Oorspronkelijke auteurs: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Gepubliceerd 2026-07-23

📖 3 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je een wereld voor waarin wiskundigen vier verschillende talen spreken, maar ze proberen allemaal exact dezelfde puzzels op te lossen. In de hooggespannen arena van "formeel bewijzen" fungeren computers als de ultieme scheidsrechters, die elke individuele stap van een wiskundig bewijs controleren om te garanderen dat het 100% correct is. Echter, net zoals mensen die Frans, Japans, Swahili en Arabisch spreken, hebben deze computersystemen (genaamd Interactive Theorem Provers, of ITP's) hun eigen unieke grammatica, vocabulaire en bibliotheken met vooraf goedgekeurde feiten. Een bewijs dat perfect is geschreven in het ene systeem, is vaak onbegrijpelijk voor de anderen. Dit creëert een eenzaam probleem: als een briljant bewijs in één taal is geschreven, kan het niet gemakkelijk door de anderen worden gebruikt of gecontroleerd. Wetenschappers proberen "universele vertalers" te bouwen om deze kloof te overbruggen, in de hoop dat Kunstmatige Intelligentie (AI) deze wiskundige bewijzen automatisch kan leren vertalen, zodat de hele gemeenschap hun werk kan delen.

Maak kennis met ITPEVAL, een nieuwe studie die fungeert als een massaal, rigoureus taalexamen voor AI. De onderzoekers wilden zien of de slimste AI-modellen van vandaag daadwerkelijk wiskundige bewijzen tussen vier belangrijke systemen konden vertalen: Lean 4, Rocq, Isabelle en HOL Light. Ze vroegen de AI niet alleen om te gokken; ze bouwden een gespecialiseerde testomgeving met meer dan 1.500 bronbestanden en bijna 7.000 stellingen. Ze verdeelden de test in twee niveaus: een "Gecontroleerd" niveau met eenvoudige, op zichzelf staande wiskundige problemen (zoals een woordenschatquiz zonder externe referenties), en een "Ecosysteem"-niveau dat gebruikmaakt van echte, rommelige bibliotheekcode die steunt op complexe, systeem-specifieke regels (zoals een volledig gesprek met straattaal en culturele referenties).

De resultaten waren een mix van "niet slecht" en "nog steeds erg moeilijk". Wanneer de AI probeerde alleen de stellingen van de bewijzen te vertalen (het "wat"), hadden de beste modellen ongeveer 29,1% goed. Maar toen de AI werd gevraagd om de daadwerkelijke bewijzen te vertalen (het "hoe"), stortte het succespercentage naar slechts 10,5%. De studie vond dat de grootste hindernis niet de wiskunde zelf of de verschillende logische fundamenten waren; het was het "ecosysteem". De AI had de meeste moeite wanneer het moest navigeren door de specifieke bibliotheken, naamgevingsconventies en automatisatiestijlen van het doel systeem. Het is alsof de AI de zin "De kat zat op de mat" kon begrijpen, maar faalde wanneer het werd gevraagd dit te vertalen naar een specifiek dialect dat een specifiek merk mat en een specifiek type kat vereiste.

Bovendien ontdekten de onderzoekers dat het simpelweg krijgen van een computer om te zeggen "Dit ziet er correct uit" (een type-check) niet genoeg is. Ze voerden een diepere "betekeniscontrole" uit en ontdekten dat zelfs wanneer de vertaling van de AI de basiscontrole van de computer doorstond, deze in 46% van de gevallen wiskundig zwakker of licht anders was dan het origineel. De studie suggereert dat hoewel AI beter wordt in de basis, het nog steeds moet leren hoe het zich moet aanpassen aan de unieke "cultuur" van elk wiskundig systeem voordat het echt een universele vertaler kan zijn. De auteurs verkenden ook een "round-trip" test, waarbij ze wiskunde naar natuurlijke taal vertaalden en weer terug, waarbij ze vonden dat de resultaten sterk varieerden afhankelijk van welk systeem werd gebruikt, wat erop wijst dat het gebruik van meerdere systemen samen zou kunnen helpen, maar dat het nog geen magische oplossing is.

Technische Samenvatting: ITPEVAL – Benchmarking van Formele Translatie Tussen Interactieve Stellingbewijzers

1. Probleemstelling

Het ecosysteem van formele stellingbewijzers is momenteel gefragmenteerd. Hoewel grote taalmodellen (LLM's) aanzienlijk succes hebben geboekt in geautomatiseerd stellingbewijs en autoformalizatie, blijven geverifieerde resultaten gesiloed binnen incompatibele Interactieve Stellingbewijzers (ITP's). Elk systeem (bijv. Lean 4, Rocq, Isabelle, HOL Light) implementeert zijn eigen logische fundament, tactiektaal en wiskundige bibliotheken. Hierdoor kan een stelling die in het ene systeem is bewezen, niet direct worden aangeroepen in een ander, wat leidt tot dubbel werk bij de formalisering en de hoeveelheid trainingsdata voor lerende bewijzers beperkt.

Cross-ITP translatie—de taak om formele bewijzen tussen systemen te converteren met behoud van correctheid—is weinig systematisch bestudeerd. Bestaande inspanningen, zoals de "Formalizing 100 Theorems" catalogi of interoperabiliteitsframeworks zoals Dedukti, richten zich op het bijhouden van dekking of het mogelijk maken van bewijsuitwisseling via intermediaire representaties, maar missen gestandaardiseerde benchmarks voor het evalueren van de kwaliteit van de translatie. Bovewerendien zijn bestaande evaluatiemethodologieën ontoereikend; eenvoudige typecontrole (type-checking) levert vaak een hoog aantal fout-positieven op voor semantische correctheid, en benchmarks voor code-translatie houden geen rekening met de diepe verschillen in logische fundamenten die inherent zijn aan ITP's.

2. Methodologie en Benchmark Design

De auteurs presenteren ITPEVAL, de eerste benchmark ontworpen om automatische formele bewijstranslatie tussen vier belangrijke ITP's te evalueren: Lean 4, Rocq (voorheen Coq), Isabelle en HOL Light. De benchmark beslaat twee verschillende logische fundamenten: de Calculus of Inductive Constructions (CIC) en Higher-Order Logic (HOL).

2.1. Datastructuur

De benchmark bestaat uit 1.560 bronbestanden en 6.848 stellingen, georganiseerd in twee onderscheidende niveaus om bronnen van moeilijkheidsgraad te isoleren:

Tier A (Gecontroleerd): Bevat 64 zelfstandige, geaxiomatiseerde bestanden (660 lemma's) afgeleid van de Babel-formal benchmark. Deze bestanden bevatten hun eigen definities en aannames, waardoor afhankelijkheid van prover-specifieke bibliotheken wordt vermeden. Dit niveau isoleert fundamentele translatieproblemen (bijv. type theory, universe levels, impliciete argumenten).
Tier B (Ecosysteem): Bevat formaliseringenheden uit echte community-bibliotheken, die API-mismatches, naamgevingsconventies en verschillen in bewijsstijl blootleggen. Dit niveau bevat:
- 232 bestanden uit Formalizing 100 Theorems (4.924 lemma's), uitgelijnd over alle vier de systemen.
- 1.264 single-theorem bestanden van miniF2F (alleen stellingen), die diverse competitieve wiskundige inhoud bieden.

Het ontwerp dwingt een vierweg-intersectievereiste af: elk bestand moet in alle vier de ITP's geformaliseerd zijn om zuivere directionele vergelijkingen mogelijk te maken zonder verwarring door ontbrekende gegevens.

2.2. Translatie-taken

ITPEVAL evalueert twee primaire taken:

Stelling-translatie (Statement Translation): Het genereren van doel-ITP-code waarbij de bewijsstructuren worden vervangen door placeholders (bijv. sorry). Verificatie vereist dat het gegenereerde bestand type-checkt in het doel systeem.
Bewijs-translatie (Proof Translation): Het genereren van volledige, compileerbare bewijsbestanden zonder placeholders. Verificatie vereist dat het volledige bestand succesvol compileert in de doel-prover.

2.3. Verificatie-infrastructuur

Een cruciaal onderdeel van de methodologie is itpeval, een uniforme multi-ITP verificatie-infrastructuur. Om de heterogeniteit van ITP-executiemodellen aan te pakken (bijv. zware opstartkosten voor Isabelle en HOL Light), gebruikt het systeem:

State-geïsoleerde warm backends: Zorgt ervoor dat elke controle observationeel equivalent is aan het verifiëren van een artefact in een verse omgeving, om lekkage van declaraties te voorkomen.
Natuurlijke doel-prover controle: Alle labels worden geproduceerd door de werkelijke doel-ITP's, niet door oppervlakkige heuristieken.
Adaptieve scheduling: Gebruik van persistente workers, sessie-batching en fork-servers om de doorvoer te beheren terwijl de per-bestand controle-semantiek behouden blijft.

2.4. Semantische Equivalentie Controle

In het besef dat type-controle noodzakelijk maar onvoldoende is voor semantische getrouwheid, implementeren de auteurs een Bidirectionale Uitgebreide Definitionele Equivalentie (BEq) check voor Lean 4 targets. Deze deterministische controle verifieert of een gegenereerde stelling $G$ en een referentiestelling $R$ elkaar impliceren ( $G \vdash R$ en $R \vdash G$ ) met behulp van beperkte bewijszoeking, om extra model-afhankelijke variantie te vermijden.

3. Belangrijkste Bijdragen

Vierweg Uitgelijnde Benchmark: Een dataset van 1.560 bestanden en 6.848 stellingen over Lean 4, Rocq, Isabelle en HOL Light, gestructureerd in gecontroleerde en ecosysteem-tiers om de kosten van bibliotheek-afhankelijkheden te kwantificeren.
Uniforme Verificatie-infrastructuur: Een state-geïsoleerde client (itpeval) die schaalbare, reproduceerbare evaluatie mogelijk maakt over heterogene provers met natuurlijke controle-semantiek.
Systematische LLM Evaluatie: Een evaluatie van vijf frontier en open-weight modellen (GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B) op 12 gerichte translatieparen.
Semantische Getrouwheidsanalyse: De toepassing van BEq om aan te tonen dat natuurlijke type-controle alleen de semantische correctheid aanzienlijk kan overschatten.
Exploratieve Round-Trip Studie: Een onderzoek naar autoformalizatie en auto-informalisatie loops om target-afhankelijke verificatiepatronen en de potentiële voordelen van multi-ITP context te beoordelen.

4. Resultaten

4.1. Translatieprestaties

Stelling-translatie: Het best presterende model, GPT-5.5, behaalde een 29.1% pass@1 rate overall. DeepSeek-V4-Pro volgde met 27.1%. De prestaties daalden aanzienlijk voor andere modellen (Gemini op 14.0%, Qwen en Claude onder de 10%).
Bewijs-translatie: De prestaties waren aanzienlijk lager, waarbij GPT-5.5 slechts 10.5% pass@1 behaalde overall.
Tier Gap: De gecontroleerde tier (Tier A) was consistent makkelijker dan de ecosysteem tier (Tier B). Voor bewijs-translatie behaalde GPT-5.5 29.7% op gecontroleerde bestanden, maar slechts 5.2% op ecosysteem-bestanden. Dit geeft aan dat bibliotheek-mismatch (API's, naamgeving, automatisering) de grootste geobserveerde bron van falen is, in plaats van verschillen in de logische fundering.
Directionele Asymmetrie: De moeilijkheidsgraad van translatie varieert aanzienlijk per doel. Isabelle en HOL Light zijn sterke targets voor stelling-translatie, maar Isabelle wordt het moeilijkste doel voor bewijs-translatie. Gelijkenis in logische fundering (bijv. CIC naar CIC) garandeert geen hogere succesratio's; de conventies van de doel-ecosystemen spelen een grotere rol.

4.2. Semantische Equivalentie (BEq)

Bij het toepassen van de BEq check op geverifieerde Lean 4 stelling-translaties uit miniF2F:

Slechts 54.0% van de geverifieerde translaties slaagde voor de equivalentiecheck.
Claude Sonnet 4.6 vertoonde de hoogste BEq pass rate (83.8%) onder de geverifieerde translaties, terwijl anderen varieerden tussen 34.5% en 48.4%.
Dit resultaat toont aan dat een stelling syntactisch geldig kan zijn (type-checkt) maar semantisch zwakker of verschoven is ten opzichte van de originele stelling.

4.3. Round-Trip en Autoformalizatie

In een multi-ITP round-trip studie (NL $\to$ Formeel $\to$ NL $\to$ Formeel), verifieerden Rocq en HOL Light ongeveer een derde van de outputs tijdens beide formaliseringsstappen, terwijl Lean 4 rond de 11% bleef en Isabelle zakte naar 4.3% bij de laatste stap. Multi-ITP context toonde potentiële voordelen voor specifieke model-target combinaties (bijv. het verbeteren van de Lean 4 step-1 pass rate van 4.8% naar 10.6%), maar de resultaten waren niet uniform over alle systemen.

5. Betekenis en Claims

Het artikel claimt dat ITPEVAL de eerste systematische, vierweg benchmark biedt voor formele translatie, waarbij wordt onthuld dat de primaire barrière voor cross-ITP translatie niet de logische fundering zelf is, maar de ecosysteem-niveau afhankelijkheden (bibliotheken, API's en bewijs-idiomen).

De auteurs benadrukken dat:

Natuurlijke verificatie essentieel is: Oppervlakkige heuristieken of type-controle alleen zijn onvoldoende om de semantische getrouwheid te evalueren.
Infrastructuur ertoe doet: Betrouwbare cross-ITP evaluatie vereist state-geïsoleerde verificatie om verwarrende factoren zoals declaratie-lekkage te voorkomen.
Toekomstige richtingen: Het veld moet prioriteit geven aan retrieval, library mapping en API-alignering boven louter fundamentele translatie. Het artikel merkt ook beperkingen op, waaronder de zero-shot evaluatie-setting, de beperking van BEq tot de Lean 4 targets, en het potentieel voor training data contaminatie in publieke datasets zoals miniF2F.

Het werk legt een fundament voor het meten van vooruitgang in formele translatie, en suggereert dat toekomstige systemen de "library mismatch" probleem moeten aanpakken om robuuste interoperabiliteit tussen formele bewijssystemen te bereiken.