@inproceedings{cao-etal-2025-informal,
    title = "From Informal to Formal {--} Incorporating and Evaluating {LLM}s on Natural Language Requirements to Verifiable Formal Proofs",
    author = "Cao, Jialun  and
      Lu, Yaojie  and
      Li, Meiziniu  and
      Ma, Haoyang  and
      Li, Haokun  and
      He, Mengda  and
      Wen, Cheng  and
      Sun, Le  and
      Zhang, Hongyu  and
      Qin, Shengchao  and
      Cheung, Shing-Chi  and
      Tian, Cong",
    editor = "Che, Wanxiang  and
      Nabende, Joyce  and
      Shutova, Ekaterina  and
      Pilehvar, Mohammad Taher",
    booktitle = "Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)",
    month = jul,
    year = "2025",
    address = "Vienna, Austria",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingestion-acl-25/2025.acl-long.1310/",
    pages = "26984--27003",
    ISBN = "979-8-89176-251-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. However, these studies intertwined multiple skills simultaneously{---}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 breaks it down into sub-tasks. We constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages (Coq, Lean4, Dafny, ACSL, and TLA+) in six tasks by distilling gpt-4o and evaluated against ten open-sourced LLMs, including recent popular DeepSeek-R1. 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. And interestingly, we observed that fine-tuning with formal data also enhances abilities in mathematics, reasoning, and coding. We hope our findings inspire further research."
}