論文の概要: VeriBase: Automated Construction of Theorem Libraries for Software Verification

• arxiv url: http://arxiv.org/abs/2611.01743v1
• Date: Sun, 01 Nov 2026 09:43:09 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-11-03 19:37:09.178103
• Title: VeriBase: Automated Construction of Theorem Libraries for Software Verification
• Title（参考訳）: VeriBase: ソフトウェア検証のための理論ライブラリの自動構築
• Abstract要約: ソフトウェア検証ライブラリを自動構築するフレームワークを提案する。 鍵となる課題は、定理のステートメントと証明と共に実装を一般化することである。 独立した4,191のプログラムから構築した汎用ライブラリは,タスクの成功率を最大17.0%向上させることを示す。
• 参考スコア（独自算出の注目度）: 29.99905659651405
• License:
• Abstract: Software verification is typically more challenging than coding. Software developers routinely build on mature libraries and APIs, but turning successful verification solutions into reusable libraries still requires substantial expert effort. In this paper, we propose VeriBase, a framework for automatically constructing software-verification libraries by jointly generalizing code and its associated theorems from successful verification solutions. The key challenge is to generalize implementations together with the theorem statements and proofs that depend on these implementations, and reconcile overlapping components across verification tasks. To this end, VeriBase treats code and its associated theorems as declaration families, and designs a three-phase pipeline, which proves seed tasks, generalizes code and associated theorems, and harvests the resulting families into shared interfaces. VeriBase updates dependent declarations as interface change and uses Lean to check the resulting code and proofs. We evaluate VeriBase across four benchmarks with three backend LLMs. The results show that the general-purpose library built from independent 4,191 programs increases the average task success rate by up to 17.0% and meanwhile reduces the proof completion time by up to 21.4%. When VeriBase constructs a benchmark-specific library, further improvement can be observed.
• Abstract（参考訳）: ソフトウェア検証はコーディングよりも難しいのが普通です。 ソフトウェア開発者は、成熟したライブラリとAPIを定期的に構築するが、成功した検証ソリューションを再利用可能なライブラリに変えるには、かなりの専門的な努力が必要だ。 本稿では,コードと関連する定理を協調的に一般化することで,ソフトウェア検証ライブラリを自動構築するフレームワークであるVeriBaseを提案する。 鍵となる課題は、これらの実装に依存する定理のステートメントや証明と共に実装を一般化し、検証タスク間で重複するコンポーネントを調整することである。 この目的のために、VeriBaseはコードとその関連する定理を宣言ファミリとして扱い、シードタスクを証明し、コードと関連する定理を一般化し、結果のファミリーを共有インターフェースに抽出する3相パイプラインを設計する。 VeriBaseは依存性の宣言をインターフェースの変更として更新し、Leanを使って結果のコードと証明をチェックする。 3つのバックエンドLLMを持つ4つのベンチマークでVeriBaseを評価した。 その結果、独立した4,191のプログラムから構築された汎用ライブラリは、平均タスク成功率を17.0%まで向上させ、一方で証明完了時間を21.4%まで短縮した。 VeriBaseがベンチマーク固有のライブラリを構築すると、さらなる改善が観察できる。

関連論文リスト

• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。 Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。 ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
  論文  参考訳（メタデータ） (2026-08-13T17:41:27Z)
• P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation [19.3449645807529]
  検証されたコード生成は、プログラムの実行可能プログラムとマシンチェック可能な証明の両方を生成するために、大きな言語モデル(LLM)を要求する。 このシーケンシャルパイプラインは、実際には非効率かつ非効率である可能性があることを観察する。 プログラムとその正当性引数を手作業で開発するべきだというディクストラの見解に触発されて、我々は$P3$を提案する。
  論文  参考訳（メタデータ） (2026-08-10T08:33:18Z)
• SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
  本稿では,スマートコントラクトデコンパイルのためのデータセットとベンチマーク手法であるSCDBenchを紹介する。 データセットには600の現実のSolidityコントラクトと、ペア化されたバイトコード入力、地味なソースコード、再生可能なセマンティックチェックポイントが含まれている。 我々は,GLM-5の変種を含むゼロショット逆コンパイル設定において,Claude Opus 4.7,GPT-5.3-Codex,GLM-5を評価した。
  論文  参考訳（メタデータ） (2026-05-27T20:08:47Z)
• Beyond Code Snippets: Benchmarking LLMs on Repository-Level Question Answering [4.120344028676837]
  大規模言語モデル(LLM)は、質問応答(QA)を含む、ソフトウェアエンジニアリングタスク全体で印象的な機能を示している。 StackRepoQAは、134のオープンソースJavaプロジェクト間で、1,318の実際の開発者質問と受け入れられた回答から構築された、最初のマルチプロジェクト、リポジトリレベルの質問応答データセットです。
  論文  参考訳（メタデータ） (2026-03-27T16:30:54Z)
• VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean [34.16542476896347]
  オープンソースのフォーマルメソッド開発から引き出された500リーン4の証明義務のベンチマークを導入します。 我々は、Mathlib型数学用に調整されたプローバーが、このリポジトリ中心の設定に不十分に移行していることを発見した。 証明の依存性のクロージャに制限されたキュレートされたコンテキストを提供することで、完全なリポジトリを公開することでパフォーマンスが向上する。
  論文  参考訳（メタデータ） (2026-02-20T16:05:06Z)
• ProjDevBench: Benchmarking AI Coding Agents on End-to-End Project Development [49.63491095660809]
  ProjDevBenchはエンドツーエンドのベンチマークで、コーディングエージェントにプロジェクト要件を提供し、その結果のリポジトリを評価する。 概念指向タスクと実世界のアプリケーションシナリオの両方をカバーし、8つのカテゴリにまたがる20のプログラミング問題をキュレートします。 エージェントは基本的な機能を扱うが、複雑なシステム設計、時間最適化、リソース管理に苦労する。
  論文  参考訳（メタデータ） (2026-02-02T05:17:23Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Towards Realistic Project-Level Code Generation via Multi-Agent Collaboration and Semantic Architecture Modeling [7.753074942497876]
  CodeProjectEvalは、12.7ファイルと2,388.6行のタスクを持つ18の現実世界リポジトリから構築されたプロジェクトレベルのコード生成データセットである。 プロジェクトをアーキテクチャ設計、スケルトン生成、コードフィリングステージに分解するマルチエージェントフレームワークであるProjectGenを提案する。 実験によると、ProjectGenは、52/124のテストケースを小さなプロジェクトレベルのコード生成データセットDevBenchに渡すことで、最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-11-05T12:12:35Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0は、AIエージェントにスクラッチからライブラリを書くよう促すベンチマークである。 エージェントには、ライブラリのAPIを概説する仕様文書と、インタラクティブなユニットテストスイートが提供されている。 Commit0はまた、モデルが生成したコードに対して静的解析と実行フィードバックを受け取る、インタラクティブな環境も提供する。
  論文  参考訳（メタデータ） (2024-12-02T18:11:30Z)
• ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
  ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。 LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
  論文  参考訳（メタデータ） (2023-11-16T12:03:21Z)

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

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