Syyskuussa MIT:n professori Dor Minzer sai ystävältään tekstiviestin. Tämä kysyi, oliko Minzer lähellä ratkaista Unique Games -konjektuurin. Pian viestejä tuli lisää, ja huhut alkoivat tarkentua: OpenAI:n kerrottiin löytäneen todistuksen ongelmalle, jonka parissa Minzer on tehnyt töitä vuosia.
Minzer ja hänen jatko-opiskelijansa Yumou Fei ja Shuo Wang kiirehtivät oman 95-sivuisen käsikirjoituksensa verkkoon kolme päivää huhujen alkamisen jälkeen, kertoo Quanta Magazine 7. lokakuuta julkaistussa jutussaan. Teksti oli matemaattisesti valmis mutta viimeistelemätön. ”Kuudennesta luvusta eteenpäin siinä ei ole kirjaimellisesti yhtään sidossanaa”, Minzer sanoi Quantalle englanniksi.
OpenAI julkaisi 6. lokakuuta satoja matemaattisia tuloksia, kuten AI Suomi kertoi, ja osa matemaatikoista on jo kehottanut kollegoitaan katkaisemaan yhteistyön yhtiön kanssa. Nyt keskustelu on siirtynyt yleisestä yksittäiseen. Unique Games on ensimmäinen tulos, jota ulkopuoliset tutkijat ovat todella alkaneet purkaa.
Mistä konjektuurissa on kyse
Subhash Khot esitti konjektuurin vuonna 2002. Arkikielellä se koskee väritystehtävää. Verkon solmut pitää värittää, ja jokainen kahta solmua yhdistävä viiva asettaa säännön sille, miten päiden värit liittyvät toisiinsa.
Jos paras mahdollinen väritys täyttää vaikkapa 99 prosenttia säännöistä, konjektuurin mukaan on silti laskennallisesti toivottoman vaikeaa löytää edes väritystä, joka täyttää prosentin niistä. Vaikeus ei siis hellitä, vaikka tavoitetta laskisi rajusti.
Väite on tärkeä seurauksiensa vuoksi. Prasad Raghavendra osoitti vuonna 2008, että jos konjektuuri pitää, monille optimointiongelmille jo tunnetut klassiset algoritmit ovat parhaita mahdollisia. Parempaa ei kannata etsiä. Joukossa on esimerkiksi Max-Cut, jossa verkko jaetaan kahtia niin, että mahdollisimman moni yhteys katkeaa.
“Unique Games -konjektuuri on tosi, vaikka sitä ei oikeastaan tarvittu sen tunnetuimpien seurausten todistamiseen.”
Moshkovitz on tutkinut samaa ongelmaa pitkään. Hänen puolisonsa, kvanttilaskennan tutkija Scott Aaronson, kirjoittaa 7. lokakuuta julkaistussa ”The Mathocalypse” -blogikirjoituksessaan, että Moshkovitz piti todistusta aluksi vaikeaselkoisena ja huonosti kirjoitettuna. Nyt hän ymmärtää sen Aaronsonin mukaan pääosin, ja apuna oli tekoälymalli, joka kävi todistusta läpi hänen kanssaan. Moshkovitzin mukaan todistus rakentaa kokonaan uudenlaisen, puurakenteeseen perustuvan koodin.
Mitä kone tarkisti ja mitä ei
Todistuksen tekee erityiseksi Lean-sertifikaatti. Lean on todistusavustaja, jossa matemaattinen väite ja sen todistus kirjoitetaan niin tarkasti, että tietokone voi tarkistaa jokaisen päättelyaskeleen. Jos Lean hyväksyy todistuksen, siinä ei ole loogista aukkoa, kunhan ohjelman oma ydin toimii oikein.
Aaronson ei pidä ytimen huijaamista todennäköisenä, koska mallin päättelyketjuissa ei näy merkkejä siitä ja käytetyt tekniikat näyttävät ongelmaan sopivilta. Kokonaan hän ei mahdollisuutta sulje pois, ennen kuin ”kaikki Leanin ytimen bugit on vakuuttavasti korjattu”.
Lean ei kerro, onko todistettu oikea asia. Kone tarkistaa, että todistus vastaa muodollista väitettä, mutta ei sitä, vastaako muodollinen väite sitä, mitä matemaatikot tarkoittavat konjektuurilla. Aaronsonin blogin kommentoija muistutti, että sertifikaatti pätee vain ”olettaen, että väitteen formalisointi on oikea”.
Tässä kohdassa lähteet eivät ole yksimielisiä. OpenAI:n Lean-luettelo kuvaa formalisoidun tuloksen polynomiaikaiseksi palautukseksi 3SAT-ongelmasta unique games -ongelmaan, mikä on konjektuurin tekninen muotoilu. Quanta taas kirjoittaa, että julkaisuun sisältyi Lean-tarkistettu todistus lähisukuiselle 2-to-1-konjektuurille. Kumpi kuvaus on tarkempi, selviää vasta, kun asiantuntijat käyvät Lean-tiedostojen väitteet läpi.
Mikä on vahvistettu, mikä ei
Vahvistettua: OpenAI on julkaissut Unique Games -todistuksen käsikirjoituksen ja siihen liittyvän Lean-formalisoinnin. Yhtiön oman repositorion mukaan noin 42 prosenttia päätuloksista on formalisoitu Leanilla, eli suurinta osaa ei ole. Quantan mukaan käsikirjoitusta ei ole toimitettu eikä riippumattomasti vertaisarvioitu.
Epäselvää: vastaako formalisoitu väite täsmälleen alkuperäistä konjektuuria, onko Leanin tarkistuksessa aukkoja ja kuinka paljon ihmiset ohjasivat työtä. Aaronsonin mukaan ”juuri kukaan ihminen ei ole vielä ymmärtänyt” näitä todistuksia, ja kilpajuoksu niiden ymmärtämiseksi on vasta alkanut.
Sama menettely, tuhansia ongelmia
Toinen uusi tieto koskee sitä, miten tulokset syntyivät. OpenAI:n GitHub-repositorion mukaan ”valtaosa tuloksista saatiin samalla menettelyllä” julkaisemattomalla sisäisellä mallilla. Mallille annettiin noin 4 000 ongelmaa, ja kukin julkaistu tulos vei keskimäärin kolme tuntia ChatGPT Pro -tason päättelylaskentaa.
Aiemmissa raporteissa menettelyä on kuvattu yhdeksi kehotteeksi yhdelle agentille. Repositorion tekstissä kehotteista ei kuitenkaan puhuta, eikä tarkkoja kehotteita ole julkaistu. Aaronsonin arvion mukaan malli ratkaisee noin viisi prosenttia sille annetuista ongelmista yhdellä kolmen tunnin yrityksellä.
Poikkeuksiakin on. Riemannin zeetafunktion nollakohdattoman alueen tulos ja eräs Hodgen konjektuuria koskeva työ tehtiin toisin, ja zeetafunktiota koskevaa tekstiä ihminen muokkasi luettavammaksi. Ihmiset myös ryhmittelivät mallin tuotokset käsikirjoituksiksi ja päättivät, mitkä tulokset ylittävät julkaisukynnyksen.
Ero on olennainen. Jos vakiomenettely tuottaa todistuksen vuosikymmenten avoimelle ongelmalle, kyse ei ole yksittäisen tutkijan ja koneen yhteistyöstä vaan toistettavasta tuotantolinjasta. Se muuttaa sekä sen, kuka saa tuloksesta kunnian, että sen, kuka ehtii tarkistaa kaiken.
Laskennan vaativuusteoria kuulostaa kaukaiselta, mutta se vastaa käytännön kysymykseen: milloin paremman algoritmin etsiminen kannattaa lopettaa. Jos konjektuuri pitää, moniin aikataulutuksen, reitityksen ja verkkosuunnittelun optimointiongelmiin ei ole tulossa olennaisesti parempia likiratkaisuja kuin nykyiset, ellei P = NP. Ohjelmistoyrityksille se on tieto siitä, mihin tuotekehitysrahaa ei kannata upottaa.
