Technische Samenvatting: Dataverificatie is de Toekomst van Quantum Computing Copilots

Probleemstelling

De generatie en compilatie van quantumprogramma's vereisen een niveau van precisie dat botst met de statistische redenering die inherent is aan Large Language Models (LLMs). Taken binnen quantum computing vereisen het overbruggen van meerdere abstractielagen (van hoogwaardige circuitbeschrijvingen tot laag-niveau gate-arrangementen) en het naleven van strikte wiskundige beperkingen (bijv. unitariteit, hardwaretopologie, gate-fidelity). In tegenstelling tot natuurlijke taal taken, waarbij fouten getolereerd of gemiddeld kunnen worden, vereist de generatie van quantumprogramma's een nul-tolerantie voor fouten; een enkele ongeldige gate-sequentie schendt fundamentele natuurwetten.

Huidige LLM-gebaseerde benaderingen kampen met drie kritieke beperkingen:

1. Onhaalbare oplossingen: Zonder dataverificatie zijn onhaalbare oplossingen wiskundig onvermijdelijk vanwege de statistische aard van LLM's, ongeacht modelschaling.
2. Dataschaarste: Omvattende, geverifieerde quantumdatasets zijn extreem moeilijk te genereren. Bestaande datasets (bijv. QDataSet) vereisten maanden aan HPC-tijd om slechts kleine systemen (1-2 qubits) te dekken.
3. Beperkingen in de zoekruimte: De geldige subspace van quantumcircuits is exponentieel klein vergeleken met de totale ontwerpruimte, begrensd door unitariteit en hardwarebeperkingen. Huidige LLM-architecturen kunnen niet intern de noodzakelijke verificatiemechanismen bieden om deze ruimte te navigeren.

Methodologie en Raamwerk

Het artikel stelt een paradigmaverschuiving voor van "inference-only" of "post-hoc filtering" naar verificatie-eerst architecturen. De auteurs definiëren drie kernposities die ondersteund worden door theoretische argumenten en voorlopige experimenten:

1. Dataverificatie als Minimale Vereiste (P1)

De auteurs stellen dat trainingsdata formeel geverifieerd moet worden voordat deze in de trainingsset wordt opgenomen.

• Concept: Een "Verification-aware model" wordt uitsluitend getraind op data waarbij elke instantie voldoet aan domeinspecifieke correctheidsbeperkingen (bijv. bewezen via automatische theorem provers zoals Lean of Z3).
• Rationale: Trainen op ongeverifieerde data (bijv. kwalitatief slechte code-repositories) vormt "impliciete datavergiftiging". In tegen tegenstelling tot natuurlijke taal, waar enorme datavolumes ruis gemiddeld, schendt een enkele ongeldige instantie in quantumcircuit-data de unitariteit, ongeacht de omliggende geldige voorbeelden. Dit leidt tot een "anti-scaling" fenomeen waarbij meer ongeverifieerde data fouten versterkt in plaats van ze te verdunnen.
• Mechanisme: Geverifieerde datasets stellen modellen in staat om beperkingen te internaliseren als geleerde structuren in plaats van statistische benaderingen.

2. A Priori Beperkingen boven A Posteriori Filtering (P2)

Verificatie moet het generatieproces beperken voordat de output wordt gegenereerd, in plaats van outputs te filteren nadat ze zijn gegenereerd.

• Rationale: Bij het ontwerpen van quantumcircuits neemt het fractie van geldige ontwerpen exponentieel af naarmate het aantal componenten (qubits/gates) toeneemt. Voor een ontwerpruimte die groeit als $O(d^n)$, reduceren beperkingen de geldige ontwerpen tot $O(\delta^n)$ waarbij $\delta < d$.
• Gevolg: Vertrouwen op post-hoc filtering (het genereren van vele kandidaten en het verwerpen van ongeldige) brengt exponentiële computationele kosten met zich mee en heeft een verwaarloosbare slaagkans. Verificatie moet worden ingebed als een architecturaal primitief om ongeldige paden tijdens de token-generatie te voorkomen.

3. Verification-First Paradigma voor AI4Research (P3)

De auteurs pleiten voor het uitbreiden van deze verificatie-eerst benadering naar andere wetenschappelijke domeinen die worden beheerst door natuurwetten of wiskundige axioma's (bijv. drug discovery, materiaalkunde, engineering design).

