論文の概要: Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques

• arxiv url: http://arxiv.org/abs/2502.03321v1
• Date: Wed, 05 Feb 2025 16:21:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-06 14:26:43.545746
• Title: Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
• Title（参考訳）: ChatGPTと基本探索技術を用いた形式証明モデルの簡易化
• Authors: Sangjun Han, Taeil Hur, Youngmi Hur, Kathy Sangkyung Lee, Myungyoon Lee, Hyojae Lim,
• Abstract要約: 本稿では,ChatGPTと基本探索技術を統合し,形式的証明の簡易化について検討する。 私たちはChatGPTのような大きな言語モデルとLeanのような形式的な言語を組み合わせることで、検証可能なメリットが加わり、形式的な証明生成の効率性とアクセシビリティが向上することを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: The challenge of formal proof generation has a rich history, but with modern techniques, we may finally be at the stage of making actual progress in real-life mathematical problems. This paper explores the integration of ChatGPT and basic searching techniques to simplify generating formal proofs, with a particular focus on the miniF2F dataset. We demonstrate how combining a large language model like ChatGPT with a formal language such as Lean, which has the added advantage of being verifiable, enhances the efficiency and accessibility of formal proof generation. Despite its simplicity, our best-performing Lean-based model surpasses all known benchmarks with a 31.15% pass rate. We extend our experiments to include other datasets and employ alternative language models, showcasing our models' comparable performance in diverse settings and allowing for a more nuanced analysis of our results. Our findings offer insights into AI-assisted formal proof generation, suggesting a promising direction for future research in formal mathematical proof.
• Abstract（参考訳）: 形式的証明生成の課題には、豊富な歴史があるが、現代の技術では、我々は最終的に現実の数学的問題において実際に進歩する段階にあるかもしれない。 本稿では,ChatGPTと基本探索技術を統合し,形式的証明の生成を簡略化し,特にMiniF2Fデータセットに着目した。 私たちはChatGPTのような大きな言語モデルとLeanのような形式的な言語を組み合わせることで、検証可能なメリットが加わり、形式的な証明生成の効率性とアクセシビリティが向上することを示す。 その単純さにもかかわらず、最高のパフォーマンスのLeanベースのモデルは、既知のすべてのベンチマークを31.15%パスレートで上回ります。 実験を他のデータセットを含むように拡張し、代替言語モデルを採用し、さまざまな設定でモデルに匹敵するパフォーマンスを示し、結果のより微妙な分析を可能にします。 本研究は,AIによる形式的証明生成に関する知見を提供し,形式的数学的証明における今後の研究の方向性を示唆するものである。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Retrieval is Accurate Generation [99.24267226311157]
  本稿では,支援文書の集合からコンテキスト認識句を選択する新しい手法を提案する。 本モデルでは,検索対象のベースラインの中で,最高の性能と低レイテンシを実現する。
  論文  参考訳（メタデータ） (2024-02-27T14:16:19Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• A Multi-Level Attention Model for Evidence-Based Fact Checking [58.95413968110558]
  シーケンス構造をトレーニング可能な,シンプルなモデルを提案する。 Fact extract and VERification のための大規模データセットの結果、我々のモデルはグラフベースのアプローチよりも優れていることが示された。
  論文  参考訳（メタデータ） (2021-06-02T05:40:12Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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