論文の概要: miniCodeProps: a Minimal Benchmark for Proving Code Properties

• arxiv url: http://arxiv.org/abs/2406.11915v2
• Date: Thu, 10 Oct 2024 16:13:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-11 14:30:01.451381
• Title: miniCodeProps: a Minimal Benchmark for Proving Code Properties
• Title（参考訳）: miniCodeProps: コードプロパティを証明するための最小ベンチマーク
• Authors: Evan Lohn, Sean Welleck,
• Abstract要約: 私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。 その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
• 参考スコア（独自算出の注目度）: 22.548472305010005
• License:
• Abstract: AI agents have shown initial promise in automating mathematical theorem proving in proof assistants such as Lean. The same proof assistants can be used to verify the correctness of code by pairing code with specifications and proofs that the specifications hold. Automating the writing of code, specifications, and proofs could lower the cost of verification, or, ambitiously, enable an AI agent to output safe, provably correct code. However, it remains unclear whether current neural theorem provers can automatically verify even relatively simple programs. We present miniCodeProps, a benchmark of 201 program specifications in the Lean proof assistant, aimed at the subproblem of automatically generating a proof for a provided program and specification. miniCodeProps contains specifications about simple, self-contained programs (e.g., lists, natural numbers, binary trees) with varied proof difficulty. Despite its simplicity, miniCodeProps is sufficient to break current LLM-based provers, with state-of-the-art methods showing promise on the easy properties in miniCodeProps, yet failing to prove nearly all of the medium and hard properties. We publicly release miniCodeProps as a benchmark for furthering automated theorem proving in the context of formally verified code.
• Abstract（参考訳）: AIエージェントは、Leanのような証明アシスタントで証明された数学的定理の自動化において、最初の約束を示している。 同じ証明アシスタントを使用して、仕様と仕様が保持する証明とをペアにすることで、コードの正しさを検証することができる。 コードや仕様、証明の記述を自動化することは、検証コストを削減したり、野心的にAIエージェントが安全かつ確実に正しいコードを出力できるようにする可能性がある。 しかし、現在のニューラル定理の証明者が、たとえ比較的単純なプログラムでも自動的に検証できるかどうかは不明である。 本稿では,提供されるプログラムと仕様の証明を自動的に生成するサブプロブレムを目的とした,201のプログラム仕様のベンチマークである miniCodeProps を紹介する。 miniCodePropsには、単純で自己完結したプログラム(リスト、自然数、バイナリツリーなど)に関する仕様が含まれており、証明の難しさは様々である。 その単純さにもかかわらず、 miniCodeProps は現在の LLM ベースのプローバーを壊すのに十分であり、最先端のメソッドは miniCodeProps の容易なプロパティを約束するが、中堅なプロパティとハードなプロパティのほとんどを証明できなかった。 公式に検証されたコードのコンテキストで証明された自動定理のベンチマークとして、MiniCodePropsを公開しています。

関連論文リスト

• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  大規模言語モデル(LLM)は、多くのソフトウェアエンジニアリング活動において有望であることを示している。 本稿では,分離論理に基づく仕様生成におけるOpenAIのGPTモデルの有効性について検討する。
  論文  参考訳（メタデータ） (2024-11-04T17:44:11Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• AutoVerus: Automated Proof Generation for Rust Code [25.56534570237484]
  AutoVerusは大規模な言語モデル(LLM)を使用して、Rustコードの正確性証明を自動的に生成する。 評価の結果,AutoVerusは90%以上の正解を自動生成できることがわかった。
  論文  参考訳（メタデータ） (2024-09-19T20:40:52Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• 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)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• 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)
• Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
  本研究では,不確実性に関する情報を伝達することで,プログラマがより迅速かつ正確にコードを生成することができるかどうかを検討する。 トークンのハイライトは、編集される可能性が最も高いので、タスクの完了が早くなり、よりターゲットを絞った編集が可能になることがわかりました。
  論文  参考訳（メタデータ） (2023-02-14T18:43:34Z)

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

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