Open6

LLMを用いた型推論の先行研究調査

黒曜黒曜

RBS GooseはRubyKaigiの一発ネタのつもりで作ったので先行研究をちゃんと調査しなかったけど、思ったより将来性がありそうなのでちゃんと先行研究を調べて参考にしたい。
ので、このスレッドに調べた先行研究をまとめる。

黒曜黒曜

The Emergence of Large Language Models in Static Analysis: A First Look through Micro-Benchmarks [Ashwin Prasad Shivarpatna Venkatesh, 2024]

https://arxiv.org/abs/2402.17679

Claude 3 Opus による要約

この論文は、大規模言語モデル(LLM)のソフトウェア工学、特に静的解析タスクにおける役割を調査したものです。
主な内容は以下の通りです。

  1. Python プログラムのコールグラフ解析と型推論においてLLMの性能を評価するため、PyCG、HeaderGen、TypeEvalPyのマイクロベンチマークを用いて26種類のLLMをテストした。
  2. 型推論ではLLMが従来手法より高い精度を示したが、コールグラフ解析では課題が見られた。これはLLMをタスクに特化して改良する必要性を示唆している。
  3. ファインチューニングしたGPT-3.5-turboは性能が向上し、ファインチューニングの可能性を示した。
  4. 一方でLLMは計算コストが高く、オープンソースモデルの方が実用的である。
  5. 従来の静的解析手法は、精度と速度のバランスが最も良い。ただし型推論のように精度が重要な場合はLLMが有効。
  6. 今後はモデル圧縮などによるLLMの効率化、説明可能性の向上、他の解析タスクへの適用などが研究課題である。

以上のように、LLMの静的解析への応用可能性と課題を複数のベンチマークを用いて多角的に評価した研究といえます。

「型推論ではLLMが従来手法より高い精度を示したが、コールグラフ解析では課題が見られた」とのこと。肌感としても型推論にLLMは有効だと思っていたが、すでにPythonで検証されていた模様。
「従来の静的解析手法は、精度と速度のバランスが最も良い」というあたりも、リアルタイムでのフィードバックよりは既存のコードに一括して型をつける用途(すでに存在するコードにRBSを導入したり、gem_rbs_collectionのようにサードパーティーで型をつけたりするとき)に適していそう、というのも肌感通り。

型推論のベンチマークとしてはTypeEvalPyが用いられている。
これについても評価手法をClaudeにまとめてもらった。

Claude 3 Opus による説明

この論文では、型推論のベンチマークとしてTypeEvalPyを使用しています。TypeEvalPyはPythonの型推論ツールを評価するための汎用フレームワークです。
詳細は以下の通りです。

  1. TypeEvalPyのマイクロベンチマークには154のコードスニペットと845の型アノテーションがあり、これらがground truthとして使われます。
  2. 評価指標としてexact matchesを使用しています。これは推論された型アノテーションのうち、ground truthと完全に一致するものの数を表します。
  3. LLMの型推論性能は、exact matchesの数で比較されます。関数の戻り値の型(FRT)、関数のパラメータの型(FPT)、ローカル変数の型(LVT)の3つのカテゴリに分けて集計もされています。
  4. さらに、各ツールがマイクロベンチマーク全体を解析するのにかかる合計実行時間も測定されています。
  5. LLMの結果は、従来の型推論ツールであるHeaderGenやHiTyperとも比較されています。
  6. 最も性能が高かったのはGPT-4で、845個中775個の型アノテーションを正しく推論しました。ファインチューニングしたGPT-3.5-turboが730個で2番目に高い性能でした。
  7. TinyLlamaのように7B未満のパラメータのモデルは、型推論タスクには不十分であることもわかりました。

以上のように、TypeEvalPyのコードスニペットをLLMに入力し、出力された型アノテーションをground truthと比較するという手法で、LLMの型推論性能を定量的に評価しています。

TypeEvalPy はRBS Goose の現状とやりたいことまとめ - 試したいこと5: RBS品質の評価ツールの作成 で欲しいものという感じがするので、これを真似して TypeEvalRuby を作ると良さそう。
exact matches のみでいいのかなというのは気になるところ(型の親子関係があるものとないものにスコア差はつけない?)

なお、TypeEvalPy で各種LLMの評価に使ったプロンプトは src/target_tools/ollama/src/prompts.py だと思われる。
このプロンプトの構成もRBS Gooseで利用するプロンプトの参考になりそう。
逆に言うと、プロンプトや引き渡す情報ごとでの性能差などはおそらく検証されていない。(マイクロベンチマークなので、そもそも引き渡せる情報がソースコード以外にほぼない、というのはありそう)

