In de stille, abstracte wereld van de theoretische informatica worstelen onderzoekers vaak met het probleem van equivalentie: bepalen of twee verschillend uitziende structuren eigenlijk dezelfde onderliggende realiteit vertegenwoordigen. Stel je een set instructies voor om een machine te bouwen. Je zou de instructies kunnen opschrijven in een lange, kronkelende paragraaf, of je zou ze kunnen opdelen in een opsomming met diagrammen. Als beide sets instructies resulteren in exact dezelfde machine die op exact dezelfde manier functioneert, zijn ze equivalent, zelfs als ze er totaal niet hetzelfde uitzien. Dit concept staat centraal in een vakgebied genaamd diagrammatisch redeneren, waarbij processen worden getekend als plaatjes — boxen verbonden door lijnen — in plaats van als vergelijkingen worden opgeschreven. Deze plaatjes worden gebruikt om complexe systemen te modelleren, van de stroom van elektriciteit tot het gedrag van quantumcomputers. In de wereld van quantumcomputing, waar machines informatie manipuleren op manieren die de alledaagse intuïtie tarten, is het verifiëren of twee verschillende circuitdiagrammen hetzelfde doen een cruciale veiligheidscontrole. Als een computer niet kan bewijzen dat twee ontwerpen identiek zijn, kan hij niet worden vertrouwd voor het optimaliseren of verifiëren van de hardware die de technologie van de toekomst zal aandrijven.

Een team van onderzoekers uit Frankrijk en Duitsland heeft nu een nieuwe reeks uitdagingen geïntroduceerd die ontworpen zijn om te testen hoe goed moderne geautomatiseerde redeneertools deze specifieke vorm van equivalentie kunnen aanpakken. Hun werk richt zich op een familie van problemen die zij diagrammatische equivalentie noemen, die een eenvoudige vraag stelt: gegeven twee verschillende circuitdiagrammen, kunnen ze in elkaar worden getransformeerd met behulp van een vaste set regels? De onderzoekers stelden niet alleen de vraag; ze bouwden een fabriek om duizenden unieke, moeilijke voorbeelden van dit probleem te generen. Ze creëerden drie verschillende niveaus van moeilijkheid, variërend van een vereenvoudigde versie die alleen het verwisselen van draden omvat tot een complexe versie die diverse soorten elektronische componenten bevat. Voor elk niveau vertaalden ze de visuele diagrammen naar een taal die computers kunnen lezen, waardoor een rigoureus testveld werd gecreëerd voor de meest geavanceerde automatische stellingbewijzers en logische oplossers ter wereld.

De onderzoekers begonnen met het definiëren van de spelregels. In hun systeem worden circuits gebouwd uit basisbouwstenen, of generatoren, die met draden zijn verbonden. Deze verbindingen kunnen op twee manieren plaatsvinden: één na de andere, zoals een ketting, of naast elkaar, als parallelle banen. De kern van het probleem ligt in het feit dat hetzelfde circuit op veel verschillende manieren getekend kan worden. Net zoals een zin kan worden herschikt zonder de betekenis te veranderen, kan een circuitdiagram worden gedraaid, uitgerekt of georganiseerd volgens specifieke wiskundige wetten die coherentievergelijkingen worden genoemd. De uitdaging voor een computer is om naar twee diagrammen te kijken die er totaal verschillend uitzien en te bepalen of ze in feite hetzelfde object zijn onder deze regels. Om dit testbaar te maken, creëerde het team drie variaties van het probleem. De eerste, en meest algemene, staat elke type component toe. De tweede verwijdert alle componenten, waardoor alleen draden overblijven die verwisseld kunnen worden, wat het probleem effectief verandert in een probleem van permutatie. De derde is een vereenvoudigde versie van de tweede, die alleen de meest basale bouwstenen gebruikt om een meer beheersbare, maar nog steeds moeilijke puzzel te creëren.

Om de gegevens te generen, schreef het team computerprogramma's die fungeren als circuitarchitecten. Deze programma's beginnen met een leeg rooster en plaatsen willekeurig componenten en draden. Vervolgens passen ze een reeks transformaties toe — zoals het draaien van een draad of het verwisselen van twee aangrenzende blokken — om een tweede versie van het circuit te creëren die wiskundig identiek is aan de eerste, maar er anders uitziet. De programma's garanderen dat de twee resulterende diagrammen equivalent zijn door constructie, wat betekent dat het antwoord altijd "ja" is, maar het pad om het te bewijzen verborgen ligt in de complexiteit van het diagram. De onderzoekers genereerden duizenden van deze paren, waarbij ze het aantal ingangsdraden en de grootte van de diagrammen varieerden om een spectrum van moeilijkheidsgraad te creëren. Vervolgens codeerden ze deze visuele puzzels in twee standaardformaten die in de wetenschappelijke gemeenschap worden gebruikt, zodat elke automatische redeneertool een oplossing kan proberen te vinden.

Toen de onderzoekers deze benchmarks aan de test onderwierpen, zetten ze ze af tegen de meest vooraanstaande geautomatiseerde redeneertools die vandaag de dag beschikbaar zijn. Ze selecteerden twee specifieke systemen: één die uitblinkt in het afhandelen van rekenkundige en logische beperkingen, en een andere die een krachtpatser is voor algemene logische deductie. De resultaten toonden een duidelijke kloof in prestaties. Het systeem dat ontworpen is om rekenkundige beperkingen te behandelen, bleek aanzienlijk bekwaamer en loste een groot deel van de eenvoudige en middelmoeilijke puzzels op. Het slaagde er in veel gevallen in om de equivalentie van circuits met tot wel twintig draden en honderden componenten te verifiëren. Het algemene deductiesysteem daarentegen had enorme moeite. Het slaagde er niet in om bijna de complexe problemen op te lossen en liep vast, zelfs bij relatief kleine circuits. De onderzoekers ontdekten dat de moeilijkheid van het probleem werd gedreven door twee hoofdfactoren: het aantal draden dat betrokken is en het totaal aantal verbindingen in het diagram. Naarmate deze aantallen groeiden, daalde het vermogen van de tools om een oplossing te vinden scherp.

De studie benadrukt een significante flessenhals in het vakgebied van de geautomatiseerde redenering. Hoewel computers steeds krachtiger worden, blijft de specifieke combinatie van rekenkundig redeneren en de manipulatie van complexe structurele regels een formidabele uitdaging. De onderzoekers observeerden dat de tools die het best presteerden, de tools waren die de wiskundige beperkingen die de draden beheersen inherent begrepen, in plaats van ze puur door logische stappen te proberen te deduceren. Dit suggereert dat, om diagrammatische equivalentie efficiënt op te lossen, toekomstige tools de rekenkundige redenering dieper in hun kernlogica moeten integreren. Het werk beweert niet het probleem van het verifiëren van quantumcircuits te hebben opgelost, maar het heeft een cruciale stresstest geleverd. Door een gestandaardiseerde, uitdagende set problemen aan te bieden, heeft het team de wetenschappelijke gemeenschap een duidelijke manier gegeven om vooruitgang te meten. De benchmarks dienen als een spiegel die de huidige beperkingen van onze automatische tools reflecteert en de weg wijst naar de specifieke verbeteringen die nodig zijn om de verificatie van complexe, op diagrammen gebaseerde systemen een betrouwbare realiteit te maken.