Хиймэл оюунаар код бичих үйл явцыг илүү найдвартай болгохын тулд албан ёсны баталгаажуулалтын аргачлалыг ашиглах хандлага нэмэгдэж байна.
Apple компанийн аюулгүй байдлын баг “corecrypto” санд хийсэн шинжилгээгээр уламжлалт аргаар илрүүлэх боломжгүй цоорхойг математик баталгаажуулалтын тусламжтайгаар олж илрүүлснээ мэдэгдсэн байна. Гэсэн хэдий ч тус компани шинэ код нэмэхдээ хяналт шалгалтын хурдыг алдагдуулахгүйн тулд маш болгоомжтой хандах шаардлагатай байгааг онцолжээ.
Нээлттэй эхийн төслүүд дээр ажилладаг хөгжүүлэгчид хиймэл оюуны тусламжтайгаар код баталгаажуулах туршилтуудыг эрчимтэй хийж байна. Тухайлбал, Beneficial AI Foundation сан Anthropic компанийн буцалтгүй тусламжийн хүрээнд шифрлэлтийн кодыг шалгах ажлыг гүйцэтгэжээ. Гэвч энэ салбарын мэргэжилтнүүд хиймэл оюуны компаниудын сайн дурын тусламжид найдах нь эрсдэлтэй бөгөөд тогтвортой санхүүжилтийн тогтолцоо шаардлагатай байгааг анхааруулж байна.
Мадан Мусувати тэргүүтэй шинэ гарааны компаниуд хиймэл оюуны тусламжтайгаар програм хангамжийн төлөв байдлыг тодорхойлох, Lean, Rocq, Isabelle зэрэг математик хэрэгслээр дамжуулан кодыг шалгах автоматжуулсан шийдлүүдийг хөгжүүлж байна. Энэ нь хиймэл оюуныг халдагчдын гарт орохоос сэргийлж, аюулгүй байдлыг сайжруулахад чухал ач холбогдолтой юм.
Proofcraft зэрэг уламжлалт баталгаажуулалтын үйлчилгээ үзүүлэгч компаниуд эрэлт хэрэгцээ огцом нэмэгдэж байгааг мэдээлж байна. Гэвч шинжээчид хиймэл оюунаар үүсгэсэн кодод хэт итгэх нь эрсдэл дагуулж болзошгүйг анхааруулж, энэхүү нарийн төвөгтэй ажлыг оньсого таахтай адилтган сонирхолтой болохыг дурджээ.
Дэлгэрэнгүйг эх сурвалжаас харах
↓Эх сурвалжийг нээх ↓
Earlier this year, Apple’s security team said that some of the issues formal verification uncovered in its “corecrypto” library, which is used for encryption, could not have been found any other way. But the company added that it has to be “conservative” when adding new code to corecrypto to ensure it can keep pace with reviewing it.
Two cybersecurity executives at major companies that haven’t formally verified any code say they aren’t sure whether automation will make it worthwhile. But the executives, who weren’t authorized to speak publicly, say they could imagine paying major AI labs for “verified” AI-generated code.
Developers of open source software projects, which are the bedrock of many apps, are increasingly experimenting with AI-aided verification. The nonprofit Beneficial AI Foundation used a grant from Anthropic to validate the same encryption code this year as Sun did at Stanford. Michael Rosenberg, a maintainer of the library known as curve25519-dalek, hopes sustainable funding emerges for ongoing verification efforts. “I have no ideas as to how that’s going to happen, though, and we certainly shouldn’t rely on the goodwill of the AI companies,” he says.
Some of the startups eager to expand verification also aren’t sure whether to deploy their tools directly to customers or through intermediaries like Anthropic. Their general plan is to use AI to automate much of the work involved in defining how a program is supposed to behave. For example, specifications for a data table might require that it contain the same items before and after sorting, just in a different order. Further automation efforts, which may not involve AI, would translate that code into a format that math tools like Lean, Rocq, and Isabelle can use to check whether the code works as intended.
Another recent entrant to the formal verification field is Madan Musuvathi, who left Microsoft Research after more than 20 years to found the startup Truidic. After incidents like the OpenAI hack of Hugging Face, he felt there was an urgent need to commercialize his studies. “AI in the hands of attackers can be extremely powerful,” Musuvathi says, but verification can “make AI safe and secure for everyone, everywhere.”
Proofcraft, one of the few companies that has long offered traditional verification, says growing excitement about the process is translating into a flood of inquiries from potential customers. June Andronick, the company’s CEO, and Gerwin Klein, its chief scientist, say interest easily outpaces what they and their competition can provide.
But both worry that AI-generated specifications could inspire “unjustified trust” in the results. Verifiers are also eager to preserve the joy their work brings them. Klein calls it “pretty addictive, like a puzzle game.” If all goes well, he’ll be doing more solving than ever.
