Claude يۈزدىن ئارتۇق ئوچۇق كودلۇق كۈتۈپخانىنىڭ بىخەتەرلىكىنى ماتېماتىكىلىق ئىسپاتلىدى

سۈنئىي ئەقىل شىركىتى Anthropic نىڭ Frontier Red Team ئەترىتى 22-ئۆكتەبىر ئېلان قىلغان تەتقىقاتىدا، چوڭ تىل مودېللىرى (LLM) نىڭ رەسمىي يۇمشاق دېتال دەلىللەش (formal verification) نى بۇرۇنقىدىن نەچچە ھەسسە چوڭ كۆلەمدە ئەمەلگە ئاشۇرالايدىغانلىقىنى كۆرسەتتى. Theorem شىركىتى بىلەن ھەمكارلىشىپ، ئۇلار Claude ئارقىلىق 100 دىن ئارتۇق ئەمەلىي ئوچۇق كودلۇق كۈتۈپخانىنىڭ بىخەتەرلىك خۇسۇسىيەتلىرىنى ئاسسېمبلېر (RISC-V) دەرىجىسىدە ئىسپاتلىغان. Anthropic نىڭ دېيىشىچە، بۇ سۈنئىي ئەقىل ئارقىلىق ئىشلەپچىقىرىش يۇمشاق دېتالىغا ماشىنا كودى دەرىجىسىدە رەسمىي دەلىللەش قوللىنىلغان تۇنجى چوڭ كۆلەملىك تىرىشچانلىق.

سىناقتىن ئىسپاتقا

ئادەتتە يۇمشاق دېتالدىكى خاتالىقلار fuzzing ئۇسۇلى بىلەن ئىزدىلىدۇ: سىناق ماتورى غايەت زور مىقداردىكى تاسادىپىي كىرگۈزمىلەرنى پروگراممىغا بېرىپ، ئۇنىڭ يىمىرىلىش-يىمىرىلمەسلىكىنى تەكشۈرىدۇ. ئەمما بۇ ئۇسۇل ھەممە يولنى سىناپ بولغانلىققا كاپالەت بېرەلمەيدۇ. ئەترەت Google نىڭ OSS-Fuzz تۈرىدىكى fuzz سىناقلىرىنى رەسمىي ئۆلچەم (specification) گە ئايلاندۇردى: «64 MB تىن كىچىك ھەر قانداق كىرگۈزمىدە پروگرامما يىمىرىلمەيدۇ». Claude ئىسپاتنى Rocq تىلىدا يازدى، Rocq يادروسى (kernel) بولسا ئۇنى ئاپتوماتىك تەكشۈردى.

نەتىجىلەر

• بىر نەچچە ھەپتە ئىچىدە 123 كۈتۈپخانىدىكى 239 كىرىش نۇقتىسى (entry point) ئۈچۈن ئىسپات تاماملاندى.
• ئىسپاتلارنىڭ ئومۇمىي ھەجمى تەخمىنەن 180 مىليون قۇر Rocq؛ بىر تىپىك ئىسپات تەخمىنەن 600 مىڭ قۇر.
• ئىسپاتلاش جەريانىدا يۈزلىگەن خاتالىق (bug) بايقالدى، Claude ئۇلارنى تۈزىتىپ ئاندىن قايتا ئىسپاتلىدى.
• تېپىلغان خاتالىقلار ئارىسىدا پەقەت تەخمىنەن 20 MB لىق ئالاھىدە كىرگۈزمىدىلا كۆرۈلىدىغان چېكىدىن ھالقىپ يېزىش (out-of-bounds write) ۋە libexpat تىكى CVE-2026-56132 نىڭ قايتا بايقىلىشى بار.

ئاممىۋى ئامبار (repository) دا 25 كۈتۈپخانىدىكى 60 كىرىش نۇقتىسىنىڭ ئىسپاتلىرى ئېلان قىلىندى، ھەر كىم ئۇلارنى ئۆزى تەكشۈرەلەيدۇ. Theorem باشقا ئوچۇق كودلۇق تۈرلەر ئۈچۈنمۇ مۇشۇ جەرياننى ئىجرا قىلىپ بېرىدىغانلىقىنى ۋە ئىجادكارلار ئۈچۈن بىر Claude ماھارىتى (skill) ئېلان قىلىدىغانلىقىنى بىلدۈردى.

باشقا تەجرىبىلەر

Claude يەنە Linux يادروسىدىكى zlib نىڭ RFC 1950 ئۆلچىمىگە ماس كېلىدىغانلىقىنى x86 ئىككىلىك ھۆججىتى دەرىجىسىدە ئىسپاتلىغان. يەنە بىر تەجرىبىدە Rust تا Python نىڭ چوڭ بىر قىسمى ئۈچۈن تەرجىمان (interpreter) يېزىپ، Verus قورالى بىلەن ئىسپاتلىغان؛ 1.7 مىليوندىن ئارتۇق تاسادىپىي پروگراممىدا CPython بىلەن 99.95% ئوخشاش نەتىجە بەرگەن.

چەكلىمىلەر

Anthropic نىڭ ئۆزى ئەسكەرتكىنىدەك، «رەسمىي دەلىللەنگەن» دېگەنلىك «خاتالىقسىز» دېگەنلىك ئەمەس. ئىسپاتلار پەقەت musl بىلەن ئۇلانغان، يالغۇز ئېقىملىق (single-threaded) RISC-V پروگراممىلىرىغا ماس كېلىدۇ؛ كۆپچىلىك ئىشلىتىدىغان x86 ياكى ARM قۇرۇلمىلىرىغا بىۋاسىتە تەدبىقلانمايدۇ. AddressSanitizer (ASan) بارلىق ئەسلەك (memory) خاتالىقلىرىنى بايقىيالمايدۇ، ھەمدە ھەر بىر كۈتۈپخانىنىڭ ھەممە كىرىش نۇقتىسى دەلىللەنمىگەن. ئۇنىڭدىن باشقا، ئىسپات يېزىش يۈز مىليونلىغان توكېن (token) تەلەپ قىلىدۇ. شۇنداقتىمۇ Opus 5.5 مودېلى سىناق ۋەزىپىلىرىنىڭ يېرىمىنى Opus 5 تىن تەخمىنەن 40% ئاز توكېن بىلەن ئىسپاتلىغان، شۇڭا تەننەرخ تۆۋەنلەۋاتىدۇ.