Изследователката от Станфорд Чуйуе Сун и нейните колеги компютърни специалисти разработиха инструмент с изкуствен интелект, който завърши инженерен проект за по-малко от половин ден и срещу под 500 долара — в сравнение с петте месеца, необходими на трима висококвалифицирани експерти да свършат същата работа ръчно. Драстичното намаляване на времето и разходите, за което Сун съобщи в неотдавнашна научна публикация, е сред първите резултати, които възраждат малко позната област на програмирането и математиката, известна като формална верификация.

В продължение на десетилетия разработчиците са си представяли използването на математика, за да докажат, че техният софтуер не съдържа грешки. Този процес е дълъг и трудоемък, изискващ от инженерите да съставят прецизни твърдения за целите на своя софтуер и да преобразуват кода си във формули, които могат да бъдат валидирани. Въпреки че компаниите вече прилагат усъвършенствани тестове за идентифициране на възможно най-много дефекти в своите програми, те рядко отделят средства за формална верификация, която може да улови още по-непредвидимо поведение.

Сега вълна от стартъпи залага на това, че генеративният изкуствен интелект ще направи формалната верификация на софтуер едновременно практична и жизненоважна. Сред тях е &Truth, към която Сун се присъедини през август и която стартира публично в четвъртък. Изследването на Сун демонстрира потенциала на технологията чрез използване на изкуствен интелект за верифициране на част от кода, който криптира разговорите в приложението за съобщения Signal.

„Мостовете и сградите не се срутват, защото хората правят математически изчисления преди изграждането им“, казва Иля Сергей, главен научен директор на &Truth. „Защо не направим същото и за кода? Технологията за математическо разсъждаване беше налице, просто беше трудно да се мащабира.“

&Truth привлече 70 милиона долара от инвеститори и има за цел в крайна сметка да верифицира всеки език за програмиране. Конкурентът Harmonic, съоснован от изпълнителния директор на Robinhood Влад Тенев и получил финансиране от 295 милиона долара, обяви тази седмица, че неговият математически насочен AI агент Aristotle поддържа верификация на софтуер, написан на C, и хардуерни проекти на Verilog. Компанията оценява технологията с потенциални потребители, включително производителите на чипове Tensordyne и Nvidia, чието подразделение за рисков капитал е сред инвеститорите на стартъпа.

Само преди седмица Anthropic и стартъпът за верификация Theorem съвместно обявиха, че са използвали изкуствен интелект за откриване на грешки в софтуер с отворен код, които трилиони тестове не са успели да засекат. Те представиха и добавка за Claude, която да помага на други разработчици при верификацията. Разходите за първоначалния проект не бяха оповестени.

Голямото обещание е бъдеще, в което софтуерът работи по-надеждно и с по-малко главоболия, свързани със сигурността. Но дали изкуственият интелект ще успее да изведе формалната верификация отвъд най-критичните системи в организации като НАСА и Apple и да я превърне в широко разпространена практика, остава открит въпрос.

Технологията все още е на етап прототип. Въпреки че търсенето е голямо, не е ясно колко са готови да платят клиентите и как предпочитат да внедрят технологията. Формалната верификация разчита на допускания за това как компютрите и хората взаимодействат със софтуера, а някои експерти са скептични относно способността ѝ да улавя грешки, произтичащи от потребителски пропуски или хардуерни повреди.

Уил Уилсън, ръководител на стартъпа за софтуер с изкуствен интелект за откриване на грешки Antithesis, нарича формалната верификация „капан“ за математически маниаци като него самия. Antithesis е похарчила милиони долари за формална верификация на част от защитите си за киберсигурност — процес, който Уилсън описва като „изключително досаден“. Въпреки това стартъпът открива допълнителни грешки с помощта на собствения си инструмент, а Antithesis е намирала дефекти и в софтуер, който няколко от клиентите ѝ са верифицирали формално. „Това може да ви даде известна сигурност, но само стабилното изчерпателно тестване може да докаже, че тази сигурност е реална“, казва Уилсън.

Или както Виталик Бутерин, инженерът, известен със създаването на криптовалутата Ethereum, написа в публикация в блога си по-рано тази година: „формалната верификация не е панацея“. Въпреки това той и други поддръжници на подхода вярват, че тя ще бъде важна защита срещу AI системи, извършващи кибератаки и предизвикващи хаос.

