Goedel-Prover-V2-8B VLG planner LoRA

Это три LoRA-адаптера (PEFT) к Goedel-Prover-V2-8B, которые превращают 8B-модель в planner для VLG-прувера. На вход — теорема Lean 4, на выход — короткий proof sketch: план прозой, Lean-блок с 2–6 промежуточными have и sorry, затем тактики закрытия основной цели. Базовые веса не входят; адаптер: r=64, α=128, 174.6M обучаемых параметров, 698.4 MB.

⚙ Ключевые особенности

• 🎯 Три варианта по объёму данных: pilot — 422 строки, planner-1k — 1 046 (рекомендуется), planner-alldata-s1 — 12 062.
• ⚙ Только SFT: masked cross-entropy на парах statement → sketch; без RL, DPO, PRM и expert iteration.
• 🧩 Каждый sketch проверен в Lean: верхнеуровневые have поднимаются до sorry, затем тактики закрывают главную цель.
• 📀 LoRA по q/k/v/o/gate/up/down во всех 36 слоях: 504 тензора, 174.6M параметров, fp32.
• ⚡ Обучение на 4× NVIDIA L4 24.2 GB: 13 мин / 26 мин / 5.05 ч для трёх адаптеров.

🎯 Пример

Вход: theorem problem_265486 : ∀ x : ℕ, 2 ∣ x ^ 3 - x ∧ 3 ∣ x ^ 3 - x := by sorry. Выход planner-1k — план из двух промежуточных фактов и Lean-заготовка: have h2 ... := by sorry, have h3 ... := by sorry, затем exact ⟨h2, h3⟩.

Подробнее

Strictly usable plans на 200 planner-VAL задачах × 4 сэмпла: base 1.8% → pilot 36.9% → planner-1k 46.1% → all-data 41.0%.
Хотя бы один строго пригодный план: 5.5% → 71.0% → 75.5% → 69.5%.
В 11.5× больше данных all-data дал на 5.1 п.п. ниже, чем 1k (95% CI [−10.0, −0.25]).
End-to-end proof rate, miniF2F/PutnamBench/ProofNet и несколько сидов не измерялись.