Registration Number
0826U004512, PhD dissertation
Status
Доктор філософії
Date
03-09-2026
popup.evolution
o
Title
Method of Static Analysis of Program Source Code Using Large Language Models
Author
Illia Vokhranov,
popup.head Bohdan V. Bulakh
popup.opponent Maksym M. Seniv
popup.opponent Andrii Glybovets
popup.review Serhii H. Stirenko
popup.review Kostiantyn V. Kharchenko
popup.rada
National Technical University of Ukraine «Igor Sikorsky Kyiv Polytechnic Institute»
Description
Об'єкт дослідження — процеси статичного аналізу програмного коду, спрямовані на виявлення дефектів та вразливостей; предмет — нейросимвольні методи аналізу, що поєднують семантичне розуміння великих мовних моделей (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), а також подальші дослідження нейросимвольних систем.
Registration Date
2026-08-11
popup.nrat_date
2026-08-11 / 2026-09-22
