Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей

Скорочена інформація про документ
dc.contributor.advisorБулах, Богдан Вікторович
dc.contributor.authorВохранов, Ілля Анатолійович
dc.date.accessioned2026-08-25T12:03:28Z
dc.date.available2026-08-25T12:03:28Z
dc.date.issued2026
dc.description.abstractВохранов І. А. Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей. — Кваліфікаційна наукова праця на правах рукопису. Дисертація на здобуття наукового ступеня доктора філософії за спеціальністю 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р.).
dc.description.abstractotherVokhranov I. A. Method of Static Analysis of Program Source Code Using Large Language Models. — Qualifying scientific work as a manuscript. Dissertation for the degree of Doctor of Philosophy in specialty 122 — Computer Science. — National Technical University of Ukraine "Igor Sikorsky Kyiv Polytechnic Institute", Ministry of Education and Science of Ukraine, Kyiv, 2026. The aim of the dissertation research is the development, formal description, and experimental evaluation of a neurosymbolic method for static analysis of program source code using large language models, which ensures controlled LLM behavior through independent symbolic verification of generated claims, enabling high defect detection recall while preserving precision and predictability of results. The object of the research is the processes of static analysis of program source code aimed at detecting defects and vulnerabilities. The subject of the research is neurosymbolic methods for static analysis that combine the semantic understanding of large language models with independent symbolic verification to ensure controlled and predictable behavior. The following research methods were used in the dissertation: analysis and systematization of scientific sources to determine the state of research in the fields of static code analysis and neurosymbolic systems; formalization for describing the architecture and algorithms of the proposed method; modeling for designing the architecture of the proposed method and the interactions of its components; experiment for empirical evaluation of the method's effectiveness on real data; comparative analysis for comparing results with existing approaches; ablation study for determining the contribution of each architectural component. These methods were chosen considering the aim and objectives of the research, as well as their suitability for addressing the problems of controllable usage of large language models in static code analysis tasks. The dissertation proposes for the first time a neurosymbolic method for static analysis of program source code, which is distinguished by the fact that at the first stage of analysis the LLM directly generates structured claims about code defects, followed by a symbolic analysis stage for their verification, whereas in existing neurosymbolic methods for static code analysis (IRIS, LLMSA, MoCQ) the opposite holds — the symbolic component performs primary detection or structuring of defects, while the neural component filters or supplements its results. The inverted direction of neurosymbolic verification "Neural → Symbolic" enables leveraging the large language model's ability to perceive code semantics while simultaneously maintaining strict control over its generated claims, facilitating the detection of a broader range of defects with minimal risks of model hallucination. For the first time, an approach to verification of structured defect claims using symbolic analysis — the Explain-Verify Gate — is proposed, whose distinctive feature is that the attributes of the defect claim (defect type, location, proposed minimally sufficient fix, and rationale) determine the selection and interpretation of subsequent symbolic checks (AST pattern matching, taint analysis, fix plausibility checking), which differs from existing verification approaches in neurosymbolic code analysis methods and ensures verification determinism without the need to re-query the language model for justification of each decision it has made. The defect decision-making process in neurosymbolic static code analysis is improved through the application of the Evidence-Weighted Suppression (EWS) mechanism, which weighs evidence from multiple independent sources (static analysis tools, AST patterns, base analyzer confidence score), differing from the defect determination process in existing neurosymbolic approaches, in which rejection of a result at the verification stage is final without considering evidence from other sources. This enables balancing analysis precision and recall by recovering valid defect detections that are rejected by symbolic verification due to the absence of matching patterns but are supported by sufficient evidence from other sources. The developed method for static code analysis enables the detection of additional defects that are missed both by rule-based tools and by direct use of the LLM. Experimental evaluation on 1,000 samples from the PySStuBs dataset confirmed the detection of 247 additional defects compared to the baseline LLM approach (379 vs. 132) and 371 additional defects compared to the rule-based tool ensemble (379 vs. 8), corresponding to a recall improvement of 187% and an F1-score improvement of 76.4% while maintaining a comparable precision level (~0.51). Detection of these additional defects at the static analysis stage prevents them from reaching later stages of development, where the cost of their remediation increases substantially. The analysis results produced by the proposed method are presented as a structured defect description (type, location, rationale, minimally required fix), which is always accompanied by symbolic verification results, reducing the developer's time spent on analyzing and resolving detected issues and substantially facilitating integration of the method into automated code quality control processes (CI/CD, code review), where defect decisions must be based on verified evidence rather than solely on language model output. The proposed analysis method does not require model fine-tuning or collection of specialized datasets, which reduces deployment and maintenance costs compared to fine-tuning-based approaches that require training data preparation, computational resources for training, and retraining when the model changes. Experimental application of GPT-5.2 (RQ2) confirmed the preservation of the proposed method's advantages over existing static code analysis methods when transitioning to a newer generation language model (+132% F1-score, +363% recall), indicating the possibility of updating the neural component without modifying the rest of the system's components, which substantially reduces costs. The method provides the ability to customize for diverse specific analysis tasks without changing the overall architecture: the analysis type and target defect classes are defined in the content of the query to the neural network component (analogous to the customizable analysis property in LLMSA), while symbolic verification coverage is extended by adding new rules, AST patterns, and taint specifications to support new programming languages and defect types. The ablation study (RQ3) confirmed the architecture's resilience to modifications of individual components: F1-score across configurations varies within the range of 0.654–0.668. The dissertation consists of five chapters. The first chapter examines the theoretical foundations of program code analysis using neural networks. Classical static analysis methods are analyzed (data flow analysis, control flow analysis, abstract interpretation, symbolic execution, model checking, syntactic analysis and pattern matching), their advantages and fundamental limitations are identified, including the path explosion problem and SMT solver limitations. The evolution of neural methods in code analysis is explored — from classical machine learning through pre-trained models (CodeBERT, GraphCodeBERT) to large language models (GPT-4, GPT-5.2). The concept of neurosymbolic integration and types of neurosymbolic systems are examined, substantiating the need for a hybrid approach that combines the semantic understanding of neural models with the formal guarantees of symbolic methods. The second chapter provides an analysis of current research in the field of static code analysis. Existing neurosymbolic program analysis methods are systematized: IRIS (symbolic → neural direction, CodeQL → LLM), LLMSA (compositional neurosymbolic analysis), MoCQ (iterative pattern refinement). A common limitation of existing methods is identified — the absence of an explicit mechanism for independent verification of LLM claims. Requirements for a method that fills this gap are formulated, and the positioning of VERIGATE as the first method implementing the Neural → Symbolic direction in the context of static code analysis is substantiated. The third chapter provides a detailed description of the proposed VERIGATE method. The architecture of the four-stage pipeline is presented: preliminary screening (tool ensemble and AST rules), Explain (generation of structured LLM claims in JSON format), Verify (symbolic verification through a multi-stage decision tree), final decision with the Evidence-Weighted Suppression mechanism. The verification process is formalized, criteria for accepting and rejecting claims are described, along with the span alignment mechanism and taint analysis. A comparison of VERIGATE's architectural decisions with existing neurosymbolic systems is conducted based on key characteristics (interaction direction, LLM role, symbolic system role, explainability). Implementation details are described: technology stack, LLM prompt format, LLM output processing. An end-to-end example of VERIGATE operation on a real code fragment from the PySStuBs dataset is provided, demonstrating neurosymbolic component interaction through the detection of a semantic logic defect. The fourth chapter presents the results of experimental evaluation. The main evaluation (RQ1) was conducted on 1,000 balanced samples from the PySStuBs (Python Single-Statement Bugs) dataset using GPT-4. Comparison of three methods (VERIGATE, GPT-4 Baseline, Rule-Based) demonstrated: an F1-score improvement of 76.4% (0.612 vs. 0.347) and a recall improvement of 187% (0.758 vs. 0.264) compared to the GPT-4 baseline at comparable precision (~0.51). Rule-based tools demonstrated very low effectiveness (F1 = 0.031), confirming the semantic complexity of defects in the dataset. Validation with GPT-5.2 (RQ2, n = 500) confirmed stable improvement: +132% F1-score, +363% recall, indicating the robustness of neurosymbolic verification as an architectural principle across language model generations. The ablation study (RQ3, n = 500) demonstrated that VERIGATE functions as an integrated pipeline with a narrow F1 range (0.654–0.668) across all configurations, where each component makes an independent contribution to overall effectiveness. The fifth chapter examines the prospects for development and generalization of the proposed method. Directions for extension to new programming languages, new defect classes, and integration with production software development processes (CI/CD, code review, IDE) are analyzed. Limitations of the current implementation and ways to overcome them are identified. The dissertation proposes the neurosymbolic VERIGATE method for static analysis of program source code, which through the use of independent symbolic verification of LLM claims enables combining the semantic understanding of program source code provided by the large language model with the justification of each detection in verified program properties. The core idea of the method lies in the inversion of the neurosymbolic interaction direction: instead of the traditional approach where symbolic analysis generates results and the neural network filters them, in VERIGATE the LLM generates structured hypotheses and symbolic analysis independently verifies them. Experimental studies confirmed the effectiveness of the proposed method: an F1-score improvement of 76.4% and a recall improvement of 187% compared to the GPT-4 Baseline, stable improvement with GPT-5.2, and a balanced contribution of each architectural component. Personal contribution of the applicant. All main results of the dissertation research presented for defense were obtained by the author personally. The applicant performed: analysis of existing methods for static code analysis and neurosymbolic systems; development of the neurosymbolic VERIGATE method with the Explain-Verify Gate and Evidence-Weighted Suppression mechanisms; formalization of the structured claim verification process; development of the software prototype; conducting the experimental evaluation and analysis of results. In co-authored publications, the applicant contributed: research of existing methods, design of the neurosymbolic method architecture, development of verification and decision-making mechanisms, experimental confirmation of the proposed method's effectiveness. Approbation of dissertation materials. The main findings and scientific results presented in this dissertation were approbated through their presentation at the international scientific conference — 4th International Scientific and Practical Conference "Science and Information Technologies in the Modern World" (Athens, Greece, December 24–26, 2025).
dc.format.extent140 с.
dc.identifier.citationВохранов, І. А. Метод статичного аналізу вихідного коду програм із використанням великих мовних моделей : дис. … д-ра філософії : 122 Комп’ютерні науки / Вохранов Ілля Анатолійович. – Київ, 2026. – 140 с.
dc.identifier.urihttps://ela.kpi.ua/handle/123456789/82694
dc.language.isouk
dc.publisherКПІ ім. Ігоря Сікорського
dc.publisher.placeКиїв
dc.subjectвеликі мовні моделі
dc.subjectнейросимвольний аналіз
dc.subjectстатичний аналіз коду
dc.subjectверифікація програм
dc.subjectсимвольний аналіз
dc.subjectвиявлення дефектів
dc.subjectаналіз вразливостей
dc.subjectсемантичний аналіз
dc.subjectмашинне навчання
dc.subjectнейронні мережі
dc.subjectштучний інтелект
dc.subjectінженерія програмного забезпечення
dc.subjectнадійність програмного забезпечення
dc.subjectінтелектуальна обробка
dc.subjectжиттєвий цикл розробки програмного забезпечення
dc.subjectlarge language models
dc.subjectneurosymbolic analysis
dc.subjectstatic code analysis
dc.subjectprogram verification
dc.subjectsymbolic analysis
dc.subjectdefect detection
dc.subjectvulnerability analysis
dc.subjectsemantic analysis
dc.subjectmachine learning
dc.subjectneural networks
dc.subjectartificial intelligence
dc.subjectsoftware engineering
dc.subjectsoftware reliability
dc.subjectintelligent processing
dc.subjectsoftware development life cycle
dc.subject.udc004.8+004.41
dc.titleМетод статичного аналізу вихідного коду програм із використанням великих мовних моделей
dc.title.alternativeMethod of Static Analysis of Program Source Code Using Large Language Models
dc.typeThesis Doctoral

Файли

Контейнер файлів
Зараз показуємо 1 - 1 з 1
Ескіз
Назва:
Vokhranov_dys.pdf
Розмір:
1.83 MB
Формат:
Adobe Portable Document Format
Завантажити
Ліцензійна угода
Зараз показуємо 1 - 1 з 1
Ескіз недоступний
Назва:
license.txt
Розмір:
8.98 KB
Формат:
Item-specific license agreed upon to submission
Опис:
Завантажити

Зібрання

Дисертації (СП)
Дисертації (вільний доступ)