モデル選びの考察 — 論文 RQ2 ablation を読む
これは hirorogo 個人の読み解きで、Nyx Foundation や論文著者の公式見解ではありません。論文 (arXiv:2604.26495) に掲載されている数値そのものは正確ですが、そこから引き出している考察 (どのモデルがどんな場面で向くか、何が面白いポイントか) は本人の主観です。
「新しいモデルほど良い」というのは直感として正しいことが多いですが、SPECA の論文に掲載されている RQ2 の ablation を読んでいると、それだけでは説明できない数値の動き方があります。ここではその読み解きを書いておきます。
RQ2 ablation の表を眺める
論文の RQ2 は RepoAudit C/C++ ベンチマークを対象にしたモデル別の性能比較です。Phase 4-6 (検証フェーズ) を担当するモデルを入れ替えて精度・コスト・発見数を測定しています。
| モデル | 精度 | F1 | コスト | 新規発見 |
|---|---|---|---|---|
| Claude Sonnet 4.5 (SPECA 推奨) | 88.9% | 0.94 | $81.05 ($1.69/bug) | 12 |
| Claude 3.7 Sonnet | 88.9% | 0.94 | $23.85 | — |
| Claude Sonnet 4 (前世代) | 81.2% | — | $100.68 | 18 |
| Claude 3.5 Sonnet (公開 baseline) | 78.4% | — | $38.10 | — |
| o3-mini | 80.0% | — | $4.50 | — |
| DeepSeek R1 | 72.7% | — | $93.51 | 7 |
| Meta Infer (静的解析) | 77.8% | — | — | — |
| Amazon CodeGuru (静的解析) | 0.0% | — | — | — |
まず目に入るのは精度の範囲です。最高の Sonnet 4.5 / Claude 3.7 Sonnet (88.9%) から DeepSeek R1 (72.7%) まで 16.2pp の差があります。「同じ pipeline に別モデルを差し込んでいるだけ」なのに、この差が出る。
強いモデルほど property scope を守る
ここが面白いと思った部分です。
Sonnet 4.5 は精度 88.9%、新規発見 12 件。Sonnet 4 (前世代) は精度 81.2%、新規発見 18 件。精度が下がると新規発見が増えています。
これは逆説的に見えますが、論文の解釈は明快です。強いモデルは property の scope を忠実に守って推論するため、property が指定した範囲の外にある「隣接領域の本物バグ」を意図的に拾わない。一方で弱いモデルは scope から drift して、property が想定していない周辺コードまで読み込んでしまう。その副作用として、scope 外の本物バグを偶発的に検出することがある。
「弱いモデルが新規発見を稼いだ」という言い方は正確ではなくて、「scope 遵守が甘いために scope 外も走査してしまった」というのが実態です。coverage を意図的に広げたいなら、property 側の scope 定義を広げるほうが再現性があります。
論文はこの状況を次のように表現しています。
"property-generation quality, not model reasoning, as the binding constraint on coverage"
（coverage を縛っているのはモデルの推論能力ではなく、property 生成の質である）
Phase 4-6 のモデルをいくら強くしても、Phase 1-3 で生成された property の範囲を超えて coverage は伸びない、という構造的な限界がここに出ています。
DeepSeek R1 は反事実推論で固めに却下する
DeepSeek R1 の数値は精度 72.7%、新規発見 7 件、コスト $93.51 です。精度は最低水準で、コストは Sonnet 4 ($100.68) に次いで高い。コストパフォーマンスで見ると最も割に合わない結果になっています。
論文でもう一点言及されているのが、争点 bug (RepoAudit が「修正対象」とフラグした境界ケース 5 件) に対する判断の違いです。Sonnet 4.5 は 5 件中 4 件を「悪用経路なし」として却下。Sonnet 4 は 5 件中 4 件を検出。DeepSeek R1 は 5 件全てを却下しました。
同じ pipeline・同じ property を使って、争点 bug への判断がモデルによってここまで分かれる。これは反事実推論 (「この条件が成立しないケースはあるか」という推論) のスタイルにモデル依存の揺らぎがあることを示していると思います。争点が多いコードベースを扱う場合は、この傾向を意識しておく価値があります。
コスト効率の意外な勝者
Claude 3.7 Sonnet は Sonnet 4.5 と同じ精度 88.9%、同じ F1 0.94 を、$23.85 で出しています。Sonnet 4.5 のコスト $81.05 の 1/3 以下です。新規候補の内訳が論文には明示されていませんが、精度・F1 の数値だけを見る限り遜色がありません。
コストを優先してベンチマーク精度を落としたくない場合、Claude 3.7 Sonnet は現実的な選択肢です。
最安は o3-mini の $4.50。精度 80.0% で静的解析ベースラインの Meta Infer (77.8%) を上回っています。スクリーニング用途で大量のリポジトリを流す場合、$4.50 は無視できないコスト差です。
Opus は前段、Sonnet は後段
SPECA の設計では Claude Opus と Claude Sonnet 4.5 が分業しています。Opus は Phase 1-3 の知識構造化を担当します。仕様書を読んで property を抽出する役割です。Sonnet 4.5 は Phase 4-6 の検証を担当します。Opus が作った property を実装コードに当てて proof gap を探す役割です。
同じ Claude ファミリーの中で、仕様理解の精度が求められる前段と、コードへの照合・推論が求められる後段を分けている。この分業は、「coverage を縛るのは property の質」という論文の知見と一致しています。前段のモデルを強くすることで property の範囲と質が上がり、後段のモデルが活用できる検証空間が広がります。
一言で
ablation から実用的に引き出せる指針を整理します。
- 精度重視なら Sonnet 4.5、コスト重視なら Claude 3.7 Sonnet。同じ精度 88.9% で $23.85 vs $81.05 の差があります。
- 新規発見数はモデルの強さより property scope 定義の問題。coverage を広げたいなら後段のモデルを変えるより前段の property 生成を見直す。
- 争点 bug が多いコードベースでは DeepSeek R1 の却下傾向に注意。全却下というパターンは pipeline の問題でなくモデル固有の傾向である可能性があります。
- スクリーニング用途なら o3-mini ($4.50) も選択肢。精度 80.0% は静的解析ベースラインを上回ります。