論文の概要: CLEVER: A Curated Benchmark for Formally Verified Code Generation

• arxiv url: http://arxiv.org/abs/2505.13938v2
• Date: Wed, 21 May 2025 03:14:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-22 13:19:52.347461
• Title: CLEVER: A Curated Benchmark for Formally Verified Code Generation
• Title（参考訳）: CLEVER: 形式的に検証されたコード生成のためのベンチマーク
• Authors: Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, Swarat Chaudhuri,
• Abstract要約: $rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
• 参考スコア（独自算出の注目度）: 57.476483009565044
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce ${\rm C{\small LEVER}}$, a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification. Unlike prior benchmarks, ${\rm C{\small LEVER}}$ avoids test-case supervision, LLM-generated annotations, and specifications that leak implementation logic or allow vacuous solutions. All outputs are verified post-hoc using Lean's type checker to ensure machine-checkable correctness. We use ${\rm C{\small LEVER}}$ to evaluate several few-shot and agentic approaches based on state-of-the-art language models. These methods all struggle to achieve full verification, establishing it as a challenging frontier benchmark for program synthesis and formal reasoning. Our benchmark can be found on GitHub(https://github.com/trishullab/clever) as well as HuggingFace(https://huggingface.co/datasets/amitayusht/clever). All our evaluation code is also available online(https://github.com/trishullab/clever-prover).
• Abstract（参考訳）: これは、リーンでエンドツーエンドのコード生成を検証した161の問題を、高品質でキュレートしたベンチマークです。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。 以前のベンチマークとは異なり、${\rm C{\small LEVER}}$は、テストケースの監督、LLM生成アノテーション、実装ロジックをリークする仕様、あるいは空白なソリューションを可能にする仕様を避けます。 すべてのアウトプットは、マシンチェック可能な正確性を保証するために、Leanの型チェッカーを使用してポストホックで検証されます。 我々は、最先端の言語モデルに基づいて、いくつかのショットとエージェントのアプローチを評価するために、${\rm C{\small LEVER}}$を使用します。 これらの手法はすべて完全な検証を達成するのに苦労し、プログラム合成と公式な推論のための挑戦的なフロンティアベンチマークとして確立した。 私たちのベンチマークはGitHub(https://github.com/trishullab/clever)とHuggingFace(https://huggingface.co/datasets/amitayusht/clever)で確認できます。 評価コードはすべてオンラインで利用可能です(https://github.com/trishullab/clever-prover)。

関連論文リスト

• Disproving Program Equivalence with LLMs [22.047880121762013]
  ProbeGenは、2つ以上の実行可能なコードと、その等価性に対する反例を検索するホワイトボックスメソッドである。 ProbeGenは、ベンチマークによる単体テストにより、基礎的真理と等価であると考えられるサンプルの18%を反証することを示した。 ProbeGenを使うことで、意味的な自己整合性のためにLLMサンプルをセマンティックにクラスタリングし、pass@1を10%改善できます。
  論文  参考訳（メタデータ） (2025-02-05T12:54:17Z)
• Simple and Provable Scaling Laws for the Test-Time Compute of Large Language Models [70.07661254213181]
  本研究では,大規模言語モデルのテスト時間計算において,証明可能なスケーリング法則を享受する2つのアルゴリズムを提案する。 1つは2段階ノックアウト方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。 もう1つは2段階のリーグ方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。
  論文  参考訳（メタデータ） (2024-11-29T05:29:47Z)
• Steering Large Language Models between Code Execution and Textual Reasoning [22.279107036500083]
  テキスト推論は、数学、論理学、最適化、探索における課題を伴うタスクの解決に固有の制限がある。 OpenAI GPT Code InterpreterとAutoGenのようなマルチエージェントフレームワークは、コード生成と実行を統合するのに顕著な能力を示している。 LLMのコード/テキスト生成を良くし、顕著な改善を実現するための3つの方法を提案する。
  論文  参考訳（メタデータ） (2024-10-04T15:44:47Z)
• Generating Unseen Code Tests In Infinitum [1.0674604700001968]
  本稿では,プログラミングタスクやプログラミング言語にまたがって一般化するベンチマークのバリエーションを作成する手法を提案する。 我々は、Pythonでテキストからコードを生成するタスクに対して、textitauto-regressionと呼ばれる1つのベンチマークを実装した。
  論文  参考訳（メタデータ） (2024-07-29T08:11:20Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。