OpenAI-nin Navier-Stokes probleminin sübutlarını dərc edərkən zəif bir səhvə yol verdiyi görünür, bir riyaziyyatçı qrupu iddia etdi. Səhv sübutların səhv olduğu və ya OpenAI-nin problemi düzgün həll etmədiyi anlamına gəlmir, lakin bu, süni intellektin modelləri tərəfindən yaradılan riyazi nəticələrin həmişə etibar oluna biləcəyini şübhə altına alır.
"Bu böyük dil modelləri tərəfindən yaradılan sübutlarla nə etmək lazımdırsa, bu da insanların oxumaları lazımdır və bu da riyaziyyatçılara böyük əlavə yük yaratır", - Kembriz Universitetində Anders Hansen deyir.
8 sentyabrda OpenAI, riyaziyyatda ən məşhur açıq problemlərdən biri olan Navier-Stokes probleminin həllini tapdığını elan etdi. Bu sübut iki versiya ilə nəşr edildi təbii dildə yazılmış bir, insan riyaziyyatçısı yazdığı kimi ingilis və riyazi simvolların birləşməsini bildirir və digərinə kompüter kodu Lean yazılmışdır. Lean sübut, kompüterə bütün məntiqi bəyanatlarının həqiqət olduğunu mexaniki şəkildə yoxlamağa imkan verən təbii dildə versiyanın formalaşması deməkdir. Hansen və komandası deyək ki, problem onların uyğunlaşmamasıdır.
"Bu formalizasiya prosesi həmkarların rəyindən istifadəni əvəz etməyə çalışır", - Kembriz Universitetindəki komanda üzvü Fabian Circelli deyir. Düşmənlər tərəfindən nəzərdən keçirilməsi dəlillərə insan gözləri baxır. Ancaq bu məqalədə göstərdiyimiz şey bu tip süni intellektin avtomatik formalaşmasının eyni məqsədə xidmət edə bilməməsidir.
OpenAIs 722 yeni məqaləsində ən maraqlı riyazi kəşflər
Açıq olsun ki, tədqiqatçılar OpenAI-nin Navier-Stokes problemini həll etmədiyini deyillər. Həm təbii dil sübutunun, həm də Lean-ın bir həllini təmin etməsi tamamilə mümkündür, çünki Pitagoras teoremasının yüzlərlə etibarlı sübutları var. Bunun əvəzinə, onların məqamı daha incədir: OpenAIs modelinin Lean-a çevrilərkən mistranslated olduğu.
Xülasə — davamını mənbədə oxuyun.