Базова сигурност

Самолетите на Boeing, сървърите на Amazon и над 2,5 милиарда активни устройства на Apple съдържат поне част от формално верифициран софтуер според публични данни на компаниите. Въпросният код обикновено е свързан със сигурността, а уязвимости в него биха могли да нанесат сериозни вреди при експлоатация.

Байрън Кук, водещ учен и вицепрезидент в Amazon Web Services, заявява, че формалната верификацията е намалила опасенията на клиентите относно облачната сигурност и е помогнала на вътрешните екипи да работят по-бързо, като елиминира сериозните грешки още на ранен етап.

Няколко средни по размер технологични компании обаче споделят пред WIRED, че обикновено верифицират най-много една ключова функция от своите продукти, ако изобщо правят това. Те посочват като причини липсата на инженери по верификация, разходите, които надвишават потенциалните рискове, и може би най-важното — опасенията, че чакането с седмици за формална верификация на код може да забави иновациите.

По-рано тази година екипът по сигурност на Apple съобщи, че част от проблемите, които формалната верификация е разкрила в библиотеката „corecrypto“ (използвана за криптиране), не биха могли да бъдат открити по никакъв друг начин. От компанията обаче допълниха, че трябва да подхождат „консервативно“ при добавянето на нов код към corecrypto, за да са сигурни, че могат да поддържат темпото на прегледа му.

Двама ръководители по киберсигурност в големи компании, които не са верифицирали формално никакъв код, споделят, че не са сигурни дали автоматизацията ще направи процеса оправдан. Въпреки това ръководителите, които нямат разрешение да говорят публично, заявяват, че биха могли да си представят да плащат на водещи AI лаборатории за „верифициран“ код, генериран от изкуствен интелект.

Разработчиците на софтуерни проекти с отворен код, които са в основата на множество приложения, все по-често експериментират с верификация, подпомагана от изкуствен интелект. Организацията с нестопанска цел Beneficial AI Foundation използва безвъзмездни средства от Anthropic, за да валидира същия криптографски код тази година, както направи Сун в Станфорд. Майкъл Розенбърг, поддържащ библиотеката, известна като curve25519-dalek, се надява да се появи устойчиво финансиране за постоянни усилия по верификация. „Нямам представа как ще се случи това обаче и със сигурност не бива да разчитаме на добрата воля на AI компаниите“, казва той.

Някои от стартъпите, които имат желание да разширят верификацията, също не са сигурни дали да предоставят инструментите си директно на клиентите, или чрез посредници като Anthropic. Техният общ план е да използват изкуствен интелект за автоматизиране на голяма част от работата по дефинирането на това как се очаква да се държи една програма. Например спецификациите за таблица с данни може да изискват тя да съдържа същите елементи преди и след сортиране, но в различен ред. По-нататъшните усилия за автоматизация, които може да не включват изкуствен интелект, биха превели този код във формат, който математически инструменти като Lean, Rocq и Isabelle могат да използват, за да проверят дали кодът функционира по предназначение.

Друг скорошен участник в областта на формалната верификация е Мадан Мусувати, който напусна Microsoft Research след повече от 20 години, за да основе стартъпа Truidic. След инциденти като компрометирането на Hugging Face от страна на OpenAI, той усеща спешна нужда да комерсиализира научните си разработки. „Изкуственият интелект в ръцете на атакуващи може да бъде изключително мощен“, казва Мусувати, но верификацията може „да направи изкуствения интелект надежден и защитен за всички и навсякъде“.

От Proofcraft, една от малкото компании, които отдавна предлагат традиционна верификация, споделят, че нарастващото вълнение около процеса води до наплив от запитвания от страна на потенциални клиенти. Джун Андроник, главен изпълнителен директор на компанията, и Гервин Клайн, неин главен научен директор, казват, че интересът лесно надхвърля това, което те и техните конкуренти могат да осигурят.

Но и двамата се притесняват, че генерираните от AI спецификации биха могли да вдъхнат „неоправдано доверие“ в резултатите. Специалистите по верификация също така държат да запазят удовлетворението, което работата им носи. Клайн я нарича „доста пристрастяваща, като пъзел игра“. Ако всичко върви добре, той ще решава повече задачи от всякога.