論文の概要: 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倍近い改善がもたらされた。 興味深いことに、フォーマルなデータによる微調整は数学、推論、コーディング能力を向上させる。 我々の発見がさらなる研究のきっかけになることを願っている。 微調整モデルがリリースされ、その後の研究が促進される

関連論文リスト

• 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)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
  大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
  論文  参考訳（メタデータ） (2024-06-06T08:25:43Z)
• 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)
• Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization [45.439933713342256]
  大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。 LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。 これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
  論文  参考訳（メタデータ） (2024-03-26T22:01:13Z)
• Direct Evaluation of Chain-of-Thought in Multi-hop Reasoning with Knowledge Graphs [52.42505579545893]
  大規模言語モデル(LLM)は、回答とともにチェーン・オブ・シントの説明を生成するよう促されたとき、強い推論能力を示す。 本稿では,LLMの推論知識と生成したCoTの精度を評価するために,新しい識別的・生成的CoT評価パラダイムを提案する。
  論文  参考訳（メタデータ） (2024-02-17T05:22:56Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• TAT-LLM: A Specialized Language Model for Discrete Reasoning over Tabular and Textual Data [73.29220562541204]
  我々は,言語モデル(LLM)の驚くべきパワーを活用して課題を解決することを検討する。 LLaMA2を微調整し,既存のエキスパートアノテートデータセットから自動生成したトレーニングデータを用いてTAT-LLM言語モデルを開発する。
  論文  参考訳（メタデータ） (2024-01-24T04:28:50Z)

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

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