【AI無双】数学の定理証明AI「DeepSeek-Prover-V2」爆誕！もう数学者いらねえんじゃね？ｗｗｗ
1: 名無しさん＠おーぷん 2025/05/13(火) 10:00:00.00 ID:DeepSeekMaster またヤバいAI出てきたぞｗｗｗ DeepSeek AIってところが数学の定理証明に特化したLLM「DeepSeek-Prover-V2」を発表したらしい。 なんでも再帰的証明探索とかいうので、自分で学習データ作って強くなるとか…もうわけわからん(´・ω・｀) ソース：DeepSeek Unveils DeepSeek-Prover-V2: Advancing Neural Theorem Proving with Recursive Proof Search and a New Benchmark
2: 名無しさん＠おーぷん 2025/05/13(火) 10:01:30.50 ID:MathemaChaoS ファッ！？ついに数学の領域までAIが進出してきたんか… MiniF2Fで88.9%って、そこらの学生より賢いやんけ！
3: 名無しさん＠おーぷん 2025/05/13(火) 10:02:15.75 ID:TheoryCraft >>2 PutnamBenchだと49/658問解決ってなってるぞ。まだまだ難問は厳しいんじゃね？ でも、この進化速度は異常だわ…
4: やる夫 ◆Yaruo.AbCd 2025/05/13(火) 10:03:00.12 ID:YaruoProof オマエラ、まだ人間が数学解いてるのかお？( ＾ω＾) DeepSeek-V3とかいう親玉AIが問題を分解して、子分AIが解くらしいお。 もう数学なんてAIに任せて、オマエラは寝てればいいんだお！
,, -──- ､._ ｒ（ ﾟ ∀ ﾟ ）｣ 数学なんてAIに任せて ヽ( と ノ ヽ お前らは寝てればいいお！ しーＪ
5: 名無しさん＠おーぷん 2025/05/13(火) 10:04:50.22 ID:Lean4User Lean 4環境で動作するってのがミソだな。 最近Lean界隈も盛り上がってるし、こういうツールが出てくるのは歓迎だわ。 しかし671Bパラメータとか、どんなGPU使ったら動くんだよ…(； ･`д･´)
6: ひろゆき＠考える人 ◆Hiroyuki.Xyz 2025/05/13(火) 10:05:30.45 ID:HiroyukiLogic あのー、recursive proof searchって具体的にどういうアルゴリズムなんすかね？ あと、DeepSeek-V3が生成したデータで学習するって、それってAIがAIの先生やってるってことっすか？ それって、なんかこう…堂々巡りになったりしないんすかね？ データ汚染とか大丈夫なんすか？🤔
7: 名無しさん＠おーぷん 2025/05/13(火) 10:06:12.88 ID:AIWatcher25 >>6 「高品質な初期化データ」って書いてあるから、そこは工夫してるんじゃない？ 強化学習でさらに精度上げてるみたいだし。 まあ、ワイら素人にはブラックボックスやけどなｗ
8: 名無しさん＠おーぷん 2025/05/13(火) 10:07:00.01 ID:BunkeiOuEn 文系ワイ、話の半分も理解できんが、なんかすごいことだけは伝わってくるで！(｀・ω・´) これで数学オリンピックとかもAIが優勝する時代が来るんか？
9: 霧雨魔理沙 ◆Marisa.DaZe 2025/05/13(火) 10:08:45.55 ID:MarisaMagic ProverBenchって新しいベンチマークも作ったのか！ AIMEの問題も入ってるって、なかなか手強そうだな！ 私の新しい魔法の理論構築にも使えるかもしれないぜ！(☆∀☆) こういうのはどんどん出てきてほしいんだぜ！
10: 名無しさん＠おーぷん 2025/05/13(火) 10:09:30.11 ID:TechGuru777 >>5 671BモデルはDeepSeek-V3-Baseがベースで、7BモデルはDeepSeek-Prover-V1.5-Baseがベースらしいな。 7Bモデルの方はコンテキスト長32Kトークンまで拡張されてるから、こっちならワンチャン個人でも…無理かｗ
11: 名無しさん＠おーぷん 2025/05/13(火) 10:10:15.99 ID:FutureShock 数学者がいらなくなる日も近い…？ ((；ﾟДﾟ))))ｶﾞｸｶﾞｸﾌﾞﾙﾌﾞﾙ ワイの数学の宿題、全部こいつにやらせたいンゴ…(^q^)
12: 名無しさん＠おーぷん 2025/05/13(火) 10:11:05.32 ID:PositiveAI >>11 いや、むしろ数学者の強力なアシスタントになるんじゃないか？ 面倒な証明の検証とか、新しい定理の探索とか、協力して進められるようになるんやで。夢があるやん！
13: やる夫 ◆Yaruo.AbCd 2025/05/13(火) 10:12:00.69 ID:YaruoProof >>6 ひろゆき、難しいこと考えすぎだお( ＾ω＾) 解ければ官軍、方式なんてどうでもいいんだお！ 結果が全てだお！
14: 名無しさん＠おーぷん 2025/05/13(火) 10:13:40.81 ID:AI Skeptic Hugging Faceで公開されてるってマジか。 proofs generated by DeepSeek-Prover-V2 for the miniF2F dataset are publicly available for download ってあるから、どんな証明してるか見れるんやな。 これはちょっと興味あるわ。嘘くさい証明してないかチェックせな。
15: ひろゆき＠考える人 ◆Hiroyuki.Xyz 2025/05/13(火) 10:14:55.23 ID:HiroyukiLogic >>13 やる夫さん、それだとAIが間違った証明を「正しい」って言い張っても分かんないじゃないすか。 プロセスも大事だと思うんすよねー。 まぁ、この分野が進化するのは面白いとは思いますけど。嘘は嘘と見抜ける人でないと(ry
16: 名無しさん＠おーぷん 2025/05/13(火) 10:16:02.58 ID:OpenSourceFan オープンソースなのは評価できる。 DeepMindとかOpenAIとかクローズドなモデルばっかだからな。 こうやって研究成果を共有してくれるのはありがたい。
17: 名無しさん＠おーぷん 2025/05/13(火) 10:17:33.19 ID:TechMatome ProverBenchが教育的なチュートリアルからも問題引っ張ってきてるってのは良いな。 基礎的な数学能力の評価にも使えるってことか。 これは研究者だけじゃなくて、教育現場にもインパクトありそう。
18: 霧雨魔理沙 ◆Marisa.DaZe 2025/05/13(火) 10:18:50.76 ID:MarisaMagic >>10 7Bモデルでも32Kトークンは魅力的だな！ 長い呪文の詠唱…じゃなくて、複雑な証明の記述にも耐えられそうだぜ！ うちのミニ八卦炉で回せるかな…(；・∀・)
19: 名無しさん＠おーぷん 2025/05/13(火) 10:20:11.43 ID:FinalAnswer これ、未解決問題とかにも挑戦してるんかな？ ABC予想とかリーマン予想とか解いたらマジで世界変わるでｗｗｗ
20: 名無しさん＠おーぷん 2025/05/13(火) 10:21:25.00 ID:DeepSeekMaster >>19 流石にそこまではまだ…って感じじゃないか？ｗ でも、こういう技術が積み重なって、いつかそういうブレイクスルーが起きるのかもな！ とりあえず、数学苦手なワイはAI様の進化に期待するわｗ (´ω｀)
まとめ
今回のDeepSeek-Prover-V2の発表、ヤバすぎワロタって感じやな！ポイントをまとめるとこんな感じか？
- 定理証明特化AI「DeepSeek-Prover-V2」登場: DeepSeek AIがLean 4環境で動くオープンソースLLMを開発。数学界隈がザワついてるぞ！
- 賢い学習方法: DeepSeek-V3っていう親玉AIが問題を分解して、それを元に学習データを自動生成。さらに強化学習でゴリゴリ鍛え上げられるらしい。まさにAIによるAIのためのスパルタ教育！
- 驚異の性能: MiniF2Fっていうベンチマークで88.9%の正解率を叩き出し、難関のPutnamBenchでも49問を解き明かす実力。もう人間超えてるかも…？
- 新ベンチマーク「ProverBench」も公開: AIME（アメリカの数学コンテスト）の問題や教科書レベルの問題を含む325問を収録。AIの数学力を測る新たな物差しになりそうやな。
- モデルは2サイズ: 超弩級の671Bモデルと、比較的お手頃（？）な7Bモデルがあるらしい。7Bでも結構な性能みたいだから、今後の展開に期待大！
今後のAIと数学の発展から目が離せへんな！ワイらの仕事、大丈夫か…？((((；ﾟДﾟ))))
コメント (0)
まだコメントはありません。