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

• arxiv url: http://arxiv.org/abs/2406.11915v1
• Date: Sun, 16 Jun 2024 21:11:23 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-20 00:46:12.073892
• Title: miniCodeProps: a Minimal Benchmark for Proving Code Properties
• Title（参考訳）: miniCodeProps: コードプロパティを証明するための最小ベンチマーク
• Authors: Evan Lohn, Sean Welleck,
• Abstract要約: 私たちはLeanの証明アシスタントで177のプログラム仕様のベンチマークであるminiCodePropsを紹介します。 その単純さにもかかわらず、 miniCodeProps は現在の LLM ベースのプロデューサにとって困難であり、仕様の約25%を証明できた。
• 参考スコア（独自算出の注目度）: 22.548472305010005
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural networks 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 a machine learning system to output 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 177 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 challenging for current LLM-based provers, which succeed in proving about 25 percent of the specifications. We publicly release miniCodeProps as a benchmark for furthering automated theorem proving in the context of formally verified code.
• Abstract（参考訳）: ニューラルネットワークは、Leanのような証明アシスタントで証明された数学的定理の自動化において、最初の約束を示している。 同じ証明アシスタントを使用して、仕様と仕様が保持する証明とをペアにすることで、コードの正しさを検証することができる。 コードや仕様、証明の記述を自動化することで、検証コストを削減したり、あるいは野心的に、機械学習システムが正当に正しいコードを出力できるようにする。 しかし、現在のニューラル定理の証明者が、たとえ比較的単純なプログラムでも自動的に検証できるかどうかは不明である。 本稿では,提供されるプログラムと仕様の証明を自動的に生成するサブプロブレムを目的とした,Lean証明アシスタントの177のプログラム仕様のベンチマークであるminiCodePropsを紹介する。 miniCodePropsには、単純で自己完結したプログラム(リスト、自然数、バイナリツリーなど)に関する仕様が含まれており、証明の難しさは様々である。 その単純さにもかかわらず、 miniCodeProps は現在の LLM ベースのプロデューサにとって困難であり、仕様の約25%を証明できた。 公式に検証されたコードのコンテキストで証明された自動定理のベンチマークとして、MiniCodePropsを公開しています。

関連論文リスト

• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 我々のデータセットには、約32KのトップレベルF*定義が含まれており、それぞれが型指向プログラムと証明合成の問題を表している。 我々は、AIを用いてプログラムと証明をF*で合成し、有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• 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)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)
• Measuring Coding Challenge Competence With APPS [54.22600767666257]
  コード生成のベンチマークであるAPPSを紹介する。 私たちのベンチマークには1万の問題が含まれています。 GPT-Neoのような最近のモデルでは、導入問題のテストケースの約15%をパスできる。
  論文  参考訳（メタデータ） (2021-05-20T17:58:42Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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