Let Solvers Reason and Models Understand: Proof-Obligation-Guided Bridging

Neuro-symbolic approaches aim to combine the flexible language understanding of neural models with the rigorous reasoning of symbolic solvers. These approaches typically use a large language model (LLM) to translate the problem expressed in natural language (NL) into formal representations and a symbolic solver to reason over these representations. However, even when individual NL statements are faithfully formalized, their semantically related expressions may still be mapped to symbolically unrelated predicates, leading to failures in downstream symbolic reasoning. To overcome this challenge, we propose Proof-Obligation-Guided Bridging (POGB). During autoformalization, POGB maintains a grounding table that records the NL semantic grounding for each formal element. When the solver encounters an unresolved proof obligation, POGB identifies candidate semantic bridges and uses an LLM to evaluate them against the recorded grounding information, thereby recovering semantic relations missing from the formal representations. This design keeps all logical reasoning under the solver's control while restricting the LLM's role to autoformalization and the evaluation of candidate semantic bridges. By letting solvers reason and models understand, POGB leverages their complementary strengths to advance neuro-symbolic integration. Theoretical analysis proves the soundness of POGB, and extensive experiments on diverse logical reasoning benchmarks demonstrate its superior performance.