論文の概要: Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

• arxiv url: http://arxiv.org/abs/2412.14063v3
• Date: Tue, 28 Jan 2025 19:56:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-30 15:52:29.888849
• Title: Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
• Title（参考訳）: Rango: 自動検証のための適応型検索拡張証明
• Authors: Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First,
• Abstract要約: 本稿では,Coq用の完全自動合成証明ツールであるRangoを紹介する。 Rangoは関連する前提と、それに類似した証明を現在のプロジェクトから特定し、合成時にそれらを使用する。 評価の結果, Rangoが文脈に関連付けると, 証明された定理の数が47%増加することがわかった。
• 参考スコア（独自算出の注目度）: 11.115201117143929
• License:
• Abstract: Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.
• Abstract（参考訳）: Coqのような証明アシスタントを用いた形式検証は、高品質なソフトウェアの作成を可能にする。 しかし、検証プロセスには、証明を書くためにかなりの専門知識と手作業が必要である。 近年,機械学習と大規模言語モデル(LLM)を用いた証明合成の自動化について検討している。 この研究は、補題や定義のような関連する前提を特定することが合成に役立つことを示した。 本稿では,Coqの完全自動証明合成ツールであるRangoについて紹介する。 Rangoは、証明のすべてのステップで検索拡張を使用して、どの証明と前提をその微調整LDMのコンテキストに含めるかを自動的に決定する。 このようにして、Rangoはプロジェクトと証明の進化状態に適応する。 我々は2,226のオープンソースCoqプロジェクトと196,929の定理からなる新しいデータセット、CoqStoqを作成しました。 このベンチマークでは、ランゴは32.0%の定理の証明を合成し、これはそれまでの最先端のツールであるTacticianよりも29%多い定理である。 また、Rangoが関連する証明を文脈に加えることで、証明された定理の数が47%増加することを示した。

関連論文リスト

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning [8.116854714039452]
  QEDCartographerは、教師付きと強化学習を組み合わせた自動証明合成ツールである。 オープンソースCoqプロジェクトの68.5K定理のCoqGymベンチマークを用いて,QEDCartographerを評価した。 本研究は,強化学習が証明合成ツールの探索機構を改善するための実りある研究方向であることを実証する。
  論文  参考訳（メタデータ） (2024-08-17T16:06:14Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
  論文  参考訳（メタデータ） (2024-05-07T12:50:28Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。 我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• 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)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• 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)

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

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