ニューラルネットワークのメモリ安全性を確保する

新しい世代のAIシステムは安全である必要がある。このレポートでは、ニューラルネットワークがどのように構築されているかを見て、NULLポインターエラー、範囲外アクセス、ダブルフリーエラー、メモリリークといったメモリ安全性の問題を調べる。目的は、これらの問題を見つけて自動的に修正すること。最初にNeuroCodeBenchというニューラルネットワークコードのデータセットのサイズをkプログラムまで自動コード変更を通じて増やす。その後、ESBMCという最新のソフトウェア検証器を使って、これらの変更されたニューラルネットワークコードのメモリ安全性をチェックする。ESBMCが問題を検出したら、大規模言語モデルを使ってコードを修正する。モデルのパフォーマンスを向上させるためのさまざまな方法も比較するよ。

従来のソフトウェア開発とは異なり、ニューラルネットワークの作成にはモデルがうまく動作するまでの多くの試行錯誤が必要。だから、ニューラルネットワークは不明なデータでのパフォーマンスが悪かったり、モデル設計が間違っていたり、壊れたライブラリを使ったり、コードにバグがあったりと、いろんな弱点にかかりやすい。残念ながら、これらの弱点の多くはシステムが使われるまで特定するのは簡単じゃない。

ニューラルネットワークをデバッグする方法はいくつかあるけど、大体は自動テストに依存していて、すべての入力に対してコードが動作することを証明することはできない。この証明の欠如は、算術エラーや無効なメモリアクセスなどの一般的な問題が間違った結果を引き起こしたり、敏感なデータを漏らしたり、システム自体に害を与える可能性があるため、クリティカルなシステムでは心配。

私たちは、エラーのないニューラルネットワークの実装を作成するという課題にいくつかの方法で取り組む。まず、すべての可能なケースをカバーするためにソフトウェア検証器を使う。以前にも言われているように、ニューラルネットワークコードはそのサイズと複雑さ、数学ライブラリへの多くの呼び出しのため、検証器が苦労する。果たしてそれが真実か確かめるために、メモリ問題を抱えたニューラルネットワークコードの大規模データセットを作成した。私たちの調査結果は、検証器がニューラルネットワークコードのメモリ安全性の問題をかなり簡単に見つけられることを示唆しており、それによってニューラルネットワークの実装の正しさをチェックするのに利用できる。

次に、大規模言語モデルをコード修正のための効果的なツールとして使用する。近年、これらのモデルはいろいろなコードタスクで promise を示していて、コードの翻訳、補完、自動修正が含まれる。しかし、以前の研究では、モデルはトレーニングされたデータとは異なるデータに対してパフォーマンスが悪化することが示された。私たちの調査結果は、ニューラルネットワークに使われるコードがこのカテゴリーに入っていて、性能低下の優れたテストケースであることを示している。私たちの結果は、標準的な大規模言語モデルがAIコードを修正できるが、効果的に行うためには特定のプロンプティング技術が必要であることを示している。

具体的には、このレポートでは以下のトピックを扱う：

• 自動的にNeuroCodeBenchデータセットを増やすためのコード特有のデータ技術を用いたAIコード例の大規模データセット生成の方法。
• 拡張されたデータセットに対してESBMCソフトウェア検証器を実行した結果、メモリ安全性の問題を特定したベンチマーク。
• 大規模言語モデルの修正パフォーマンスを向上させるためのさまざまな手法の比較。また、限られた入力空間、コードの正しいフォーマット化、コンパイラやソフトウェア検証器からのフィードバックの統合などの課題への解決策も提案する。
• 大規模言語モデルがAIコードの修正にどれほどうまく機能するかについての初期結果。構文の正確さ、タスクへの関連性、コードがコンパイルされるか、成功した修正の4つの観点から出力を調べる。
• 入力履歴が反復コード修正プロセスに与える影響。

このレポートの構造は次のとおり：セクション1では、NeuroCodeBench、ニューラルネットワークにおける一般的なメモリ問題、プログラムを変更するための技術を紹介。セクション2では、AIコードデータセットを作成するアプローチを説明し、ESBMCを使ったラベル付けの結果を共有。セクション3では、さまざまな先進的なプロンプティング技術を紹介し、それをコード修正にどう使うか説明し、ChatGPTとの効果を比較する。

この文書は、公式のソフトウェアリポジトリの公式記録として機能する。https://github.com/emanino/plain_c_nn_benchmark、そしてステージングリポジトリはhttps://github.com/Yiannis128/plain_c_nn_benchmarkで利用可能。

#Neural Networks in NeuroCodeBench

