miniCodeProps: a Minimal Benchmark for Proving Code Properties

要約

AI エージェントは、Lean などの証明アシスタントでの数学定理証明の自動化において、最初の有望性を示しています。
同じ証明アシスタントを使用して、コードと仕様および仕様が保持する証明をペアにすることにより、コードの正しさを検証できます。
コード、仕様、証明の作成を自動化すれば、検証コストを削減でき、あるいは意欲的には、AI エージェントが安全で正しいと証明できるコードを出力できるようになります。
しかし、現在の神経定理証明装置が比較的単純なプログラムであっても自動的に検証できるかどうかは依然として不明である。
提供されたプログラムと仕様の証明を自動的に生成する副問題を目的とした、リーン証明アシスタントの 201 のプログラム仕様のベンチマークである miniCodeProps を紹介します。
miniCodeProps には、さまざまな証明難易度を備えた単純な自己完結型プログラム (リスト、自然数、二分木など) に関する仕様が含まれています。
そのシンプルさにもかかわらず、miniCodeProps は現在の LLM ベースの証明器を打ち破るのに十分です。最先端のメソッドは miniCodeProps の簡単なプロパティについては有望ですが、中程度のプロパティと難しいプロパティのほぼすべてを証明することはできません。
私たちは、正式に検証されたコードのコンテキストで自動化された定理証明を促進するためのベンチマークとして miniCodeProps を一般公開します。

要約(オリジナル)

AI agents have shown initial promise in automating mathematical theorem proving in proof assistants such as Lean. The same proof assistants can be used to verify the correctness of code by pairing code with specifications and proofs that the specifications hold. Automating the writing of code, specifications, and proofs could lower the cost of verification, or, ambitiously, enable an AI agent to output safe, provably correct code. However, it remains unclear whether current neural theorem provers can automatically verify even relatively simple programs. We present miniCodeProps, a benchmark of 201 program specifications in the Lean proof assistant, aimed at the subproblem of automatically generating a proof for a provided program and specification. miniCodeProps contains specifications about simple, self-contained programs (e.g., lists, natural numbers, binary trees) with varied proof difficulty. Despite its simplicity, miniCodeProps is sufficient to break current LLM-based provers, with state-of-the-art methods showing promise on the easy properties in miniCodeProps, yet failing to prove nearly all of the medium and hard properties. We publicly release miniCodeProps as a benchmark for furthering automated theorem proving in the context of formally verified code.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google