Bedrijf PSI publiceert met hulp van AI vijf quantumbewijzen die een computer kan controleren
Physical Superintelligence heeft met een eigen AI-systeem vijf open vragen uit de quantum-informatietheorie aangepakt. Elk bewijs staat ook in Lean, een programma dat bewijzen stap voor stap controleert. Vakgenoten kunnen ze nu zelf nalopen.
Physical Superintelligence (PSI), een jong bedrijf dat geld ophaalt voor een natuurkundelab waarin AI vanaf het begin meewerkt, heeft op 23 oktober nieuwe resultaten gepubliceerd over vijf open vragen in de quantum-informatietheorie. Dat vakgebied onderzoekt hoe je informatie kunt opslaan, versturen en bewerken met de regels van de quantumwereld. Het is de basis onder quantumcomputers en quantumcommunicatie.
De vijf vragen komen uit de Open Quantum Problems, een lijst met onopgeloste vraagstukken uit het vakgebied. De onderzoekers van PSI werkten daarvoor samen met het eigen AI-onderzoekssysteem. Volgens het bedrijf hielp de AI mee, terwijl de onderzoekers het werk stuurden en controleerden. Per resultaat staat beschreven hoe AI is gebruikt.
Bewijzen die een computer kan nalopen
Het bijzondere zit vooral in de vorm. Bij elk resultaat hoort niet alleen een wetenschappelijk artikel, maar ook een versie van het bewijs in Lean. Lean is een programma dat een wiskundig bewijs stap voor stap controleert. Het werkt een beetje als een spellingscontrole, maar dan voor logica: klopt één stap niet, dan keurt Lean het bewijs af.
Dat is juist bij AI belangrijk. AI-modellen kunnen teksten schrijven die overtuigend klinken, maar toch fouten bevatten. Een bewijs dat Lean heeft goedgekeurd, hoeft niemand op zijn woord te geloven. PSI noemt de publicatie daarom een vroege test van het idee dat AI kan helpen bij onderzoek dat je echt kunt controleren, en niet alleen bij tekst die geloofwaardig klinkt.
Alles staat openbaar op GitHub: per resultaat het artikel en de Lean-bestanden, met alles wat nodig is om de controle zelf te draaien. Een apart script laat zien wanneer de eerdere versies van de artikelen zijn gemaakt.
Wat er is bewezen
De resultaten zijn technisch, maar ze gaan bijna allemaal over verstrengeling. Dat is een bijzondere quantumband tussen deeltjes: meet je het ene deeltje, dan weet je meteen iets over het andere, ook als het ver weg is. Verstrengeling is de grondstof van quantumcommunicatie.
- Niet elke verstrengeling is bruikbaar. Voor een bepaalde soort quantumtoestanden, de Werner-toestanden, bewijst PSI dat je uit drie exemplaren nooit de zuivere verstrengelde paren kunt halen die nodig zijn voor quantumcommunicatie, binnen een bepaald bereik. Of dat ook geldt voor meer dan drie exemplaren, blijft een open vraag.
- Verbonden, maar niet meer aan te tonen. In een eenvoudig model van het lege vacuüm blijven twee ruimtegebieden verstrengeld, hoe ver ze ook uit elkaar liggen. Toch bewijst PSI dat je vanaf een bepaalde afstand met de bekende CHSH-test niet meer kunt laten zien dat hun samenhang sterker is dan de gewone natuurkunde toestaat.
- De beste manier van meten. Bij een andere test, de CGLMP-test, laat PSI zien welke manier van meten het sterkste quantumeffect geeft, en dat elke beste manier in wezen op die ene neerkomt.
- Verstrengeling verbreken. Een recent stuk van OpenAI meldde dat twee bewerkingen van een bepaalde soort (PPT-afbeeldingen) in het algemeen niet genoeg zijn om verstrengeling helemaal te verbreken. PSI bewijst hoeveel er wel altijd genoeg zijn: 2(d−1), waarbij d staat voor de grootte van het quantumsysteem.
- Een tegenvoorbeeld. Tot slot vond PSI een tegenvoorbeeld voor een vermoeden over causale processen. Niet elk proces waarin oorzaak en gevolg netjes op volgorde blijven, past in een groter, omkeerbaar quantumproces van eindige grootte.
Nu is het aan vakgenoten
Het gaat om voorpublicaties. Ze hebben nog geen DOI of arXiv-nummer, de vaste kenmerken van een wetenschappelijke publicatie, en zijn nog niet door andere onderzoekers beoordeeld. De stellingen zijn dus claims van PSI zelf. Dankzij de Lean-bewijzen kunnen vakgenoten ze nu wel zelf nalopen: dat is de volgende stap.
PSI heeft daarnaast plannen voor datacenters. Die staan volgens het bedrijf los van dit onderzoek.
Wat betekent dit voor de weg naar de singulariteit?
AI die meehelpt aan nieuwe wiskundige bewijzen, is een stap richting AI die de wetenschap versnelt. Het grootste probleem daarbij is dat AI fouten kan maken die overtuigend klinken. Worden bewijzen standaard door een programma als Lean gecontroleerd, dan kunnen onderzoekers sneller en met meer vertrouwen op elkaars werk voortbouwen, ook als een deel ervan door AI is gedaan. Deze vijf resultaten zijn een vroege proef. Als vakgenoten de bewijzen hebben nagelopen, wordt duidelijk hoe goed deze werkwijze werkt en of hij ook in andere vakgebieden past. En de quantum-informatietheorie is zelf een bouwsteen voor de quantumcomputers van de toekomst.
