Використання фреймворку Lean для перевірки коректності математичних міркувань
Loading...
Date
2026
Authors
Кривошея, Олександр
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Магістерську роботу присвячено розробці та дослідженню інтелектуальної програмної системи автоматизованої перевірки розгорнутих геометричних міркувань учнів 7–9 класів на основі фреймворку Lean 4 та великих мовних моделей. Об’єкт дослідження: процеси автоматизованої перевірки правильності математичних викладів у інтелектуальних навчальних середовищах. Предмет дослідження: методи та програмні інструменти інтеграції середовища Lean у рекомендаційну систему для перевірки геометричних доведень. Мета дослідження: розробити та дослідити архітектуру програмного додатка, який використовує ядро Lean для перевірки геометричних міркувань учнів, діагностує рівень їхньої підготовки та надає адаптивні рекомендації на основі виявлених прогалин.
Description
Keywords
Lean 4, перевірка математичних міркувань, нейро-символічна інтеграція, формальна верифікація, великі мовні моделі, планіметрія, формувальне оцінювання, магістерська робота