Constructor Institute of Technology (CIT) — это институт в Шаффхаузене, Швейцария, в котором я провёл два года моей аспирантуры в области верификации программного обеспечения на Эйфеле. К сожалению, СIT было решено закрыть в 2025. В этом посте я хочу сохранить ссылки на некоторые проекты, над которыми мы работали.
Я работал на кафедре программной инженерии под руководством Бертрана Мейера. В моё время на кафедре было ещё несколько аспирантов: Ли Хуан (успела защититься и получила степень, поздравляю!), Алессандро Скена и Рето Вебер. Нашу научную и преподавательскую деятельность поддерживал Марко Пиччони.
Статическая верификация в AutoProof
Наша работа охватывала различные области программной инженерии. Особое внимание уделялось статической верификации. Главным продуктом команды в этой сфере является AutoProof, который является частью научного окружения Reif. AutoProof — это статический верификатор для программ на Эйфеле. С его помощью можно автоматически проверить согласуется ли тело процедуры с контрактами.
Основная часть моего вклада в код верификатора заключается в реализации и расширении подхода, описанного в статье нашей кафедры “The concept of class invariant in object-oriented programming”. К сожалению, наша работа была прервана закрытием института.
Могут ли LLM помочь с исправлением верифицированного ПО?
Наше последнее исследование в институте изучало насколько чаты с LLM могут помочь в исправлении багов, когда у программистов есть доступ к верификтору. Отчёт об этом исследовании называется “Do AI models help produce verified bug fixes?”.
Я считаю, что верификация ПО может взять случайность в ответах больших языковых моделей под контроль. Верификатор может подтвердить, что исправление в самом деле “корректно”, а не просто “статистически выглядит подходящим”.
Мы попросили 25 программистов исправить баги в программах. Некоторым был доступен чат-бот и верификатор, некоторым было разрешено работать только с верификатором.
Результаты показали, что LLM наиболее полезны начинающим пользователям (чтобы добиться хоть какого-то результата) и экспертам (быстро реализовать самостоятельно придуманное решение). Разработчики со средним уровнем знаний получают меньше пользы от LLM.
Я писал больше об эксперименте в блоге кафедры. Конечно, в самой статье можно получить ещё больше информации.
Планы на будущее
У меня есть ещё несколько проектов из Constructor Institute of Technology, которые я бы хотел подсветить, но я оставлю их для будущих постов. Подпишитесь на RSS ленту, чтобы их не пропустить!
В общем, я рад, что у меня была возможность работать над продвинутыми темами программной инженерии в профессиональной команде, возглавляемой Бертраном Мейером. Условия работы были великолепными и позволили нам сконцентрироваться на науке. Лично мне грустно, что наша работа прервалась так резко.
Я надеюсь, что у нас ещё будет возможность собраться командой и продолжить нашу работу.