QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning

要約

形式検証は、信頼性の高いソフトウェアを作成するための有望な方法ですが、手動で検証証明を作成することの難しさにより、実際の実用性は大幅に制限されます。
最近の方法では、定理証明器を使用して証明空間全体の検索をガイドすることにより、一部の証明合成が自動化されています。
残念ながら、定理証明者は進行状況の最も大まかな推定値しか提供しないため、事実上無向の検索になります。
この問題に対処するために、教師あり学習と強化学習を組み合わせて証明空間をより効果的に探索する自動証明合成ツールである QEDCartographer を作成しました。
QEDCartographer には証明の分岐構造が組み込まれているため、報酬なしの検索が可能になり、形式的検証に固有の報酬が少ないという問題が克服されます。
124 のオープンソース Coq プロジェクトからの 68.5K の定理の CoqGym ベンチマークを使用して QEDCartographer を評価します。
QEDCartographer は、テストセット定理の 21.4% を完全に自動的に証明します。
教師あり学習のみに依存する以前の検索ベースの証明合成ツールである Tok、Tac、ASTactic、Passport、および Proverbot9001 は、それぞれ 9.6%、9.8%、10.9%、12.5%、および 19.8% を証明しました。
62 のツールを組み合わせた Diva は 19.2% であることがわかります。
最も効果的な以前のツールである Proverbot9001 と比較して、QEDCartographer は、両方のツールが証明する定理よりも平均して 34% 短い証明を 29% 速く生成します。
QEDCartographer と非学習ベースの CoqHammer を合わせると、定理の 30.3% が証明されますが、CoqHammer だけでは 26.6% が証明されます。
私たちの研究は、強化学習が証明合成ツールの検索メカニズムを改善するための有益な研究方向であることを示しています。

要約(オリジナル)

Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs’ branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 34% shorter proofs 29% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 30.3% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools’ search mechanisms.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google