Тест бичих эрин төгсөх үү? Anthropic AI-аар 123 нээлттэй эхийн сангийн алдаагүйг математикаар нотлов

Компьютер шинжлэх ухааны домогт эрдэмтэн Эдсгер Дейкстрагийн (Edsger W. Dijkstra) алдартай үг бий: "Программ туршилт (testing) нь алдаа байгааг л харуулж чадахаас, алдаа огт байхгүйг хэзээ ч баталж чадахгүй."

Хөгжүүлэгчид бид олон арван жилийн турш кодоо шалгахын тулд Unit test, Integration test бичиж, сүүлийн жилүүдэд триллион удаагийн санамсаргүй оролтоор системийг нүддэг Fuzz testing (OSS-Fuzz) дээр найдаж ирсэн. Гэвч практик дээр хэчнээн олон тест бичсэн ч санах ойн цоорхой (memory safety bug), race condition, эсвэл логик алдаа үлдсээр л байдаг.

Үүнийг үндсээр нь шийдэх цорын ганц арга нь Албан ёсны математик нотолгоо (Formal Software Verification) юм. Гэвч энэ нь маш их хөдөлмөр, өртөг шаарддаг тул сансар судлал болон батлан хамгаалах салбарын цөөн хэдэн критикал системээс өөр газар ашиглагдаж чаддаггүй байв. Харин саяхан Anthropic компани энэхүү түүхэн саадыг AI-ийн тусламжтайгаар бүрэн нурааснаа зарлалаа.

20 жилийн хөдөлмөрийг хэдхэн долоо хоногт багтаасан нь

Албан ёсны нотолгоо хэр их хүч шаарддаг байсны бодит жишээ бол seL4 үйлдлийн системийн микрокернел юм. seL4-ийн эх кодыг бичихэд 2 хүн-жил (person-years) зарцуулсан бол түүнийг алдаагүй гэдгийг математикаар нотлоход дэлхийн шилдэг эрдэмтэд 20 хүн-жил зарцуулж байжээ.

Anthropic-ийн Frontier Red Team судалгааны баг formal methods чиглэлээр дагнасан Theorem байгууллагатай хамтран Claude моделийг ашиглан дэлхий даяар өргөн хэрэглэгддэг 123 нээлттэй эхийн сангийн (Google OSS-Fuzz-ийн 239 entry point) хөрвүүлсэн хоёртын кодыг бүрэн нотолж чадсан байна.

Claude энэ явцдаа нийт 180 сая мөр Rocq (хуучнаар Coq) нотолгооны код үүсгэсэн бөгөөд нэг сангийн дундаж нотолгоо нь ойролцоогоор 600,000 мөр болжээ. Хамгийн гол нь энэ асар том ажлыг хүн биш, AI агентууд хэдхэн долоо хоногийн дотор хийж дуусгасан явдал юм.

Яагаад эх код биш, RISC-V машины ассемблер түвшинд нотлов?

Энэ төслийн техникийн хамгийн сонирхолтой шийдэл нь C эсвэл C++ эх кодыг бус, харин Clang компилятороор хөрвүүлэгдсэн RISC-V машины хоёртын зааврыг (assembly level) шууд нотолсон явдал юм.

Яагаад заавал машины код гэж? Хөгжүүлэгчийн бичсэн эх код математикийн хувьд хичнээн зөв байлаа ч:

Компиляторын хэт оновчлол (compiler optimizations) нь тодорхойгүй төлөвийг (undefined behavior) арилгаж, аюулгүй байдлын цоорхой үүсгэдэг.
Эх кодын семантик болон бодит техник хангамжийн (CPU) заавар хоёрын хооронд зөрүү гарах эрсдэлтэй.

Иймээс судалгааны баг RISC-V архитектур болон Linux процессын албан ёсны математик загварыг тодорхойлж өгчээ. Claude-ийн гаргасан теорем нь: "64 MB хүртэлх ямар ч өгөгдөл орж ирсэн тухайн RISC-V машин код нь AddressSanitizer-ийн алдаа, санах ойн заагчийн хязгаар давах (out-of-bounds) болон ямар нэгэн сүйрэл (crash) үүсгэхгүйгээр хэвийн ажиллаж дуусна" гэдгийг хатуу нотолсон байна.

