論文の概要: Cobblestone: Iterative Automation for Formal Verification

• arxiv url: http://arxiv.org/abs/2410.19940v2
• Date: Thu, 31 Jul 2025 22:29:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-04 18:08:53.431582
• Title: Cobblestone: Iterative Automation for Formal Verification
• Title（参考訳）: Cobblestone: 形式検証の反復的自動化
• Authors: Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First,
• Abstract要約: 証明合成のための分割・対数手法である Cobblestone を導入する。 Cobblestoneは大きな言語モデル(LLM)を使用して潜在的な証明を生成する。 各コブルストーンの走行時間は1.25ドルであり、平均14.7分である。
• 参考スコア（独自算出の注目度）: 11.445689801392657
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to prove only a fraction of desired software properties. We introduce Cobblestone, a divide-and-conquer approach for proof synthesis. Cobblestone uses a large language model (LLM) to generate potential proofs, uses those proofs to break the problem into simpler parts, automatically identifies which of those parts were successfully proven, and iterates on the remaining parts to build a correct proof that is guaranteed to be sound, despite the reliance on unsound LLMs. We evaluate Cobblestone on four benchmarks of open-source Coq projects, controlling for training data leakage. Fully automatically, Cobblestone outperforms state-of-the-art non-LLM tools, and proves many theorems that other LLM-based tools cannot, and on many benchmarks, outperforms them. Each Cobblestone run costs only $1.25 and takes 14.7 minutes, on average. Cobblestone can also be used with external input, from a user or another tool, providing a proof structure or relevant lemmas. Evaluated with such an oracle, Cobblestone proves up to 58% of theorems. Overall, our research shows that tools can make use of partial progress and external input to more effectively automate formal verification.
• Abstract（参考訳）: Coqのような証明アシスタントを使った形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、かなりの努力と専門知識が必要である。 機械学習は自動的に証明を合成できるが、これらのツールは必要なソフトウェアプロパティのごく一部しか証明できない。 証明合成のための分割・対数手法である Cobblestone を導入する。 Cobblestoneは、潜在的な証明を生成するために、大きな言語モデル(LLM)を使用し、これらの証明を使用して問題をより単純な部分に分割し、どの部分が成功したかを自動的に識別し、未解決のLLMに頼っているにもかかわらず、正しい証明を構築するために残りの部分を繰り返す。 オープンソースのCoqプロジェクトの4つのベンチマークで、Cobblestoneを評価し、データ漏洩のトレーニングを制御します。 完全に自動で、Cobblestoneは最先端の非LLMツールより優れており、他のLLMベースのツールではできない多くの定理を証明し、多くのベンチマークではそれらより優れている。 各コブルストーンの走行時間は1.25ドルであり、平均14.7分である。 Cobblestoneは、ユーザまたは他のツールからの外部からの入力でも使用することができ、証明構造や関連する補題を提供する。 そのようなオラクルで評価すると、コブルストーンは最大で58%の定理を証明している。 全体としては、ツールが部分的な進捗と外部からの入力を利用して、より効果的に形式的検証を自動化できることが示されている。

関連論文リスト

• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [8.056359341994941]
  APOLLOは、Leanコンパイラの強みとLLMの推論能力を組み合わせた、モデルに依存しないパイプラインである。 エージェントのセットが証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定します。 修理されたサブステイストは再結合され、再検証され、ユーザ制御された最大試行回数まで反復される。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
  バックエンドのコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。 我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。 本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることがわかった。
  論文  参考訳（メタデータ） (2025-04-13T16:49:37Z)
• START: Self-taught Reasoner with Tools [51.38785489790888]
  ツール統合長チェーン・オブ・シークレット(CoT)推論LSMであるSTART(Self-Taught Reasoner with Tools)を紹介する。 STARTは複雑な計算、自己チェック、多様な方法の探索、そして自己老化を行うことができる。 基礎となるQwQ-32Bを著しく上回り、最先端のオープンウェイトモデルR1-Distill-Qwen-32Bに匹敵する性能を達成する。
  論文  参考訳（メタデータ） (2025-03-06T17:11:51Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification [11.115201117143929]
  本稿では,Coq用の完全自動合成証明ツールであるRangoを紹介する。 Rangoは関連する前提と、それに類似した証明を現在のプロジェクトから特定し、合成時にそれらを使用する。 評価の結果, Rangoが文脈に関連付けると, 証明された定理の数が47%増加することがわかった。
  論文  参考訳（メタデータ） (2024-12-18T17:08:42Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning [8.116854714039452]
  QEDCartographerは、教師付きと強化学習を組み合わせた自動証明合成ツールである。 オープンソースCoqプロジェクトの68.5K定理のCoqGymベンチマークを用いて,QEDCartographerを評価した。 本研究は,強化学習が証明合成ツールの探索機構を改善するための実りある研究方向であることを実証する。
  論文  参考訳（メタデータ） (2024-08-17T16:06:14Z)
• Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code [0.0]
  Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。 人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。 このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
  論文  参考訳（メタデータ） (2024-03-19T10:53:40Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Zero-shot Fact Verification by Claim Generation [85.27523983027471]
  我々は,堅牢な事実検証モデルをトレーニングするフレームワークであるQACGを開発した。 われわれは自動的に生成されたクレームを使って、Wikipediaのエビデンスからサポートしたり、反論したり、検証したりできる。 ゼロショットシナリオでは、QACGはRoBERTaモデルのF1を50%から77%に改善し、パフォーマンスは2K以上の手作業による例に相当する。
  論文  参考訳（メタデータ） (2021-05-31T03:13:52Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)
• Self-Supervised Log Parsing [59.04636530383049]
  大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。 既存のアプローチは、ログ特化や手動ルール抽出に依存している。 本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
  論文  参考訳（メタデータ） (2020-03-17T19:25:25Z)

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

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