TypeEvalPyについてはそれ自体の論文があったので、それについては後述。

黒曜黒曜

TypeT5: Seq2seq Type Inference using Static Analysis [Jiayi Wei, 2023]

https://arxiv.org/abs/2303.09564

Claude 3 Opus による要約

この論文は、PythonやJavaScriptのような型アノテーションのない言語に対して、型推論を行う新しい手法TypeT5を提案しています。主なポイントは以下の通りです。

  1. TypeT5は、事前学習済みの大規模言語モデルCodeT5をベースに、型推論をコード補完タスクとして扱います。これにより、まれな型や複雑な型に対しても高い精度で予測できるようになりました。
  2. 静的解析を用いて、予測対象の要素に関連するコード片を動的にモデルの入力コンテキストに含めることで、ローカルな情報だけでなくグローバルな情報も活用します。
  3. 反復デコーディングスキームを導入し、過去の型予測結果をモデルの入力に含めることで、関連するコード要素間で情報を伝播させ、より一貫性のある予測を可能にしました。
  4. 提案手法をPythonの型アノテーション予測に適用し、先行研究と比較した結果、全体的な精度、特にまれで複雑な型の精度を大幅に改善しました。またタイプエラーも減少し、一貫性の高い予測ができました。
  5. ユーザが予測結果を確認し修正を加えられるインタラクティブなデコーディングの使用例も示され、TypeT5がDeveloper Toolとして有用であることを示唆しています。

全体として、大規模言語モデルと静的解析を組み合わせた画期的なアプローチにより、型推論の新しい可能性を示した論文と言えます。

CodeT5はセールスフォースが2021年に作ったコーディング用のLLMモデル。
あえて今使う必要はなさそうだが、手法については「静的解析で関連するコンテキストを埋める」というのが参考になるかも(今は全コードを埋め込んでいるが、推論対象メソッドの呼び出しコードのみを集めればかなり短いプロンプトで推定できそう)。TypeProfのデータフローグラフが流用できるかも?

生成した型アノテーションの評価はいくつかの手法の組み合わせで、独自評価ツールを書いていそう。

Claude 3 Opus による評価周りの説明

この論文において、生成した結果の評価はどのように行っていますか? 特に型推論の精度を機械的な手法で数値尺度を持って評価しているのか、それとも主観的な質の評価を行っているのかを教えて下さい。

この論文では、生成した型アノテーションの評価を主に以下の2つの方法で行っています。

  1. 精度 (Accuracy) の評価: 論文中で定義されているいくつかの精度指標を用いて、機械的に数値評価を行っています。
    • Full Accuracy: 正規化後の型アノテーションが完全に一致するかどうかを評価。
    • Adjusted Accuracy: None型とAny型を除外し、修飾名を単純名に変換するなどの調整を加えた上での精度。(主要評価指標)
    • Base Accuracy: 最も外側の型のみが一致するかどうかを評価。

これらの指標を用いて、提案手法TypeT5と、3つの最新手法(Typilus, Type4Py, HiTyper)や、CodeT5ベースラインとの比較評価を行っています。

  1. 型エラー数 (Type Error) の評価: モデルが予測した型アノテーションを実際のコードに適用し、型チェッカー(mypy)で検出されるエラー数を報告することで、予測された型の一貫性を評価しています。これは品質の指標の1つと見なせます。

以上より、この論文では主観的な質の評価は行わず、客観的かつ機械的な評価指標を用いて生成結果の評価を行っていると言えます。精度指標による直接的な評価と、型エラー数による間接的な品質評価の両方を行うことで、提案手法の有効性を多角的に示しています。

djusted Accuracy を算出するためのツールが既存で存在するのか、新規に構築したのか、算出を人力で行ったのかはわかりますか?

論文中には、Adjusted Accuracyの計算に用いたツールについての明確な言及はありません。しかし、以下の理由から、著者らが新規にツールを構築したか、既存のツールを拡張して使用したと推測されます。

  1. Adjusted Accuracyは、この論文で新たに定義された評価指標です。具体的には、以下の調整を加えた上で型の一致を評価しています。
    • None型とAny型のアノテーションを除外
    • 完全修飾名を単純名に変換 (例: torch.Tensorをtensorに)
    • 最外部のOptional[T]とFinal[T]をTに書き換え

