論文の概要: From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

• arxiv url: http://arxiv.org/abs/2501.16207v1
• Date: Mon, 27 Jan 2025 17:00:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-28 13:56:57.689493
• Title: From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
• Title（参考訳）: インフォーマルからフォーマルへ-自然言語要求のLLMの導入と評価から検証可能な形式証明へ
• Authors: Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian,
• Abstract要約: 本稿では,形式的推論の即時適用シナリオである形式的検証に注目し,それを6つのサブタスクに分解する。 我々は5つの主流形式仕様言語に18kの高品質な命令応答ペアを構築した。 LLMは、コードまたは証明手順の詳細な記述が与えられたときに、証明セグメントを書くのに長けていることがわかりました。
• 参考スコア（独自算出の注目度）: 25.69931278771869
• License:
• Abstract: The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO, showing significant progress. However, these studies intertwined multiple skills simultaneously, i.e., problem-solving, reasoning, and writing formal specifications, making it hard to precisely identify the LLMs' strengths and weaknesses in each task. This paper focuses on formal verification, an immediate application scenario of formal reasoning, and decomposes it into six sub-tasks. We constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages (Coq, Lean4, Dafny, ACSL, and TLA+) in six formal-verification-related tasks by distilling GPT-4o. They are split into a 14k+ fine-tuning dataset FM-alpaca and a 4k benchmark FM-Bench. We found that LLMs are good at writing proof segments when given either the code, or the detailed description of proof steps. Also, the fine-tuning brought about a nearly threefold improvement at most. Interestingly, we observed that fine-tuning with formal data also enhances mathematics, reasoning, and coding abilities. We hope our findings inspire further research. Fine-tuned models are released to facilitate subsequent studies
• Abstract（参考訳）: AIに基づく公式な数学的推論の研究は、持続不可能な成長傾向を示している。 これらの研究は、IMOのような数学の競争に優れており、大きな進歩を見せている。 しかしながら、これらの研究は複数のスキル、すなわち問題解決、推論、形式仕様の作成を同時に行うことで、各タスクにおけるLSMの長所と短所を正確に識別することが困難になった。 本稿では,形式的推論の即時適用シナリオである形式的検証に注目し,それを6つのサブタスクに分解する。 GPT-4oを蒸留することにより,5つの主要な形式仕様言語(Coq,Lean4,Dafny,ACSL,TLA+)で18kの高品質な命令応答対を構築した。 14k以上の微調整データセットFM-alpacaと4kベンチマークFM-Benchに分けられる。 LLMは、コードまたは証明手順の詳細な記述が与えられたときに、証明セグメントを書くのに長けていることがわかりました。 また、微調整によって、最大で3倍近い改善がもたらされた。 興味深いことに、フォーマルなデータによる微調整は数学、推論、コーディング能力を向上させる。 我々の発見がさらなる研究のきっかけになることを願っている。 微調整モデルがリリースされ、その後の研究が促進される

関連論文リスト

• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
  本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。 英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
  論文  参考訳（メタデータ） (2024-08-28T06:33:03Z)
• LokiLM: Technical Report [0.0]
  500Bトークンでトレーニングされた1.4Bパラメータ大言語モデルであるLokiLMを紹介する。 LokiLMは1.5B以下のパラメータを持つモデル間で最先端のパフォーマンスを実現する。 その有望なパフォーマンスにもかかわらず、LokiLMは、TruthfulQAベンチマークにおいて、必要な量の幻覚とスコアを示しています。
  論文  参考訳（メタデータ） (2024-07-10T05:05:47Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Orca: Progressive Learning from Complex Explanation Traces of GPT-4 [22.526048553548726]
  我々は, LFMの推論過程を模倣する13ビリオンパラメータモデルOrcaを開発した。 Orcaは、説明トレース、ステップバイステップの思考プロセス、その他の複雑な命令を含む、GPT-4から豊富な信号から学習する。 Orcaは、複雑なゼロショット推論ベンチマークにおいて、Vicuna-13Bのような最先端の命令チューニングモデルを100%以上上回る。
  論文  参考訳（メタデータ） (2023-06-05T08:58:39Z)
• Knowledge-Augmented Reasoning Distillation for Small Language Models in Knowledge-Intensive Tasks [90.11273439036455]
  大規模言語モデル(LLM)は知識集約推論タスクにおいて有望なパフォーマンスを示している。 外部知識ベースから得られた知識を付加したLPMから理性を生成するための,小型LMを微調整する新しい手法であるKARDを提案する。 我々は,KARDが知識集約型推論データセットにおいて,小さなT5モデルとGPTモデルの性能を著しく向上させることを示す。
  論文  参考訳（メタデータ） (2023-05-28T13:00:00Z)

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

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