Çində hazırlanmış süni intellekt sistemi, 2014-cü ildə Amerikalı riyaziyyatçı Dan Anderson tərəfindən irəli sürülən uzun müddətdir davam edən riyaziyyat problemini həll etməyi bacarıb. Pekin Universitetində Donq Binin rəhbərliyi altında hazırlanmış sistem, onilliklər boyu davam edən riyazi ədəbiyyatı təhlil edərək problemi təxminən 80 saat ərzində həll edib. Tədqiqatçılar prosesin demək olar ki, tamamilə insan müdaxiləsi olmadan baş verdiyini bildiriblər.
Yeni sistem iki əsas komponentdən ibarətdir. “Rethlas” adlı komponent, riyaziyyatçıların istifadə etdiyi metodlara bənzər həll strategiyaları hazırlayır. Daha sonra, “Archon” adlı ikinci sistem bu həlli təsdiqlənə bilən bir quruluşa çevirir. Bu mərhələdə interaktiv teoremi sübut edən dil olan Lean 4 istifadə olunur. Tədqiqatçılar vurğulayıblar ki, tədqiqat hələ həmyaşıdların rəyindən keçməyib və arXiv platformasında dərc edilib. Lakin nəticələr göstərir ki, süni intellekt təkcə hesablamada deyil, həm də inkişaf etmiş riyazi düşüncədə əhəmiyyətli irəliləyiş əldə edib.
Alimlərin fikrincə, bu yanaşma gələcəkdə riyazi tədqiqatları əsasən avtomatlaşdıra bilər. Buna baxmayaraq, mütəxəssislər bizə riyazi sübutların mütləq dəqiqlik tələb etdiyini və süni intellektin hələ də insan nəzarətinə ehtiyacı ola biləcəyini xatırladırlar. Tədqiqat qrupu böyük dil modellərində səhvlər və “hallüsinasiyalar” riskini qeyd edərək, hazırlanmış sistemin bu problemi aradan qaldırmaq üçün həm təbii dil mühakiməsini, həm də rəsmi yoxlamanı birləşdirdiyini bildirir.
