WybeCoder: 検証済みの命令型コード生成

arXiv cs.AI / 2026/4/1

💬 オピニオンSignals & Early TrendsIdeas & Deep AnalysisModels & Research

共有:

要点

本論文は、ソフトウェア検証の改善がLLMによるコード生成や定理証明ほど進んでいない点を背景に、コード生成と不変条件・証明を同時に育てる「prove-as-you-generate」型のエージェント的検証フレームワークWybeCoderを提案しています。
WybeCoderは、検証条件生成とSMTソルバに加え、Leanでの対話型証明を組み合わせており、コード・不変条件・証明が相互に更新される“co-evolve（共進化）”を中核に据えています。
検証の体系的評価のため、Leanベースの2つの機能的検証ベンチマーク（VerinaとClever）を、等価な命令型（imperative）コード仕様へ翻訳することで比較可能な実験環境を整えています。
Heapsortのような複雑アルゴリズムで、スケールさせることで有効な不変条件やサブゴールを多数生成し、従来の到達率の停滞（plateau）を超えて、目標タスクの達成率（Verina 74%、Clever 62%）を中程度の計算予算で大幅に向上させたと報告しています。

要旨: 大規模言語モデル（LLM）の最近の進歩により、自動コード生成や形式的定理証明は前進しましたが、ソフトウェア検証は同様の改善を見ていません。このギャップに対処するために、本稿では WybeCoder を提案します。これは、コード、不変条件、証明が共進化する prove-as-you-generate（生成しながら証明）型の開発を可能にする、エージェント的コード検証フレームワークです。これは、Lean における対話的証明と、自動検証条件生成および SMT ソルバを組み合わせる最近のフレームワークに基づいています。体系的な評価を可能にするために、Lean における関数型検証の 2 つのベンチマークである Verina と Clever を、同等の命令型コード仕様へと翻訳します。Heapsort のような複雑なアルゴリズムにおいては、アプローチをスケールさせることで一貫した性能改善が観測されます。具体的には、数十個の妥当な不変条件を合成し、数十個の部分目標をディスパッチして、検証済みコードは数百行に達し、先行研究で報告されていた停滞（プラトー）を乗り越えます。最良のシステムでは、適度な計算予算のもとで Verina の課題の 74% と Clever の課題の 62% を解決し、以前の評価を大きく上回るとともに、検証済みの命令型コードからなる大規模データセットを自動的に構築する道筋を切り開きます。