NeuroCodeBenchは、ソフトウェア検証用に設計されたニューラルネットワーク実装をテストするためのプレーンCベンチマーク。複雑な構造を持ち、自動的にテストできるけど検証が難しい主流の機械学習ライブラリ（PyTorchやTensorFlowなど）と比較して、NeuroCodeBenchはマイクロコントローラフレームワークを使用。ここでは、ネットワークのソースコードが完全に利用可能。高レベルのニューラルネットワーク仕様をスタンドアロンCコードに変換する2つの既存ツール（onnx2cとkeras2c）を利用する。2023年11月から、NeuroCodeBenchは国際ソフトウェア検証コンペティション（SV-COMP）の公式ベンチマークの一部となった。

#Overview of Neural Architectures in NeuroCodeBench

これらのアーキテクチャは、さまざまな機械学習とエンジニアリングのタスクに取り組む。詳細は以下：

• Hopfield Networks：再帰的ニューラルネットワークは、エラー修正デコーダとして機能できる。主なアイデアは、ビットシーケンスをベクトルにエンコードして、ネットワークがエラーを修正すること。特にHebbian重みを持つHopfieldネットワークを使用。
• Polynomial Approximation Networks：ニューラルネットワークは電気部品の転送関数をモデル化できる。このプロセスを振動する挙動を持つ仮想多項式部品を使ってシミュレーションする。
• VNN-COMP Networks：国際ニューラルネットワーク検証コンペティション（VNN-COMP）は、実装の詳細を含まないベンチマークを公開し、より高い抽象度に焦点を当てている。ONNX形式からCにネットワークを翻訳してリファレンス実装を提供する。

#Safety Properties

最初は、NeuroCodeBenchは到達可能性の特性に関連する難しい検証問題でソフトウェア検証器をテストすることを目指していた。それに対して、私たちのAIコードデータセットは大規模言語モデルがコードを修正できるかどうかをテストする。実世界のバグのほとんどはプログラミングミスから生じるため、メモリ安全性の問題に焦点を当て、ソフトウェアの脆弱性の主な原因を考える。ここでは、さまざまな安全性の特性を簡単に説明する：

• Reachability：ニューラルネットワークにとって、これらの特性は入力と出力のセットに対する必要な条件を定義する。例えば、特定の条件が満たされると、Hopfieldネットワークはノイズの中でコードを再構築できるかもしれない。
• Memory Safety：これは、NULLポインタの逆参照、範囲外アクセス、ダブルフリーエラー、メモリリークのような脆弱性をチェックすることを含む。全てのメモリ操作が有効で正確に追跡されていることをESBMCに指示する。

#Generative Language Models

AIはコードを自動的に修正するために利用されてきた。最近では、大規模な言語モデルが注目されている。しかし、彼らが生成するコードにはまだ弱点が含まれることがある。LLMは、エンコーダ/デコーダ構造を持つ再帰的ニューラルネットワークの一種で、しばしばアテンションメカニズムを使用する。隠れ状態のシーケンスで動作する従来の方法とは異なり、LLMは高度に並列化でき、トレーニングを加速する。重要な進展はOpenAIのGPT-3.5-Turboで、1750億パラメータを持つクローズドソースモデルで、私たちは実験にこれを使用する。

#Software Verification

ソフトウェアを検証する方法はいくつかあるが、このレポートではBounded Model Checking（BMC）を使用してメモリ脆弱性を見つける。BMCは、特定の深さで与えられた特性が成り立つかどうかをチェックする。システムを展開し、それを検証条件に翻訳して真実性を評価する。ESBMCはBMCを使用してAI Cコードのサンプルに対して脆弱性をテストする。

#Creating an AI Code Dataset

大規模な言語モデルがAIコードを修正する能力を訓練し評価するために、ニューラルネットワーク実装のデータセットが必要。既存のデータセットは小さく、ほんの数百サンプルしか含まれていない。だから、データ拡張技術を使ってデータセットを大幅に拡大し、重要な評価指標を狙う。

#Program Mutation

この作業には、CおよびC++のためのミューテーションテストツールであるMullを使用する。Mullには、コンパイラプラグインとMull Runnerの2つの主要なコンポーネントがある。プラグインは、コンパイル中にコードの変異を生成し、それをLLVMビットコードに挿入する。各変異はプログラムの動作を変更するが、ランタイムで有効化できる条件付きフラグの背後に隠れている。

Mull Runnerは、異なる変異を有効にした状態でプログラムを何度も実行して、これらの変更が実行にどう影響するかを見ている。各変異はパッチファイルに保存できる。

#Data Augmentation

