Un modul de inteligență artificială (IA) a respins cinci conjecturi (teoreme nedovedite) în ciuda faptului că acesta nu a primit nicio informație cu privire la ipoteze.
Adam Zsolt Wagner din cadrul Universității Tel Aviv din Israel a folosit un modul IA pentru a căuta exemple care să infirme o serie de conjecturi, care se refereau la teoria grafurilor, o ramură a matematicii care implică studierea obiectelor formate din noduri și legături. Matematicienii erau de părere că aceste presupuneri erau adevărate, dar nu reușiseră să le demonstreze.
Pentru fiecare presupunere, Wagner a creat o unitate de măsură prin care putea cuantifica cât de aproape a fost un exemplu de respingerea conjecturii. De exemplu, dacă o conjectură ar propune faptul că o anumită problemă nu ar putea fi rezolvată în mai puțin de cinci pași, un exemplu de rezolvare în șase pași ar fi mai aproape de o infirmare a acesteia decât unul în șapte pași, iar o soluție în patru pași ar servi drept contraexemplu pentru conjectură.
Wagner a programat o rețea neuronală pentru a crea exemple aleatorii și pentru a le folosi cu scopul de a evalua dacă acestea sunt un contraexemplu valid. Modulul IA a renunțat la cele mai slabe punctaje și le-a înlocuit cu exemple mai aleatorii înainte de a reîncepe analiza. În zeci de cazuri, modulul IA nu a reușit să găsească un exemplu care să infirme teoria, dar, în cinci cazuri, acesta a ajuns la o soluție, care demonstra faptul că presupunerea este falsă.
„Cu fiecare iterație, eliminăm cele mai slabe rezultate și învățăm din cele mai bune exemple. Practic, este cel mai simplu lucru posibil. Nu se întâmplă nimic fantezist”, a declarat Wagner.
„Este foarte impresionant. Dintr-o perspectivă matematică, ceea ce vedem aici este un avantaj imens adus de inteligența artificială, fără a exista nici un dezavantaj. Contraexemplele sunt foarte rare”, a declarat Leslie Hogben din cadrul Universității de Stat din Iowa, care a avut una dintre conjecturile ei respinse de către IA.
În timp ce modulul IA a reușit să respingă presupunerile, dovedirea lor este mult mai dificilă. A respinge o idee necesită crearea și testarea unei cantități vaste de soluții potențiale pentru a vedea dacă vreuna contrazice conjectura, o sarcină care poate fi automatizată, dar dovedirea unei ipoteze presupune realizarea unei lucrări creative, care implică înțelegerea mai multor pași logici.
Prima teoremă care a fost demonstrată cu ajutorul unui computer a fost teorema celor patru culori, care afirmă că orice hartă poate fi colorată folosind doar patru culori, astfel încât să nu existe două țări vecine, care să aibă aceeași culoare. Demonstrația, realizată în anul 1976, a implicat utilizarea unui computer pentru a verifica o listă vastă de exemple. La acel moment, demonstrația a fost considerată de unii cercetători de neegalat. Totuși, utilizarea computerelor pentru rezolvarea problemelor matematice a devenit mult mai răspândită.
Totuși, Hogben a declarat faptul că este important ca matematicienii să poată fi capabili să verifice aceste demonstrații. „Eu personal nu aș avea niciodată o problemă cu o infirmare care poate fi verificată. O dovadă creată pe un computer și care nu poate fi verificată manual ridică îngrijorări. Pentru mine, asta încalcă standardul de aur al matematicii”, a adăugat acesta.
Timothy Gowers din cadrul Collège de France din Paris a declarat pe Twitter faptul că abordarea este o demonstrație interesantă a conceptului. „Este greu de imaginat faptul că acesta este sfârșitul poveștii. Poate că această metodă poate fi transformată într-un simplu instrument de „verificare a ipotezelor”, care ar fi de mare ajutor cercetătorilor din domeniul matematicii.”
