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

• arxiv url: http://arxiv.org/abs/2403.12627v2
• Date: Tue, 2 Apr 2024 13:54:47 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-04 07:58:37.266134
• 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

関連論文リスト

• Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation [24.081573908824353]
  一階述語論理(FOL)推論はインテリジェントシステムにおいて重要である。 既存のベンチマークは、広範囲の人間のアノテーションや手作りテンプレートに依存していることが多い。 本稿では,大言語モデルの生成強度を記号型プローサの厳密性と精度で相乗化するProverGenという新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-02-10T15:31:54Z)
• Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning [85.635988711588]
  我々は,大規模言語モデルの能力向上には,数学的データセットの設計におけるパラダイムシフトが必要であると論じる。 1949年にG. P'olyaが導入した「動機付き証明」の概念は、より良い証明学習信号を提供するデータセットの青写真として機能する。 数学データセットに特化して設計されたアンケートでは、クリエーターにデータセットを含めるよう促します。
  論文  参考訳（メタデータ） (2024-12-19T18:55:17Z)
• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification [11.115201117143929]
  本稿では,Coq用の完全自動合成証明ツールであるRangoを紹介する。 Rangoは関連する前提と、それに類似した証明を現在のプロジェクトから特定し、合成時にそれらを使用する。 評価の結果, Rangoが文脈に関連付けると, 証明された定理の数が47%増加することがわかった。
  論文  参考訳（メタデータ） (2024-12-18T17:08:42Z)
• MAmmoTH-VL: Eliciting Multimodal Reasoning with Instruction Tuning at Scale [66.73529246309033]
  MLLM(Multimodal large language model)は、多モーダルタスクにおいて大きな可能性を秘めている。 既存の命令チューニングデータセットは、中間的合理性のないフレーズレベルの答えのみを提供する。 そこで本研究では,大規模マルチモーダル・インストラクション・チューニング・データセットを構築するためのスケーラブルで費用対効果の高い手法を提案する。
  論文  参考訳（メタデータ） (2024-12-06T18:14:24Z)
• OpenCoder: The Open Cookbook for Top-Tier Code Large Language Models [70.72097493954067]
  コードのための大規模言語モデル(LLM)は、コード生成、推論タスク、エージェントシステムなど、さまざまな領域で必須になっている。 オープンアクセスのコード LLM はプロプライエタリなモデルの性能レベルに近づきつつあるが、高品質なコード LLM は依然として限られている。 トップクラスのコードLLMであるOpenCoderは、主要なモデルに匹敵するパフォーマンスを達成するだけでなく、研究コミュニティの"オープンクックブック"としても機能します。
  論文  参考訳（メタデータ） (2024-11-07T17:47:25Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• 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)

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

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