論文の概要: Towards Repository-Level Program Verification with Large Language Models

• arxiv url: http://arxiv.org/abs/2509.25197v1
• Date: Sun, 31 Aug 2025 02:44:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-06 05:29:07.807214
• Title: Towards Repository-Level Program Verification with Large Language Models
• Title（参考訳）: 大規模言語モデルを用いたレポジトリレベルプログラム検証に向けて
• Authors: Si Cheng Zhong, Xujie Si,
• Abstract要約: 実世界のプロジェクトに自動的な形式検証をスケールするには、モジュール間の依存関係とグローバルなコンテキストを解決する必要がある。 RVBenchは,4つの多種多様な複雑なオープンソースのVerusプロジェクトから構築された,リポジトリレベルの評価のために明示的に設計された最初の検証ベンチマークである。 RagedVerusは、マルチモジュールリポジトリの証明を自動化するために、コンテキスト認識で検索拡張を同期するフレームワークである。
• 参考スコア（独自算出の注目度）: 8.05666536952624
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advancements in large language models (LLMs) suggest great promises in code and proof generations. However, scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are crucial challenges overlooked by existing LLM-based methods with a special focus on targeting isolated, function-level verification tasks. To systematically explore and address the significant challenges of verifying entire software repositories, we introduce RVBench, the first verification benchmark explicitly designed for repository-level evaluation, constructed from four diverse and complex open-source Verus projects. We further introduce RagVerus, an extensible framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories. RagVerus triples proof pass rates on existing benchmarks under constrained model inference budgets, and achieves a 27% relative improvement on the more challenging RVBench benchmark, demonstrating a scalable and sample-efficient verification solution.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、コードと証明世代における大きな約束を示唆している。 しかし、実際のプロジェクトに自動的な形式検証を拡大するには、モジュール間の依存関係とグローバルコンテキストの解決が必要である。 ソフトウェアリポジトリ全体の検証に関する重要な課題を体系的に調査し,対処するために,4つの多種多様な複雑なオープンソースVerusプロジェクトから構築された,リポジトリレベルの評価用に明示的に設計された最初の検証ベンチマークであるRVBenchを紹介した。 さらに、マルチモジュールリポジトリの証明合成を自動化するために、コンテキスト認識で検索拡張生成を同期する拡張可能なフレームワークであるRagVerusを紹介する。 RagVerusは制約付きモデル推論予算の下で既存のベンチマークのパスレートを3倍にし、より困難なRVBenchベンチマークで相対的に27%の改善を実現し、スケーラブルでサンプル効率のよい検証ソリューションを実証している。

関連論文リスト

• Loong: Synthesize Long Chain-of-Thoughts at Scale through Verifiers [103.4410890572479]
  スケーラブルな合成データ生成と検証のためのオープンソースのフレームワークであるLoong Projectを紹介します。 LoongBenchは、12のドメインにまたがる8,729の人為的なサンプルを含む、キュレートされたシードデータセットである。 LoongEnvはモジュラー合成データ生成環境であり、新しい質問応答コードのトリプルを生成する複数のプロンプト戦略をサポートする。
  論文  参考訳（メタデータ） (2025-09-03T06:42:40Z)
• SaraCoder: Orchestrating Semantic and Structural Cues for Profit-Oriented Repository-Level Code Completion [37.66834526941521]
  リポジトリレベルのコード補完のための検索拡張生成(RAG)は、一般的に表面テキストの類似性に依存している。 階層的特徴量検索フレームワークであるSaracoderを紹介する。
  論文  参考訳（メタデータ） (2025-08-13T11:56:05Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Crossing the Reward Bridge: Expanding RL with Verifiable Rewards Across Diverse Domains [92.36624674516553]
  検証可能な報酬付き強化学習(RLVR)は、大規模言語モデル(LLM)の数学的推論と符号化性能の向上に成功している。 本稿では,医学,化学,心理学,経済学,教育など,さまざまな現実世界領域におけるRLVRの有効性と拡張性について検討する。 我々は,2値検証による制限を克服するために,ソフトなモデルに基づく報酬信号を生成する生成的スコアリング手法を利用する。
  論文  参考訳（メタデータ） (2025-03-31T08:22:49Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation [24.081573908824353]
  一階述語論理(FOL)推論はインテリジェントシステムにおいて重要である。 既存のベンチマークは、広範囲の人間のアノテーションや手作りテンプレートに依存していることが多い。 本稿では,大言語モデルの生成強度を記号型プローサの厳密性と精度で相乗化するProverGenという新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-02-10T15:31:54Z)
• RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation [4.934638689939017]
  我々は,複数モジュールリポジトリの証明合成を自動化するために,検索拡張生成とコンテキスト認識を併用するフレームワークであるRagVerusを紹介した。 R RagVerusは、制約付き言語モデル予算の下で、既存のベンチマークのパスレートを3倍にします。
  論文  参考訳（メタデータ） (2025-02-07T21:30:37Z)
• DiscoveryBench: Towards Data-Driven Discovery with Large Language Models [50.36636396660163]
  我々は、データ駆動探索の多段階プロセスを形式化する最初の包括的なベンチマークであるDiscoveryBenchを紹介する。 我々のベンチマークには、社会学や工学などの6つの分野にまたがる264のタスクが含まれている。 私たちのベンチマークでは、自律的なデータ駆動型発見の課題を説明し、コミュニティが前進するための貴重なリソースとして役立ちます。
  論文  参考訳（メタデータ） (2024-07-01T18:58:22Z)

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

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