https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

\n","updatedAt":"2024-08-16T02:38:46.297Z","author":{"_id":"60f1abe7544c2adfd699860c","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1674929746905-60f1abe7544c2adfd699860c.jpeg","fullname":"AK","name":"akhaliq","type":"user","isPro":false,"isHf":true,"isHfAdmin":false,"isMod":false,"followerCount":9178,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.4283837080001831},"editors":["akhaliq"],"editorAvatarUrls":["https://cdn-avatars.huggingface.co/v1/production/uploads/1674929746905-60f1abe7544c2adfd699860c.jpeg"],"reactions":[],"isReport":false}},{"id":"66bf0f0585c8bcb5f2075987","author":{"_id":"63a369d98c0c89dcae3b8329","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63a369d98c0c89dcae3b8329/AiH2zjy1cnt9OADAAZMLD.jpeg","fullname":"Adina Yakefu","name":"AdinaY","type":"user","isPro":false,"isHf":true,"isHfAdmin":false,"isMod":false,"followerCount":1145,"isUserFollowing":false},"createdAt":"2024-08-16T08:34:13.000Z","type":"comment","data":{"edited":false,"hidden":false,"latest":{"raw":"Congrats on the paper 🔥 Impressive work!","html":"

Congrats on the paper 🔥 Impressive work!

\n","updatedAt":"2024-08-16T08:34:13.544Z","author":{"_id":"63a369d98c0c89dcae3b8329","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63a369d98c0c89dcae3b8329/AiH2zjy1cnt9OADAAZMLD.jpeg","fullname":"Adina Yakefu","name":"AdinaY","type":"user","isPro":false,"isHf":true,"isHfAdmin":false,"isMod":false,"followerCount":1145,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.838934600353241},"editors":["AdinaY"],"editorAvatarUrls":["https://cdn-avatars.huggingface.co/v1/production/uploads/63a369d98c0c89dcae3b8329/AiH2zjy1cnt9OADAAZMLD.jpeg"],"reactions":[],"isReport":false}},{"id":"66bffda4eb4f43ee8a97dc77","author":{"_id":"63d3e0e8ff1384ce6c5dd17d","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1674830754237-63d3e0e8ff1384ce6c5dd17d.jpeg","fullname":"Librarian Bot (Bot)","name":"librarian-bot","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":318,"isUserFollowing":false},"createdAt":"2024-08-17T01:32:20.000Z","type":"comment","data":{"edited":false,"hidden":false,"latest":{"raw":"This is an automated message from the [Librarian Bot](https://huggingface.co/librarian-bots). I found the following papers similar to this paper. \n\nThe following papers were recommended by the Semantic Scholar API \n\n* [Lean-STaR: Learning to Interleave Thinking and Proving](https://huggingface.co/papers/2407.10040) (2024)\n* [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://huggingface.co/papers/2407.17227) (2024)\n* [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://huggingface.co/papers/2407.03203) (2024)\n* [Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent](https://huggingface.co/papers/2407.14521) (2024)\n* [Large Language Model for Verilog Generation with Golden Code Feedback](https://huggingface.co/papers/2407.18271) (2024)\n\n\n Please give a thumbs up to this comment if you found it helpful!\n\n If you want recommendations for any Paper on Hugging Face checkout [this](https://huggingface.co/spaces/librarian-bots/recommend_similar_papers) Space\n\n You can directly ask Librarian Bot for paper recommendations by tagging it in a comment: `@librarian-bot recommend`","html":"

This is an automated message from the Librarian Bot. I found the following papers similar to this paper.

\n

The following papers were recommended by the Semantic Scholar API

\n

\n
• Lean-STaR: Learning to Interleave Thinking and Proving (2024)
\n
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover (2024)
\n
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts (2024)
\n
• Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent (2024)
\n
• Large Language Model for Verilog Generation with Golden Code Feedback (2024)
\n

\n

Please give a thumbs up to this comment if you found it helpful!

\n

If you want recommendations for any Paper on Hugging Face checkout this Space

\n

You can directly ask Librarian Bot for paper recommendations by tagging it in a comment: \n\n@librarian-bot\n\t recommend

