Путь к совершенному ПО: Искусственный интеллект в автоматической формальной верификации

При написании высококачественного программного обеспечения не обойтись без этапа формальной верификации. Несмотря на то, что наша жизнь уже была в некоторой степени упрощена, благодаря таким помощникам доказательства как Coq и Isabelle/HOL, обучающим модель предсказывать один шаг доказательства за раз, оптимизация формальной верификации еще не была достигнута. 

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

Baldur превосходит все существующие подходы, он может самостоятельно полностью за раз доказывать 47.9% теорем, и даже этот результат – не предел.

В данной статье я познакомлю Вас со всей теоретической и практической подноготной данной модели, этапами реализации и оценки метода, чтобы стать чуточку ближе к созданию идеального ПО!

Приятного прочтения :)

1. Введение

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

Например, CompCert, компилятор языка С, проверенный с помощью интерактивного теоретического анализатора Coq, оказался единственным компилятором из списка, включающего общеизвестные GCC и LLVM, в котором всестороннее исследование не нашло ошибок.

Coq – это интерактивная оболочка для доказательства теорем, в которой используется собственный функциональный язык программирования с зависимыми типами – Gallina.

GCC (GNU Compiler Collection) – это свободный компилятор, разработанный проектом GNU. Он поддерживает множество языков программирования, включая C, C++, Java, Fortran и другие. GCC позволяет преобразовывать исходный код на этих языках в машинный код, который может выполняться на различных архитектурах процессоров. GCC также предоставляет набор инструментов для оптимизации кода, создания статических и динамических библиотек и т. д.

LLVM (Low Level Virtual Machine) – это набор компиляторов и инструментов для разработки программного обеспечения с открытым исходным кодом. Он предоставляет модульную и гибкую архитектуру, которая позволяет разработчикам создавать собственные компиляторы, оптимизаторы и другие инструменты. LLVM имеет собственный набор инструкций, называемый LLVM-IR (Intermediate Representation), который является промежуточным представлением кода, используемым для оптимизации и генерации машинного кода.

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

Существует два многообещающих подхода к автоматизации синтеза доказательств. Первый – использование инструмента Sledgehammer для доказательств в Isabelle.

"Sledgehammer" – это подсистема доказательного помощника (proof assistant) Isabelle/HOL, которая выполняет доказательства, используя готовые автоматические теоремные средства. Она эвристически выбирает несколько фактов – лемм, определений или аксиом – из тысяч, доступных в фоновых библиотеках и формализации пользователя, переводит задачу в символику теоремных средств, запускает теоремные средства и восстанавливает все найденные ими доказательства в Isabelle.

Второй подход – использование нейронных теоретических анализаторов, основанных на поиске, таких как DeepHOL, GPT-f, TacticZero, Lisa, Evariste, Diva, TacTok и ASTactic. Получив частичное доказательство и текущее состояние доказательства (которое состоит из текущей цели и списка известных предположений), эти инструменты используют нейронные сети для предсказания следующего индивидуального шага доказательства. Они используют proof assistant для оценки предложенных следующих шагов доказательства, что возвращает новый набор состояний доказательства.

В данной работе исследователи предлагают более простой подход к синтезу доказательств – Baldur. Основным принципом является использование больших языковых моделей (LLM), с помощью которых возможно создавать полноценные доказательства для теорем. 

LLM – это масштабированные модели-трансформеры, обученные на большом объеме текстовых данных, включающих естественный язык и код, которые показали удивительную эффективность во множестве приложений, включая ответы на вопросы, генерацию текста и кода. 

Baldur спроектирован так, чтобы он мог работать с любыми внутренними LLM. Реализация оценивается на двух версиях Minerva, одна с 8 миллиардами параметров, а другая с 62 миллиардами параметров (параметры — это переменные, присутствующие в модели и изменяющиеся в процессе обучения).

Minerva – языковая модель, представленная Google, обученная дополнительным 118 гигабайтам научных статей и основанная на другой, более масштабной (540 миллиардов параметров), языковой модели – Pathways (PaLM).  

Baldur оценивался на наборе данных, содержащем теоремы помощника Isabelle/HOL и их доказательства. Набор данных состоит из 183 000 теорем, из которых используются 6 336 для измерения эффективности.

Результаты оценки следующие:

1. Baldur (без дополнительных настроек или исправлений) способен полностью автоматически генерировать целые доказательства для 47.9% теорем, в то время как подходы, основанные на поиске, доказывают 39.0% теорем.

