アブストラクト: 検証アーティファクトを再利用するには、プログラムとそれらの仕様書の間における構造的および意味論的な類似性を特定する必要がある。本論文では、この目標に向けた基礎的なステップとしてグラフ構築に焦点を当てる。我々は、命令型プログラムとその注釈を、型付き・属性付きグラフへ変換するパイプラインを提示する。我々の実験では、ACSL を用いた C、JML を用いた Java、そして C y についての Dafny（C y 用）を含むデータセットを扱う。パイプラインは、抽象構文木のパースと、SentenceTransformer や CodeBERT のようなモデルから得られる意味論的埋め込みを統合する。これにより、構造的関係と意味的文脈の両方を捉えるグラフ表現の生成が可能になる。我々の結果は、異なる言語や注釈スタイルにまたがって一貫したグラフ表現を構築できることを示している。本研究は、今後の意味的な強化や、スケーラブルな検証アーティファクト再利用のための近似的なグラフマッチングに向けた実践的な基盤を提供する。
ニューラルおよび構造的手法による命令型プログラムのグラフ構築とマッチング
arXiv cs.AI / 2026/4/30
💬 オピニオンDeveloper Stack & InfrastructureIdeas & Deep AnalysisModels & Research
要点
- 本論文は、検証アーティファクトの再利用を支えるために、命令型プログラムとその形式アノテーションを「型付きの属性付きグラフ」に変換するパイプラインを提案している。
- AST（抽象構文木）解析と、SentenceTransformerやCodeBERTといったモデルから得たセマンティック埋め込みを組み合わせることで、構造関係と意味的文脈の両方を捉えるグラフ表現を作る。
- C（ACSL）、Java（JML）、Dafny（C#）を含む実験により、言語やアノテーションのスタイルが異なっても一貫したグラフ表現を構築できることを示している。
- 本手法は、今後のセマンティック拡充や近似グラフマッチングへつなげ、検証アーティファクトをスケールして再利用するための実践的基盤になるとしている。
