Yutong Cheng


2026

Automated reasoning is critical in domains such as law and governance, where verifying claims against facts in documents requires both accuracy and interpretability.Recent work has adopted a structured reasoning paradigm that parses first-order logic (FOL) rules from natural language and delegates inference to automated solvers.With the rise of large language models (LLMs), methods such as GCD and CODE4LOGIC leverage their reasoning and code generation capabilities to enhance logic parsing.However, these approaches suffer from (1) fragile syntax control, due to weak enforcement of global grammar consistency, and (2) low semantic faithfulness, as they lack fine-grained clause-level semantic understanding.To address these challenges, we propose , a FOL translation framework that uses an AST as an intermediate layer, combining a recursive LLM-based semantic parser with an AST-guided generator that deterministically produces solver-ready code.On the FOLIO, LogicNLI, and ProofWriter benchmarks, attains 99% syntactic accuracy and improves semantic correctness by 30% over state-of-the-art baselines.Moreover, integrating into Logic-LM yields near-perfect executability and improves downstream reasoning accuracy by ~31% over Logic-LM’s original few-shot unconstrained FOL translation module.