Семинар АИРИ
Следующий семинар AIRI по искусственному интеллекту пройдет уже 12 апреля в 17:00, делимся подробностями:

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

Докладчик: Ермек Капушев, AIRI
Оппонент: Лев Беклемишев, МИАН, академик РАН

Описание: в докладе будет рассмотрена задача генерации доказательств математических теорем на формальном языке Lean.

Современные большие языковые модели (LLM) умеют решать широкий круг задач, включая математические, но не гарантируют корректность сгенерированных ответов. Использование формальных языков позволяет обойти эту проблему.

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