NeuroCodeBenchデータセットを増やすために、できるだけ自動生成する。必要なサイズが大きいため、kサンプルを手動で作成するのは現実的ではない。パイプラインは3つのステージから構成される：

1. 基本サンプルの構築：NeuroCodeBenchの指示に従って、さまざまな種類のネットワークを含む初期データセットを作成する。
2. 変異パッチの生成：変異テストスイートを使用して基本データセットを変更してコードのバリエーションを作成する。
3. 新しいデータセットの分類：データセットが拡張された後、ESBMCを使って各サンプルの安全性を確認する。

#Empirical Results

このセクションでは、ESBMCを使用して拡張されたNeuroCodeBenchデータセットを処理した結果と実験設定について議論する。

#Classification Results

ESBMCの結果に基づく各サンプルの分類を提示する。異なるカテゴリは、安全なケースと危険なケースの数にばらつきがある。Hopfieldネットワークは複雑な構造のせいで安全なケースが少ない傾向がある。一方、多項式近似と強化学習ネットワークは、安全なインスタンスと危険なインスタンスの割合が高い。

#Verification Time

安全および危険なプログラムのサブセットに対する検証時間を分析する。私たちの結果は、Hopfieldネットワークと多項式近似ネットワークが一般的に他のものよりも早く検証されることを示している。しかし、明確な結論を出すにはもっとデータが必要。ESBMCが一部のサンプルを分類できなかったが、多くのサンプルが数分のうちに処理された。

#Lessons Learned

全体的に見て、ESBMCはニューラルネットワークコードのメモリ安全性の脆弱性をかなり効果的に検証している。これは、ニューラルネットワークコードに対する検証が難しいという以前の主張に挑戦する。一方で、多くの不確定な判決と長い検証時間が目立つため、改善の余地がある。今後の戦略は、偽造ツールと検証ツールを組み合わせることかもしれない。

#Repairing AI Code with Large Language Models

先ほど作成したAIコードデータセットは、不明なデータの代表的な例。オリジナルのNeuroCodeBenchは最近リリースされたため、ほとんどの先進的な大規模言語モデルのトレーニングセットには含まれていなかったと思われる。また、私たちの自動変異方法により、この新しいデータセットは既存のモデルがトレーニングされた典型的なソフトウェアとは異なる。

このコンテキストを考慮して、大規模言語モデルが導入されたメモリの脆弱性を特定し、コードを修正できるかどうかを探る。

#Prompt Templates

自然言語処理コミュニティでは、大規模言語モデルのパフォーマンスはプロンプトの与え方に大きく依存していることが理解されている。これにより、プロンプトエンジニアリング技術に焦点が当たっており、時には微調整が不要になることもある。コード生成に関連するいくつかの効果的なプロンプト戦略を挙げる。私たちの目標は、実際のパフォーマンスを比較すること。

#Previous Experience with ESBMC-AI

以前の研究では、大規模言語モデルに脆弱なコードを修正するように促すことで良好な結果が得られた。それを評価の基準として含めるため、彼らのプロンプトテンプレートの簡略版を以下に示す：

あなたは安全なコード生成器で、脆弱なソースコードとプログラムESBMCの出力を解析する。ESBMCの結果を使って問題を特定し、ソースコードを修正すべき。ここからは修正されたコードのみを返答して。

#Simple Prompts

前の長いプロンプトテンプレートは、提供される情報に特定の順序を課す。比較のために、コードとエラーメッセージの順序を変えた短いプロンプトも考慮する。情報の異なる組み合わせを持ついくつかのプロンプトのペアを含める。

#Persona Prompts

最近の研究によると、大規模言語モデルは特定の役割を与えるとパフォーマンスが向上することがわかっている。この手法はペルソナプロンプティングとして知られており、結果を最適化できる。割り当てられた役割がパフォーマンスに影響を与えるかどうかを尋ね、比較のためにいくつかの役割を提供する。

あなたは役割です。Cコードが示されます。それを修正してコードを見せて。コードはソースです。

#Source Code Limitations

大規模言語モデルは限られた入力長しか処理できない。たとえば、ChatGPTは最大Kトークンを扱うことができるため、大きなコードの塊を与えるのはしばしば不可能。これらの制限に対処するために2つの戦略を使用する。

1. Contextual：多くのソフトウェア検証器は、脆弱性の存在だけでなく、それを引き起こした行も含む。したがって、報告された脆弱性の周辺にあるコードウィンドウを選択して、利用可能なスペースに収める。
2. One Line：特定のメモリ問題については、エラーを引き起こした同じ行のコードを変更するだけでも済むかもしれない。大規模言語モデルが1行だけを見るように複数のテストを実行。

#Verifier Feedback

