論文の概要: VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean

• arxiv url: http://arxiv.org/abs/2602.18307v1
• Date: Fri, 20 Feb 2026 16:05:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-23 18:01:41.370826
• Title: VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
• Title（参考訳）: VeriSoftBench: リーンのためのリポジトリ規模の形式検証ベンチマーク
• Authors: Yutong Xin, Qiaochu Chen, Greg Durrett, Işil Dillig,
• Abstract要約: オープンソースのフォーマルメソッド開発から引き出された500リーン4の証明義務のベンチマークを導入します。 我々は、Mathlib型数学用に調整されたプローバーが、このリポジトリ中心の設定に不十分に移行していることを発見した。 証明の依存性のクロージャに制限されたキュレートされたコンテキストを提供することで、完全なリポジトリを公開することでパフォーマンスが向上する。
• 参考スコア（独自算出の注目度）: 34.16542476896347
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models have achieved striking results in interactive theorem proving, particularly in Lean. However, most benchmarks for LLM-based proof automation are drawn from mathematics in the Mathlib ecosystem, whereas proofs in software verification are developed inside definition-rich codebases with substantial project-specific libraries. We introduce VeriSoftBench, a benchmark of 500 Lean 4 proof obligations drawn from open-source formal-methods developments and packaged to preserve realistic repository context and cross-file dependencies. Our evaluation of frontier LLMs and specialized provers yields three observations. First, provers tuned for Mathlib-style mathematics transfer poorly to this repository-centric setting. Second, success is strongly correlated with transitive repository dependence: tasks whose proofs draw on large, multi-hop dependency closures are less likely to be solved. Third, providing curated context restricted to a proof's dependency closure improves performance relative to exposing the full repository, but nevertheless leaves substantial room for improvement. Our benchmark and evaluation suite are released at https://github.com/utopia-group/VeriSoftBench.
• Abstract（参考訳）: 大規模な言語モデルは、特にリーンにおいて、インタラクティブな定理証明において大きな成果を上げています。 しかし、LLMベースの証明自動化のためのほとんどのベンチマークは、Mathlibエコシステムの数学から引き出されたものであるのに対し、ソフトウェア検証の証明は、プロジェクト固有のライブラリを持つ定義に富んだコードベースの中で開発されている。 VeriSoftBenchは、オープンソースのフォーマルメソッド開発から引き出された500リーン4の証明義務のベンチマークで、現実的なリポジトリコンテキストとファイル間の依存関係を保存するためにパッケージ化されています。 我々は,フロンティアLLMと特殊プロデューサの3つの観測結果を得た。 第一に、Mathlib型数学のために調整されたプローバーは、このリポジトリ中心の設定に不十分に移行した。 第二に、成功は推移的なリポジトリ依存と強く相関している: 証明が大きなマルチホップ依存のクロージャに描画されるタスクは、解決される可能性が低い。 第三に、検証の依存性のクロージャに制限されたキュレートされたコンテキストを提供することで、完全なリポジトリを公開することによるパフォーマンスが向上するが、それでも改善の余地は十分にある。 ベンチマークと評価スイートはhttps://github.com/utopia-group/VeriSoftBench.comで公開されています。

関連論文リスト

• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。 我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
  論文  参考訳（メタデータ） (2026-01-30T08:29:01Z)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs [54.231935013127206]
  大型言語モデル (LLM) は, CoT (Chain-of-Thought) による数学的問題に対して高い性能を示す 我々は、有向非巡回グラフ(DAG)上の一定の規則に基づくプロセスとしてCoTをモデル化することを提案する。 ここでは,モデルのCoT軌道がDAG構造にどの程度よく依存するかを定量化する計量である論理的近接性を導入する。
  論文  参考訳（メタデータ） (2025-10-19T21:05:17Z)
• The SWE-Bench Illusion: When State-of-the-Art LLMs Remember Instead of Reason [1.6249398255272318]
  本稿では,SWE-Bench-Verifiedの性能向上は,真の問題解決よりも記憶によってもたらされる可能性があることを示す。 現状のモデルでは,リポジトリ構造にアクセスすることなく,問題記述のみを用いて,バグのあるファイルパスを識別する精度を最大76%向上することを示す。 これらの結果は、既存の結果の有効性に関する懸念を提起し、より堅牢で汚染に強いベンチマークの必要性を浮き彫りにした。
  論文  参考訳（メタデータ） (2025-06-14T00:25:26Z)
• DI-BENCH: Benchmarking Large Language Models on Dependency Inference with Testable Repositories at Scale [39.92722886613929]
  DI-BENCHは、大規模言語モデルの依存性推論能力を評価するために設計された、大規模なベンチマークおよび評価フレームワークである。 ベンチマークでは、Python、C#、Rust、JavaScriptにまたがるテスト環境を備えた581のリポジトリが提供されている。 テキストと実行ベースのメトリクスによる大規模な実験により、現在の最高のパフォーマンスモデルは42.9%の実行パス率しか達成していないことが明らかになった。
  論文  参考訳（メタデータ） (2025-01-23T14:27:11Z)
• MR-Ben: A Meta-Reasoning Benchmark for Evaluating System-2 Thinking in LLMs [55.20845457594977]
  大規模言語モデル(LLM)は、問題解決と意思決定の能力の向上を示している。 本稿ではメタ推論技術を必要とするプロセスベースのベンチマークMR-Benを提案する。 メタ推論のパラダイムは,システム2のスロー思考に特に適しています。
  論文  参考訳（メタデータ） (2024-06-20T03:50:23Z)
• On the Impacts of Contexts on Repository-Level Code Generation [5.641402231731082]
  本稿ではレポジトリレベルのコード生成を評価するために設計された新しいベンチマークであるRepoExecを紹介する。 実行可能性、包括的なテストケース生成による機能的正当性、ファイル間のコンテキストの正確な利用という3つの重要な側面に注目します。
  論文  参考訳（メタデータ） (2024-06-17T10:45:22Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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