\n","updatedAt":"2024-08-17T01:32:20.813Z","author":{"_id":"63d3e0e8ff1384ce6c5dd17d","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1674830754237-63d3e0e8ff1384ce6c5dd17d.jpeg","fullname":"Librarian Bot (Bot)","name":"librarian-bot","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":318,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.7230165004730225},"editors":["librarian-bot"],"editorAvatarUrls":["https://cdn-avatars.huggingface.co/v1/production/uploads/1674830754237-63d3e0e8ff1384ce6c5dd17d.jpeg"],"reactions":[],"isReport":false}}],"primaryEmailConfirmed":false,"paper":{"id":"2408.08152","authors":[{"_id":"66bebba0c55655c7150bb379","user":{"_id":"6532a060a78e70d19c669103","avatarUrl":"/avatars/3cc9309b0e31da0fb83f1c3ef87dbe9f.svg","isPro":false,"fullname":"HuajianXin","user":"HuajianXin","type":"user"},"name":"Huajian Xin","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:34:26.149Z","hidden":false},{"_id":"66bebba0c55655c7150bb37a","name":"Z. Z. Ren","hidden":false},{"_id":"66bebba0c55655c7150bb37b","user":{"_id":"6565a2dd131d13ccc5d8cb12","avatarUrl":"/avatars/f5c5441ba74791b64c9740911f952bac.svg","isPro":false,"fullname":"Junxiao Song","user":"haha-point","type":"user"},"name":"Junxiao Song","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:34:35.317Z","hidden":false},{"_id":"66bebba0c55655c7150bb37c","user":{"_id":"65db64f8b62d242ed8711701","avatarUrl":"/avatars/753e9f980eb6786c6b53b2f1becbf745.svg","isPro":false,"fullname":"Zhihong Shao","user":"ZhihongShao","type":"user"},"name":"Zhihong Shao","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:34:41.552Z","hidden":false},{"_id":"66bebba0c55655c7150bb37d","name":"Wanjia Zhao","hidden":false},{"_id":"66bebba0c55655c7150bb37e","name":"Haocheng Wang","hidden":false},{"_id":"66bebba0c55655c7150bb37f","user":{"_id":"635e3a76106f984574c36409","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1667120725800-635e3a76106f984574c36409.png","isPro":false,"fullname":"Bo Liu","user":"Benjamin-eecs","type":"user"},"name":"Bo Liu","status":"claimed_verified","statusLastChangedAt":"2024-08-16T08:19:20.542Z","hidden":false},{"_id":"66bebba0c55655c7150bb380","name":"Liyue Zhang","hidden":false},{"_id":"66bebba0c55655c7150bb381","user":{"_id":"65965cd1c4941e82831cb659","avatarUrl":"/avatars/1aefb9cf4a124cd82f1db58d3a004a0e.svg","isPro":false,"fullname":"Xuan Lu","user":"lx09","type":"user"},"name":"Xuan Lu","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:35:20.244Z","hidden":false},{"_id":"66bebba0c55655c7150bb382","name":"Qiushi Du","hidden":false},{"_id":"66bebba0c55655c7150bb383","user":{"_id":"663a24590966eef8680e70ed","avatarUrl":"/avatars/32cd23e8f8405d62e245723510b2e36a.svg","isPro":false,"fullname":"wenjun gao","user":"wjga001","type":"user"},"name":"Wenjun Gao","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:35:35.828Z","hidden":false},{"_id":"66bebba0c55655c7150bb384","user":{"_id":"63cd76b4374057a338e8e703","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63cd76b4374057a338e8e703/i4Qk5-0aYx3oRhC8b50aJ.jpeg","isPro":false,"fullname":"zhuqihao","user":"zqh11","type":"user"},"name":"Qihao Zhu","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:35:46.380Z","hidden":false},{"_id":"66bebba0c55655c7150bb385","user":{"_id":"6225bb44c6e650de3a65dbaa","avatarUrl":"/avatars/99c99ced2461978df572c27c1b3a4904.svg","isPro":false,"fullname":"DejianYang","user":"DejianYang","type":"user"},"name":"Dejian Yang","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:35:55.805Z","hidden":false},{"_id":"66bebba0c55655c7150bb386","user":{"_id":"62dcf5d4169bd1d2ef2ca724","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/62dcf5d4169bd1d2ef2ca724/oRFFmJDJTLYtPRVPCweQ_.jpeg","isPro":false,"fullname":"Zhibin Gou","user":"zubingou","type":"user"},"name":"Zhibin Gou","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:36:06.134Z","hidden":false},{"_id":"66bebba0c55655c7150bb387","name":"Z. F. Wu","hidden":false},{"_id":"66bebba0c55655c7150bb388","user":{"_id":"6538815d1bdb3c40db94fbfa","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6538815d1bdb3c40db94fbfa/id7aSY8JUgKK2agKWLERt.jpeg","isPro":false,"fullname":"Fuli Luo","user":"luofuli","type":"user"},"name":"Fuli Luo","status":"admin_assigned","statusLastChangedAt":"2024-08-16T08:36:54.274Z","hidden":false},{"_id":"66bebba0c55655c7150bb389","user":{"_id":"6398203609f12714ed1935c2","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6398203609f12714ed1935c2/uXgl0LgKnFYjq1Wz39-a6.jpeg","isPro":false,"fullname":"Chong Ruan","user":"Chester111","type":"user"},"name":"Chong Ruan","status":"claimed_verified","statusLastChangedAt":"2024-08-17T05:38:46.449Z","hidden":false}],"publishedAt":"2024-08-15T13:40:03.000Z","submittedOnDailyAt":"2024-08-16T01:08:46.289Z","title":"DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for\n Reinforcement Learning and Monte-Carlo Tree Search","submittedOnDailyBy":{"_id":"60f1abe7544c2adfd699860c","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1674929746905-60f1abe7544c2adfd699860c.jpeg","isPro":false,"fullname":"AK","user":"akhaliq","type":"user"},"summary":"We introduce DeepSeek-Prover-V1.5, an open-source language model designed for\ntheorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both\ntraining and inference processes. Pre-trained on DeepSeekMath-Base with\nspecialization in formal mathematical languages, the model undergoes supervised\nfine-tuning using an enhanced formal theorem proving dataset derived from\nDeepSeek-Prover-V1. Further refinement is achieved through reinforcement\nlearning from proof assistant feedback (RLPAF). Beyond the single-pass\nwhole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a\nvariant of Monte-Carlo tree search that employs an intrinsic-reward-driven\nexploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5\ndemonstrates significant improvements over DeepSeek-Prover-V1, achieving new\nstate-of-the-art results on the test set of the high school level miniF2F\nbenchmark (63.5%) and the undergraduate level ProofNet benchmark (25.3%).","upvotes":61,"discussionId":"66bebba1c55655c7150bb3ac","githubRepo":"https://github.com/deepseek-ai/deepseek-prover-v1.5","githubRepoAddedBy":"auto","ai_summary":"DeepSeek-Prover-V1.5 improves theorem proving by optimizing training and inference, utilizing reinforcement learning, and proposing RMaxTS for diverse proof paths, achieving state-of-the-art results on miniF2F and ProofNet benchmarks.","ai_keywords":["DeepSeek-Prover-V1.5","language model","theorem proving","Lean 4","DeepSeekMath-Base","supervised fine-tuning","RLPAF","Monte-Carlo tree search","RMaxTS","intrinsic-reward-driven exploration","miniF2F","ProofNet"],"githubStars":552,"organization":{"_id":"652faff917096ceb6bf53f3f","name":"deepseek-ai","fullname":"DeepSeek","avatar":"https://cdn-uploads.huggingface.co/production/uploads/6538815d1bdb3c40db94fbfa/xMBly9PUMphrFVMxLX4kq.png"}},"canReadDatabase":false,"canManagePapers":false,"canSubmit":false,"hasHfLevelAccess":false,"upvoted":false,"upvoters":[{"_id":"621d6f532165dc431641e438","avatarUrl":"/avatars/56ccef10a8426d7160ef3586a771bd63.svg","isPro":false,"fullname":"Kiran Kamble","user":"kiranr","type":"user"},{"_id":"620783f24e28382272337ba4","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/620783f24e28382272337ba4/zkUveQPNiDfYjgGhuFErj.jpeg","isPro":false,"fullname":"GuoLiangTang","user":"Tommy930","type":"user"},{"_id":"62fc758172a7ab50b4b89c8c","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/1677251053045-62fc758172a7ab50b4b89c8c.jpeg","isPro":false,"fullname":"Zhicheng Sun","user":"feifeiobama","type":"user"},{"_id":"6565a2dd131d13ccc5d8cb12","avatarUrl":"/avatars/f5c5441ba74791b64c9740911f952bac.svg","isPro":false,"fullname":"Junxiao Song","user":"haha-point","type":"user"},{"_id":"641aef7b1911d3be67425338","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/641aef7b1911d3be67425338/CmCbWWB6NxkAaus59q31w.jpeg","isPro":false,"fullname":"Qi Liu (SJTU & SII)","user":"purewhite42","type":"user"},{"_id":"637c6703ca8542a0ba900ccb","avatarUrl":"/avatars/288ed63a1efa566c3f01e850c6ba5dd5.svg","isPro":false,"fullname":"Wang","user":"Benyou","type":"user"},{"_id":"638efcf4c67af472d316d424","avatarUrl":"/avatars/97a57859d7d87a3a8f1bb41d32a72bc2.svg","isPro":false,"fullname":"Ge Zhang","user":"zhangysk","type":"user"},{"_id":"6032802e1f993496bc14d9e3","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6032802e1f993496bc14d9e3/w6hr-DEQot4VVkoyRIBiy.png","isPro":false,"fullname":"Omar Sanseviero","user":"osanseviero","type":"user"},{"_id":"62a4ac6fd83c3facafa50892","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/62a4ac6fd83c3facafa50892/qFpobw9B5XaLZvwn0XbmB.jpeg","isPro":false,"fullname":"Mohammed Brıman","user":"mohammedbriman","type":"user"},{"_id":"63a369d98c0c89dcae3b8329","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63a369d98c0c89dcae3b8329/AiH2zjy1cnt9OADAAZMLD.jpeg","isPro":false,"fullname":"Adina Yakefu","user":"AdinaY","type":"user"},{"_id":"646ddc68deb963805b31b9f8","avatarUrl":"/avatars/2c266d28e947af7b447df426ab78423d.svg","isPro":false,"fullname":"martin","user":"martintomov","type":"user"},{"_id":"63486df1f8f01fcc4b23e97d","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/63486df1f8f01fcc4b23e97d/RDpX29ibKTJhgisgtvZ6M.png","isPro":false,"fullname":"Satyam","user":"satyamt","type":"user"}],"acceptLanguages":["*"],"dailyPaperRank":1,"organization":{"_id":"652faff917096ceb6bf53f3f","name":"deepseek-ai","fullname":"DeepSeek","avatar":"https://cdn-uploads.huggingface.co/production/uploads/6538815d1bdb3c40db94fbfa/xMBly9PUMphrFVMxLX4kq.png"}}">