N環球 
Si Claude ay Sumulat ng 180 Milyong Linya ng Mathematical Proof sa Unang Large-Scale AI Formal Verification ng Open-Source Software
Opisyal na pananaliksik ng Anthropic: gamit ang Theorem, pormal na na-verify ni Claude ang mga pag-aari ng seguridad sa antas ng pagpupulong ng RISC-V sa 123 open-source na aklatan at 239 na entry point — at naghukay ng daan-daang mga bug na nakaiwas sa trilyon na mga automated na pagsubok.
Bakit ito mahalaga
Dati ang pormal na pag-verify ay isang marangyang kaya lang ng mga eksperto sa paglipas ng mga taon — ang seL4 microkernel ay tumagal ng 2 tao-taon upang magsulat at 20 tao-taon upang ma-verify. Ipinakita na ngayon ng Anthropic na magagawa ito ng isang frontier model para sa higit sa isang daang tunay na open-source na library sa loob ng ilang linggo, habang nakakakuha ng mga bug na nakaligtas sa "trilyon" ng mga automated na pagsubok na tumatakbo.
Buong ulat
Inanunsyo ng Anthropic sa opisyal na pahina ng pananaliksik nito noong Oktubre 22: sa pakikipagtulungan ng kumpanya ng pag-verify ng software na Theorem, pormal na na-verify ni Claude ang mga pag-aari ng seguridad sa antas ng pagpupulong ng RISC-V sa 123 real-world na open-source na library na nakuha mula sa OSS-Fuzz ng Google, na sumasaklaw sa 239 na entry point ng programa. Tinatawag ito ng kumpanya na "ang unang malakihang pagsisikap na gumamit ng AI upang maglapat ng pormal na pag-verify sa software ng produksyon sa antas ng code ng pagpupulong."
Kapansin-pansin ang sukat: humigit-kumulang 180 milyong linya ng Rocq proof, na may karaniwang patunay na tumatakbo sa humigit-kumulang 600,000 linya, na sumasaklaw sa mga binary na may median na haba na 18,000 RISC-V na mga tagubilin — lahat ay natapos sa loob ng ilang linggo. Independiyenteng sinusuri ng Rocq kernel ang bawat patunay, kaya walang manu-manong line-by-line na pagsusuri ang kailangan.
Ang pamamaraan ay nagko-convert ng mga kasalukuyang fuzz test sa mathematical na mga detalye: para sa anumang input na mas mababa sa 64 MB, ang isang single-threaded statically linked RISC-V binary sa Linux ay dapat palaging lumabas nang normal, na walang mga paglabag sa memory-safety. Nang maghinala si Claude ng isang bug sa kalagitnaan ng patunay, direktang na-patch nito ang code at muling pinatunayan ang bagong spec.
Daan-daang mga bug ang lumitaw sa daan, kabilang ang isang counter underflow sa isang decompressor copy na humahantong sa isang out-of-bounds na pagsusulat (ma-trigger lang ng ~20 MB na mga input na may isang pambihirang layout), isang out-of-bounds na nabasa sa isang image decoder, at isang muling pagtuklas ng CVE-2026-56132 sa loob ng maraming taon — ang ilang mga kahinaan ay naging mahina sa loob ng maraming taon.
Kinikilala ng Anthropic ang mismong mga limitasyon: ang isang nakapasa na pormal na pag-verify ay hindi nangangahulugang walang bug — ang mga patunay ay sumasaklaw lamang sa mga binary na may single-threaded na static na RISC-V, habang ang karamihan sa mga code ay aktwal na tumatakbo sa x86/ARM. Nag-publish ito ng subset ng mga patunay sa GitHub para sa independiyenteng pag-verify, at sinabi ng Theorem na tatakbo ito ng parehong pipeline para sa iba pang mga open-source na proyekto.
Ang mga side result ay kapansin-pansin din: ang pagpapatupad ng zlib ng Linux kernel ay napatunayang umaayon sa RFC 1950 sa x86 binary level, at isang malaking subset ng isang Python interpreter na nakasulat sa Rust ang tumugma sa gawi ng CPython sa 99.95% ng 1.7 million-plus na randomized na mga programa.
💬 Comments
No comments yet. Be the first!