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 SemanticPref, 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[<https://github.com/sysulic/PrefRAG>].Extensive evaluations across both in-distribution (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.