НЕЙРОМЕРЕЖЕВІ МЕТОДИ ФОРМАЛІЗАЦІЇ МАТЕМАТИЧНИХ ТЕКСТІВ

Анотація

У цій статті досліджуються можливості великих мовних моделей (ВММ) для автоматизації перетворення математичних тверджень із природної мови у формальні вирази, що спрощує процес пошуку та генерації розв’язань. Завдяки досягненням в області штучного інтелекту, такі моделі як GPT-4 і LLaMA-3 представляють перспективні можливості для вирішення задачі математичної формалізації текстів. Ці моделі демонструють значні здібності до розуміння та перекладу текстів, що зменшує невизначеності у природномовній версії математичних задач та поліпшує процес збільшення математичної бази знань відповідних систем. Ефективність цих моделей оцінюється в переході від природної мови до математичного формалізму. Хоча ВММ показують значні результати у семантичному аналізі, точні обчислення і символічні маніпуляції потребують подальших удосконалень. Інтеграція з системами автоматичних доведень, такими як LEAN, досліджується для поліпшення процесу побудови формальних доведень. Отримані результати вказують на великий потенціал використання моделей штучного інтелекту в автоматизації математичного міркування.