@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://aclanthology.org/2026.findings-acl.795/",
doi = "10.18653/v1/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."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="zhou-liu-2026-prefrag">
<titleInfo>
<title>PrefRAG: Correcting Semantic Errors in Auto-Formalization for Logical Reasoning with Program Preference RAG</title>
</titleInfo>
<name type="personal">
<namePart type="given">Yuyin</namePart>
<namePart type="family">Zhou</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Yongmei</namePart>
<namePart type="family">Liu</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-07</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Findings of the Association for Computational Linguistics: ACL 2026</title>
</titleInfo>
<name type="personal">
<namePart type="given">Maria</namePart>
<namePart type="family">Liakata</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Viviane</namePart>
<namePart type="given">P</namePart>
<namePart type="family">Moreira</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jiajun</namePart>
<namePart type="family">Zhang</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">David</namePart>
<namePart type="family">Jurgens</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">San Diego, California, United States</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-395-1</identifier>
</relatedItem>
<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 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[\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.</abstract>
<identifier type="citekey">zhou-liu-2026-prefrag</identifier>
<identifier type="doi">10.18653/v1/2026.findings-acl.795</identifier>
<location>
<url>https://aclanthology.org/2026.findings-acl.795/</url>
</location>
<part>
<date>2026-07</date>
<extent unit="page">
<start>16193</start>
<end>16208</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T PrefRAG: Correcting Semantic Errors in Auto-Formalization for Logical Reasoning with Program Preference RAG
%A Zhou, Yuyin
%A Liu, Yongmei
%Y Liakata, Maria
%Y Moreira, Viviane P.
%Y Zhang, Jiajun
%Y Jurgens, David
%S Findings of the Association for Computational Linguistics: ACL 2026
%D 2026
%8 July
%I Association for Computational Linguistics
%C San Diego, California, United States
%@ 979-8-89176-395-1
%F zhou-liu-2026-prefrag
%X 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[\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.
%R 10.18653/v1/2026.findings-acl.795
%U https://aclanthology.org/2026.findings-acl.795/
%U https://doi.org/10.18653/v1/2026.findings-acl.795
%P 16193-16208
Markdown (Informal)
[PrefRAG: Correcting Semantic Errors in Auto-Formalization for Logical Reasoning with Program Preference RAG](https://aclanthology.org/2026.findings-acl.795/) (Zhou & Liu, Findings 2026)
ACL