70 milijonų dolerių startuolis gavo programų teisingumui įrodyti

70 milijonų dolerių pradinį finansavimą gavęs startuolis „&Truth“ kuria technologiją, kuri matematiniu būdu tikrintų, ar programos atitinka nustatytus reikalavimus. Spalio 29 dieną apie bendrovę parašęs „Wired“ nagrinėja, ar DI galėtų tokį ilgai užtrunkantį tikrinimą padaryti plačiau pritaikomą.

Formalusis tikrinimas skiriasi nuo įprastų programų testų: jis siekia įrodyti tiksliai aprašytas savybes, o ne vien patikrinti pasirinktus pavyzdžius. Leidinys pabrėžia, kad procesas priklauso nuo teisingai suformuluotų reikalavimų ir prielaidų, todėl savaime nėra garantija nuo visų įmanomų klaidų.

„Wired“ pateikia Stanfordo tyrėjos Chuyue Sun ir kolegų darbą, kuriame DI padėjo užbaigti projektą greičiau nei per pusę paros. Skaičiavimai kainavo mažiau kaip 500 dolerių, o anksčiau panašiam darbui trys aukštos kvalifikacijos specialistai skyrė penkis mėnesius, rašo leidinys.

Tas projektas apėmė dalį kodo, naudojamo „Signal“ pokalbiams šifruoti, todėl rezultatas nėra visos programėlės ar visos jos infrastruktūros patikra. Sun rugpjūtį prisijungė prie „&Truth“, kuri tikisi ilgainiui galėti tikrinti įvairiomis programavimo kalbomis parašytą kodą, nurodo „Wired“.

Oficialiame spalio 29 dienos pranešime „&Truth“ skelbia buvusi įkurta 2026 metų pradžioje ir veikianti Palo Alte bei Singapūre. Tarp įkūrėjų yra Stanfordo profesorius Clark Barrett, formaliojo tikrinimo tyrėjas Ilya Sergey ir bendrovės vadovas bei vykdomasis pirmininkas Chris Hsu.

Bendrovė remiasi atvira įrodymų sistema „Lean“ ir kitomis technologijomis, siekdama verslo reikalavimus paversti tiksliais formaliais aprašymais, teigiama jos pranešime. Technologijos pažadai dar nereiškia visuotinai prieinamo produkto, o „Wired“ pažymi, kad didelė dalis šios rinkos sprendimų tebėra prototipų stadijoje.

Leidinys aprašo ir konkurentę „Harmonic“, kurios kuriamas matematinis DI agentas „Aristotle“ pradėjo palaikyti C kalbos programas bei „Verilog“ aparatinės įrangos aprašymus. Bendrovė, surinkusi 295 milijonus dolerių finansavimo, technologiją vertina kartu su galimais klientais, tarp kurių minimos lustų kūrėjos „Tensordyne“ ir „Nvidia“.

Kritikai „Wired“ primena, kad net matematiškai patikrintos sistemos gali turėti klaidų, jeigu tikrinamas aprašymas neapima svarbios realaus naudojimo aplinkybės. „Antithesis“ vadovas Will Wilson pasakoja, jog jo bendrovė papildomų klaidų aptiko net po milijonus dolerių kainavusio dalies apsaugos tikrinimo.

„Proofcraft“ vadovė June Andronick ir vyriausiasis mokslininkas Gerwin Klein leidiniui taip pat išreiškia nerimą dėl nepagrįsto pasitikėjimo DI parašytomis specifikacijomis. Šis apribojimas palieka vietos testavimui ir žmogaus darbui net tada, kai paties matematinio įrodymo patikra gali būti automatizuota.

Toliau „&Truth“ ketina plėsti Singapūro komandą ir paskelbti pagrindines bibliotekas atviru kodu, nurodoma oficialiame bendrovės pristatymo pranešime. „Wired“ dar palieka atvirą komercinį klausimą: kiek klientai už tokį tikrinimą mokės ir ar paslaugas pirks tiesiogiai, ar per didžiąsias DI laboratorijas.