Automated Repair of Declarative Software Specifications in the Era of Large Language Models

要約

宣言型ソフトウェア仕様言語の採用が増えていることと、その固有のデバッグの難しさにより、そのような言語に適用できる効果的で自動化された修復技術の必要性が強調されています。
研究者らは最近、テンプレートベースの修復、フィードバック駆動の反復修復、限定された徹底的なアプローチなど、宣言的なソフトウェア仕様を自動的に修復するさまざまな方法を研究しています。
大規模な言語モデルの最新の開発により、宣言的な仕様を自動的に修復する新たな機会が提供されています。
この研究では、Alloy 宣言言語で書かれたソフトウェア仕様を修復するために OpenAI の ChatGPT を利用する有効性を評価します。
命令型言語とは異なり、Alloy の仕様は実行されません。むしろ論理式に変換され、バックエンド制約ソルバーを使用して評価され、仕様のインスタンスとアサーションの反例が特定されます。
私たちの評価は、自動修復を通じて Alloy 宣言仕様の正確性と完全性を向上させる ChatGPT の機能に焦点を当てています。
ChatGPT によって生成された結果を分析し、主要な自動合金修復方法の結果と比較します。
私たちの研究では、ChatGPT は既存の技術と比較すると不十分ではあるものの、他の技術では対処できなかったバグを正常に修復できることが明らかになりました。
私たちの分析では、不適切な演算子の使用、型エラー、高次ロジックの誤用、関係性の不一致など、ChatGPT によって生成された修復のエラーも特定されました。
さらに、ChatGPT によって生成された修復での幻覚の例とその結果の不一致が観察されました。
私たちの調査は、宣言的仕様の修復に ChatGPT を検討しているソフトウェア実務者、研究者、ツール作成者に貴重な洞察を提供します。

要約(オリジナル)

The growing adoption of declarative software specification languages, coupled with their inherent difficulty in debugging, has underscored the need for effective and automated repair techniques applicable to such languages. Researchers have recently explored various methods to automatically repair declarative software specifications, such as template-based repair, feedback-driven iterative repair, and bounded exhaustive approaches. The latest developments in large language models provide new opportunities for the automatic repair of declarative specifications. In this study, we assess the effectiveness of utilizing OpenAI’s ChatGPT to repair software specifications written in the Alloy declarative language. Unlike imperative languages, specifications in Alloy are not executed but rather translated into logical formulas and evaluated using backend constraint solvers to identify specification instances and counterexamples to assertions. Our evaluation focuses on ChatGPT’s ability to improve the correctness and completeness of Alloy declarative specifications through automatic repairs. We analyze the results produced by ChatGPT and compare them with those of leading automatic Alloy repair methods. Our study revealed that while ChatGPT falls short in comparison to existing techniques, it was able to successfully repair bugs that no other technique could address. Our analysis also identified errors in ChatGPT’s generated repairs, including improper operator usage, type errors, higher-order logic misuse, and relational arity mismatches. Additionally, we observed instances of hallucinations in ChatGPT-generated repairs and inconsistency in its results. Our study provides valuable insights for software practitioners, researchers, and tool builders considering ChatGPT for declarative specification repairs.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google