リーンソフトウェアのスケーリング則

コードベースのサイズに応じて、コーディングLLMのパープレキシティ（予測困難性）がどのようにスケールするかを測定するための研究提案です。Leanをテストケースとして、形式言語がより良い予測可能性の指数を持ち、世界中でより安全でセキュアなソフトウェアにつながる可能性があるかを検証します。2025-09-01–2026-06-23 完了 確実性: 可能 重要度: 7 類似参考文献 言語事前分布 スケール 失敗 ボトルネック 予測可能性 プロキシ測定 設計 クロスオーバー 予測 バイアス 制御 コンテキスト 学習 失敗モード 研究アイデア：コードベースのサイズに対するコーディングLLMのパープレキシティのスケーリングを経験的に測定し、「予測可能性」のスケーリング則をプログラミング言語やその他の要因によって推定します。これは、全体的なセキュリティと安全性につながるはずです。現代のLLMで、ゼロから学習させたりファインチューニングしたりすることで高コストでこれを測定することもできますし、ソースコードのコンテキストウィンドウを徐々に拡大してパープレキシティを測定することで安価に測定することもできます。コードベースやプログラミング言語が、そのスケーリング則においてより良い指数を持つ場合、最終的にはLLMが理解し、修正し、書くのが容易になるでしょう。特に、Leanプログラミング言語は、2026年頃のLLMで、既存のコードベースに対するベースライン定数と総損失は悪いかもしれませんが、より良いスケーリング指数を持つ可能性が高いです。これは、Leanでの実装が最終的に勝利し、プログラムの正確性においてグローバル規模で大きな利益をもたらすことを意味します。それゆえ、既存のコードベースをLeanで書き直したり、新しいLeanコードに投資したりすることを正当化するのに役立ち、それによってグローバルなサイバーセキュリティを向上させることができます。 コーディングLLMは現在、将来のほとんどのソフトウェアを生成する軌道に乗っていますが、一般的に品質は平凡か、あるいは完全に安全ではありません（特にvibecodedソフトウェアはひどいです）。将来のコーディングLLMによる書き直しは役立つかもしれませんが、それが起こることや、私たちが広範なサイバーセキュリティLLM攻撃に対して安全であるために必要なほど多くの穴を塞ぐことが保証されているわけではありません。これをどう回避できるでしょうか？LLMは、形式検証可能なシステムのように、証明可能な安全な方法で全てのソフトウェアを書くことができるかもしれませんが、その進歩は遅れています。どれくらい遅れているのでしょうか？ 言語事前分布 ニューラルスケーリング則の方法論は、既存のアプローチを検証し、将来のアプリケーションを予測するために、ディープラーニングにおいて依然として十分に適用されていません。コーディングエージェントはその一例です。LLMは、より多くのデータが利用可能であるため、より一般的な言語でより優れていることが一般的に観察されています。Luoら（2025）は、プログラミングは特にデータ飢餓であり、そのため長期的な「ロックイン」が生じ、HaskellやRust、Leanのようなより良い技術へのアップグレードが不可能になる可能性があると主張しています。しかし、これは必ずしもそうではありません。人気のある言語であり、多くのトレーニングデータがあるということは、LLMがデフォルトでうまく機能することから始まるだけです。（プログラミング言語をエコシステム全体から切り離すのは難しいため、ここでは「言語」と呼びます。）任意のコーパスは「事前分布」と見なすことができ、言語間にはある交換レートが存在し、Pythonのスキルが向上すると、例えばHaskellにも部分的に転移する可能性があります（Yangら、2025を参照）。したがって、「潮が全ての船を持ち上げる」可能性があり、実際、より良いコーディングLLMは、LLMが「十分に良くなる」につれて、プログラマーがすべてを再学習するのに何年も費やす必要がなくなるにつれて、よりマイナーな言語のルネッサンスにつながる可能性があります。 スケール失敗 また、コードベースが拡大するにつれて、それらがパフォーマンスを維持し続けることを意味するわけでもありません。多くのことは小規模ではうまく機能しますが、大規模になるにつれてますます失敗します。Haskellのような言語の「BDSM」規律は、一時的なプログラムを書く場合にはイライラして痛みを伴うかもしれませんが、100万行の複雑なコードを書く場合には不可欠になるかもしれません。したがって、LLMが少しのPythonを書くのは簡単かもしれませんが…大量の場合はどうでしょうか？短いスクリプトは書きやすく、特にLLMが全体をコンテキストウィンドウで見ることができるため、多くの落とし穴がありません。しかし、コードベースが大きくなり、より複雑になり、古くなり、コンテキストウィンドウに収まらなくなるとどうなるでしょうか？動的型付けや例外を正確に把握できるでしょうか？あの暗い隅にあるモンキーパッチングはどうでしょうか？あるいは、アップグレード中に実行時動作が変更された依存関係はどうでしょうか？もしそれができない場合、単一のエラーでさえ致命的になり、人間のプログラマーに数週間かけて微妙なエラーをデバッグさせる可能性があります。 おそらく、実行速度とプログラミング言語のパワーの点で、大規模なソフトウェアプログラムを実装するために最も現実的なプログラミング言語はLeanです。Leanは、定理証明を超えて、実際のプログラムの実装にその使用法が発見されるにつれて、突然の人気を博しています。Leanでのzlibのリライトのようなものさえあります！ Leanボトルネック 私たちは今、Leanでソフトウェアを書き直し、新しいソフトウェアを書き直すことを想像できます。これにより、メモリ安全性、例外、境界外エラーを排除し、ロスレス圧縮のような主要なプロパティの正確性を証明することができます。欠点は…Leanのソースコードがあまり多くないことです。したがって、驚くことではありませんが、LLMはそれほど得意ではありません。まだzlibよりも複雑なI/Oや動作を持つ大規模で複雑なコードベースを自律的に翻訳できるほどではありません。そのため、チキンと卵の問題のようなものがあります。私たちは、学習するための大規模なLeanコードベースを作成するためにLLMを使用し、それによって既存のコードをすべてLeanに置き換えることができます。ただし、そのためには、まず大規模なLeanコードベースがたくさん必要であり、おそらく既存のコードをLeanに置き換えることによってそれらを入手したことになります。そして、Leanがそれほど優れているのか、あるいはLeanコードベースが存在し、LLMがそれらに学習させられたとしても、LLMが効果的に大規模なLeanコードベースを書くことができるのかどうかは不明です。Leanは単に設計が悪いため、どうすればわかるでしょうか？おそらく、実際のLeanコードベースは泥の塊に崩壊したり、多くの場当たり的な特殊ケースの総当たり証明（最終的に「mathslop」と名付けられたもの）を持ったりするかもしれません。 予測可能性プロキシ これをテストする一つの方法は、LLMの視点から、うまく設計された言語がどのように見えるかを尋ねることです。もしそれが場当たり的な設計上の選択、大量の総当たり、バグ、または重複で満たされている場合、LLMの視点からは、それは「読みにくい」コードベースのように見えるはずです。何が起こっているかを理解するために、ますます多くのトークンを読む必要があり、グローバルな状態やオーバーライド、「落とし穴」があるため、非常に予測不可能な動作があるでしょう。単一のファイルを単独で見て何が起こっているかを理解することはできず、他の1ダースのファイルを見て、置換や書き直しを追跡して、通常はXを行うが、ユーザーが設定したこの文書化されていないシェル変数がある場合はYを行う（おそらく）ということを突き止める必要があります。これは、次に何を読むか決して確信できないことを意味します。いつでも、ランダムなものが中断する可能性があり、元のコードが単にバグっているために行を誤って予測する可能性があります…現在のモジュールがうまく書かれており、事実上の「安全なサブセット」のみを使用している場合でも、大規模になると、コードベースは「キュレーターの卵」（良い点と悪い点が混在している状態）になります。プログラマー、時間、複雑さが関わるほど、コードベースは継ぎはぎだらけになります。逆に、強力な型付けメモリ安全言語を備えた、うまく設計されたコードベースは逆であるべきです。エスケープハッチやバックドアがなく、すべてがその通りに見えるため、コードを単独で読むのは簡単です。すべてが文書化されたインターフェースに出入りし、それは、まあ…一言で言えば…予測可能です。しかし、それは単に予測可能であるということではありません。なぜなら、大量のボイラープレート、データ、または冗長なテストケースも予測可能である可能性があるからです。実際、この種のアイデアをテキストやコードに適用しようとするたびに、個々の単語の予測不可能性（パープレキシティ）を見たり、gzipで圧縮されたコードベースのサイズを見たりすると、失敗します。「悪い」単語は問題なく、修正する必要がないか、gzipはJavaScriptを最もよく圧縮するか、あるいは結果はそうでなければ説得力がありません。圧縮を設計プロキシとして使用するという考え方はうまくいかないのでしょうか？おそらく何も問題はなく、単に間違った方法で使用しているだけかもしれません（「創造性」/「新規性」圧縮ベースのメトリクスを参照）。おそらく、それは本質的に圧縮可能なのではなく、セコン