Claude süni intellekti Fermat sübutu üçün 13 milyon sətir kod yazdı

    “Anthropic” “Claude” süni intellekt sistemi ilə Fermatın son teoreminin kompüterin başdan sona yoxlaya bildiyi versiyasını hazırlayıb. İş 11 günə, demək olar ki, insan nəzarəti olmadan tamamlanıb. Yekun sübut 13 milyon sətir “Lean” kodundan ibarətdir. Şirkət əvvəlcə bu layihənin bir neçə il çəkəcəyini gözləyirdi.

    Fermatın son teoremini riyaziyyatçı Pierre de Fermat 1637-ci ildə irəli sürüb. Andrew Wiles teoremin ilk tam riyazi sübutunu 1995-ci ildə yazıb. Həmin sübut 129 səhifə olub. Formallaşdırma zamanı sübutdakı riyazi məntiq kompüterin yoxlaya biləcəyi koda çevrilir. Beləcə, proqram hər addımın doğru olub-olmadığını ayrıca yoxlayır.

    Proses zamanı “Claude” agentləri, yəni tapşırıqları özü yerinə yetirən süni intellekt proqramları təxminən 30 300 ayrı teoremi sübut edib. Onlardan 29 500-ü yekun versiyaya daxil edilib. İnsanlar yalnız arabir işin ümumi istiqamətini göstərib, kodu isə özləri yazmayıb. Riyaziyyatçılar üçün hazırlanmış “Lean” dili bütün sübutu kompüterlə yoxlamağa şərait yaradıb.

    “Anthropic” uğurlu nəticəyə çatmazdan əvvəl formallaşdırmanı bir neçə dəfə sınaqdan keçirib. Standart və təkrarlanan kod hissələri çıxarıldıqda əvvəlki cəhdlər yekun sübutun təxminən 7 faizinə bərabər olub. Hazırlanan kod “Mathlib” adlı əsas icma kitabxanasından 5 dəfədən çox böyükdür. Riyaziyyatçı Kevin Buzzard deyib ki, sübut yalnız riyazi aksiomlara əsaslanır və sonrakı araşdırmalarda işlədilə bilər.

    Nəticənin əldə olunmasında “Prove2Me” adlı açıq mənbəli proqram da rol oynayıb. Bu alət süni intellekt agentlərinə uzun və çoxmərhələli araşdırma zamanı növbəti faydalı addımı seçməyə kömək edir. Eyni zamanda hesablama üçün tələb olunan resursların xərcini azaldır. “Anthropic” formallaşdırma layihələri üzərində çalışan riyaziyyatçılar üçün pulsuz çıxışı, tədqiqat kreditlərini və qrantları da artırıb.

    Bu iş “Anthropic”-in Riemann zeta funksiyası ilə bağlı başqa nəticəni açıqlamasından 1 ay sonra yayımlanıb. Həmin funksiya riyaziyyatın ən çətin və hələ həll edilməmiş problemlərindən biri sayılan Riemann hipotezinin əsasındadır. “OpenAI” də “Astra” modeli ilə klassik Erdős problemlərindən bir neçəsi üzərində işləyir. Bununla belə, prosesin 11 gün çəkməsi tam formallaşdırmanın güclü süni intellekt sistemləri üçün də böyük iş olduğunu göstərir.