PyVeritas: Pythonの検証におけるLLMベースのトランスパイルとC言語向けのバウンデッドモデルチェック

Pythonは汎用プログラミングの主流言語となった一方で、形式的検証を支える堅牢なツールを欠いている。これに対し、C言語などの環境では、CBMCをはじめとする成熟したモデル検査ツールが利用可能であり、これらは包括的な記号的推論とバグの局所化を可能にしている。一方で、Pythonの本質的な複雑性に加え、既存のトランスパイラ（例：Cython）の冗長さや低レベル性が、形式的検証をPythonプログラムに適用する上での大きな制約となってきた。本論文では、大規模言語モデル（LLM）を活用してPythonを高レベルにC言語にトランスパイルする新規フレームワーク「PyVeritas」を提案する。その後、生成されたCコードに対して境界付きモデル検査（bounded model checking）およびMaxSATに基づくバグ局所化を実施する。PyVeritasにより、既存のC言語向けモデル検査ツールを活用してPythonコードの検証とバグ局所化が可能となる。2つのPythonベンチマークを対象とした実証評価の結果、LLMを用いたトランスパイルは高い精度を達成でき、一部のLLMでは80～90％に達するものもあった。これにより、小さなながらも非自明なPythonプログラムに対して、アサーションベースの検証と解釈可能なバグ診断を支援する有効な開発環境の構築が可能となった。