Lean-STaR: Учим чередовать мышление и доказательство в математических теоремах

Lean-STaR — это фреймворк, который дает ИИ степень PhD по математике. Он учит языковые модели сочетать рассуждения с жесткими математическими доказательствами и переворачивает мир автоматизированного доказательства теорем.

Lean-STaR использует LLM, чтобы излагать мысли на простом английском языке для каждого этапа проверки, основываясь на примерах из Mathlib, которая, по сути, является Ленинкой для Lean доказательств.

Затем эти рассуждения объединяются с соответствующими шагами проверки, создавая прокачанный набор данных, который помогает модели не только предсказать следующий шаг в проверке, но и понять "почему", стоящее за ним.

Но на этом дело не заканчивается. Lean-STaR использует "expert iteration" для совершенствования своих навыков. Она отбирает потенциальные доказательства, и только те, которые проходят проверку, используются для повторного обучения модели. Представьте, что профессиональный спортсмен просматривает видеозапись игры, чтобы улучшить свои выступления - вот это оно.

Почему это важно? Неформальные знания — своего рода интуитивные рассуждения, которые обычно не учитываются при формальном доказательстве. Lean-STaR умеет изучать различные аспекты процесса доказательства, повышая его точность и масштабируемость.

Lean-STaR бьет рекорды в тестировании miniF2F, значительно превосходя другие модели. Это не просто расширяет границы доказательства теорем, это открывает новые возможности для искусственного интеллекта в математике.

Чтобы попробовать локально все прелести Lean-STaR, авторы подготовили для вас 4 модели:

Lean-CoT: Обе версии Lean-CoT генерируют идеи и предсказывают тактику проверки, но “plus” обладает лучшей логикой;

Lean-STaR: более продвинутая версия Lean-CoT, в нее добавлен этап expert iteration, "plus" обладает лучшей логикой, чем "base".

Установка и запуск:

# # Install Python packages:

bash scripts/prepare_env.sh

# Install Lean:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

source $HOME/.elan/env

lake

# Configure LeanDojo:

export CONTAINER="native"

# Evaluation:

cd gpt-fast

bash scripts_intern/inverse_intern_math_7b.sh

bash scripts_intern/sample_cot_7b.sh

# Finetune:

cd gpt-fast

bash scripts_intern/prepare_intern_math_7b.sh

bash scripts_intern/finetune_7b_intern.sh

bash scripts_intern/finetune_7b_cot.sh

bash scripts_intern/finetune_7b_star.shy

Страница проекта (https://leanstar.github.io/)

Набор моделей (https://huggingface.co/collections/ScalableMath/lean-star-6692d8c18db712bad78f0862)

Arxiv (https://arxiv.org/pdf/2407.10040)

Github (https://github.com/Lagooon/LeanSTaR) [ Stars: 10 | Issues: 2 | Forks: 1]

Источник: leanstar.github.io

Комментарии: