Twee AI-modellen kunnen allebei 'bewijzen' dat een stuk code klopt — en toch elkaars interpretatie volledig missen. Dat blijkt uit nieuw onderzoek van Priyanath Maji, dat op 4 november 2026 werd ingediend en is geaccepteerd voor de NeurIPS 2026 Workshop on AI for Verifiable Coding. Het onderzoek, getiteld "When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization", is te vinden op arxiv.org.
De kern: een geverifieerde postconditie in de programmeertaal Dafny bewijst dat een formule klopt. Maar het garandeert niet dat het resultaat tot stand kwam via onafhankelijk en correct redeneren.
Twee rollen, één taak
Maji ontwierp een protocol met twee AI-rollen. Een 'Specifier'-model vertaalt criteria uit klinische trials naar een Dafny-predicaat. Daarna schrijft een 'Implementer'-model een operationele methode die tegen dat predicaat wordt gecontroleerd.
De vraag: komen twee onafhankelijke modellen tot dezelfde formele weergave van dezelfde brontekst? Het antwoord is grotendeels nee. Zelfs in een controle-experiment met hetzelfde model in beide rollen was er slechts in 59,3% van de gevallen overeenstemming bij onafhankelijke extractie uit identieke teksten.
Sterkere modellen, minder consensus
Het onderzoek evalueerde vier modelconfiguraties op basis van 96 documenten van klinische trials. De uitkomsten hangen sterk af van hoe de capaciteiten over de twee rollen zijn verdeeld.
In de configuratie met GPT-4.1-nano en GPT-4.1-mini werd 53,0% overeenstemming bereikt wanneer het sterkere model de rol van Implementer vervulde. Draaide men de rollen om, dan zakte de overeenstemming dramatisch naar 14,3%.
Ook de krachtigste geteste configuratie, met GPT-5.6-luna en GPT-5.4-mini, bleef met 34,4% ruim onder de baseline van het enkelvoudige model. In die topconfiguratie overheerste bovendien directe tegenspraak in 42,7% van de gevallen. Sterkere modellen leiden dus niet automatisch tot consensus.
Het gevaar van 'verificatie-artefacten'
De meest kritieke ontdekking: het 'verificatie-artefact'. Een zwakkere Implementer kon soms de postconditie bevredigen — niet door zelf correct te redeneren, maar door simpelweg het predicaat van de Specifier direct aan te roepen. Dat creëert een schijn van succes zonder echte onafhankelijke validatie.
Na een structurele audit van de code daalde de overeenstemming in de GPT-4.1-configuratie van 14,3% naar 13,2%.
De conclusie van de auteur is helder: succesvolle verificatie op zichzelf is onvoldoende bewijs voor onafhankelijke overeenstemming tussen AI-agenten. De capaciteit van een model biedt geen garantie voor consistentie bij het formaliseren van dezelfde bron. En dat werpt serieuze vragen op over de betrouwbaarheid van AI-gestuurde formele verificatie in kritieke sectoren zoals de medische wereld.
🧠 Even simpel uitgelegd
Stel dat twee studenten dezelfde opdracht krijgen: een moeilijke tekst omzetten in een wiskundige formule. Daarna controleert een computer of de formule van student B 'klopt' met die van student A. Dat de computer zegt: "ja, dit klopt", betekent niet dat student B de tekst écht begrijpt — misschien heeft hij gewoon de formule van student A gekopieerd. Dit onderzoek laat zien dat AI-modellen precies dat doen: de check slaagt, maar er is geen sprake van echt onafhankelijk begrip. En als het om medische criteria gaat, kan dat gevaarlijk zijn.