Unit Test хангалтгүй болсон үед: Google AI-ийн бичсэн аюулгүй байдлын дүрмийг Z3-аар математик аргаар батлах CEL Formal Verification-ийг танилцууллаа

Программ хангамж болон дэд бүтцийн хөгжүүлэлтэд AI агентууд хүч түрэн орж ирж, кодын логик бичихээс гадна хандалтын удирдлага (IAM), сүлжээний хамгаалалт, Kubernetes-ийн кластерын бодлогыг (Policy) бие даан өөрчилдөг боллоо. Гэвч үүнтэй зэрэгцэн нэгэн том эрсдэл гарч ирсэн нь: AI агент дэд бүтцийн дүрмийг өөрчлөхдөө өчүүхэн л логик цоорхой үлдээвэл түүнийг уламжлалт Unit Test барьж чадах уу?

Хариулт нь "Үгүй". Хязгааргүй олон боломжит оролтоос хэдхэн тест кэйсээр шалгадаг уламжлалт арга барил агентуудын үүсгэсэн нарийн хийдлийг алдаж, production орчинд нөхөж баршгүй хохирол дагуулах эрсдэлтэй.

Энэхүү тулгамдсан асуудлыг шийдвэрлэхийн тулд Google компани өргөн хэрэглэгддэг Common Expression Language (CEL) хэлэндээ зориулан математикийн хатуу баталгаанд суурилсан CEL Formal Verification Framework-ийг нээлттэй эхээр зарлалаа.

Асуудал юунд байв? Unit Test-ийн хязгаарлалт

Орчин үеийн Cloud Native экосистемд (тухайлбал Kubernetes Validating Admission Policies, Envoy Proxy, Firebase Security Rules, Google Cloud IAM) дэд бүтцийн зөвшөөрөл, дүрмийг тодорхойлоход CEL хэлийг стандартын түвшинд ашигладаг.

AI агент одоо байгаа CEL дүрмийг илүү цэгцтэй болгох (refactor) эсвэл шинэ хязгаарлалт нэмэх үед өөрийн зохиосон 10-20 ширхэг Unit Test-ийг амжилттай давуулж болно. Гэвч тестийн хүрээнээс гадуурх тодорхой өгөгдлийн хослол (жишээ нь, операторын эрэмбэ буруу тооцогдох, port range-ийн захын утга алдагдах, бүхэл тооны overflow үүсэх) дээр дүрэм буруу ажиллаж, зөвшөөрөлгүй хүсэлтийг систем рүү нэвтрүүлдэг.

Тестийн хувьд True гарсан ч бодит ертөнц дэх бүх боломжит оролтын огторгуйд (infinite input space) дүрэм үнэн эсэхийг туршилтаар биш зөвхөн математик баталгаагаар л нотлох боломжтой.

Шийдэл: Z3 Prover ба Математик Баталгаа

Google энэхүү асуудлыг шийдэхийн тулд алдарт Microsoft Z3 Theorem Prover (SMT Solver)-ийг CEL хэлтэй холбожээ.

CEL Formal Verification нь хөгжүүлэгчийн болон AI агентын бичсэн дүрмийг математик тэгшитгэл, логик хэлбэрт хөрвүүлж дараах 3 гол түвшний шалгалтыг автомат хийдэг:

1. Equivalence Checking (Дүйцлийн баталгаа)

AI агент хуучин дүрмийг шинэчлэн оновчлох (refactor) үед шинэ дүрэм нь хуучин дүрмийнхээ бүх боломжит төлөвтэй ЯГ ТАГ ижил үр дүн өгч чадаж буй эсэхийг 100% математик аргаар шалгана. Хэрэв нэг л нөхцөлд үр дүн зөрсөн бол уг гажуудлыг үүсгэж буй тодорхой оролтын утгыг шууд зааж өгнө.

2. Validity & Safety Invariant Checking

Дүрэм ямар ч үед тооцооллын алдаа (evaluation error) гаргахгүй байх, assume болон assert нөхцөлүүд бүх төлөвт биелж буйг батална. Жишээ нь: "Ямар ч нөхцөлд isAdmin == false хэрэглэгч систем рүү бичих эрх авах боломжгүй" гэсэн аксиомыг бүх оролтын хувьд математикаар нотолдог.

3. Edge-case / Operator Precedence цоорхойг илрүүлэх

CEL дээр && болон || үйлдлүүдийн эрэмбийг хаалт дутуу хийснээс шалтгаалан хүний нүд болон энгийн тестэнд анзаарагдахгүй өнгөрдөг аюулгүй байдлын цоорхойг уг хэрэгсэл хэдхэн миллисекундын дотор барьж, counter-example буюу алдааг өдөөх бодит өгөгдлийг гаргаж ирнэ.

AI эрин үеийн CI/CD: "Proof-as-Code"

Энэхүү шинэ хэрэгсэл нь интерактив REPL горимоор ажиллахаас гадна шууд хөгжүүлэлтийн CI/CD пайплайн руу интеграци хийгдэх боломжтой.

Хөгжүүлэгчид болон DevOps инженерүүд одоо AI агентад "Манай Kubernetes Validating Admission Policy-г шинэчил" гэсэн даалгавар өгөөд, гарч ирсэн PR (Pull Request)-ийг шалгахдаа зөвхөн хөгжүүлэгчийн нүдээр харах бус, Z3 Proof Runner-аар "FAIL / PASS" үнэлгээ хийлгэх хамгаалалтын давхаргыг үүсгэх боломжтой боллоо. Хуурамч алдааны мэдээлэл (false positives) үүсгэхээс сэргийлж "three-pass taint tracking" архитектурыг ашигласан тул танай CI пайплайныг үндэслэлгүйгээр гацаахгүй.

Дүгнэлт: Хөгжүүлэгчдэд ямар сургамж авчрах вэ?

AI кодинг агентууд улам хүчирхэгжиж байгаа өнөө үед хөгжүүлэлтийн дараагийн том давалгаа нь зүгээр л кодоо хурдан бичих биш, харин AI-ийн бичсэн эгзэгтэй кодын найдвартай байдлыг батлах (Verification Layer) дээр төвлөрч байна.

Google-ийн энэхүү нээлттэй төсөл нь цаашид бусад хэл, системийн түвшинд ч Formal Verification (албан ёсны математик баталгаажуулалт) улам бүр өдөр тутмын хөгжүүлэгчийн салшгүй багаж болохыг харууллаа.

Эх сурвалж: Google Open Source Blog: "Securing the agentic era: Introducing formal verification for CEL" (Sean Huh, Common Expression Language Team)