ほとんどのソフトウェア検証器は、エラー状態の詳細なトレースを含むバグレポートを提供する。この情報が大規模言語モデルに利益をもたらすかどうかを調査する。

#Prompt Combinations

実験中に使用されたプロンプトの組み合わせを要約する。各組み合わせは、メモリ問題を修正するモデルの効果を評価することを目的とする。

#Comparing Templates

検証器のフィードバックに関連する異なるプロンプトテンプレートのパフォーマンスを比較し、有効な修正を生成する可能性を検討する。

#Syntax of the LLM Patches

大規模言語モデルが出力として本物のCコードを生成していることを確認したい。自動コード検出器を使用して出力を評価する。

#Relevance of the LLM Patches

脆弱性は小さなコードの変更であるため、効果的なパッチは修正された行を除いて入力コードに非常に似ていると期待する。入力と出力コードの間の文字の重複を測定する。

#Compiling the Repaired Code

大規模言語モデルに有効なCコードを提供するように頼むが、それが成功する保証はない。したがって、修正されたパッチが正常にコンパイルされるかどうかを確認する。

#Verifying the Repaired Code

最後に、修正されたコードがメモリ安全性のチェックを通過するかどうかをテストする。修正されたコードをESBMCで実行し、いくつのプログラムが成功した検証を受けるかを数える。

#Comparing Individual Prompts

ここまでの実験で実行されたすべてのプロンプトを比較し、コンテキスト特定アプローチと1行アプローチの両方において最も効果的なものを強調する。

#Best Prompt Takeaway

最高の結果は、「自動コード修正ツール」の役割を持つ2番目のプロンプトテンプレートを使用することによって達成される。

#Further Fine-Tuning of the Best Prompts

結果を改善するためにプロンプトを洗練させることができる。最良の2つのプロンプトに焦点を当て、パフォーマンスを向上させるためにフォーマットや説明指示の役割を調べる。

#Lessons Learned from Iterative Automated Program Repair

反復修正戦略により、大規模言語モデルは問題を修正する機会が複数回与えられる。私たちの実験では、非反復修正が18％の成功率を達成したのに対し、反復アプローチはこれを25％に引き上げた。

#Conclusions and Future Work

要するに、私たちはNeuroCodeBenchを拡張して、変異を通じてメモリに脆弱なAI Cコードのより大きなデータセットを作成した。私たちはこれらのサンプルをESBMCを使って分類し、どれがメモリ問題を含んでいるかを検証した。

GPT-3.5-Turboを使用して、変更されたコードを修正するためのさまざまなプロンプト戦略を探った。私たちは、特に「自動コード修正ツール」の役割を持つ長いペルソナプロンプトが最も効果的であることを発見した。また、モデルのコンテキストウィンドウの制限を回避するために、大規模データセットから問題のあるコードを抽出する策略を開発した。さらに、自動プログラム修正の反復プロセスをテストし、成功率が7％改善された。

今後の研究では、異なる大規模言語モデルでさらにテストを行い、私たちの発見がGPT-3.5-Turboを超えて真実であるかどうかを確認する計画を立てている。オープンソースモデルは、プログラム修正タスクにカスタマイズ可能なため、特に私たちの研究を助ける可能性がある。

#Testing Backtick Performance Effectiveness

ソースコードの周りにバックチックを使用することがどれほど効果的であるかを分析するために、再度実験を実施し、バックチックを除外して変更する。これにより、バックチックの存在がコード修正の正確性に影響を与えるかどうかを判断できる。

#C/C++ Detector Results

コード検出器によって付与されたスコアの分布を調べ、バックチックを使用した実験結果とバックチックなしの結果を比較する。

#Relevance Results

次に、モデルが作成したパッチが元のコードにどれだけ似ているかを分析する。

#Compilation Results

モデルが生成したパッチが異なる実験設定でどのくらい成功裏にコンパイルされるかも観察する。

#Verifying the Code Results

最後に、さまざまなプロンプトの検証成功率とバックチックを使用するかスキップするかでどう異なるかを評価する。

#Iterative Repair Experiment Details

さまざまな温度設定でプロンプトの成功した検証率を調査し、温度がパフォーマンスにどのように影響するかを理解する。特に、フォワードヒストリーに焦点を当てる。

#Successful Verifications By Prompt Per Temperature

異なる温度レベルでのプロンプトの効果を分析し、モデルのコード修正能力がどのように変化するかを確認する。

#Successful Verifications By Attempt Per Temperature

最後に、各プロンプトの成功率が温度の変化に伴ってどのように変化するかを要約し、成功修正のための最良の条件についての洞察を提供する。