3 papers
cs.AI2024
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
Xiaohan Lin, Qingxing Cao, Yinya Huang +5
Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs). However, current formal verificati…
cs.CL2024
Process-Driven Autoformalization in Lean 4
Jianqiao Lu, Yingjia Wan, Zhengying Liu +10
Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing effort…
cs.AI2024
Proving Theorems Recursively
Haiming Wang, Huajian Xin, Zhengying Liu +8
Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually base…