LLM-ийн хий үзэгдэл (Hallucination)-д хэрхэн итгэх вэ?

Олон программистууд "AI код бичихдээ алдаа гаргадаг (hallucination), тэгвэл 180 сая мөр нотолгоонд яаж итгэх вэ?" гэж асуух нь гарцаагүй.

Энд л Formal Verification-ийн гайхамшиг оршиж байгаа юм. Код бичихээс ялгаатай нь математик нотолгоог шалгадаг Rocq хөдөлгүүр (kernel) нь өөрөө маш цомхон, математикийн хувьд батлагдсан алгоритм байдаг.

Хэрэв Claude худлаа залах эсвэл логикийн хувьд буруу нотолгоо үүсгэвэл Rocq шалгагч компилятор түүнийг тэр даруй Reject хийнэ.
Шалгагчийг амжилттай давсан 180 сая мөр кодыг хүн нэг бүрчлэн уншиж шалгах шаардлагагүй, энэ нь 100% математик үнэн гэдэг нь автоматаар батлагддаг.

AI энэ системд "ухаалаг теорем үүсгэгч" үүрэг гүйцэтгэсэн бөгөөд алдаа гаргах бүртээ Rocq-ийн хариу алдааг уншиж, нотолгоогоо сайжруулан дахин бичих замаар төгс болгожээ.

Триллион удаа туршаад илрүүлээгүй алдааг олсон нь

Хамгийн гайхалтай нь, нотолгоо бичих явцдаа Claude тухайн сангуудад олон жил нуугдаж, Google-ийн автомат тестүүд триллион удаа гүйхдээ ч олж чадаагүй байсан маш нарийн цоорхойнуудыг илрүүлжээ:

Зөвхөн 20 MB-ийн маш ховор бүтэцтэй өгөгдөл орж ирэх үед л санах ойн хязгаараас хальж бичдэг (out-of-bounds write) ноцтой цоорхой.
Зураг тайлагч (image decoder) санд 64 MB хэмжээтэй зураг боловсруулах үед 2 GB-аас дээш RAM шаардан унадаг алдаа.
libexpat сангийн алдарт CVE-2026-56132 цоорхойг өөрөө бие даан олж илрүүлсэн явдал.

Нотолгоо гаргахын тулд загвар эхлээд эдгээр алдааг засах patch бичиж, кодыг нь сайжруулсны дараа сая "Алдаагүй" гэх нотолгоогоо бүрэн дуусгасан байна.

Хөгжүүлэгчдэд энэ юу гэсэн үг вэ?

Энэ туршилт нь одоогоор single-threaded, санах ойн хатуу хязгаартай RISC-V орчинд хийгдсэн тул бүх төрлийн веб, мобайл системд маргааш шууд нэвтрэх болоогүй. Гэвч энэ нь программ хангамжийн аюулгүй байдалд шинэ эрин үе эхэлснийг зарлалаа:

Тест бичих дадал өөрчлөгдөнө: Ирээдүйд хөгжүүлэгчид кодын мөр бүрд Unit test бичиж, Code Coverage хувь хөөцөлдөхийн оронд кодоо математикийн теорем болгон "Formal Verification CI/CD"-ээр батлуулдаг болох зам нээгдэж байна.
AI аюулгүй байдлын аудит: Шинжээчдийн таамаглаж буйгаар 2027 оны сүүл гэхэд Nix экосистемийн нээлттэй эхийн сангуудын 95% нь ийм төрлийн AI нотолгоогоор бүрэн баталгаажих боломжтой юм.

Программчлалын ертөнцөд "Алдаагүй код гэж байдаггүй, зөвхөн илрээгүй алдаа л гэж бий" гэсэн бичигдээгүй дүрэм удахгүй түүх болон үлдэж магадгүй нь.

Эх сурвалж:

Anthropic Research: "LLMs are making formal software verification feasible at a much larger scale" (October 22, 2026)
Theorem & Anthropic Frontier Red Team Technical Report: Formal RISC-V Binary Verification on OSS-Fuzz