@inproceedings{zhou-liu-2026-prefrag,
    title = "{P}ref{RAG}: Correcting Semantic Errors in Auto-Formalization for Logical Reasoning with Program Preference {RAG}",
    author = "Zhou, Yuyin  and
      Liu, Yongmei",
    editor = "Liakata, Maria  and
      Moreira, Viviane P.  and
      Zhang, Jiajun  and
      Jurgens, David",
    booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {ACL} 2026",
    month = jul,
    year = "2026",
    address = "San Diego, California, United States",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-acl-workshops/2026.findings-acl.795/",
    pages = "16193--16208",
    ISBN = "979-8-89176-395-1",
    abstract = "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 \textbf{SemanticPref}, a program preference dataset to model these patterns. Using the dataset as the knowledge base, we introduce \textbf{PrefRAG}, a general RAG framework for refinement in auto-formalization, which enables LLMs to detect and repair syntactic and semantic errors[{\ensuremath{<}}https://github.com/sysulic/PrefRAG{\ensuremath{>}}].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."
}