Agentic Geometry Problem Solving via Human-like Parallel Bidirectional Reasoning

Formal Geometric Problem Solving requires every step of reasoning within a strict logical framework, and has been a core challenge in artificial intelligence. This paper presents a unified neuro-symbolic reasoning framework, named Reflect Agent Verified Solve (RAVS), which deeply integrates large language models, agent architectures, and formal symbolic solvers. The core innovations of RAVS lie in two parts. First, we propose a role-separated neuro-symbolic collaboration mechanism: the LLM serves as a planner responsible for high-level semantic understanding and path reflection, while the symbolic solver acts as an executor responsible for formal verification and rigorous theorem application. The neural reasoning capability of the LLM and the logical completeness of the symbolic system complement each other, fundamentally eliminating the risk of hallucinations. Second, we construct the first bidirectional symbolic reasoning engine that fully unifies forward and backward solving. For each theorem, we define two reversible operations: forward application and backward decomposition. We further provide a theoretical analysis that bidirectional reasoning achieves an exponential complexity advantage over unidirectional reasoning. Together, these two mechanisms form an iterative closed loop between neural planning and symbolic execution. On the FormalGeo7K benchmark, RAVS achieves a 95.8% solving accuracy, substantially outperforming existing state-of-the-art methods, without requiring any additional problem-specific annotated data.