ИИ учится доказывать корректность программ. Этой задачей мы в НГУ занимались ещё в 1990 году

Генеральный директор Robinhood — американской финансово-технологической платформы для инвестиций — и сооснователь Harmonic, разрабатывающей ИИ для формальной верификации, Влад Тенев заявил, что через два года весь программный код будет проходить формальную верификацию — математическую проверку соответствия заданным требованиям.

Harmonic развивает Aristotle — систему, которая применяет ИИ для построения математических доказательств корректности программ и аппаратных решений.

Читаю — и вспоминаю университет.

В 1990 году в Новосибирском государственном университете я начал заниматься этой темой под руководством Валерия Александровича Непомнящего. Учился по книге «Прикладные методы верификации программ», вышедшей в 1988 году. Он написал её в соавторстве с О. М. Рякиным под редакцией академика А. П. Ершова.

Готовя этот материал, я узнал, что Валерий Александрович ушёл из жизни в 2021 году. С благодарностью вспоминаю своего учителя.

Математически проверять программы нас учили уже тогда. Что же изменилось с появлением ИИ?

Представьте банковский перевод.

Вы отправили 10 тысяч тенге, приложение зависло, и вы снова нажали кнопку. Деньги должны уйти один раз.

При тестировании разработчики воспроизводят разные ситуации: повторное нажатие, потерю связи, одновременные запросы. Проверяют, правильно ли работает программа.

Формальная верификация позволяет поставить более строгую задачу: доказать, что при точно описанных условиях один платёж не может быть списан дважды.

Это условный пример, но он показывает принцип: проверка выбранных ситуаций и доказательство для всех случаев в заданных условиях — разные вещи.

Однако такое доказательство нужно построить. Точно сформулировать требования, описать поведение программы, найти промежуточные утверждения. Всё это требует времени и квалификации. Непомнящий и его коллеги уже тогда занимались автоматизацией этой работы.

Что изменилось сегодня?

ИИ помогает искать доказательства. Он предлагает варианты рассуждений, а специальный формальный механизм проверяет их математическую корректность. Ошибочные доказательства не принимаются.

Aristotle работает непосредственно с исходным кодом. Система предлагает свойства, которые можно проверить, показывает, какие из них удалось доказать, какие остались неподтверждёнными и на каких предположениях основан результат. Инженер должен проверить и сами свойства, и эти предположения.

Сейчас Harmonic заявляет поддержку программ на C и аппаратных описаний на Verilog. Возможный эффект — сделать формальную верификацию доступнее большему числу команд разработки.

Но обещание проверить «весь код за два года» я бы воспринимал осторожно. Сам Тенев говорит о постепенном распространении технологии: сначала на критически важный код, затем на более широкий круг программ.

И здесь есть принципиальный момент.

Вернёмся к банковскому переводу. Можно доказать, что конкретная функция не допускает повторного списания при заданных условиях, но при этом не проверить, тому ли получателю уйдут деньги.

Доказательство отвечает на тот вопрос, который ему поставили. Если требования сформулированы неполно, математически безупречное доказательство не спасёт от ошибки в самой постановке задачи.

Поэтому человеку по-прежнему нужно понимать, какие требования важны и что осталось за пределами проверки.

В 1990 году мы учились ставить задачу так, чтобы корректность программы можно было доказать. Сегодня ИИ помогает найти само доказательство. Но решать, какие свойства действительно важны, по-прежнему приходится человеку.

Источники:

Заявление Влада Тенева — X

Harmonic — Aristotle: верификация программ и аппаратуры

Документация — Aristotle: верификация программ на C

Книга Непомнящего и Рякина — каталог МГТУ

Даурен Керейбаев - www.linkedin.com/in/dauren-kereibayev-59169461
Главный редактор REAL DIGITAL