Un algoritm bazat pe inteligență artificială (IA) poate traduce problemele de matematică scrise în limba engleză într-un cod formal, făcându-le mai ușor de rezolvat de către computere. Acesta ar putea fi un pas crucial către dezvoltarea unei mașini capabile să descopere noi tipuri de matematică.
Deși calculatoarele sunt deja folosite de ceva timp pentru verificarea demonstrațiilor matematice, acestea funcționează doar dacă problemele sunt pregătite într-un limbaj special conceput pentru demonstrare. Din cauza faptului că acest proces, cunoscut sub numele de formalizare, poate dura ani doar pentru o singură demonstrație, doar o mică parte din cunoștințele matematice a fost formalizată și apoi demonstrată de o astfel de mașină.
Yuhuai Wu și colegii acestuia din cadrul companiei Google au folosit o rețea neuronală denumită Codex, care a fost creată de compania de cercetare AI OpenAI. Aceasta a fost instruită pe cantități mari de text și date de programare de pe web și poate fi folosită de programatori pentru a genera un cod funcțional.
Datorită faptului că limbile demonstrative sunt similare cu limbajele de programare, echipa a decis să vadă dacă Codex ar putea formaliza o bază de date formată din 12.500 de probleme de matematică pentru școala secundară. Algoritmul a fost capabil să traducă un sfert din probleme într-un format compatibil cu un program formal de rezolvare a problemelor denumit Isabelle. „Multe dintre traducerile nereușite au fost rezultatul faptului că sistemul nu a înțeles anumite concepte matematice. Dacă instruim sistemul cu un exemplu care explică acel concept, algoritmul îl poate prelua rapid”, a declarat Wu.
Pentru a testa eficacitatea acestui proces de auto-formalizare, echipa a utilizat sistemul pe un set de probleme care fuseseră deja formalizate de oameni. Codex a generat propriile versiuni formale ale acestor probleme, iar echipa a folosit un alt algoritm IA, denumit MiniF2F, pentru a rezolva ambele versiuni.
Problemele auto-formalizate au îmbunătățit rata de succes a algoritmului MiniF2F de la 29% la 35%, sugerându-se faptul că sistemul Codex a fost mai bun în formalizarea acestor probleme decât oamenii.
Deși aceasta este o îmbunătățire modestă, Wu este de părere că munca echipei este doar o dovadă a conceptului. „Dacă scopul este acela de a antrena o mașină care este capabilă să opereze la același nivel cu cei mai buni oameni, atunci auto-formalizarea pare să fie o soluție esențială”, a adăugat Wu.
„Îmbunătățirea în continuare a ratei de succes ar permite algoritmului să concureze cu matematicienii umani. Un algoritm cu o rată de succes de 100% ar putea fi capabil să câștige o medalie de aur la Olimpiada Internațională de Matematică”, a declarat Albert Jiang, membru al echipei din cadrul Universității din Cambridge.
Un astfel de sistem ar putea fi utilizat pentru sarcini de verificare într-o gamă largă de domenii. „Putem verifica dacă o parte a unui software face exact ceea ce i s-a cerut să facă sau putem verifica cipurile hardware. Așadar, sistemul ar putea avea aplicații în algoritmi de tranzacționare financiară și design hardware”, a adăugat Jiang.
