Факультет комп'ютерних наук, фізики та математики
Permanent URI for this communityhttps://ekhsuir.kspu.edu/handle/123456789/10254
Browse
Item ВИКОРИСТАННЯ МЕТОДІВ МАШИННОГО НАВЧАННЯ ДЛЯ ДОВЕДЕННЯ ТЕОРЕМ(2025) Болюк, І. І.Кваліфікаційна робота присвячена дослідженню та розробці методів машинного навчання для автоматизації процесу доведення математичних теорем. Актуальність теми зумовлена обмеженнями класичних алгоритмічних підходів, які стикаються з проблемою комбінаторного вибуху при пошуку доказів у складних формальних системах. У роботі проведено аналіз сучасних архітектур (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.