Что происходит, когда агенты ИИ могут переписывать миллионы строк кода на порядки быстрее, чем люди успевают их проверять?
В Microsoft мы работаем именно над этой задачей.
Мы создаем и запускаем агенты ИИ, которые преобразуют крупнейшие кодовые базы в мире, включая Windows и Azure. Наша работа варьируется от миграции кодовой базы объемом 400 миллионов строк на новую цепочку инструментов компилятора до модернизации устаревшего кода C и C++ в Rust — все чаще при поддержке формальной верификации.
Генерация кода становится легкой частью задачи. Понимание того, можно ли ему доверять, — вот настоящий вызов. Когда агенты вносят изменения в сотни миллионов строк кода, как мы можем быть уверены, что они не сломали что-то незаметное? Как сохранить поведение, безопасность и архитектурный замысел? И как небольшая команда инженеров может с уверенностью отвечать за изменения, которые агенты ИИ вносят в таком масштабе?
С 2024 года мы объединяем агенты ИИ со статический анализом, тестированием и формальной верификацией, чтобы сделать масштабную трансформацию программного обеспечения практичной и надежной.
Эти вопросы лежат в основе нашей работы. С 2024 года мы объединяем агенты ИИ со статическим анализом, тестированием и формальной верификацией, чтобы сделать масштабную трансформацию программного обеспечения практичной и надежной.
По ходу дела поток управления инвертировался. Мы начинали с жестко запрограммированных рабочих процессов, которые вызывали LLM в качестве подпрограмм; к маю 2025 года агенты стали лучшими планировщиками, чем наши конвейеры, и нашей задачей стало создание инструментов, которые вызывают агенты. Самыми ценными из этих инструментов являются те, которые говорят агенту — и стоящим за ним инженерам, — является ли изменение правильным.
Теперь мы непрерывно обновляем наш подход с помощью гибкой инфраструктуры (harness), чтобы использовать формальные методы, декомпозировать крупномасштабные цели в сложных системах и решать проблемы, с которыми сталкиваются зрелые компании с большими и сложными кодовыми базами. Мы также переосмысливаем то, как люди и агенты работают вместе. Даже по мере совершенствования моделей и агентских инфраструктур когнитивная нагрузка на экспертов-людей растет. Человеческое внимание стало самым дефицитным ресурсом в разработке ПО с использованием агентов, и мы проектируем наши инструменты так, чтобы расходовать его там, где это важнее всего.
Человеческое внимание стало самым дефицитным ресурсом в разработке ПО с использованием агентов, и мы проектируем наши инструменты так, чтобы расходовать его там, где это важнее всего.
Это первая статья в серии о том, что мы создаем, чему научились и на какие вопросы все еще пытаемся найти ответы. Здесь мы представляем некоторые проблемы, над которыми работаем, и идеи, которые их связывают.
Миграция
Представьте, что вам нужно внести аналогичные изменения в сотни миллионов строк кода, поддерживаемых тысячами инженеров. В этом и заключается сложность крупномасштабной миграции кода. Сгенерировать любое отдельное изменение легко. Сложность заключается в том, чтобы сделать тысячи изменений правильным образом: зафиксировать то, что знают эксперты, подтвердить эти знания и применять их последовательно, не привлекая к этой работе каждого инженера в организации.
Мы определяем миграцию как трансформацию, применяемую ко всей кодовой базе для достижения конкретной инженерной цели, такой как обновление зависимостей, внедрение нового компилятора, устранение результатов статического анализа или переход на новую платформу. Наши примеры из практики включают миграцию всей кодовой базы Windows, насчитывающей несколько сотен миллионов строк кода, для добавления поддержки цепочки инструментов Clang/LLVM; устранение проблем, выявленных анализаторами CodeQL, PREfast и Roslyn в различных кодовых базах; а также перенос сервисов с архитектуры x86 на ARM.
Мы делаем осознанный выбор в отношении операционной модели: очень небольшая команда экспертов по миграции может — и должна — руководить масштабной миграцией. Вместо того чтобы распределять ответственность за миграцию между более широкой инженерной организацией, мы концентрируем экспертизу и усиливаем ее с помощью агентов.
Агенты сначала изучают базу знаний-кандидат на основе выборочных результатов. Агент-рецензент оценивает каждое предложенное исправление на предмет корректности, минимализма, соответствия файловым соглашениям и удобства поддержки, а его выводы уточняют базу знаний. Затем эксперты утверждают базу знаний, а не отдельные исправления, и агенты применяют ее ко всей кодовой базе. Обратная связь от человека остается важной, но мы направляем ее туда, где она имеет наибольшую отдачу: на утверждение знаний и разрешение новых или неоднозначных случаев. Группировка похожих исправлений для проверки дополнительно снижает когнитивную нагрузку на рецензентов.
Модернизация языков
Большая часть наиболее критически важного ПО в мире написана на таких языках, как C/C++, в которых ошибки безопасности памяти легко допустить и сложно устранить. Переписывание на Rust обещает безопасность по умолчанию (safety by construction) — но только в том случае, если переписанный код точно воспроизводит работу оригинального. В масштабе реальных систем ручное переписывание редко бывает практичным, а автоматизированное полезно только тогда, когда мы можем ему доверять.
Наша работа сосредоточена на переходе устаревших кодовых баз на Rust, и быстрое совершенствование моделей и агентов изменило то, что теперь возможно:
Каждый шаг смещал «узкое горлышко» — от компиляции к прохождению тестов и к проверенному поведению в масштабе. По мере улучшения генерации задачей стало определение того, что именно нужно модернизировать, и доказательство правильности результата.
Мы создали интерактивные интерфейсы, которые помогают инженерам визуализировать структуру модулей и слои кодовой базы, а также решать, какие компоненты модернизировать и в каком порядке. Затем наши инструменты создают как модернизированный код, так и стратегию его валидации.
Мы обнаружили, что миграция по принципу «функция за функцией» работает лучше, чем покомпонентный перевод строчка за строчкой. Функция — это единица видимого пользователем поведения, которую мы можем проверить от начала до конца с помощью сценарных тестов, и каждая функция получает свой собственный шлюз проверки. Дифференциальное тестирование сравнивает поведение исходного и целевого кода, а тесты, скрытые от агента (чтобы он не мог переобучиться на них), измеряют надежность перевода. Совсем недавно мы начали извлекать формальные спецификации из исходного кода, переносить их в целевой язык и использовать Verus, чтобы доказать, что модернизированный код удовлетворяет им.
Разработка на основе спецификаций
Агенты могут производить изменения быстрее, чем люди успевают их оценивать, а локально правдоподобный код все равно может нарушать архитектурные допущения, распределенные протоколы, границы безопасности или операционные инварианты. Тесты выявляют некоторые из этих проблем, рецензенты — другие, но ни то, ни другое не поспевает за тем темпом, с которым агенты вносят изменения. Мы считаем, что решение заключается в том, чтобы сделать намерения явными. Поскольку агенты пишут все большую часть нашего кода, внимание разработчиков смещается с написания кода на управление спецификациями, которые направляют агентов и проверяют их результат. Мы создаем инструменты, которые ставят формальные, интерпретируемые спецификации в центр жизненного цикла разработки программного обеспечения.
Наш первый шаг — вывод формальных спецификаций (например, TLA+) из существующих баз кода с помощью агентов. Эти спецификации фиксируют параллелизм, отказоустойчивость и другие аспекты критических компонентов программного обеспечения. Мы используем такие инструменты, как TLC, чтобы проверять, поддерживаются ли спецификациями трассы выполнения реализации. Это дает нам основание полагать, что спецификации допускают наблюдаемое поведение реализации; отражают ли они также то, что система должна делать по задумке — вопрос более сложный, к которому мы вернемся ниже. Когда трасса не поддерживается, несоответствие может указывать на дефект реализации, неточную спецификацию или неверный тест, и агенты исправляют то, что оказалось неверным.
Получив спецификации, мы заставляем их работать. Они служат отличным источником сложных тестовых сценариев, проверяющих неочевидные пересечения потоков и сценарии сбоев. Мы проводим моделенную проверку свойств-кандидатов и индуктивных инвариантов на небольших конечных конфигурациях для быстрого поиска контрпримеров, а также доказываем свойства для всех конфигураций в F* и Lean с помощью разрабатываемого нами компилятора из TLA+ в F* и Lean. Для существующих баз кода этот уровень спецификаций, тестовых сценариев и свойств становится защитным барьером для будущих изменений, управляемых ИИ.
Наша цель — предоставить возможности формальных методов каждому инженеру, не требуя от него становиться экспертом в TLA+ или формальной верификации. Инженер проверяет и одобряет свойства, которым должна соответствовать система; агенты находят индуктивные инварианты, необходимые для их доказательства. По мере того как спецификации становятся всеобъемлющими, они также могут служить основой для модернизации — именно так мы подходим к трансляции C/C++ в верифицируемый с помощью Verus Rust.
Открытые вопросы
Вот несколько открытых вопросов, над которыми мы размышляем:
- Можно ли доверять спецификациям, написанным ИИ? Когда агент выводит спецификацию из того самого кода, который он должен проверять, как узнать, отражает ли спецификация то, что система должна делать, а не просто то, что она делает в данный момент?
- Можем ли мы верифицировать больше, чем просто функциональную корректность? Могут ли агенты помочь нам рассуждать о безопасности, производительности и надежности, выходя за рамки простой проверки того, выдает ли код ожидаемый результат?
- Перестанут ли инженеры со временем читать код? Если агенты генерируют код, а инструменты верификации доказывают, что он удовлетворяет утвержденным спецификациям, смогут ли инженеры перестать читать код и работать исключительно на уровне спецификаций?
- Кому принадлежит код, когда каждый агент может изменить всё? Традиционное владение кодом предполагает, что инженеры работают в относительно четко определенных границах. Разработка на основе агентов ставит это предположение под сомнение. Что приходит ему на смену?
Для нас это не гипотетические вопросы. Они определяют то, что мы создаем дальше.
Мы будем рады услышать о том, с чем вы сталкиваетесь в собственной работе, в чем вы с нами не согласны и какие проблемы вы считаете наиболее важными. Пожалуйста, не стесняйтесь делиться своими мыслями.
