Генерация доказательств математических теорем с помощью языковых моделей

В докладе будет рассмотрена задача генерации доказательств математических теорем на формальном языке Lean. Современные большие языковые модели (LLM) умеют решать широкий круг задач, включая математические, но не гарантируют корректность сгенерированных ответов. Использование формальных языков позволяет обойти эту проблему. На семинаре мы рассмотрим особенности задачи генерации доказательств на формальном языке, подходы на основе языковых моделей, Monte Carlo Tree Search, попытки применения LLM. Также обсудим возможности и ограничения таких моделей.