DeepSeek-Prover-V2 ヤバいほど詳細な手順を生成するAIが登場！
引用元：https://news.ycombinator.com/item?id=43847432
“The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals”
LLMが複雑な問題を小さく解きやすいピースに分解する能力って、次のレベルの複雑さを解き明かすカギになるって直感的に感じるね。
これって、ジュニアエンジニアによく教えられるテクニックみたいだ。数週間のプロジェクトを一口サイズのタスクに分解する方法とかさ。このモデルは明らかに数学に特化してるけど、コードベースの問題解決にもめちゃくちゃ強力じゃないかな？
（200字以内要約済）
ほんと、どこまで細かくできるか笑えるレベルだね。
例えばさ、問題文を与えると、それを達成するためのステップの配列を返すボットを作ったことがあるんだ。そのステップを選んでクリックすると、さらに分解してリストに追加できる。クリックし続けると、信じられないくらい詳細になるんだ。
例えば、ゴミ出しとか、本当に詳細に掘り下げると70以上の個別のステップになるよ。いくつか例を挙げると、
ゴミ箱の近くに立つ
片手をゴミ箱の縁に置く
もう一方の手で袋の上の縁を掴む
そっと袋を持ち上げる
必要ならゴミ箱を少し傾ける
急な動きは避ける
（200字以内要約済）
これ、昔うちの学校の導入エンジニアリングコースの一部だったなー。ピーナッツバター＆ジェリーサンドイッチの作り方をXXページの文書で記述するってやつ。
これ、うちの小学校の２年生のときの宿題だったよ！次の日に授業で自分たちの書いた手順通りにサンドイッチ作らなきゃいけなくて、それがめちゃくちゃ面白かったんだ。自分にとっては形成的な経験だったな！
パパが子供たち相手にこれ試してる動画これだよ。
https://www.youtube.com/watch?v=cDA3_5982h8
僕、新しいLLMのテストとして、特定のスタイルでこれ（手順生成）をやるようにしてるんだ。
LLMがロボティクスで使われるときって、多分これにあと1、2レベル詳細な説明が加わる感じで使われるんだろうなって想像してる。
これ、潜入した宇宙人向けのマニュアルみたいだね。「人類として過ごす方法 第一巻」とか。
もしくはゴブリン向けとかね。
https://goblin.tools/
こことか有名だよね。
http://www.drawtoast.com/
うん、LLMは頼めば無限にデタラメを生み出せるよ．
俺の考えだと、今のモデルでも問題を細かく分けられるけど、全体のコンテキスト維持と連続タスクをこなせるエージェント型ツールの実用化が課題だと思う．ツールは最初は良いけど、タスクが進むと混乱しがち．手動で計画ファイルを維持しても限界があるし、Clineみたいなツールは小さな変更でも大量のトークンを使うのが難点だね．
＞壮大なタスクのサブタスクの細かい作業をしてる時に，プロジェクト全体の状況や目標のコンテキスト（何が終わってて，何がまだか）を維持すること＜br＞これ，俺が一緒に仕事した人間みんなが苦労してることだよ．
これはたぶん，コードを書いたことがある人と，絶対コードを書くべきじゃない人の最大の違いだろうね．論理的な矛盾なく複数の関連ファイルを書けない人もいる．まるで脳のコンテキストがファイル1つ分しか持てないみたいにね．
うん．今後の方向性として，チームで働くエージェントのシステムを作るのがいいんじゃないかな，”アーキテクト”とか”テックリード”役のAIが，もっと専門的な実行AIの作業を指示するみたいな．こうすれば，小さい問題に取り組むときにテックリードが全部のコンテキストを持つ必要がなくなるから，コンテキスト汚染の問題を軽減できるかもね．やべ，アジャイルAIが必要になるのか？
これ，roo codeのモードが今やってることと似てるんだよね．俺はこれでうまくいってる．orchestratorモードが他のモード（code，architectなど）を使い分けて，適切なコンテキストを渡してくれる．モードごとにLLMを変えることもできる（Gemini 2.5 Proやgpt o4-mini）．複雑なタスクでも40万トークンを超えることはあまりないよ．詳細はこのリンクを見てね．＜br＞https://docs.roocode.com/features/boomerang-tasks＜br＞https://docs.roocode.com/features/custom-modes
俺はcopilot-instructions.mdファイルに「Boyd’s Law of Iteration」という原則（問題を小さな部分に分解し，一つずつ確認しながら進める）を書いてるんだ．LLMはこれに従って問題を分解してくれる．ファイルサイズを300－400行以下に保つといい感じ．AIはリファクタリングも得意だよ．
1950年代のものが全部また新しいものになってるね：dynamic programming＜br＞https://en.m.wikipedia.org/wiki/Dynamic_programming#Computer…
思考の推論チェーンを分解するのにも強力そうだね。
これが良いのは、重みが静的だから突然気まぐれで使えないアップデートに悩まされなくて済むことだね。
あるいは、Claudeみたいに、北米のビジネス時間中は実質的に能力が落ちるのがね。太平洋標準時午前3時？絶好調。午前8時？…頭がちょっと…。
親コメントはたぶん容量制限のこと言ってるんだと思うよ。朝アメリカ人がオンラインになると、Claudeは需要に追いつけなくて、システムが容量いっぱいってエラーメッセージがよく出るんだ。
ClaudeとDeepseekにはOpenrouterを使ったよ。これはモデルごとに代替ホストを選んでくれるんだ。Deepseekプロバイダは性能がいまいちだから除外したけど。リンクはこれね。https://openrouter.ai/deepseek/deepseek-chat-v3-0324
私もそれに気づいたよ。それが始まってから容量オーバーのメッセージが出なくなったんだ。混雑時間帯はパラメータが少ないモデルに切り替えてるんだと思う。
著者はLeanからのエラーフィードバックをモデルに取り入れようとしたかな？2023年の研究［1］では、エラーフィードバックを取り入れた汎用モデルの方が性能が良いって出てたけど、minif2fのSOTAモデルにはそれが見られないんだよね。［1］へのリンク。https://arxiv.org/abs/2310.04353
DeepSeek Proverのサブゴール分解はエラーフィードバックへの一歩だよ。（証明をサブゴールに分解して個別に攻める。）前のSOTAモデルKiminaとは違うアプローチだね。Kiminaはフィードバックなしでも中程度の証明はできたけど、長い証明にはサブゴール分解が必要だろう。エラーフィードバックの組み込み方は興味深い研究分野だよ。（GDMのAlphaProofは既に使ってる噂も。）
それは知らなかったな、驚きだね。生の型理論じゃなくて実際のLeanコードを使うことにびっくりだよ。
openrouter.aiで無料でモデル試せるよ。leanで”mathematics in lean”勉強しててさ、”convergesTo_unique”って定理で詰まってたんだ。面白そうだからopenrouter.aiの無料モデルで試したら、一発で答え出たよ！
答えのコードも雰囲気わかるように載せとくね。（コード本体は文字数・記号の関係で省略）
関連してさ、将来は”専門家”みたいなLLMがいくつか出てきて、ラッパーが”ツール”みたいに必要に応じてタスクを振るようになると思うんだ。そうすれば専門分野を分けられるじゃん？ 個々のモデルが一つのことだけ得意になる感じ。
今回のプロバーみたいなモデルは、近い将来そういうツールとして使われるかもね。
今日の具体的な例は、ここ見てみてよ。 https://openrouter.ai/openrouter/auto
もっとコメントを表示（1）
それはいいけど、まず特定の専門分野に特化したモデルがいる状況を想像してみてよ。ルーティングは簡単な部分みたいだよ（ただ利用可能なモデルを自分のラッパーLLMへのツールとして渡すだけだし）。
それってMoEモデルが既にやってることじゃないの？
MoEモデルは、各transformer層で、各トークンを現在の表現から計算したスコアで、特化したfeed-forward networks（簡単に言うとfully-connected perceptrons）のセットに振り分けてるんだよ。
ここに分かりやすい図解解説があるよ。 https://deepgram.com/learn/mixture-of-experts-ml-model-guide
違うよ。MoEのエキスパートはそれぞれ別に学習されてないし、違う概念を保持してるかもだけど、特定の分野のエキスパートってわけじゃないんだ。
でも、違う専門分野のエキスパートLLMとか、fine-tuningアダプターにリクエストを振り分ける技術はあるよ。RouteLLMみたいにね。
手作業で設定する”異なる専門分野”の振り分けが、MoEの学習ベースのアプローチより優れてるって、なんでそう思うの？
まず、これらは全く違う技術だから単純比較は難しいよ。でも一つの見方として、外部ルーティングだと複数のデカいモデル（例えばDeepseek R1とかQwenとかLLaMAとか）を組み合わせるから、合計で扱うパラメータ数がすごく多くなるんだ（兆単位とか）。一方、MoEのエキスパートだけを使う場合は、合計パラメータ量はそれより少ないんだ（数千億単位）。
テストタイム計算って呼んでるやつの中で，すでにそれが起こってるかもね．
テストタイム計算を使うモデルの多くはMoEsだけど，test-time computeって普通はモデルに与えられたプロンプトとか問題について推論することを指すんだよね．どのモデルを選ぶかについての推論じゃないし，その名前でLLMルーターを公開した人，いないと思うな．
OAIが推論するときにどうやってベストな答えを見つけてるかは分からないけど，同じモデルのバリエーションをいくつか持ってるのはその一環だとかなり確信してるよ．
No Free Lunch Theoremによると，こういうのは避けられない運命らしいよ．リンクはこれね．https://en.wikipedia.org/wiki/No_free_lunch_in_search_and_op…
NFLTに関しては，n個の専門家システムは単一の専門家と変わりないよ．その定理はこの考え方には完全に無関心なんだ（つまり“同じくらい懐疑的”）．
関連して：将来はいくつかの“専門家”LLM’sがいて，ラッパーが必要に応じて“ツール”みたいにタスクを割り当てるようになるんじゃないかって想像するんだ．そうすれば専門知識を分離できて，個々のモデルは一つのことに特化できるよね．将来だって？僕，すでにみんなやってるってかなり確信してるけど．
いや，僕は違う意見．ChatGPTに専門家モデル（生化学，コーディング，物理とか）をツールとして使ってほしいんだ．特定の分野の専門家モデルは，なんでもできるモデルよりその分野では優れてるはず．でも，ドメインデータでファインチューニングすると他のトピックで一貫性がなくなる話も聞くけどね．
＞ have seen anecdotes where finetuning a small model on domain data makes the model lose coherence on other topics
これは想定内の挙動だよ．
知ってるよ．だから，なんで消費者向けLLM製品でドメイン特化モデルをツールとして使わないんだろうね？
でも，雑にやられてるんだよね．
MistralのモデルってMixture-of-Expertsモデルらしいよ。
オレが考える「知性」は、正しい仮説立て、文脈記憶の利用、そして常識外れの思考って要素が重要だと思うんだ。今のLLMは特に仮説立てが下手だし、自分で文脈覚えて推論するのも苦手。既存の枠にとらわれず、新しい問題を解くための独自の方法を生み出すのが最終段階だけど、今のボットにはまだまだだな。
人間とAIのやり取りデータ、これ公開すべきだよ。これこそがAI時代の集合知、Wikipediaみたいなもんだからさ。そうしないと、2022年以降の進歩は空欄になっちゃうよ。昔の人が巨岩をどうやって動かしたか記録しなかったみたいに、やり方が分からなくなるかも。
671Bと7Bを選んだのが超面白いね。32Bみたいな「スイートスポット”」って感じのサイズじゃないんだ。
彼らが他に適切なSoTAベースモデルを持ってなかったから、既存のDeepSeek V3（671B）やDeepSeek-Prover-v1.5（7B）をベースにしたんじゃないかな。DeepSeek-Coder-V2（16B, 236B）もあったけど、V2.5に統合されててV3より性能が低いんだ。あるいはQwenのモデルを使った可能性もあるね。
あと注目すべきは、新しいモデルを好意的に迎えられるようなリリースの初期計画では、パラメータサイズとスキルタイプ両方に基づいた市場セグメンテーションが含まれるかもってことだね。
→「どんどん混み合ってるLLM分野で、ウチの（作るのが高い）モデルはどうやって目立つの？」ってこと。
こういうやり方ってすごく論理的だなって思うんだ。
小さいモデルで仮説をテストして、色々試して、上手くいったらその知見を大きなモデルに応用するっていう。
それか、試したけど「スイートスポット”」じゃなかったのかも？（分からないけど、論文出す前には普通試すと思うけどね）
Putnam benchのグラフ、真ん中のやつ見て。論文によるとDeepSeek-Prover-V2-671BはPutnamBenchの658問中49問を解いたってあるんだけど、これ計算すると7%にしかならないよ。
DeepSeek-Prover-V2ならそんなミス絶対しないだろうね、賭けてもいいわ
これぞ人間の典型的な幻覚（ミス）だね
DeepSeekの学習データにPutnamの解答が含まれてた可能性ってどれくらいあるの？
Putnamの解答は非公開で、自動生成も難しいみたい。開発者が人手でデータを用意した可能性もあるけど、このベンチマークの重要度考えるとコスパ悪くて考えにくいね。以前のSOTAは7bモデルでpass@3200使って10問解けた程度だったよ。
もっとコメントを表示（2）
AoPSにPutnam専門のフォーラム（2024年の分もある）があるみたいだよ。リンクこれね：https://artofproblemsolving.com/community/c3249_putnam
あと、これPutnam 2023の解答PDF：https://kskedlaya.org/putnam-archive/2023s.pdf
これらの解答はまだLeanで形式化する必要があるんだよね。それが問題解くより大変な時もあるんだよな
このモデルってDeepseek chatでも使えるの？昨日見つけられなかったんだよね。良いハードウェア持ってないから自分でホストしたくないんだ
これは君が話しかけるようなもんじゃないよ。概念的にはAlphaProofみたいな感じ。彼らの研究成果の一部（たぶん後で論文とかテクニカルレポートも出るだろうけど）がコミュニティに共有されたものだよ。
人間がこのレベルのベンチマークでやるには、どれくらいの教育が必要なの？
Leanを使ってPutnam competitionの問題を厳密に証明できるようになるには、大学中〜上級レベルの数学とCSの知識が必要だよ。（Leanを使わずにPutnam competitionの一部だけなら、高校レベルの高い数学力と大学初級レベルの数学力があれば十分で、競技向けトレーニングがあるとさらに良い感じ）
ollama経由でインストールできる？ollama run deepseek-ai／DeepSeek-Prover-V2-7Bみたいにさ
コンパイラのバックエンド向けに似たようなアイデアを開発してる人いるの？
＞”an open-source large language model”って書いてるけど、本当にオープンソース？何か変わったの？
みんな”open weight”モデルを”open source”って呼んでるけど，それは間違ってるんだよね．この戦い方は変えなきゃ．多分”open data and pipeline”とかかな．