このように、Adjusted Accuracyは一般的な型の比較とは異なる特殊な処理を含んでいるため、既存のツールをそのまま使用することは難しいと考えられます。

  1. 論文中のA.5節「Type Normalization」で、著者らが型の正規化手順を詳細に説明しています。このことから、彼らが独自の正規化処理を実装したことがわかります。

以上の理由から、著者らが評価指標の計算を完全に手作業で行ったとは考えにくく、少なくとも型の正規化と比較は自動化されていたと推測されます。ただし、これらの処理を完全に新規に実装したのか、既存のツールを拡張して実現したのかまでは、論文からは判断できません。

正規化のあたりは参考になるかもしれないが、TypeEvalPyベースのほうがオープンソースで参考にしやすそう。

黒曜黒曜

TypeEvalPy: A Micro-benchmarking Framework for Python Type Inference Tools [Ashwin Prasad Shivarpatna Venkatesh, 2023]

https://arxiv.org/abs/2312.16882

Claude 3 Opus による要約

この論文は、Pythonの型推論ツールを評価するためのマイクロベンチマーキングフレームワークであるTypeEvalPyを提案しています。主な内容は以下の通りです。

  1. TypeEvalPyは、18のカテゴリーにまたがる154のコードスニペットと845の型アノテーションを含む包括的なマイクロベンチマークを提供します。
  2. TypeEvalPyのフレームワークは、コンテナ化されたツールの実行を管理し、推論された型を標準化された形式に変換し、評価のための有意義な指標を生成する3つの主要モジュールで構成されています。
  3. 6つの最先端の型推論ツールを評価した結果、HeaderGenが最高の性能を示し、続いてJediとPyrightが高い性能を示しました。
  4. 機械学習ベースのアプローチは、純粋な静的解析ベースのアプローチと比較して全体的な性能が低いですが、HiTyper-DLのようなハイブリッドアプローチは有望な結果を示しています。
  5. 型推論ツールの健全性と完全性を向上させるには、まだ課題が残っています。
  6. TypeEvalPyの比較分析により、ツール間の違いが明らかになり、今後の研究と最適化の基盤が提供されます。

全体として、この論文はPythonの型推論ツールを評価するための標準化されたベンチマーキングの重要性を強調し、TypeEvalPyフレームワークを通じて現在のツールの長所と短所を浮き彫りにしています。

前述の "The Emergence of Large Language Models in Static Analysis: A First Look through Micro-Benchmarks" より前の論文なので機械学習ベースのアプローチは全体的な性能が低いとされている。
ツールの全体構成や指標について書かれているので、Rubyに移植する場合に参考になりそう。

黒曜黒曜

Sound, heuristic type annotation inference for Ruby [Milod Kazerounian, 2020]

https://www.semanticscholar.org/paper/Sound%2C-heuristic-type-annotation-inference-for-Ruby-Kazerounian-Ren/add3566e4a8efeeec427cb58553845a0741afc76

Claude 3 Opus による要約

この論文は、Ruby向けの新しい型推論システムInferDLについて述べています。主なポイントは以下の通りです。

  1. InferDLは型エラーを発見するだけでなく、メソッドや変数に対して有用な型アノテーションを生成することを目的としている。
  2. 制約ベースの型推論では一般的すぎる型になりがちなため、InferDLはヒューリスティックを用いて、プログラマが書くような型を推測する。
  3. ヒューリスティックの正当性はInferDLが既存の制約に照らしてチェックするため、型の安全性が保たれる。ヒューリスティックはコードブロックとして提供されるため、高い設定性がある。
  4. InferDLの型と制約の言語、制約解消規則、標準的な型ソリューションの生成法、ヒューリスティックを用いたアノテーション生成法を形式的に定義した。
  5. 既存の型チェッカーRDLの上にInferDLを実装し、制約生成、ヒューリスティック、オーバーロードメソッドのためのchoice型をサポートした。
  6. Railsアプリに適用したところ、ヒューリスティック無しでは58%、ヒューリスティック有りでは80%の型アノテーションを正しく推論できた。他のRubyプログラムにも適用し、6つの未知のバグを発見した。

以上から、InferDLは有用で正しい型アノテーションを生成する効果的な型推論システムであり、将来性のあるアプローチだと考えられる。

アプローチとしてはRBS Gooseとかなり近しそう。RBSとSteepを使う代わりにRDL を使うらしい(そもそもRDLのことを知らなかった)

黒曜黒曜

SimTyper: sound type inference for Ruby using type equality prediction [Milod Kazerounian, J. Foster, 2021]

