Daily Arxiv

世界中で発行される人工知能関連の論文をまとめるページです。
このページはGoogle Geminiを活用して要約し、非営利で運営しています。
論文の著作権は著者および関連機関にあり、共有する際は出典を明記してください。

Cobblestone: Iterative Automation for Formal Verification

Created by
  • Haebom

作者

Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First

概要

CobblestoneはCoq proof assistantのための新しい証明合成法で、大規模言語モデル（LLM）を活用した分割征服戦略を採用しています。 LLMによって生成された部分的な証明を活用して、問題をより小さなサブ問題に分割し、正常に証明された部分を自動的に識別します。残りの部分に対して繰り返し証明プロセスを実行し、最終的に正確で健全な全体証明を構成します。オープンソースCoqプロジェクトを対象とした実験の結果、従来のLLMベースのツールと非LLMツールを凌駕する性能が見られ、平均$1.25のコストと14.7分の時間がかかりました。ユーザーや他のツールから部分的な証明構造や関連補助整理を入力して活用することもでき、この場合、最大58％の整理を証明できました。

Takeaways、Limitations

•
Takeaways：
◦
LLMの不正確さにもかかわらず、分割征服戦略と部分的な進捗状況を活用することで、効果的にフォーマット検証を自動化できることを示しています。
◦
従来のLLMベースおよび非LLMベースのツールよりも優れたパフォーマンスを達成します。
◦
ユーザー入力や他のツールの出力を活用して、証明プロセスを向上させることができます。
◦
費用対効果が高く、実用的なレベルの時間内に証明を生成します。
•
Limitations：
◦
特定のCoqプロジェクトの評価結果であるため、一般化の可能性に関するさらなる研究が必要です。
◦
すべてのクリーンアップを証明することはできず、証明可能なクリーンアップの割合は依然として制限されています。
◦
LLMの性能に依存しているため、LLMの発展によって性能が変動する可能性があります。
👍
Made with Slashpage