論文の概要: Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code

• arxiv url: http://arxiv.org/abs/2403.12627v1
• Date: Tue, 19 Mar 2024 10:53:40 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-20 14:33:18.687233
• Title: Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
• Title（参考訳）: 形式的定理証明の強化:Coqコード上でAIモデルをトレーニングするための総合データセット
• Authors: Andreas Florath,
• Abstract要約: Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。 人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。 このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and machine learning, the specialized nature of Coq syntax and semantics poses unique challenges for Large Language Models (LLMs). Addressing this gap, we present a comprehensive dataset specifically designed to enhance LLMs' proficiency in interpreting and generating Coq code. This dataset, derived from a collection of over 10,000 Coq source files, encompasses a wide array of propositions, proofs, and definitions, enriched with metadata including source references and licensing information. Our primary aim is to facilitate the development of LLMs capable of generating syntactically correct and semantically meaningful Coq constructs, thereby advancing the frontier of automated theorem proving. Initial experiments with this dataset have showcased its significant potential; models trained on this data exhibited enhanced accuracy in Coq code generation. Notably, a particular experiment revealed that a fine-tuned LLM was capable of generating 141 valid proofs for a basic lemma, highlighting the dataset's utility in facilitating the discovery of diverse and valid proof strategies. This paper discusses the dataset's composition, the methodology behind its creation, and the implications of our findings for the future of machine learning in formal verification. The dataset is accessible for further research and exploration: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1
• Abstract（参考訳）: 形式的定理証明の領域では、Coq証明アシスタントは数学的主張とソフトウェア正当性を検証するための厳密なアプローチで際立っている。 人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は、大規模言語モデル(LLM)に固有の課題をもたらす。 このギャップに対処するため,我々は,LLMのコーク符号の解釈・生成能力を高めるために設計された包括的データセットを提案する。 このデータセットは1万以上のCoqソースファイルのコレクションから派生したもので、ソース参照やライセンス情報を含むメタデータに富んだ幅広い命題、証明、定義を含んでいる。 我々の主な目的は、構文的に正し、意味的に意味のある Coq 構造を生成することができる LLM の開発を促進することであり、それによって自動定理証明のフロンティアを前進させることである。 このデータセットでの最初の実験では、その大きな可能性を示しており、このデータに基づいてトレーニングされたモデルは、Coqコード生成の精度を向上した。 特に、特定の実験では、微調整されたLLMが基本的な補題に対して141の有効な証明を生成することができ、多種多様な有効な証明戦略の発見を容易にするためのデータセットの有用性を強調した。 本稿では、データセットの構成、その作成の背景となる方法論、そしてフォーマルな検証における機械学習の将来に対する我々の発見の意味について論じる。 データセットは、さらなる調査と調査に利用可能である。 https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1

関連論文リスト

• OpenCoder: The Open Cookbook for Top-Tier Code Large Language Models [70.72097493954067]
  コードのための大規模言語モデル(LLM)は、コード生成、推論タスク、エージェントシステムなど、さまざまな領域で必須になっている。 オープンアクセスのコード LLM はプロプライエタリなモデルの性能レベルに近づきつつあるが、高品質なコード LLM は依然として限られている。 トップクラスのコードLLMであるOpenCoderは、主要なモデルに匹敵するパフォーマンスを達成するだけでなく、研究コミュニティの"オープンクックブック"としても機能します。
  論文  参考訳（メタデータ） (2024-11-07T17:47:25Z)
• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
  本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。 英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
  論文  参考訳（メタデータ） (2024-08-28T06:33:03Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• MARIO: MAth Reasoning with code Interpreter Output -- A Reproducible Pipeline [12.186691561822256]
  我々は,大規模言語モデル(LLM)の本質的な性質が,数学的推論のモデル化における課題を提起していると仮定する。 本稿では,Pythonコードインタプリタを利用した新しい数学データセットを提案する。 本稿では,数学固有のLLMの微調整のための仮的かつ容易に複製可能なプロトコルを提案する。
  論文  参考訳（メタデータ） (2024-01-16T08:08:01Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Disentanglement via Latent Quantization [60.37109712033694]
  本研究では,組織化された潜在空間からの符号化と復号化に向けた帰納的バイアスを構築する。 本稿では,基本データレコーダ (vanilla autoencoder) と潜時再構成 (InfoGAN) 生成モデルの両方に追加することで,このアプローチの広範な適用性を実証する。
  論文  参考訳（メタデータ） (2023-05-28T06:30:29Z)
• Chain-of-Knowledge: Grounding Large Language Models via Dynamic Knowledge Adapting over Heterogeneous Sources [87.26486246513063]
  Chain-of-knowledge (CoK)は、大規模な言語モデルを拡張するフレームワークである。 CoKは推論準備、動的知識適応、解答統合の3段階からなる。
  論文  参考訳（メタデータ） (2023-05-22T17:34:23Z)

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

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