AI-avusteinen Kollektion hypoteesin todistus epäonnistui Lean-järjestelmässä
Tekoälyllä avustettu yritys todistaa Kollektion hypoteesi Lean-järjestelmällä on todettu epäkelvoksi. Puutteet Lean 4.32.2 -version ytimessä korjattiin nopeasti.
Teknologiamedia Gigazine raportoi, että tekoälyä hyödyntänyt yritys kumota Kollektion hypoteesi epäonnistui. Todistus, joka tehtiin Lean-formaalijärjestelmällä, todettiin virheelliseksi sen jälkeen, kun asiantuntijat havaitsivat merkittävän vian itse järjestelmässä.
Kollektion hypoteesi, joka tunnetaan myös nimellä 3n+1 -ongelma, on yksinkertaisesti muotoiltu, mutta ratkaisematon matemaattinen arvoitus. Se väittää, että mikä tahansa positiivinen kokonaisluku päätyy lopulta lukuun 1, kun siihen sovelletaan iteratiivisesti sääntöjä: parillinen luku jaetaan kahdella, pariton kerrotaan kolmella ja lisätään yksi.
Alun perin Ramana Kumar ilmoitti GitHubissa 25. heinäkuuta löytäneensä keinon todistaa, että on olemassa lukuja, jotka eivät päädy yhteen. Hän käytti Lean-järjestelmää, joka varmistaa matemaattisten todistusten oikeellisuuden ohjelmallisesti. Kumarin väite oli, että hänen AI-avusteinen todistuksensa osoitti tämän.
Myöhemmin paljastui, että Kumarin käyttämä menetelmä salli Lean-järjestelmän hyväksyä virheellisiä väittämiä. Tutkija Kiran Gopinathan rajasi ongelman pienempään toistettavaan koodiin ja raportoi siitä Leanin kehitystiimille 28. heinäkuuta. Vika oli Leanin ytimessä ja liittyi "sisäkkäisten induktiivisten tyyppien" käsittelyyn, minkä vuoksi jotkin parametrit jäivät vahvistuksen ulkopuolelle.
Leanin kehitystiimi korjasi vian nopeasti. Leonardo de Moura, yksi Leanin kehittäjistä, vahvisti ongelman olleen toteutuksen tarkistusmekanismeissa. Noin tunnin kuluessa raportoinnista tiimi julkaisi korjatun version, Lean 4.32.2, 28. heinäkuuta, mikä palautti järjestelmän luotettavuuden. Vaikka hypoteesin todistusyritys epäonnistui, korjaus varmistaa Lean-järjestelmän kyvyn jatkossa toimia luotettavana työkaluna matemaattisessa tutkimuksessa.