# A Neurosymbolic Approach to Natural Language Formalization and Verification

arXiv: https://arxiv.org/abs/2511.09008 · HTML: https://mlsanity.com/paper/2511.09008/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 47 references that are in the map.
- First posted on arXiv 12 Nov 2025.

## Builds on (most cited first, 30 of 31)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Models](https://mlsanity.com/paper/2303.08896/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Hallucination is Inevitable: An Innate Limitation of Large Language Models](https://mlsanity.com/paper/2401.11817/) (2024)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [MiniCheck: Efficient Fact-Checking of LLMs on Grounding Documents](https://mlsanity.com/paper/2404.10774/) (2024)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Same Task, More Tokens: the Impact of Input Length on the Reasoning Performance of Large Language Models](https://mlsanity.com/paper/2402.14848/) (2024)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers](https://mlsanity.com/paper/2311.09000/) (2023)
- [Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text](https://mlsanity.com/paper/2307.07696/) (2023)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [The FACTS Grounding Leaderboard: Benchmarking LLMs' Ability to Ground Responses to Long-Form Input](https://mlsanity.com/paper/2501.03200/) (2025)
- [The Ethics of ChatGPT in Medicine and Healthcare: A Systematic Review on Large Language Models (LLMs)](https://mlsanity.com/paper/2403.14473/) (2024)
- [Leveraging Large Language Models to Generate Answer Set Programs](https://mlsanity.com/paper/2307.07699/) (2023)
- [ConditionalQA: A Complex Reading Comprehension Dataset with Conditional Answers](https://mlsanity.com/paper/2110.06884/) (2021)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [Logic-of-Thought: Injecting Logic into Contexts for Full Reasoning in Large Language Models](https://mlsanity.com/paper/2409.17539/) (2024)
- [Cats Confuse Reasoning LLM: Query Agnostic Adversarial Triggers for Reasoning Models](https://mlsanity.com/paper/2503.01781/) (2025)
- [Catala: A Programming Language for the Law](https://mlsanity.com/paper/2103.03198/) (2021)
- [Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning](https://mlsanity.com/paper/2409.17270/) (2024)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoning](https://mlsanity.com/paper/2501.14540/) (2025)
- [HYBRIDMIND: Meta Selection of Natural Language and Symbolic Language for Enhanced LLM Reasoning](https://mlsanity.com/paper/2409.19381/) (2024)

## Built on by (most cited first, 9 of 9)

- [VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generation](https://mlsanity.com/paper/2512.14744/) (2025)
- [Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification](https://mlsanity.com/paper/2602.24111/) (2026)
- [MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents](https://mlsanity.com/paper/2605.06334/) (2026)
- [FregeLogic at SemEval 2026 Task 11: A Hybrid Neuro-Symbolic Architecture for Content-Robust Syllogistic Validity Prediction](https://mlsanity.com/paper/2604.18328/) (2026)
- [LLMs + Security = Trouble](https://mlsanity.com/paper/2602.08422/) (2026)
- [Neurosymbolic Auditing of Natural-Language Software Requirements](https://mlsanity.com/paper/2605.13817/) (2026)
- [Managing Uncertainty in LLM-Generated Procedural Knowledge for Virtual Laboratory Planning](https://mlsanity.com/paper/2605.26333/) (2026)
- [Verifiable Checks for Business Rule Consistency](https://mlsanity.com/paper/2608.00396/) (2026)
- [MENTOR: Procedural Shielding of Tool-Using LLM Agents](https://mlsanity.com/paper/2610.17039/) (2026)

## Abstract (arXiv)

Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and health-care that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc): a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. ARc performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.