DeepMind atinge o etapă în soluția problemelor matematice - următoarea mare provocare pentru AI

Cercetătorii au obținut rezultate mixte atunci când răspund la întrebări matematice cu modele vocale - tipul de sistem care conduce chatbots precum Chatt. Uneori, modelele dau răspunsul corect, dar nu pot explica raționamentul lor rațional, și alteori

Abia săptămâna trecută, o echipă de companii de software Numina și Huggingface au folosit un model vocal pentru a câștiga un „preț de progres” intermediar Amio, bazat pe versiuni simplificate ale problemelor IMO. Companiile au făcut ca întregul lor sisteme să fie deschis și l -au pus la dispoziție pentru descărcarea altor cercetători. Dar câștigătorii au spus Nature că modelele de limbă singure nu ar fi probabil suficiente pentru a rezolva probleme dificile.

alphaproof combină un model vocal cu tehnologia de consolidare a învățării, pe care motorul „alphazero” pentru jocuri de atac, cum ar fi, precum și unele Probleme matematice specifice . Odată cu creșterea învățării, o rețea neuronală învață prin experimente și erori. Acest lucru funcționează bine dacă răspunsurile sale pot fi evaluate folosind o scară obiectivă. În acest scop, Alphaproof a fost instruit să citească și să scrie dovezi într -un limbaj formal numit Lean, care este utilizat în pachetul software „Asistent de probă” cu același nume care este popular în rândul matematicienilor. Pentru aceasta, Alphaproof a testat dacă cheltuielile sale au fost corecte făcând -o în pachetul Lean, ceea ce a contribuit la completarea unora dintre pașii din cod.

Pregătirea unui model vocal necesită cantități masive de date, dar doar câteva dovezi matematice au fost disponibile în Lean. Pentru a depăși această problemă, echipa a dezvoltat o rețea suplimentară care a încercat să traducă o înregistrare existentă a unui milion de probleme care au fost scrise în limbaj natural, dar fără a traduce soluții scrise în Lean, spune Thomas Hubert, un cercetător de cursanți de la Deepmind Machine care a condus la dezvoltarea Alphaproof cu. "Putem învăța să ne dovedim abordarea, chiar dacă nu ne -am antrenat inițial pe dovezi scrise de oameni?" (Compania a fost similară cu Go, unde AI -ul său a învățat să joace jocul jucând împotriva ei înșiși, în loc de modul în care fac oamenii.)

cheie magică

Multe dintre traducerile slabe nu aveau sens, dar suficient au fost suficient de bune pentru a aduce alfaproof până la punctul în care ar putea începe ciclurile sale de învățare crescânde. Rezultatele au fost mult mai bune decât se aștepta, a spus Gowers la consultația de presă. "Multe probleme cu IMO au această proprietate a cheii magice. Problema arată mai întâi dificilă până când găsești o cheie magică care o deschide", a spus Gowers, care lucrează la Collège de France din Paris.

În unele cazuri, alfaproof părea să poată face acest pas suplimentar de creativitate, oferindu -i un pas corect dintr -o soluție posibilă infinit de mare. Dar este necesară o analiză suplimentară pentru a determina dacă răspunsurile au fost mai puțin surprinzătoare decât arătau, a adăugat Gowers. Un discurs similar a apărut după surprinzător 'zug 37' , DeepMinds alphago-bot la Faimoasă victorie în 2016 despre cel mai bun jucător al lumii din lume -Un punct de cotitură pentru KI.

rămâne de văzut dacă tehnicile pot fi perfecționate pentru a lucra la un nivel de cercetare în matematică, a spus Myers la revizuirea presei. "Se poate extinde la alte tipuri de matematică în care nu pot fi instruite milioane de probleme?"

"Am ajuns la punctul în care nu numai că puteți dovedi probleme de cercetare deschise, ci și probleme care sunt foarte dificile pentru cei mai buni tineri matematicieni din lume", a declarat David Silver, specialistul în calculatoare Deepmind, care a fost principalul cercetător în dezvoltarea Alphago la mijlocul anului 2010.