Реєстраційний номер
0826U004512, Дисертація доктора філософії
На здобуття
Доктор філософії
Дата захисту
03-09-2026
Статус
Наказ про видачу диплома
Назва роботи
Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей
Здобувач
Вохранов Ілля Анатолійович,
Керівник Булах Богдан Вікторович
Опонент Сенів Максим Михайлович
Опонент Глибовець Андрій Миколайович
Рецензент Стіренко Сергій Григорович
Рецензент Харченко Костянтин Васильович
Установа, організація, у вченій раді якої відбудеться/відбувся захист
Національний технічний університет України "Київський політехнічний інститут імені Ігоря Сікорського"
Опис
Об'єкт дослідження — процеси статичного аналізу програмного коду, спрямовані на виявлення дефектів та вразливостей; предмет — нейросимвольні методи аналізу, що поєднують семантичне розуміння великих мовних моделей (LLM) з незалежною символьною верифікацією.
Мета — розробка, формалізований опис та експериментальна оцінка нейросимвольного методу, який забезпечує контрольовану поведінку LLM через незалежну символьну верифікацію генерованих тверджень і дозволяє досягти високої повноти виявлення дефектів при збереженні точності та передбачуваності результатів. Дослідження виконано в рамках ініціативної науково-дослідної роботи СП-01/2023 «Впровадження сервіс-орієнтованого підходу до реалізації процесів діджиталізації суспільства» (№ держреєстрації 0123U101333).
Методи дослідження: аналіз і систематизація наукових джерел; формалізація архітектури та алгоритмів; моделювання взаємодії компонентів; обчислювальний експеримент на реальних даних; порівняльний аналіз з існуючими підходами; абляційне дослідження внеску кожного компонента. Програмно-апаратна база: власний програмний прототип, що поєднує ансамбль інструментів статичного аналізу, зіставлення AST-патернів і taint-аналіз із зверненням до API моделей GPT-4 та GPT-5.2; набір даних PySStuBs.
Наукова новизна. Вперше запропоновано нейросимвольний метод, у якому на першому етапі LLM безпосередньо генерує структуровані твердження про дефекти коду, а символьний аналіз їх верифікує, на відміну від існуючих методів (IRIS, LLMSA, MoCQ), де символьний компонент виконує первинне виявлення, а нейронний лише фільтрує чи доповнює його результати. Інвертований напрямок взаємодії Neural → Symbolic дозволяє скористатися здатністю моделі сприймати семантику коду за одночасного жорсткого контролю згенерованих нею тверджень і мінімальних ризиків галюцинації.
Вперше запропоновано спосіб верифікації структурованих тверджень про дефекти Explain-Verify Gate, у якому атрибути твердження (тип дефекту, локалізація, пропозиція мінімально достатнього виправлення, обґрунтування) визначають вибір та інтерпретацію подальших символьних перевірок — зіставлення AST-патернів, taint-аналізу, перевірки правдоподібності виправлення. Це забезпечує детермінізм верифікації без повторних звернень до мовної моделі за обґрунтуванням кожного її рішення.
Удосконалено процес прийняття рішень щодо дефектів завдяки механізму Evidence-Weighted Suppression, який зважує докази з кількох незалежних джерел (інструменти статичного аналізу, AST-патерни, показник впевненості базового аналізатора) і відновлює валідні виявлення, відхилені символьною верифікацією за відсутності відповідних патернів, але підтверджені достатніми доказами. Це дозволяє збалансувати точність і повноту аналізу.
Практичні результати. Оцінка на 1000 збалансованих зразках набору PySStuBs показала виявлення 379 дефектів проти 132 у базового LLM-підходу та 8 в ансамблю інструментів на основі правил, що відповідає зростанню recall на 187% та F1-score на 76,4% за співставного рівня точності (близько 0,51). Валідація з моделлю GPT-5.2 (n=500) підтвердила збереження переваг при переході на новіше покоління моделі (+132% F1-score, +363% recall), абляційне дослідження — стійкість архітектури до модифікації окремих компонентів (F1-score у діапазоні 0,654–0,668). Метод не потребує донавчання моделей і збору спеціалізованих наборів даних, допускає заміну нейронного компонента без модифікації решти системи, а покриття символьної верифікації розширюється додаванням правил, AST-патернів і taint-специфікацій для нових мов програмування та класів дефектів. Результат аналізу подається структурованим описом дефекту (тип, локалізація, обґрунтування, мінімально необхідне виправлення) разом із результатами символьної верифікації, що скорочує час розробника на опрацювання виявлень.
Ступінь упровадження: розроблено та експериментально апробовано програмний прототип методу; результати використано для покращення інструментарію забезпечення якості програмного забезпечення в рамках виконання зазначеної науково-дослідної роботи. Упровадження методу в автоматизовані процеси контролю якості програмного коду планується.
Галузь використання: інженерія програмного забезпечення, забезпечення якості та надійності програмних систем, аналіз захищеності вихідного коду, автоматизовані процеси контролю якості (CI/CD, code review, IDE), а також подальші дослідження нейросимвольних систем.
Дата реєстрації
2026-08-11
Додано/оновлено в НРАТ
2026-08-11 / 2026-09-22
