Накратко
Формалната верификация превежда твърдение - математическо доказателство или поведение на програма - на език, който машина може да провери ред по ред. Системи като Lean, Coq и Isabelle не приемат почти вярно: липсва ли една стъпка, цялото доказателство не минава. Затова формално проверен резултат не зависи от това кой го е написал - човек, екип или AI модел.
Разликата с обикновената проверка е като между дегустатор и везна. Дегустаторът е опитен, но е човек: уморява се, пропуска, понякога му се иска резултатът да е верен. Везната не иска нищо. Показва каквото е.
Точно затова формалната верификация става важна в ерата на моделите. Текст от модел може да звучи безупречно и да е грешен по средата. Мине ли през Lean, въпросът кой го е писал спира да съществува. Проверена стъпка е проверена стъпка.
Не вярвай на автора. Не вярвай и на машината. Вярвай на проверката, която не приема почти.
Къде я срещаш
В математиката, когато резултат от AI система търси легитимност. В критичния софтуер: авионика, медицински устройства, ядрото на операционна система. И все по-често в разговора за AI безопасност - като единственият вид отговор, който не зависи от честността на този, който отговаря.
Първоизточници
Lean: официалният сайт на доказващата системаВизуалът е генериран код-арт, без чужди изображения.