핵심 개념
大規模言語モデル(LLM)を用いて、与えられた仕様を満たすCプログラムを自動生成し検証するフレームワーク「SynVer」を提案する。
초록
LLM生成Cプログラムの自動検証に向けて
本稿では、大規模言語モデル(LLM)を用いて、与えられた仕様を満たすCプログラムを自動生成し検証する新しいフレームワーク「SynVer」を提案する。
SynVerは、LLMが生成したプログラム候補を自動検証ツールを用いて検証する。
検証プロセスを効率化するために、LLMが生成するプログラムに対して、構文的および意味的なバイアスをかける。
これにより、自動推論に適したプログラムが生成される。
構文的なバイアス
新しいヘルパー関数の使用を禁止する。
ループの代わりに再帰の使用を要求する。
意味的なバイアス
VSTなどの検証ツールで自動推論がしやすい述語を用いて仕様を記述する。
SynVerは、以下の3つの主要な構成要素から成る。
LLM:プログラム候補を生成する。
構文・意味解析器:生成されたプログラムが構文的および意味的なバイアスに準拠しているか検証する。
SepAuto:VSTをベースとした検証ツールであり、プログラムが仕様を満たすか検証する。