論文の概要: From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
- arxiv url: http://arxiv.org/abs/2501.16207v3
- Date: Wed, 05 Mar 2025 15:26:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-03-06 17:18:40.410215
- 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要約: 本稿では,形式的推論の即時適用シナリオである形式的検証に焦点を当てる。
我々は5つの形式仕様言語で18kの高品質な命令応答ペアを構築した。
フォーマルなデータによる微調整は、数学、推論、コーディング能力も強化する。
- 参考スコア（独自算出の注目度）: 25.69931278771869
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made significant progress. This paper focuses on formal verification, an immediate application scenario of formal reasoning, and breaks it down into sub-tasks. We constructed 18k high-quality instruction-response pairs across five formal specification languages (Coq, Lean4, Dafny, ACSL, and TLA+) by distilling gpt-4o and evaluated against ten open-sourced LLMs, including recent popular DeepSeek-R1. We also fine-tuned several 7~8B small models to achieve comparable performance with Deepseek-R1-671B. Interestingly, we observed that fine-tuning with formal data also enhances mathematics, reasoning, and coding capabilities. Fine-tuned models are released at https: //huggingface.co/fm-universe.
- Abstract（参考訳）: AIに基づく公式な数学的推論の研究は、持続不可能な成長傾向を示している。
これらの研究は、IMOのような数学の競争に優れており、大きな進歩を遂げている。
本稿では,形式的推論の即時適用シナリオである形式的検証に注目し,それをサブタスクに分解する。
我々はgpt-4oを蒸留することにより,5つの形式仕様言語(Coq,Lean4,Dafny,ACSL,TLA+)で18kの高品質な命令応答ペアを構築し,最近普及しているDeepSeek-R1を含む10のオープンソースLLMに対して評価を行った。
また、Deepseek-R1-671Bで同等のパフォーマンスを達成するために、いくつかの7～8Bの小型モデルを微調整しました。
興味深いことに、フォーマルなデータによる微調整は数学、推論、コーディング能力を向上させる。
微調整されたモデルはhttps: //huggingface.co/fm-universeでリリースされる。
関連論文リスト
- Phi-4-Mini-Reasoning: Exploring the Limits of Small Reasoning Language Models in Math [135.1260782461186]
CoT(Chain-of-Thought)は大規模言語モデル(LLM)の形式推論能力を著しく向上させる
しかし、Small Language Models (SLM) における推論の改善は、モデル能力が限られているため、依然として困難である。
本研究では,(1)多種多様な蒸留長CoTデータによる大規模中等教育,(2)高品質長CoTデータによる微調整,(3)厳格な選好データセットを活用したロールアウトDPO,(4)検証リワードを用いた強化学習(RL)の4段階からなるSLMの体系的トレーニングレシピを提案する。
論文 参考訳（メタデータ） (2025-04-30T00:04:35Z) - Leanabell-Prover: Posttraining Scaling in Formal Reasoning [26.534511088861446]
本稿では, 自然言語の推論モデルにおけるブレークスルーと整合性を持たせることを目的として, ATPのポストトレーニング全体について検討する。
我々は,DeepSeek-Prover-v1.5やGoedel-Proverなど,既存のフォーマルプロバーの改良に成功した。
論文 参考訳（メタデータ） (2025-04-08T15:15:26Z) - MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving [30.112351299773632]
State-of-the-artメソッドは、単一の大規模言語モデル(LLM)をエージェントまたはプロバーとして使用し、完全な証明を生成するか、ツリー検索を実行する。
マルチエージェントリーンベースのLong Chain-of-ProverフレームワークであるMA-LoTを提案する。
我々のフレームワークはMiniF2F-TestデータセットのLean4バージョンで61.07%の精度を実現している。
論文 参考訳（メタデータ） (2025-03-05T05:50:31Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。
英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
論文 参考訳（メタデータ） (2024-08-28T06:33:03Z) - TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。
我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
論文 参考訳（メタデータ） (2024-07-03T15:36:18Z) - 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) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。