https://www.semanticscholar.org/paper/SimTyper%3A-sound-type-inference-for-Ruby-using-type-Kazerounian-Foster/f33f857c2223bdabb3821c65682299706f3ae21d

Claude 3 Opus による要約

この論文は、Ruby向けの型推論システムSimTyperについて述べています。主なポイントは以下の通りです。

  1. SimTyperは、標準的な制約ベースの型推論に加えて、手動で書かれたヒューリスティックと、機械学習ベースの型の等価性予測を組み合わせることで、より実用的な型を推論することを目指している。
  2. 型の等価性予測には、深層学習を用いたDeepSimネットワークを使用している。DeepSimは、2つの引数や返り値が同じ型を持つ可能性を予測する。
  3. DeepSimは、CodeBERTを使用してソーストークンをベクトル化し、同じ引数や返り値のベクトルをプーリングして、それらのペアの類似度を予測する。
  4. SimTyperは、制約ベースの型推論の後、各型変数についてDeepSimを使って最も似ている実用的な型を予測し、その予測が制約と矛盾しなければ採用する。
  5. 8つのRubyプログラムでの評価により、SimTyperは制約ソルバーのみの場合と比べて69%多くの型アノテーションを正しく推論できることが示された。また、DeepSimはヒューリスティックよりも多くの型を推論できた。
  6. DeepSimは、訓練データに現れない型も推論することができた。

以上のように、SimTyperは機械学習を型推論に統合することで、Rubyプログラムに対してより実用的な型推論を実現している。

制約ベースの型推論に機械学習ベースの手法を部分的に組み合わせるアプローチ。

性能評価に関しては以下の通り。

Claude 3 Opus による性能評価の解説

性能評価にはどのような手法を使っていますか?

性能評価には主に以下のような手法が使われています。

  1. 推論された型が人手で書かれた型アノテーションと一致するかどうかを評価。一致する型の数を、制約ソルバーのみ、制約ソルバー+ヒューリスティック、制約ソルバー+DeepSim、制約ソルバー+ヒューリスティック+DeepSimの4つの設定で比較している。
  2. 一致の判定は完全一致(Match)とパラメータを除いた一致(Match up to Parameter)の2種類で行っている。
  3. Precision(適合率)とRecall(再現率)も測定している。Precisionは推論された型のうち正解と一致した割合、Recallは正解の型のうち推論できた割合として計算されている。
    引数、返り値、インスタンス変数、クラス変数、グローバル変数など、推論対象の種類ごとの性能も評価している。
  4. 標準ライブラリにある型、学習データにはあるが標準ライブラリにはない型、学習データにもベンチマークにも出現しない型、という珍しさの度合いを3段階に分けて、珍しい型の推論性能も評価している。
  5. DeepSimネットワークの設計選択(上位いくつの予測を使うか、引数の埋め込みに何を使うかなど)が性能に与える影響も評価している。

これらの手法により、SimTyperの型推論性能を定量的に多角的に評価し、提案手法の有効性を示しています。

評価対象のコードや、評価に利用したツールについての詳細はわかりますか?

評価対象のコードについては以下のような詳細が述べられています。
評価には2種類のベンチマークが使用されました。

  1. InferDLベンチマーク: InferDLの評価に使われた4つのRailsウェブアプリ
    • code.org: code.orgのウェブサイトアプリ
    • Discourse: オンラインディスカッションプラットフォーム
    • Journey: 調査の作成と回答の収集を行うサイト
    • Talks: トークの告知を共有するサイト
  2. YARDベンチマーク: YARDドキュメントが豊富な4つの有名なライブラリ
    • TZInfo: タイムゾーンデータを扱うライブラリ
    • MiniMagick: ImageMagickラッパー
    • Ronin: 脆弱性研究や悪用開発のためのプラットフォーム
    • Money: 通貨計算と変換のためのライブラリ

これらのベンチマークには合計で844のメソッド(5,853行)が含まれており、84の非ローカル変数の型が推論されました。
評価ツールについては、SimTyperはInferDLをベースに構築されており、InferDLはRubyの型チェッカーRDL上に構築されています。DeepSimネットワークはPythonのTensorFlowライブラリを使って実装・学習・実行されており、RubyインタプリタとPythonの間のインタフェースにはローカルWebサーバーが使われています。

評価対象にしているアプリは参考になりそう。
一方で評価ツールはコードが見つからず、そもそもRDLベースなのでRBSベースのツールでは適用できなさそう。