2. LLM могут исправлять доказательства, включая свои собственные ошибочные попытки доказательства, в связи с чем, Baldur доказывает дополнительные 1,5% теорем при наличии доступа к предыдущей ошибочной попытке доказательства и сообщениям об ошибках.

3. Контекстное обучение удивительно эффективно при доказательстве теорем на основе LLM, поэтому с помощью контекста Baldur доказывает 47,5% теорем, а без контекста - только 40,7% при том же размере модели.

Кроме того, ансамбль из 10 различных тонко настроенных моделей Baldur доказывает 58,0%.

Эти результаты будут подробнее рассмотрены ниже :)

2. Подход “Baldur”

Предыдущие подходы к синтезу доказательств используют нейронную модель для прогнозирования следующего шага доказательства на основе текущего состояния доказательства. Прогнозы шагов доказательства затем определяют стратегию поиска, к ней могут относиться: 

1. “best-first search” (поиск по первому наилучшему совпадению – алгоритм поиска, исследующий граф путём расширения наиболее перспективных узлов, выбираемых в соответствии с указанным правилом; он использует эвристику для руководства поиском, в качестве эвристики он выбирает оценку затрат для достижение цели) 

2. “depth-first search” (поиск в глубину – один из методов обхода графа, данная стратегия состоит в том, чтобы идти «вглубь» графа, насколько это возможно)

Во время поиска proof assistant должен проверять каждый прогноз шага доказательства, чтобы определить его допустимость. Это означает, что для существующих инструментов синтеза доказательств требуется тесное взаимодействие между нейронной сетью и “помощником”. По мере того как мы переходим к использованию LLM, это приводит к созданию сложных систем, поскольку LLM необходимо запускать на специализированном оборудовании (GPU (графический процессор, обрабатывающий данные быстрее, так как задачи выполняет параллельно, а не последовательно, как CPU) или TPU (тензорный процессор, предназначенный для тренировки нейросетей)), в то время как для помощника требуется CPU (процессор общего назначения, основанный на архитектуре фон Неймана).

В данной работе рассматривается более простой, но эффективный метод: настройка LLM для генерации полных доказательств. Это упрощение позволяет избежать детализированного взаимодействия между нейронной моделью и помощником, позволяя запускать задачи генерации доказательств и проверки полностью отдельно друг от друга. Кроме уменьшения сложности, это также может улучшить эффективность, потому что (1) это позволяет использовать большие размеры пакетов, что значительно улучшает использование аппаратного обеспечения во время вывода, и (2) при предоставлении дополнительного контекста модели, контекст теперь не нужно перерабатывать для каждого шага доказательства, а только один раз для всего доказательства. 

Создатели Baldur настраивали LLM на доказательных данных для генерации целых доказательств и изучали влияние предоставления LLM дополнительной информации. Данный подход и реализация включают следующее:

1. LLM настраивается для генерации полного доказательства только на основе утверждения теоремы. Эту модель называют моделью генерации доказательства (Раздел 2.1).

2. Модели предоставляется попытка доказательства, которая не прошла проверку, вместе с соответствующим сообщением об ошибке от помощника, чтобы модель могла попытаться найти лучшее доказательство. Эта модель называется моделью восстановления доказательства (Раздел 2.2).

3. Предоставляется текст из того же файла с теорией, из которого была взята проблема. Добавляются только те строки из файла теории, которые непосредственно предшествуют теореме, которую мы хотим доказать. Эту добавленную информацию называют контекстом файла теории и добавляют ее в модель генерации доказательства (Раздел 2.3).

4. LLM, настраиваемые и лежащие в основе всего этого, – Minerva, которая предварительно обучена на корпусе математических данных (Раздел 2.4).

Настроенные LLM и их взаимодействие с помощником Isabelle составляют инструмент Baldur. Далее подробно рассматривается подход Baldur, который включает создание обучающих наборов данных и использование LLM для генерации и восстановления доказательств.

2.1. Генерация доказательств 

Повторюсь, что Baldur генерирует доказательства целиком, вместо пошагового доказательства, это продемонстрировано на рисунке ниже. 

Здесь используется утверждение теоремы, как входные данные для предсталвенной модели генерации доказательств. Затем выбирается попытка доказательства из этой модели и выполняется проверка с помощью Isabelle. Если Isabelle принимает попытку доказательства без ошибок, то теорема считается доказанной. В противном случае есть возможность попробовать выбрать другую попытку доказательства из модели.

Пример: для демонстрации подхода генерации доказательств с помощью инструмента Baldur, рассмотрим теорему fun_sum_commute. 

Эта теорема утверждает, что для аддитивной функции