AI RESEARCH
Automated Formalization via Conceptual Retrieval-Augmented LLMs
arXiv CS.AI
•
ArXi:2508.06931v2 Announce Type: replace Interactive theorem provers (ITPs) require manual formalization, which is labor-intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hallucination (e.g., undefined predicates, symbol misuse, and version incompatibility) and the semantic gap caused by ambiguous or missing premises in natural language descriptions. To address these issues, we propose CRAMF, a Concept-driven Retrieval-Augmented Mathematical Formalization framework.