Maanantaina 26. lokakuuta Scott Aaronsonin opiskelijat tulivat hänen työhuoneeseensa Texasin yliopistossa Austinissa kertomaan uutisen. Aaronson on yksi tunnetuimmista laskennan vaativuuden tutkijoista, ja uutinen oli hänen alallaan suuri. OpenAI kertoi, että sen malli on kumonnut eksponentiaalisen ajan hypoteesin (Exponential Time Hypothesis, ETH). Hypoteesi on ollut alan perusoletuksia yli 25 vuotta.
Kyse on toistaiseksi OpenAI:n omasta väitteestä. Yhtiö julkaisi 25. lokakuuta päivätyn käsikirjoituksen nimeltä The Exponential Time Hypothesis is False GitHub-palvelussa. Tekijäksi on merkitty pelkästään OpenAI. Työtä ei ole vertaisarvioitu, eikä yksikään riippumaton tutkija ole julkisesti vahvistanut todistusta oikeaksi.
“Opiskelijani tulivat juuri työhuoneeseeni kertomaan, että OpenAI:n malli on nyt kumonnut eksponentiaalisen ajan hypoteesin. – – Vaikka yritämme yhä sulatella edellisiä ruokalajeja, loputon noutopöytä jatkuu!”
Mitä ETH oikeastaan väittää
Russell Impagliazzo ja Ramamohan Paturi muotoilivat ETH:n vuosituhannen vaihteessa. Hypoteesi koskee 3-SAT-ongelmaa eli loogista palapeliä, jossa joukolle kyllä/ei-muuttujia etsitään arvot, joilla kaikki annetut ehdot täyttyvät. Yksinkertaisin tapa on kokeilla kaikki vaihtoehdot. Jokainen uusi muuttuja kuitenkin kaksinkertaistaa vaihtoehtojen määrän.
ETH:n mukaan oikotietä ei ole. Nopeinkin algoritmi tarvitsee aikaa, joka kasvaa eksponentiaalisesti muuttujien määrän mukana. Hypoteesia ei ole koskaan todistettu, mutta sitä on pidetty niin uskottavana, että sadat tutkimukset ovat ottaneet sen lähtöoletukseksi. Niissä on päätelty, että jos ETH pitää, monia muitakaan ongelmia ei voi ratkaista nopeasti.
Aaronsonin mukaan OpenAI:n algoritmi ratkaisee 3-SAT:n ajassa, joka kasvaa suunnilleen kuten exp(n/√log n). Tämä on yhä valtava luku, mutta kasvu on hitaampaa kuin ETH sallii. Unite.AI:n mukaan Lean-dokumentaatiossa tulos on muotoiltu niin, että deterministinen kone laskee k-SAT-kaavan ratkaisujen tarkan määrän aliksponentiaalisessa ajassa ja polynomisessa muistissa.
Salaus ei murru huomenna
Pankkiyhteydet ja viestisovellukset eivät ole vaarassa. Nykyinen salaus perustuu erityisiin matemaattisiin ongelmiin, kuten suurten lukujen tekijöihin jakoon ja elliptisiin käyriin, eikä suoraan 3-SAT:n vaikeuteen. ETH:n kumoaminen ei siksi tuo uutta hyökkäystä mitään käytössä olevaa salausmenetelmää vastaan.
Käytännön ohjelmistoihinkaan vaikutus ei ole välitön. Vaikka algoritmi on teoriassa nopeampi, tuhansien muuttujien tehtävissä laskenta-aika on yhä tähtitieteellinen. Logistiikan, piirisuunnittelun ja ohjelmistojen verifioinnin SAT-ratkaisijat toimivat jo nyt hyvin käytännön tapauksissa, koska ne hyödyntävät tehtävien rakennetta.
Suurin vaikutus olisi tutkimukseen. Jos todistus kestää, satojen ETH:n varaan rakennettujen vaativuustulosten perusta katoaa. Silloin raja sille, mitä tietokoneella voi tehdä tehokkaasti, piirretään uudelleen. Tutkimusrahoitusta ja uusia algoritmeja suunnataan juuri tällaisten rajojen perusteella, joten tieto rajan siirtymisestä ulottuisi lopulta myös yrityksiin.
Kuka tarkistaa koneen todistuksen?
Unite.AI:n mukaan malli tuotti todistuksen 16. lokakuuta, ja seuraavana päivänä se formalisoitiin Lean-todistusavustimella. Lean tarkistaa koneellisesti, että jokainen päättelyaskel on pätevä. Mallin nimeä OpenAI ei kerro.
Lean-tarkistuskaan ei ratkaise kaikkea. Gizmodo muistuttaa, että OpenAI:n aiemmin julkaisemaa Lean-todistusta Navier–Stokesin ongelmasta lukeneet tutkijat päätyivät Science-lehden mukaan siihen, että Lean tarkisti heikomman väitteen kuin yhtiö julkisti. Koneen tarkistus on vain yhtä hyvä kuin väitteen muotoilu, jota se tarkistaa.
Siksi OpenAI on pyytänyt mukaan ihmisiä, joita se kutsuu paimeniksi (shepherds). ETH-tuloksen tarkistusta johtavat Unite.AI:n mukaan hypoteesin alkuperäiset muotoilijat Impagliazzo ja Paturi Kalifornian yliopistosta San Diegosta. Mukana on myös MIT:n Ryan Williams. OpenAI on luvannut julkaista kaiken raakadatan ja rahoittaa tuloksen seurauksia käsittelevän konferenssin. Yhtiö kuvaa mallinsa käsikirjoituksia ilmaisulla "best understood as a form of raw research data" eli parhaiten ymmärrettäviksi eräänlaisena raakana tutkimusdatana.
Paimenet eivät ole vielä esittäneet omaa arviotaan todistuksesta. AI Suomi ei saanut jutun julkaisuun mennessä kommenttia suomalaiselta teoreettisen tietojenkäsittelyn tutkijalta.
