Daily Arxiv

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

VERINA: Benchmarking Verifiable Code Generation

Created by
  • Haebom

作者

Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song

概要

大規模言語モデル（LLM）はソフトウェア開発に広く使用されていますが、LLMによって生成されたコードの正確さを保証することは依然として困難であり、しばしば高価な手動レビューが必要です。検証可能なコード生成は、コード、仕様、およびコード仕様のソート証明をまとめて生成し、この問題を解決し、コーディングにおけるLLMの利点をさらに活用するための有望な方法を提供します。しかし、現在のベンチマークは、すべてのタスクを包括的に評価するフレームワークを提供するのではなく、個々のコンポーネントにのみ焦点を当てるなど、評価に大きなギャップがあります。この論文では、コード、仕様、および証明の生成とその構成を包括的に評価できる高品質のベンチマークであるVerina（Verifiable Code Generation Arena）を紹介します。 VerinaはLeanで189の手動でキュレーションされたコーディングタスクで構成されています。最先端のLLMの広範な評価は、検証可能なコード生成、特に証明生成において深刻な課題を明らかにし、検証ドメインでLLMベースのクリーンアップ証明書を改善する必要性を強調しています。最も優れたモデルであるOpenAI o4-miniは、61.4％のコード精度、51.0％の仕様の健全性と完全性、および3.6％の証明の成功率を達成します（作業ごとに1回の試行基準）。 Verinaは厳格で包括的なベンチマークを提供することで、検証可能なコード生成の進歩を促進すると期待しています。データセットはhttps://huggingface.co/datasets/sunblaze-ucb/verina에서 、評価コードはhttps://github.com/sunblaze-ucb/verina에서公開します。

Takeaways、Limitations

•
Takeaways：
◦
Verinaベンチマークは、コード、仕様、証明の生成、およびその構成を包括的に評価するための新しいツールを提供します。
◦
ＬＬＭベースの検証可能なコード生成の問題を明らかにし、特に証明生成分野の改善の必要性を強調する。
◦
研究コミュニティがその分野の発展を加速するための厳密で包括的なベンチマークを提供します。
◦
オープンソースのデータセットと評価コードを提供し、研究の再現性と拡張をサポートします。
•
Limitations：
◦
最も優れたモデル（OpenAI o4-mini）の証明成功率は非常に低く、証明生成技術の発展が緊急であることを示しています。
◦
評価結果は特定のモデルと設定によって異なり、一般化には限界があります。
◦
ベンチマークの作業はLean言語に制限されており、他のプログラミング言語や環境への拡張が必要です。
◦
本論文はVerinaのベンチマークを提示することに焦点を当てており、LLMのパフォーマンスを向上させるための具体的な方法論的改善を示していません。
👍
Made with Slashpage