ВИКОРИСТАННЯ МЕТОДІВ МАШИННОГО НАВЧАННЯ ДЛЯ ДОВЕДЕННЯ ТЕОРЕМ
| dc.contributor.author | Болюк, І. І. | |
| dc.date.accessioned | 2025-12-22T11:17:15Z | |
| dc.date.issued | 2025 | |
| dc.description | Болюк, І. І. Використання методів машинного навчання для доведення теорем = Using machine learning methods to prove theorems Testing : кваліфікаційна робота на здобуття ступеня вищої освіти «магістр» / І. І. Болюк; наук. к., д. ф.-м. наук, професор, І. Песчаненко; Міністерство освіти і науки України ; Херсонський держ. ун-т, ф-т комп’ютерних наук, фізики та математики, кафедра комп’ютерних наук та програмної інженерії. – Херсон : ХДУ, 2025. – 34 с. | |
| dc.description.abstract | Кваліфікаційна робота присвячена дослідженню та розробці методів машинного навчання для автоматизації процесу доведення математичних теорем. Актуальність теми зумовлена обмеженнями класичних алгоритмічних підходів, які стикаються з проблемою комбінаторного вибуху при пошуку доказів у складних формальних системах. У роботі проведено аналіз сучасних архітектур (Transformer, Graph Neural Networks) та методологій навчання (Supervised Learning, Reinforcement Learning). Розроблено експериментальну гібридну систему, що поєднує формальне середовище (симулятор логіки висловлювань) та агента на основі графової нейронної мережі (GNN), реалізованого за допомогою бібліотеки PyTorch Geometric. Практична частина включала створення синтетичного набору даних (50000 прикладів), навчання моделі для вибору тактик доведення та ітеративне вдосконалення компонентів системи (парсера, словника токенів). Навчена модель досягла точності 79.3% на валідаційній вибірці. У фінальному тестуванні агент продемонстрував здатність самостійно доводити 50% тестових теорем, успішно застосовуючи вивчені логічні патерни. Результати дослідження підтверджують перспективність використання GNN як евристичного інструменту для керування пошуком доказів та окреслюють напрями для подальшого вдосконалення, зокрема впровадження стратегій пошуку променем (Beam Search). / The master's thesis is devoted to the research and development of machine learning methods for automating the process of mathematical theorem proving. The relevance of the topic is driven by the limitations of classical algorithmic approaches, which face the problem of combinatorial explosion when searching for proofs in complex formal systems. The paper analyzes modern architectures (Transformer, Graph Neural Networks) and learning methodologies (Supervised Learning, Reinforcement Learning). An experimental hybrid system was developed, combining a formal environment (propositional logic simulator) and an agent based on a Graph Neural Network (GNN), implemented using the PyTorch Geometric library. The practical part involved creating a synthetic dataset (50000 examples), training the model for proof tactic selection, and iteratively improving system components (parser, token vocabulary). The trained model achieved an accuracy of 79.3% on the validation set. In final testing, the agent demonstrated the ability to independently prove 50% of the test theorems, successfully applying learned logical patterns. The research results confirm the promise of using GNNs as a heuristic tool for guiding proof search and outline directions for future improvements, particularly the implementation of Beam Search strategies. | |
| dc.identifier.uri | https://ekhsuir.kspu.edu/handle/123456789/21738 | |
| dc.subject | машинне навчання | |
| dc.subject | автоматизоване доведення теорем | |
| dc.subject | графові нейронні мережі (GNN) | |
| dc.subject | формальна верифікація | |
| dc.subject | PyTorch Geometric | |
| dc.subject | штучний інтелект | |
| dc.subject | machine learning | |
| dc.subject | automated theorem proving | |
| dc.subject | Graph Neural Networks (GNN) | |
| dc.subject | formal verification | |
| dc.subject | artificial intelligence. | |
| dc.title | ВИКОРИСТАННЯ МЕТОДІВ МАШИННОГО НАВЧАННЯ ДЛЯ ДОВЕДЕННЯ ТЕОРЕМ | |
| dc.title.alternative | USING MACHINE LEARNING METHODS TO PROVE THEOREMS | |
| dc.type | Other |