• Concept: Deze domeinen delen problemen met "leaky abstraction" en "non-decomposability", waarbij lokaal optimale keuzes geen globale optimaliteit garanderen. Verificatie-bewuste architecturen zijn noodzakelijk om deze harde beperkingen aan te kunnen.

Experimentele Resultaten

Om Positie 1 te onderbouwen, voerden de auteurs een evaluatie uit met een dataset afgeleid van geverifieerde MAJ/UMA (Majority/UnMajority-and-Add) circuit corpora.

• Setup: 34 publiekelijk beschikbare LLM's (variërend van 270M tot 120B parameters) werden getest op 70.000 meerkeuzevragen over quantum adder optimalisatie (2 tot 8 qubits). De grondwaarheid (ground truth) is het circuit met de minimale gewogen score van Toffoli-count, diepte en totaal aantal gates.
• Nauwkeurigheid: Modellen die getraind of gefinetuned zijn met verificatiekennis (bijv. gemma3:12b, gpt-oss:120b) behaalden een nauwkeurigheid tussen de 0,60 en 0,79. In contrast hiermee bleven generieke modellen zonder verificatiebewustzijn nabij de random baseline (0,21–0,29).
• Kalibratie: Verificatie-bewuste modellen vertoonden superieure onzekerheidskwantificering. gpt-oss modellen gaven 60–80% vertrouwen aan correcte antwoorden, terwijl gemma3 modellen in de 20–35% range bleven.
• Foutmodi: Verschillende modellen (bijv. mixtral:8x7b, deepseek-r1 varianten) scoorden onder de random baseline door malafide outputs (weliswaar uitgebreide weigeringen of verklaringen in plaats van enkelvoudige letter-antwoorden), wat bevestigt dat zonder verificatietraining modellen niet betrouwbaar kunnen omgaan met formeel beperkte taken.
• Zoekruimte Analyse: De auteurs genereerden een dataset van 200.000 geverifieerde adder-ontwerpen. Ze merkten op dat hoewel de totale mogelijke gate-arrangementen voor MAJ/UMA modules over dieptes 3–6 de 148 biljoen configuraties overstijgen, formele verificatie slechts ~200.000 geldige ontwerpen identificeerde (een ratio van $\approx 10^{-9}$), wat de onhoudbaarheid van post-hoc filtering illustreert.

Belangrijkste Bijdragen

1. Formele Definitie van Verification-Aware Modellen: Het onderscheid tussen modellen getraind op geverifieerde beperkingen versus modellen getraind op ongeverifieerde code-repositories.
2. Drie Kernposities: Het vaststellen dat dataverificatie een minimale vereiste is, dat beperkingen a priori moeten zijn, en dat dit paradigma essentieel is voor wetenschappelijke AI.
3. Empirisch Bewijs: Het leveren van kwantitatieve data die aantoont dat zonder dataverificatie, LLM's niet in staat zijn tot hoge nauwkeurigheid of correcte kalibratie op quantum optimalisatie taken, ongeacht de parameter schaal.
4. Identificatie van "Leaky Abstraction": Het benadrukken hoe quantum program generatie het samenvoegen van abstractieniveaus vereist (bijv. module design vs. gate decompositie) op een manier die lokale optimalisatie onvoldoende maakt voor globale correctheid.

Betekenis en Toekomstige Richtingen

Het artikel betoogt dat voor AI levensvatbaar te zijn in domeinen die geregeerd worden door strikte fysieke of wiskundige wetten, verificatie moet worden verheven van een "bijzaak" naar een "architecturale fundering".

De auteurs stellen twee specifieke toekomstige onderzoeksrichtingen voor:

• FD1 (Architectuur): Quantum copilot architecturen moeten formele verificatie (bijv. Satisfiability Modulo Theories of symbolische specificaties) direct integreren in de token-generatie loop van de LLM, waardoor verificatie transformeert van een binaire filter naar een gestructureerde exploratiegids.
• FD2 (Benchmarks): De gemeenschap heeft behoefte aan beperkingsrijke benchmarks gekoppeld aan uitvoerbare verificatie-oracles. Deze moeten verder gaan dan eenvoudige adders en ook modulaire vermenigvuldiging, quantum Fourier transforms en hardware-specifieke routing moeten bevatten, om reproduceerbare standaarden voor cross-systeem vergelijking mogelijk te maken.

Het artikel concludeert dat hoewel de argumenten zich richten op quantum computing, de principes breed toepasbaar zijn op elk veld waar correctheid binair is, geldige oplossingen een exponentieel kleine subspace bezetten en formele verificatiemethoden bestaan.