Et nyt open source-projekt præsenterer, hvad skaberen betegner som den første formelt verificerede implementation af en 3D constructive solid geometry (CSG) operation – mesh intersection. Projektet er skrevet i Lean 4 og verificeret mod en kompakt specifikation på blot 93 linjer, der fastlår overfladen af det resulterende mesh og garanterer praktiske velformethedsbetingelser for trianguleringen, ifølge projektets beskrivelse.
Det interessante er ikke kun den tekniske bedrift, men hvad den betyder for tillid til AI-genereret kode. I stedet for at mennesker skal gennemgå tusindvis af linjer AI-skrevet implementation – her over 1000 linjer – kan en reviewer nøjes med at læse specifikationen og køre Lean-checkeren. AI'en har autonomt skrevet over 60.000 linjer Lean-beviser, som heller aldrig behøver menneskelig inspektion. Lean garanterer overensstemmelse med specifikationen ved kompilering, uden at der lægges nogen tillid i LLM'en. Som skaberen skriver: "This allows us to treat the implementation and proofs as a black box."
For beslutningstagere og professionelle, der overvejer at bruge AI-genereret kode i produktionssammenhænge, er dette et konkret eksempel på en ny arbejdsgang: i stedet for at stole på AI'ens output, stoler man på en formel specifikation og en bevischecker. Det kan dramatisk reducere risikoen ved at anvende AI-kode i kritiske systemer – fra CAD-software til robotstyring. Projektet inkluderer også en web-demo, der kører den verificerede kerne kompileret til WebAssembly.
