PrefRAG: Correcting Semantic Errors in Auto-Formalization for Logical Reasoning with Program Preference RAG

Recent advances in large language models (LLMs) have spurred interest in neuro-symbolic methods for logical reasoning based on auto-formalization, where LLMs first formalize problems into symbolic programs, for solvers to perform reasoning over. However, existing auto-formalization methods remain prone to both syntactic and semantic errors. Specifically, the absence of a program-level semantic verification mechanism leaves semantic errors largely unaddressed. In this paper, we propose a novel approach to semantic error correction via program preference retrieval-augmented generation (RAG). First, we conduct an in-depth analysis of semantic error patterns, and then automatically synthesize Seman-ticPref, a program preference dataset to model these patterns. Using the dataset as the knowledge base, we introduce PrefRAG, a general RAG framework for refinement in auto-formalization, which enables LLMs to detect and repair syntactic and semantic errors 1 . Extensive evaluations across both indistribution (ID) benchmarks (i.e., AR-LSAT and FOLIO) and out-of-distribution (OOD) datasets show that PrefRAG consistently outperforms strong baselines, achieving an average accuracy improvement of 2.39% on ID and 6.23% on OOD datasets.