При написании высококачественного программного обеспечения не обойтись без этапа формальной верификации. Несмотря на то, что наша жизнь уже была в некоторой степени упрощена, благодаря таким помощникам доказательства как 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 для измерения эффективности.
Результаты оценки следующие:
Baldur (без дополнительных настроек или исправлений) способен полностью автоматически генерировать целые доказательства для 47.9% теорем, в то время как подходы, основанные на поиске, доказывают 39.0% теорем.
LLM могут исправлять доказательства, включая свои собственные ошибочные попытки доказательства, в связи с чем, Baldur доказывает дополнительные 1,5% теорем при наличии доступа к предыдущей ошибочной попытке доказательства и сообщениям об ошибках.
Контекстное обучение удивительно эффективно при доказательстве теорем на основе LLM, поэтому с помощью контекста Baldur доказывает 47,5% теорем, а без контекста - только 40,7% при том же размере модели.
Кроме того, ансамбль из 10 различных тонко настроенных моделей Baldur доказывает 58,0%.
Эти результаты будут подробнее рассмотрены ниже :)
2. Подход “Baldur”
Предыдущие подходы к синтезу доказательств используют нейронную модель для прогнозирования следующего шага доказательства на основе текущего состояния доказательства. Прогнозы шагов доказательства затем определяют стратегию поиска, к ней могут относиться:
“best-first search” (поиск по первому наилучшему совпадению – алгоритм поиска, исследующий граф путём расширения наиболее перспективных узлов, выбираемых в соответствии с указанным правилом; он использует эвристику для руководства поиском, в качестве эвристики он выбирает оценку затрат для достижение цели)
“depth-first search” (поиск в глубину – один из методов обхода графа, данная стратегия состоит в том, чтобы идти «вглубь» графа, насколько это возможно)
Во время поиска proof assistant должен проверять каждый прогноз шага доказательства, чтобы определить его допустимость. Это означает, что для существующих инструментов синтеза доказательств требуется тесное взаимодействие между нейронной сетью и “помощником”. По мере того как мы переходим к использованию LLM, это приводит к созданию сложных систем, поскольку LLM необходимо запускать на специализированном оборудовании (GPU (графический процессор, обрабатывающий данные быстрее, так как задачи выполняет параллельно, а не последовательно, как CPU) или TPU (тензорный процессор, предназначенный для тренировки нейросетей)), в то время как для помощника требуется CPU (процессор общего назначения, основанный на архитектуре фон Неймана).
В данной работе рассматривается более простой, но эффективный метод: настройка LLM для генерации полных доказательств. Это упрощение позволяет избежать детализированного взаимодействия между нейронной моделью и помощником, позволяя запускать задачи генерации доказательств и проверки полностью отдельно друг от друга. Кроме уменьшения сложности, это также может улучшить эффективность, потому что (1) это позволяет использовать большие размеры пакетов, что значительно улучшает использование аппаратного обеспечения во время вывода, и (2) при предоставлении дополнительного контекста модели, контекст теперь не нужно перерабатывать для каждого шага доказательства, а только один раз для всего доказательства.
Создатели Baldur настраивали LLM на доказательных данных для генерации целых доказательств и изучали влияние предоставления LLM дополнительной информации. Данный подход и реализация включают следующее:
LLM настраивается для генерации полного доказательства только на основе утверждения теоремы. Эту модель называют моделью генерации доказательства (Раздел 2.1).
Модели предоставляется попытка доказательства, которая не прошла проверку, вместе с соответствующим сообщением об ошибке от помощника, чтобы модель могла попытаться найти лучшее доказательство. Эта модель называется моделью восстановления доказательства (Раздел 2.2).
Предоставляется текст из того же файла с теорией, из которого была взята проблема. Добавляются только те строки из файла теории, которые непосредственно предшествуют теореме, которую мы хотим доказать. Эту добавленную информацию называют контекстом файла теории и добавляют ее в модель генерации доказательства (Раздел 2.3).
LLM, настраиваемые и лежащие в основе всего этого, – Minerva, которая предварительно обучена на корпусе математических данных (Раздел 2.4).
Настроенные LLM и их взаимодействие с помощником Isabelle составляют инструмент Baldur. Далее подробно рассматривается подход Baldur, который включает создание обучающих наборов данных и использование LLM для генерации и восстановления доказательств.
2.1. Генерация доказательств
Повторюсь, что Baldur генерирует доказательства целиком, вместо пошагового доказательства, это продемонстрировано на рисунке ниже.
Здесь используется утверждение теоремы, как входные данные для предсталвенной модели генерации доказательств. Затем выбирается попытка доказательства из этой модели и выполняется проверка с помощью Isabelle. Если Isabelle принимает попытку доказательства без ошибок, то теорема считается доказанной. В противном случае есть возможность попробовать выбрать другую попытку доказательства из модели.
Пример: для демонстрации подхода генерации доказательств с помощью инструмента Baldur, рассмотрим теорему fun_sum_commute.
Эта теорема утверждает, что для аддитивной функции ?, для которой ?(0) = 0, и произвольной функции ?, применение функции ? к сумме множества, полученного применением функции ? к каждому элементу в данном множестве, равно сумме применения функции ?, за которым следует применение функции ?, к каждому элементу в этом множестве. Эта теорема взята из проекта в Archive of Formal Proofs под названием Polynomials, конкретно из файла Utils.thy. В ручном доказательстве, составленном человеком, делается различие между двумя случаями: когда множество конечно и когда оно не конечно. Для случая конечного множества используется индукция.
Если бы мы хотели вывести обучающий пример из этого примера, входные данные были бы утверждением теоремы, а целью было бы это ручное доказательство.
Baldur способен сгенерировать следующее правильное доказательство для данного утверждения:
Baldur распознает, что необходимо применить индукцию, и применяет специальное правило – “infinite_finite_induct”, следуя тому же общему подходу, что и ручное доказательство, но гораздо более кратко. Интересно отметить, что Sledgehammer для Isabelle, по умолчанию не может доказать эту теорему, поскольку для этого требуется индукция.
Создание обучающих данных. Для обучения модели создается новый набор данных для генерации доказательств. Существующие наборы данных для обучения моделей нейронных доказателей теорем содержат примеры отдельных шагов доказательства. Каждый обучающий пример включает как минимум состояние доказательства (вход) и следующий шаг доказательства к применению (цель). Учитывая набор данных, содержащий отдельные шаги доказательства, необходимо создать новый набор данных, чтобы обучить модель предсказывать целые доказательства сразу. Для этого извлекаются шаги доказательства из каждой теоремы из набора данных и объединяются, чтобы восстановить исходные доказательства.
Вывод. Разработчики донастраивают языковую модель на основе полученных данных для предсказания целого доказательства, имея только утверждение теоремы. Чтобы сгенерировать доказательство с использованием донастроенной LLM, предоставляется потенциально неизвестное утверждение теоремы и выбирается фиксированное количество последовательностей (обычно 16 или 64) из языковой модели. Также настраивается температура выборки из небольшого набора (от 0,0 до 1,4 с шагом 0,2), который является множителем для логарифма вероятностей распределения выбранных токенов на каждом шаге.
Проверка доказательств. После выборки доказательств из модели они проверяются с помощью помощника. Это означает, что сначала разработчики загружают контекст, в котором теорема была доказана, а затем заменяют оригинальное доказательство теоремы на то, которое взяли из модели. Если Isabelle принимает любое из выбранных доказательств – теорема доказана.
2.2. Восстановление доказательства
Если доказательство не принимается, Isabelle возвращает сообщение об ошибке. При этом существующие методы генерации доказательств не могут использовать сообщения об ошибках.
Для постановки задачи используется модель, рассмотренная в Разделе 2.1. Если Isabelle принимает попытку доказательства, можно остановиться. В противном случае, используется сообщение об ошибке и неправильная попытка доказательства для построения примера, который будет использоваться в качестве входных данных для модели восстановления доказательства (как показано выше). Затем выбирается попытка доказательства из этой модели и выполняется проверка таким же образом, как и в подходе генерации доказательства.
В явном виде входные и выходные данные выглядят следующим образом:
• Вход: утверждение теоремы, неправильное доказательство, сообщение об ошибке.
• Выходные данные: доказательство кандидата
Пример: Начиная с теоремы fun_sum_commute, разработчики иллюстрируют пример подхода к исправлению доказательства в Baldur. Они применяют модель генерации доказательств для получения дополнительных попыток доказательств. Ниже приведена попытка доказательства, сгенерированная Baldur, которая не проходит проверку.
Baldur пытается применить индукцию, но не может сначала разбить доказательство на два случая (конечное и бесконечное множество). Isabelle возвращает следующее сообщение об ошибке:
Детали сообщения об ошибке указывают на то, где произошла ошибка (строка 1), и что проблема касается правила индукции. С использованием модели восстановления доказательства Baldur может попытаться сгенерировать правильное доказательство для утверждения с этими строками в качестве входных данных. Если мы хотим вместо этого получить тренировочный пример для восстановления доказательства из этих строк, то необходимо объединить утверждение теоремы, неудачную попытку доказательства и сообщение об ошибке в качестве входных данных, а в качестве цели используем правильное доказательство, написанное человеком (как было показано в предыдущем разделе).
Создание обучающих данных. Используя модель генерации доказательств, выбирается одно доказательство с температурой 0 для каждой проблемы в исходном обучающем наборе (температура 0 означает, что генерация будет очень консервативной, склонной к выбору наиболее вероятных вариантов вывода). Используя proof assistant, записываются все неудачные доказательства и сообщения об ошибках. Затем необходимо приступить к созданию нового обучающего набора для восстановления доказательств. Для каждого исходного учебного примера нужно объединить утверждение теоремы, (неправильное) доказательство, сгенерированное моделью генерации, и соответствующее сообщение об ошибке, чтобы получить входную последовательность нового учебного примера. Для целевой последовательности используется доказательство истинности из исходного обучающего примера.
2.3. Добавление контекста
LLM обладают впечатляющими способностями к контекстному обучению, что позволяет им гибко использовать информацию, которая предоставляется как часть входной последовательности (и, фактически, как часть их собственного вывода). Чтобы изучить, в какой степени контекстное обучение может помочь в области доказательства теорем, разработчики расширили их входные данные потенциально полезным контекстом.
Таким образом, контексты файла теории (строки, предшествующие утверждению теоремы) используются в качестве входных данных для модели генерации доказательств. В явном виде вход и выход выглядят следующим образом:
• Входные данные: контекст файла теории и утверждение теоремы.
• Выходные данные: доказательство кандидата.
Пример: Продолжая пример, контекст файла теории, прямо предшествующий fun_sum_commute, представляет собой следующее утверждение теоремы и связанное с ним доказательство:
Строки, которые находятся в утверждении теоремы для fun_sum_commute, такие как "?(0) = 0", снова появляются в этом контексте, и поэтому дополнительная информация о них может помочь модели делать лучшие предсказания.
Создание обучающих данных. Добавленный контекст из теории может включать в себя высказывания, такие как предыдущие теоремы, определения, доказательства, а также комментарии на естественном языке. Для использования доступной длины входных данных LLMs, сначала добавляют до 50 предшествующих высказываний из того же файла теории. Во время обучения разработчики сначала токенизируют все эти высказывания, затем обрезают левую часть последовательности, чтобы она соответствовала длине ввода.
2.4 Большая языковая модель
Как уточнялось ранее, в работе используется модель Minerva с 8 миллиардами параметров и та же модель, но с 62 миллиардами параметров. Архитектура Minerva основана на оригинальной архитектуре Transformer, но имеет несколько заметных различий. Это только декодирующий трансформер с максимальной длиной последовательности в 2 048 токенов.
Детали реализации, специфичные для Baldur. Для обучения модели генерации доказательств необходимо конкатенировать входные и выходные данные и после обработать их с использованием двунаправленного внимания – bidirectional attention для контекста (что позволяет модели учитывать контекст как слева, так и справа от текущей позиции в последовательности) и причинного внимания – causal attention для целей (что позволяет модели "смотреть" только на предыдущую часть последовательности во время генерации следующего токена).
Поскольку у трансформера максимальная длина контекста 2048, разработчики заполняют последовательности нулями, если они слишком короткие, и обрезают их, если они слишком длинные. Входные данные для модели обрезаются до максимальной длины ввода путем удаления токенов слева. Обоснование для удаления токенов слева заключается в том, что дополнительный контекст предоставляется перед утверждением теоремы и его можно обрезать более безопасно, чем само утверждение теоремы. Аналогично, цели (т.е. доказательство, которое необходимо сгенерировать) обрезаются справа до максимальной длины.
Разработчики использовали максимальную длину ввода 1536 и максимальную длину цели 512 для всех экспериментов, за исключением исследования по восстановлению доказательства, где вместо этого были использованы 1024 и 1024. Также используется коэффициент отсева 0.1 как для моделей генерации, так и для моделей восстановления, чтобы бороться с переобучением.
Во время выборки из языковой модели необходимо ограничить выбор следующего токена 40 токенами с наивысшим баллом, также называемым верхней K-выборкой. Далее избираются последовательности с максимальной длиной 256 токенов. Модель обучалась на генерацию до 512 токенов, но поскольку большинство успешных доказательств относительно короткие, это ограничение имеет незначительное влияние на скорость доказательств, при этом экономя вычислительные ресурсы.
Разработчики используют размер пакета – 32 и донастраивают до 100 000 шагов. Однако было замечено, что модель начинает переобучаться на обучающем наборе после 50 000 – 70 000 шагов. Для вывода были выбраны контрольные точки, сделанные прямо перед тем, как модель начала переобучаться.
3. Результаты оценки модели
Основные результаты экспериментов представлены в следующей таблице.
Уровень доказательности различных моделей:
*Подход к исправлению использует половину количества образцов, а затем одну попытку исправления для каждого образца
Важно уточнить, что для большинства тренировочных прогонов модели 8b были использованы 64 ядра TPUv3, распределенных по 8 хостам. В свою очередь для обучения модели 62b были задействованы 256 ядер TPUv3, распределенных по 32 хостам. Кроме того, была использована кодовая база PISA, которая позволяет взаимодействовать с помощником Isabelle для проверки доказательств.
3.1. Генерация цельных доказательств
Если проводить сравнение со стандартными методами по возможности генерации цельных доказательств теорем, то выходит, что Sledgehammer и подход, основанный на поиске, достигают показателей в 25,6% и 39,0% соответственно. В сравнении, рассматриваемый подход к генерации доказательств с языковой моделью на 8 бит достигает процентного показателя доказательства в 34,8% с 16 образцами и 40,7% с 64 образцами. Сравнение становится еще более благоприятным, если учесть другие варианты Baldur, которые достигают процентного показателя доказательств до 47,9%.
Кроме того, важно учитывать разницу во времени: для получения одного доказательства стандартные методы требуют TPUv3 с 8 ядрами в течение 216 секунд, в то время как наш метод также требует TPUv3 с 8 ядрами в течение 35 секунд для проверки 64 доказательств ⇒ разница в 6 раз.
3.2. Использование LLM для восстановления доказательства
На основе моделей генерации и восстановления доказательств, рассмотренных ранее, удалось определить, что если один раз выбрать образец из модели генерации доказательств с температурой 0, собрать неудачные доказательства, а затем один раз восстановить их также с температурой 0, можно получить дополнительно 266 или 4,2% правильных доказательств. Однако в этом сравнении подход generate + repair (генерация + восстановление) использует две выборки, а подход generate – только одну. Чтобы сравнение было корректным, мы должны сравнить подход repair с подходом generate с дополнительными попытками вывода.
На рисунке показан график успешности доказательств в подходах generate и repair в зависимости от количества проб для доказательства.
Обратите внимание, что количество образцов для подхода восстановления не полностью совпадает с количеством образцов для подхода генерации. Это связано с тем, что подход генерации имеет тенденцию создавать несколько копий одних и тех же доказательств, которые дедуплицируют перед повторной парой, и генерировать только одну попытку восстановления для каждой неудачной попытки доказательства. Для каждого количества образцов подхода generate настраивается температура в диапазоне от 0,0 до 1,4 с шагом 0,2, а для подхода repair всегда используется температуру 0.
Мы видим, что подход восстановления последовательно превосходит обычную модель генерации доказательств, которая использует только утверждение теоремы в качестве входных данных. Тем не менее, это еще не отвечает на вопрос о том, откуда берутся эти преимущества.
Для решения этого вопроса была обучена новая модель восстановления, которая получает ту же информацию, за исключением того, что она не видит сообщение об ошибке. Построение графика успешности доказательства этой модели на графике показывает, что хотя она способна доказывать дополнительные теоремы, она все равно не превосходит производительность модели генерации при нормализации по стоимости вывода. Это подтверждает, что информация в сообщении об ошибке является ключевой для наблюдаемых преимуществ подхода ремонта.
3.3. Способность LLM извлекать пользу из использования контекста теоремы
На рисунке выше построен график зависимости успешности доказательства модели генерации с контекстом и без него от количества попыток доказательства. Мы видим, что модели генерации доказательств с контекстом неизменно превосходят обычную модель генерации.
Подробнее это можно рассмотреть на примерах, которые модель, использующая контекст, смогла решить, а без контекста – нет:
В примерах 1, 3 демонстрируется, что модель легко копирует и адаптирует доказательства, существующие в ее контексте:
В примере 2 модель использовала предпосылку, не встречающуюся в ее контексте, которая, как оказалось, также использовалась в доказательстве истинности, но с другой тактикой:
В примере 4 модель нашла более простое доказательство, которое не встречалось в контексте. Это говорит о том, что добавление контекста не играет такой же роли, как выбор предпосылок:
3.4. Влияние размера LLM на эффективность синтеза доказательств
Разработчики доработали и оценили 62b-версию Minerva на задаче генерации доказательств с контекстом. В таблице, приведенной в начале раздела мы видим, что для 16 примеров большая модель может доказать на 1,3 % больше, чем модель 8b, в результате чего общая скорость доказательства составляет 42,2 %. Для 64 примеров большая модель может доказать на 0,4 % больше, чем модель 8b, в результате чего общая скорость доказательства составляет 47,9 %.
Таким образом, производительность доказательства теорем улучшается с ростом масштаба языковой модели.
Вывод
Я считаю, что не стоит ограничиваться только одним подходом, обращающимся к Baldur, несмотря на все его преимущества. Совмещая разработанные методы, основанные на LLM, и стандартные методы, основанные на поиске, действительно можно прийти к большому выигрышу в доказательной силе.
По данным разработчиков, работая вместе с Thor (инструментом, который объединяет обученную модель, поиск и Sledgehammer), Baldur может полностью автоматически доказать 65,7 % теорем, что превосходит результаты каждого из инструментов по отдельности. Поэтому с уверенностью можно сказать, что Baldur – отличная база для автоматической формальной верификации.
Кроме того, разработанный метод может стать основой для создания новой обучающей стратегии поиска доказательств, благодаря возможности интеграции моделей генерации и исправления (восстановления), чего не было раньше. Это не только повлияет на повышение эффективности формальной верификации, но и поможет решить более сложные математические проблемы.
На этом все!
Будем ждать Вас в комментариях! Спасибо за прочтение :)
