Son aylarda süni intellekt riyaziyyatda heyrətamiz irəliləyişlər əldə edib, onlarca il ərzində insanları qaçırmış tikə bucaqların həllini tapıb. Texnologiya şirkətlərinin bu mürəkkəb yeni tapıntıları açıqlaya bilməsinin əsasını formalaşdırma adlanan nisx sahəsidir.
Ancaq son zamanlar formalaşdırma vasitələrinin arxasında olan inkişaf etdiricilər süni intellekt modellərinin uğur qazanmaq üçün yollarını aldatma potensialına malik olduğunu başa düşdülər. İndi döyüş vasitələri sərtləşdirmək və bunun baş verməsinin qarşısını almaq üçün davam edir.
Riyazi nəzəriyyələri formalaşdırmaq əsasən kompüterlərin onlarla birbaşa mübarizə aparmasına imkan verən kodlara çevirir, metodik olaraq məntiqlə işləyir və hər hansı bir qüsurları ortaya qoyur. Proses o qədər dərindir ki, əgər bir teorema sağlam olsa, bütün məntiqli şübhələrdən kənarda doğru olduğunu sübut edilmiş hesab edilir.
Riyaziyyatın qızıl dövrü yaranır və riyaziyyatçılar çıldırırlar.
Bunu etmək üçün aparıcı proqram, Lean, süni intellekt dünyasında öz modellərinin çıxışı sürətli və qətiyyətlə sübut etmək üçün texnologiya nəhəngləri üçün əlverişli bir yol olaraq nüfuz qazanıb. Şirkətlər Lean-dan istifadə edərək mürəkkəb puzzlların həll edilməsi haqqında cəsarətli elanlar edə bilərlər. Onsuz da, onlar yalnız bu puzzlların mümkün həllini tapdıqlarını iddia edə biləcəklər və sonra həllini qiymətləndirmək üçün insan riyaziyyatçılarını dəvət edəcəklər. Bu iş həftələr və ya aylar çəkə bilər.
Leonardo de Moura, Microsoft Research-də işləyərkən 2010-cu illərdə Lean-ı yaradıb. O deyir ki, proqram ilk başda yalnız insan riyaziyyatçıları tərəfindən istifadə olunan bir nisə aləti idi və heç vaxt hiylə və ya manipulyasiya cəhdləri olmamışdı.
Xülasə — davamını mənbədə oxuyun.
