Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей
Дата
2026
Автори
Науковий керівник
Назва журналу
Номер ISSN
Назва тому
Видавець
КПІ ім. Ігоря Сікорського
Анотація
Вохранов І. А. Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей. — Кваліфікаційна наукова праця на правах рукопису. Дисертація на здобуття наукового ступеня доктора філософії за спеціальністю 122 — Комп'ютерні науки. — Національний технічний університет України «Київський політехнічний інститут імені Ігоря Сікорського», Міністерство освіти і науки України, Київ, 2026.
Метою дисертаційного дослідження є розробка, формалізований опис та експериментальна оцінка нейросимвольного методу статичного аналізу програмного коду з використанням великих мовних моделей, який забезпечує контрольовану поведінку LLM через незалежну символьну верифікацію генерованих тверджень, що дозволяє досягти високої повноти виявлення дефектів при збереженні точності та передбачуваності результатів. Об'єктом дослідження є процеси статичного аналізу програмного коду, спрямовані на виявлення дефектів та вразливостей. Предметом дослідження є нейросимвольні методи статичного аналізу, що поєднують семантичне розуміння великих мовних моделей з незалежною символьною верифікацією для забезпечення контрольованої та передбачуваної поведінки. У ході роботи над дисертацією було використано такі методи дослідження: аналіз та систематизація наукових джерел для визначення стану досліджень у галузі статичного аналізу коду та нейросимвольних систем; формалізація для опису архітектури та алгоритмів запропонованого методу; моделювання для побудови архітектури запропонованого методу та взаємодії його компонентів; експеримент для емпіричної оцінки ефективності методу на реальних даних; порівняльний аналіз для зіставлення результатів із існуючими підходами; абляційне дослідження для визначення внеску кожного архітектурного компоненту. Зазначені методи було обрано з огляду на мету та завдання дослідження, а також на їх придатність для вирішення проблем контрольованого використання великих мовних моделей у задачах статичного аналізу коду. У дисертації вперше запропоновано нейросимвольний метод статичного аналізу програмного коду, який відрізняється тим, що на першому етапі аналізу LLM безпосередньо генерує структуровані твердження про дефекти коду, за чим слідує етап символьного аналізу для їх верифікації, в той час, як в існуючих нейросимвольних методах статичного аналізу коду (IRIS, LLMSA, MoCQ) навпаки - символьний компонент виконує первинне виявлення або структуризацію дефектів, а нейронний компонент фільтрує чи доповнює його результати. Інвертований напрямок нейросимвольної верифікації "Neural → Symbolic" дозволяє скористатися здатністю великої мовної моделі сприймати семантику коду при одночасному жорсткому контролі згенерованих нею тверджень, що сприяє виявленню ширшого кола дефектів при мінімальних ризиках галюцинації моделі. Вперше запропоновано спосіб верифікації структурованих тверджень про дефекти коду із застосуванням символьного аналізу Explain-Verify Gate, особливість якого полягає у тому, що атрибути твердження про дефект (тип дефекту, локалізація, пропозиція мінімально задовілього виправлення та обґрунтування) визначають вибір та інтерпретацію подальших символьних перевірок (зіставлення AST-патернів, taint-аналіз, перевірка правдоподібності виправлення), що є відмінним від існуючих способів верифікації у нейросимвольних методах аналізу коду та забезпечує детермінізм верифікації за відсутності потреби повторного звернення до мовної моделі за обґрунтуванням кожного прийнятого нею рішення. Удосконалено процес прийняття рішень щодо дефектів у нейросимвольному статичному аналізі програмного коду шляхом застосування механізму Evidence-Weighted Suppression (EWS), який зважує докази з кількох незалежних джерел (інструменти статичного аналізу, AST-патерни, показник впевненості базового аналізатора), що відрізняється від процесу визначення дефектів в рамках існуючих нейросимвольних підходів, в яких відхилення результату на етапі верифікації є остаточним без урахування доказів з інших джерел. Це дозволяє збалансувати точність і повноту аналізу шляхом відновлення валідних виявлень дефектів, що відхиляються символьною верифікацією за відсутності відповідних патернів, але підтверджуються достатніми доказами з інших джерел. Розроблений метод статичного аналізу коду дає змогу виявляти додаткові дефекти, які не виявляються як інструментами на основі правил, так і безпосереднім використанням LLM. Експериментальна оцінка на 1000 зразків із набору даних PySStuBs підтвердила виявлення 247 додаткових дефектів порівняно з базовим LLM-підходом (379 проти 132) та 371 додаткового дефекту порівняно з ансамблем інструментів на основі правил (379 проти 8), що відповідає покращенню recall на 187% та F1-score на 76.4% при збереженні співставного рівня точності (~0.51). Виявлення цих додаткових дефектів на етапі статичного аналізу запобігає їх потраплянню на подальші етапи розробки, де вартість їх виправлення суттєво зростає. Результати аналізу в рамках запропонованого методу представлені структурованим описом дефекту (тип, локалізація, обґрунтування, мінімально необхідне виправлення), який завжди супроводжується результатами символьної верифікації, що скорочує час розробника на аналіз та усунення виявлених проблем та суттєво полегшує інтеграцію методу в автоматизовані процеси контролю якості коду (CI/CD, code review), де рішення про дефект має спиратися на перевірені докази, а не лише на вихід мовної моделі. Запропонований метод аналізу не потребує донавчання моделей та збору спеціалізованих датасетів, що зменшує витрати на впровадження та супровід порівняно з підходами на основі fine-tuning, які вимагають підготовки навчальних даних, обчислювальних ресурсів для тренування та повторного навчання при зміні моделі. Експериментальне застосування GPT-5.2 (RQ2) підтвердило збереження переваг запропонованого методу у порівнянні з існуючими методами статичного аналізу коду при переході на новіше покоління мовної моделі (+132% F1-score, +363% recall), що свідчить про можливість оновлення нейронного компоненту без модифікації решти складових системи, що суттєво економить витрати. Метод забезпечує можливість налаштування під різноманітні конкретні задачі аналізу без зміни загальної архітектури: тип аналізу та цільові класи дефектів визначаються у змісті запиту до нейромережевого компоненту (аналогічно до властивості customizable analysis у LLMSA), а покриття символьної верифікації розширюється додаванням нових правил, AST-патернів та taint-специфікацій для підтримки нових мов програмування та типів дефектів. Абляційне дослідження (RQ3) підтвердило стійкість архітектури до модифікацій окремих компонентів: F1-score між конфігураціями варіюється у діапазоні 0.654–0.668. Дисертація складається з п'яти розділів. У першому розділі розглянуто теоретичні основи аналізу програмного коду з використанням нейронних мереж. Проаналізовано класичні методи статичного аналізу (аналіз потоку даних, аналіз потоку управління, абстрактна інтерпретація, символьне виконання, model checking, синтаксичний аналіз та pattern matching), визначено їх переваги та фундаментальні обмеження, зокрема проблему вибуху шляхів та обмеження SMT-вирішувачів. Досліджено еволюцію нейронних методів в аналізі коду — від класичного машинного навчання через попередньо навчені моделі (CodeBERT, GraphCodeBERT) до великих мовних моделей (GPT-4, GPT-5.2). Розглянуто концепцію нейросимвольної інтеграції та типи нейросимвольних систем, що обґрунтовує необхідність гібридного підходу, який поєднує семантичне розуміння нейронних моделей з формальними гарантіями символьних методів. У другому розділі проведено аналіз сучасних досліджень у галузі статичного аналізу коду. Систематизовано існуючі нейросимвольні методи аналізу програм: IRIS (символьний → нейронний напрямок, CodeQL → LLM), LLMSA (композиційний нейросимвольний аналіз), MoCQ (ітеративне уточнення патернів). Визначено спільне обмеження існуючих методів — відсутність явного механізму незалежної верифікації тверджень LLM. Сформульовано вимоги до методу, що заповнює цю прогалину, та обґрунтовано позиціонування VERIGATE як першого методу, що реалізує напрямок Neural → Symbolic у контексті статичного аналізу коду. У третьому розділі детально описано запропонований метод VERIGATE. Представлено архітектуру чотириетапного методу: попередній скринінг (ансамбль інструментів та AST-правила), Explain (генерація структурованих тверджень LLM у форматі JSON), Verify (символьна верифікація через багатоетапне дерево рішень), фінальне рішення з механізмом Evidence-Weighted Suppression. Формалізовано процес верифікації, описано критерії прийняття та відхилення тверджень, механізм вирівнювання спанів та taint analysis. Проведено порівняння архітектурних рішень VERIGATE з існуючими нейросимвольними системами за ключовими характеристиками (напрямок взаємодії, роль LLM, роль символьної системи, пояснюваність). Описано деталі реалізації: технологічний стек, формат промпту для LLM, обробку виходу LLM. Наведено наскрізний приклад роботи VERIGATE на реальному фрагменті коду з датасету PySStuBs, що демонструє нейросимвольну взаємодію компонентів на прикладі виявлення семантичного логічного дефекту. У четвертому розділі представлено результати експериментальної оцінки. Основна оцінка (RQ1) проведена на 1 000 збалансованих зразках із датасету PySStuBs (Python Single-Statement Bugs) з використанням GPT-4. Порівняння трьох методів (VERIGATE, GPT-4 Baseline, Rule-Based) продемонструвало: покращення F1-score на 76.4% (0.612 проти 0.347) та recall на 187% (0.758 проти 0.264) порівняно з GPT-4 Baseline при порівняному precision (~0.51). Інструменти на основі правил продемонстрували дуже низьку ефективність (F1 = 0.031), що підтверджує семантичну складність дефектів у датасеті. Валідація з GPT-5.2 (RQ2, n = 500) підтвердила стабільне покращення: +132% F1-score, +363% recall, що свідчить про стійкість нейросимвольної верифікації як архітектурного принципу при розвитку мовних моделей. Абляційне дослідження (RQ3, n = 500) продемонструвало, що VERIGATE функціонує як інтегрований поетапний процес з вузьким діапазоном F1 (0.654–0.668) для всіх конфігурацій, де кожен компонент робить незалежний внесок у загальну ефективність. У п'ятому розділі досліджено перспективи розвитку та узагальнення запропонованого методу. Проаналізовано напрямки розширення на нові мови програмування, нові класи дефектів та інтеграцію з виробничими процесами розробки програмного забезпечення (CI/CD, code review, IDE). Визначено обмеження поточної реалізації та шляхи їх подолання. У дисертації запропоновано нейросимвольний метод VERIGATE для статичного аналізу програмного коду, який через використання незалежної символьної верифікації тверджень LLM дозволяє поєднати семантичне розуміння програмного коду великої мовної моделі із обґрунтуванням кожного виявлення у верифікованих властивостях програми. Основна ідея методу полягає в інверсії напрямку нейросимвольної взаємодії: замість традиційного підходу, де символьний аналіз генерує результати, а нейронна мережа їх фільтрує, у VERIGATE LLM генерує структуровані гіпотези, а символьний аналіз незалежно їх верифікує. У ході експериментальних досліджень було підтверджено ефективність запропонованого методу: покращення F1-score на 76.4% та recall на 187% порівняно з GPT-4 Baseline, стабільне покращення з GPT-5.2, а також збалансований внесок кожного архітектурного компоненту. Особистий внесок здобувача. Усі основні результати дисертаційного дослідження, представлені до захисту, одержані автором особисто. Здобувачем виконано: аналіз існуючих методів статичного аналізу коду та нейросимвольних систем; розробку нейросимвольного методу VERIGATE з механізмами Explain-Verify Gate та Evidence-Weighted Suppression; формалізацію процесу верифікації структурованих тверджень; розробку програмного прототипу; проведення експериментальної оцінки та аналіз результатів. У публікаціях у співавторстві здобувачеві належать: дослідження існуючих методів, проектування архітектури нейросимвольного методу, розробка механізмів верифікації та прийняття рішень, експериментальне підтвердження ефективності запропонованого методу. Апробація матеріалів дисертації. Основні положення та отримані наукові результати, що викладені в даній дисертації, пройшли апробацію через їх презентацію на міжнародній науковій конференції — 4th International Scientific and Practical Conference «Science and Information Technologies in the Modern World» (Афіни, Греція, 24–26 грудня 2025р.).
Опис
Ключові слова
великі мовні моделі, нейросимвольний аналіз, статичний аналіз коду, верифікація програм, символьний аналіз, виявлення дефектів, аналіз вразливостей, семантичний аналіз, машинне навчання, нейронні мережі, штучний інтелект, інженерія програмного забезпечення, надійність програмного забезпечення, інтелектуальна обробка, життєвий цикл розробки програмного забезпечення, large language models, neurosymbolic analysis, static code analysis, program verification, symbolic analysis, defect detection, vulnerability analysis, semantic analysis, machine learning, neural networks, artificial intelligence, software engineering, software reliability, intelligent processing, software development life cycle
Бібліографічний опис
Вохранов, І. А. Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей : дис. … д-ра філософії : 122 Комп’ютерні науки / Вохранов Ілля Анатолійович. – Київ, 2026. – 140 с.