From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912418578300928 |
|---|---|
| author | Cao, Jialun Lu, Yaojie Li, Meiziniu Ma, Haoyang Li, Haokun He, Mengda Wen, Cheng Sun, Le Zhang, Hongyu Qin, Shengchao Cheung, Shing-Chi Tian, Cong |
| author_facet | Cao, Jialun Lu, Yaojie Li, Meiziniu Ma, Haoyang Li, Haokun He, Mengda Wen, Cheng Sun, Le Zhang, Hongyu Qin, Shengchao Cheung, Shing-Chi Tian, Cong |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_16207 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs Cao, Jialun Lu, Yaojie Li, Meiziniu Ma, Haoyang Li, Haokun He, Mengda Wen, Cheng Sun, Le Zhang, Hongyu Qin, Shengchao Cheung, Shing-Chi Tian, Cong Artificial Intelligence Computation and Language Programming Languages 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. |
| title | From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs |
| topic | Artificial Intelligence Computation and Language Programming Languages |
| url | https://arxiv.org/abs/2501.16207 |