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

要約

AIベースの正式な数学的推論の研究では、止められない成長傾向が示されています。
これらの研究は、IMOのような数学的競争に優れており、大きな進歩を遂げています。
このペーパーでは、正式な検証、正式な推論の即時アプリケーションシナリオに焦点を当て、それをサブタスクに分割します。
GPT-4Oを蒸留し、最近の人気のあるDeepseek-R1を含む10のオープンソースLLMSに対して評価された5つの正式な仕様言語（COQ、LEAN4、DAFNY、ACSL、およびTLA+）にわたって18K高品質の命令応答ペアを構築しました。
また、DeepSeek-R1-671Bで同等のパフォーマンスを実現するために、いくつかの7〜8Bの小さなモデルを微調整しました。
興味深いことに、正式なデータで微調整すると数学、推論、コーディング機能が強化されることが観察されました。
微調整されたモデルは、https：//huggingface.co/fm-universeでリリースされます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google