Papers by Mengda He
From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs (2025.acl-long)
Copied to clipboard
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
| Challenge: | Recent studies in formal mathematical reasoning have shown an unstoppable growth trend. |
| Approach: | They constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages and evaluated them against ten open-sourced LLMs. |
| Outcome: | The proposed model compared instruction-response pairs across five formal specification languages and found that the LLMs were good at writing proof segments when given either the code, or the detailed description of proof steps. |