個人ブログの著者Aditya Kumar氏は、モデルが書くコードの質を決めるのはモデルの賢さだけではなく、出力を検証する側の厳しさだと論じる。コード生成AIを使う開発者にとっての効き目は具体的だ。検証器が誤りを通さない言語なら、生成→検証→修復のループがそのまま品質保証になり、人が目で確認する負担が減る。検証器が緩い言語では、コンパイルが通っても品質の保証にならない。これは、AIにコードを書かせる際の言語選定が「学習データの多さ」だけでなく「検証コストの低さ」で決まる方向への動きを示す読みだ。ただし本稿の根拠は著者個人の経験則と公開ベンチマーク数値の引用であり、査読や企業発表ではない。

何が起きたか

Kumar氏は2026年9月1日公開のブログ記事で、自身の経験として「返ってくるRustはC++より良く、Leanはそのどちらよりも良い」と述べている。その理由として、型システムやコンパイラを、誤りを握りつぶさず明示的な承認なしには通さない「探索のオラクル」と捉える見方を提示した。

仕組み・詳細

  • 「コンパイルが通る」の意味は言語で違う: C++では、名前の解決やオーバーロードの選択が検査されるだけで、use-after-free、イテレータの無効化、データ競合などは検査されない。コンパイルが通っても、これらの誤りは残りうる。
  • Rustの検査は回避しにくい: 同記事は、検査器を言い負かすことはできず、突破するには unsafe と書く必要があると述べる。unsafe は字面で見え、grepで探せる「承認の明示」になる。
  • Leanは検証コストが低い: 検証が安いため、学習データが少なくても、力任せの探索（brute force）でモデルが高い性能を出せるという主張である。

数字で見る

記事は具体例として、32個の候補証明をサンプリングし、検証を通った1つを採る手順は健全な手法だと述べる。Delta Proverはこの方式で、ファインチューニングなしの汎用モデルを使い、miniF2Fで95.9%に達したと記事は記している（数値は記事中の記載であり、本稿では独立に再検証していない）。

なぜ重要か

本当の問いは、「モデルが書きやすい言語」とは何かだ。人間にとっての書きやすさではなく、誤りを検証器がどれだけ確実に弾くかが、モデルの出力品質を左右するという読みである。検証が安く確実なほど、生成の質に頼らず「たくさん作って通ったものを採る」運用が成り立つ。どの言語がどこまで該当するかの評価や、言語選定への踏み込んだ提言は、本稿では扱わない。