​​🤩DeepSeek-Prover-V1.5: использование обратной связи помощника по доказательствам для обучения с подкреплением и поиска по дереву Монте-Карло

Языковая модель с открытым исходным кодом, разработанную для доказательства теорем в Lean 4, которая улучшает DeepSeek-Prover-V1 за счет оптимизации как процессов обучения, так и вывода.

Предварительно обученная на DeepSeekMath-Base со специализацией на формальных математических языках, модель проходит контролируемую тонкую настройку с использованием улучшенного набора данных для формального доказательства теорем, полученного из DeepSeek-Prover-V1.

Дальнейшее уточнение достигается за счет обучения с подкреплением с обратной связью помощника по доказательству (RLPAF).

🤗 Hugging Face
💾 Arxiv
📂 PDF

@Devsp — Подписаться