Сферы применения генеративного ИИ (GenAI), такие как создание контента, разговорный ИИ и перевод языков, разнообразны и постоянно расширяются, затрагивая аспекты разработки ПО: от оптимизации и генерации кода до исправления ошибок, документирования и непрерывной интеграции, сообщает портал The New Stack.
С тех пор как в конце ноября 2022 г. компания OpenAI представила своего чатбота ChatGPT, распространение инструментов GenAI и больших языковых моделей (LLM) резко ускорилось. Они проникают в организации всех форм, размеров и секторов, и разработчики ПО не остались в стороне от этого порыва.
Разработчики все чаще рассматривают GenAI как полезный инструмент, заявили ИИ-эксперты в блоге Института программной инженерии Университета Карнеги-Меллона в октябре 2023 г.: «Первоначальный ажиотаж вокруг использования LLM для разработки ПО уже начал остывать, и ожидания стали более реалистичными. Разговор перешел от ожиданий, что LLM заменят разработчиков ПО, к рассмотрению LLM в качестве партнеров и сосредоточению на том, где их лучше всего применять (т. е. от искусственного к дополненному интеллекту)».
LLM и верификация ПО
Группа ученых-компьютерщиков под руководством Массачусетского университета в Амхерсте (UMass Amherst) недавно заявила, что они используют возможности генеративного ИИ и LLM для решения сложной задачи проверки кода, чтобы предотвратить появление уязвимостей в ПО.
В частности, команда сосредоточилась на использовании ИИ для разработки метода автоматической генерации целых доказательств для проверки программного кода (метод Baldur) — кропотливого, дорогого и трудоемкого процесса, который обычно выполняется вручную. Еще более сложным процессом является машинная проверка: создание математического доказательства, показывающего, что код делает то, что ожидается, а затем использование провайдера теорем для проверки правильности доказательства.
Эмили Ферст, которая стала постдокторантом Калифорнийского университета в Сан-Диего после получения степени доктора компьютерных наук в UMass Amherst (исследование LLM и верификации ПО было частью ее диссертации), отмечает, что написание доказательств вручную может занимать гораздо больше времени, чем написание самого программного кода.
По словам Юрия Бруна, профессора Колледжа информационных и компьютерных наук UMass Amherst, количество систем, прошедших формальную верификацию, довольно невелико. «Это сложно, — поясняет он. — Вот тут-то мы и вступаем в игру. Проблема, которую мы пытаемся решить, заключается в том, что мы пытаемся автоматически генерировать эти доказательства».
ПО с ошибками просто не должно приниматься
Это поможет решить еще более серьезную проблему: наличие недостатков в ПО, которые могут быть раздражающими или — если ими воспользуются киберзлоумышленники или они присутствуют в сложных системах, отказ которых может иметь широкие негативные последствия — опасными.
«ПО — важная часть нашей повседневной жизни, — говорит Брун. — Без него вы не можете ничего делать. Вы не можете водить машину, не можете ездить в лифте. К сожалению, сегодня ПО, как правило, глючит. Любое ПО, которое вы покупаете в магазине, почти всегда содержит ошибки. Просто это слишком сложная проблема для решения, поэтому существует множество различных способов попытаться улучшить качество ПО».
Один из способов — доказать корректность ПО. Это эффективный метод, но и один из самых сложных. Он применяется в некоторых областях — в здравоохранении для некоторых медицинских устройств или в НАСА, «потому что если у вас возникнет аварийная ситуация на космическом корабле и ваше ПО даст сбой, это будет дорого стоить, поэтому стоит потратиться на то, чтобы разработчики и инженеры-программисты официально доказали корректность функции», — говорит Брун.
Некоторые исследователи создали модели, которые могут писать доказательство по строчке за раз: они пишут первые 10 строк доказательства, а затем просят модель по сути отыскать следующую наиболее вероятную строку, основываясь на том, что уже написано и что пытаются доказать.
Создание Baldur
Исследователи из UMass Amherst обратились к LLM как к возможному решению для автоматической генерации доказательств. Однако и здесь возникли проблемы, главная из которых заключается в том, что модели не всегда корректны. Вместо того, чтобы «упасть» и тем самым сообщить разработчику о том, что что-то не так, они «молча отказывают», выдавая неверный ответ, но представляя его так, будто он правильный. По словам Бруна, часто молчаливый отказ — это худшее, что может случиться.
Исправить ситуацию призван Baldur, новый метод разработки доказательств на основе ИИ, созданный командой UMass Amherst. Исследователи использовали систему Minerva LLM от Google, которая была обучена на большом количестве текстов на естественном языке. Затем она была обучена на
В результате Baldur генерирует все доказательство, а анализатор теорем Isabelle проверяет его. Если чекер находит ошибку, информация о ней возвращается в LLM, чтобы она могла извлечь уроки из своей ошибки и затем сгенерировать другое доказательство с меньшим количеством ошибок или — надеемся — без них.
Таким образом, Baldur «получает некий контекст, чтобы сказать: „Вот еще немного информации о состоянии, о вопросе, на который ты мне отвечаешь“, — говорит Брун. — Когда мы предоставили ему эту дополнительную информацию, он смог ответить на вопрос более полно. Мы сделали эту итерацию один раз, и вы можете представить себе, что это можно делать много раз. Но это очень непросто с такими пошаговыми моделями, даже если они используют LLM. Это малоэффективно».
Baldur в cвязке с Thor
Брун и его команда, в которую также входили Маркус Рабе, работавший в то время в Google, и Талия Рингер, доцент Университета Иллинойса-Урбана-Шампейн, обратили внимание на Thor, фреймворк для интеграции языковых моделей и автоматизированных доказательств теорем. По его словам, сам по себе Thor мог создавать доказательства в 57% случаев.
Объединив его с Baldur (братом Thor в норвежской мифологии) они смогли создавать доказательства в 65,7% случаев. Эти два метода дополняют друг друга.
Тор «использует LLM, чтобы попытаться предсказать следующий вероятный шаг в доказательстве, но он также использует вещи, называемые „молотками“, — поясняет Брун. — Молотки — это математические инструменты, которые говорят: „Я знаю кучу математических тегов. Позвольте мне попробовать их. Давайте я попробую это, это и это“. Это как бить молотком по проблеме, просто пробовать разные вещи и смотреть, работает ли что-нибудь. Это попытка попробовать все эти вещи одновременно».
Метод Балдура отличается тем, что он создает целые доказательства, а не перебирает строку за строкой, хотя и здесь есть совпадения, говорит он, добавляя, что «есть некоторые вещи, которые оба метода могут доказать. Но, пытаясь сгенерировать все доказательство сразу, мы можем доказать другой набор вещей, чем при итеративном подходе, когда мы пытаемся сгенерировать по одной вещи за раз».
Еще много предстоит сделать
Брун признает, что степень погрешности все еще велика, но отмечает, что Baldur пока представляет собой наиболее эффективный и действенный способ проверки правильности программного кода. Технологии ИИ продолжают совершенствоваться, поэтому он ожидает, что возможности Baldur также будут улучшаться.
В будущем исследователи намерены улучшить показатель в 65,7% за счет более точной настройки данных, на которых обучается LLM. Сложность проверки заключается в том, что на данный момент существует не так много подходящих данных, поэтому создавать наборы данных нелегко. Они работают над набором данных, который позволит тонко настроить модель.
Они также хотят, чтобы разработчики могли давать модели обратную связь, что поможет модели развиваться по мере того, как она будет работать над созданием доказательства.
«Разработчик может сказать: „Хорошо, это отлично сработало“. Но если это не сработало, разработчик мог бы взглянуть и сказать: „Я вижу, что вы попробовали индукцию здесь, но вы пробуете ее не на той вещи“. Он может дать модели обратную связь, и тогда модель может попробовать еще раз. Такой итеративный подход, скорее всего, действительно упростит работу разработчика и позволит модели доказать то, что она не может сделать самостоятельно», — полагает Брун.
Это полуавтоматизированный подход.
«Первоначальный итерационный подход не предполагал участия разработчика, — говорит Брун. — Модель делала все сама, сама все проверяла. Мы пытаемся вовлечь в процесс инженера-программиста, поэтому это полуавтоматизированный подход, при котором большая часть автоматизирована, но есть немного обратной связи от инженера, чтобы направлять процесс в тех случаях, когда модель не может сделать все сама».
