From Informal to Formal — Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

要約

AIベースの正式な数学的推論の研究では、止められない成長傾向が示されています。
これらの研究は、IMOのような数学的競争に優れており、大きな進歩を示しています。
ただし、これらの研究は、複数のスキルを同時に絡み合っています。つまり、問題解決、推論、正式な仕様の作成により、各タスクのLLMSの長所と短所を正確に特定することを困難にしました。
このペーパーでは、正式な検証、正式な推論の即時のアプリケーションシナリオに焦点を当て、6つのサブタスクに分解します。
GPT-4Oを蒸留することにより、6つの正式な検証関連のタスクで、5つの主流の正式な仕様言語（COQ、LEAN4、DAFNY、ACSL、およびTLA+）に18K高品質の命令応答ペアを構築しました。
それらは、14K+微調整データセットFM-ALPACAと4KベンチマークFMベンチに分割されます。
LLMは、コードまたは証明手順の詳細な説明が与えられた場合、証明セグメントを作成するのが得意であることがわかりました。
また、微調整はせいぜい3倍近くの改善をもたらしました。
興味深いことに、正式なデータで微調整すると数学、推論、コーディング能力が向上することが観察されました。
私たちの調査結果がさらなる研究を促すことを願っています。
微調整されたモデルは、その後の研究を促進するためにリリースされます

要約(オリジナル)

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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google