Modelet e inteligjencës artificiale (AI) po arrijnë të zgjidhin probleme matematikore me një ritëm gjithnjë e më të lartë, duke përdorur një teknikë të njohur si formalizimi, përmes së cilës verifikohet saktësia e zgjidhjeve të tyre.
Sipas një artikulli të publikuar nga “New Scientist”, formalizimi është thelbësor për të siguruar se zgjidhjet e pretenduara nga AI janë të sakta. Megjithatë, një incident i fundit ka ngritur pikëpyetje nëse vetë procesi i formalizimit mund të manipulohet.
Ramana Kumar, një inxhinier softueri, pretendoi se kishte hedhur poshtë konjekturën Collatz, një nga problemet më të njohura të hapura në matematikë, duke përdorur formalizimin në Lean, një softuer i njohur për formalizimin e teoremeve.
Por më vonë u zbulua se në këtë proces ishin shfrytëzuar dy gabime në dy bërthama të ndryshme të kodit. Rasti nxori në pah një rrezik të mundshëm: sistemet e AI mund të shfrytëzojnë dobësitë e mjeteve të formalizimit për të prodhuar rezultate që duken të sakta, por në të vërtetë nuk janë.
Leonardo de Moura, krijuesi i Lean, shprehu shqetësim se një incident i tillë mund të inkurajojë aktorë të këqij që të përdorin AI për të mashtruar. Për këtë arsye, ai dhe ekipi i tij kanë nisur punën për forcimin e mjeteve të formalizimit, me qëllim parandalimin e manipulimeve të ngjashme në të ardhmen.
Një pjesë e kësaj përpjekjeje është formalizimi i vetë bërthamës së kodit të Lean. Ideja është që Lean të përdoret për të verifikuar se bërthama e tij nuk përmban gabime që mund të shfrytëzohen.
Përveç kësaj, de Moura dhe zhvillues të tjerë po krijojnë bërthama të ndryshme, në mënyrë që të ulet rreziku që një gabim i vetëm universal të ndikojë në të gjitha sistemet. Këto bërthama do të testohen në një platformë online, ku do të vlerësohet saktësia e tyre në prova të njohura.
Megjithatë, pavarësisht këtyre masave që synojnë të rrisin sigurinë, rreziku i manipulimit nga AI mbetet.
Matematikanët përballen tashmë me sfidën e shfrytëzimit të AI si një mjet për zgjidhjen e problemeve komplekse, ndërsa duhet të kenë parasysh edhe mundësinë që sistemet të shfrytëzojnë dobësitë në proceset e verifikimit.
De Moura është shprehur optimist se përpjekjet e reja do të ndihmojnë në krijimin e një sistemi më të besueshëm, por ka pranuar se për të arritur një nivel të plotë besueshmërie do të nevojitet një përpjekje e madhe.
Sinjali – aty ku e vërteta flet para lajmit!


