本論文では、Why3向けの段階的なLLMベースのパイプラインであるDiversify2Verifyを紹介しています。これは、再帰的および命令型の配列/リストの実装を多様に生成し、自動検証性を高めるものです。この手法は表現固有の契約を推論し、検証失敗に対処するために有界な検証者支援注釈修復を採用しています。

  • 著者らは整数、配列、リストに関する73タスクのベンチマークを構築し、292種類の実装バリエーションを生み出しました。
  • Diversify2Verifyは初期に96個のアーティファクトを検証し、2回の修復パス後に154個に増加しました。
  • アーティファクトレベルでの検証率は32.9%から52.7%に改善しました。
  • タスクレベルでは、73タスク中49タスクで少なくとも1つのバリエーションが検証され、67.1%の成功率を達成しました。

これらの結果は、実装の多様性がタスク同等プログラムの中から検証に適したアーティファクトを見つけるのに役立つことを示しています。