ترجمه فارسی مقاله Deepseek-Prover-V1.5: بازخورد دستیار اثبات برای یادگیری تقویت و جستجوی درخت مونت کارلو

چکیده

We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark ($63.5\%$) and the undergraduate level ProofNet benchmark ($25.3\%$).

چکیده به فارسی (ترجمه ماشینی)

ما Deepseek-Prover-V1.5 را معرفی می کنیم ، یک مدل زبان منبع باز که برای اثبات قضیه در Lean 4 طراحی شده است ، که با بهینه سازی هر دو فرآیند آموزش و استنباط ، Deepseek-Prover-V1 را تقویت می کند.پیش از آموزش در Deepseekmath-Base با تخصص در زبانهای رسمی ریاضی ، این مدل با استفاده از یک مجموعه داده رسمی اثبات شده اثبات شده از Deepseek-Prover-V1 ، تنظیم دقیق نظارت شده را تحت نظارت قرار می دهد.پالایش بیشتر از طریق یادگیری تقویت از بازخورد دستیار اثبات (RLPAF) حاصل می شود.فراتر از رویکرد نسل یک پاس کاملاً ضد Deepseek-Prover-V1 ، ما Rmaxts را پیشنهاد می کنیم ، نوعی از جستجوی درخت مونت کارلو که از یک استراتژی اکتشافی ذاتی-رای محور برای تولید مسیرهای اثبات متنوع استفاده می کند.Deepseek-Prover-V1.5 پیشرفت های قابل توجهی نسبت به Deepseek-Prover-V1 نشان می دهد ، و دستیابی به نتایج جدید پیشرفته در مجموعه آزمون معیار MINIF2F سطح دبیرستان (63.5 \ $ $) و معیار سطح کارشناسی(25.3 دلار \ ٪ $).