mlsanityData to 7 Oct 2026

A Neurosymbolic Approach to Natural Language Formalization and Verification

arXiv 2511.09008 ↗First posted 12 Nov 2025cs.CL cs.AI cs.LGcited by 8

Not on the map. Why?

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.

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

Builds on

31 of 47 references.

References · 31

  1. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  2. 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,160
  3. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,155
  4. 2023SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Modelscited by 787
  5. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 379
  6. 2024Hallucination is Inevitable: An Innate Limitation of Large Language Modelscited by 329
  7. 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 309
  8. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  9. 2022Autoformalization with Large Language Modelscited by 252
  10. 2024MiniCheck: Efficient Fact-Checking of LLMs on Grounding Documentscited by 251
  11. 2022FOLIO: Natural Language Reasoning with First-Order Logiccited by 233
  12. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
19 more
  1. 2024Same Task, More Tokens: the Impact of Input Length on the Reasoning Performance of Large Language Modelscited by 150
  2. 2023SatLM: Satisfiability-Aided Language Models Using Declarative Promptingcited by 100
  3. 2024Faithful Logical Reasoning via Symbolic Chain-of-Thoughtcited by 99
  4. 2023Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkerscited by 86
  5. 2023Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Textcited by 59
  6. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 52
  7. 2025The FACTS Grounding Leaderboard: Benchmarking LLMs' Ability to Ground Responses to Long-Form Inputcited by 49
  8. 2024The Ethics of ChatGPT in Medicine and Healthcare: A Systematic Review on Large Language Models (LLMs)cited by 45
  9. 2023Leveraging Large Language Models to Generate Answer Set Programscited by 33
  10. 2021ConditionalQA: A Complex Reading Comprehension Dataset with Conditional Answerscited by 29
  11. 2024Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoningcited by 27
  12. 2024Logic-of-Thought: Injecting Logic into Contexts for Full Reasoning in Large Language Modelscited by 23
  13. 2025Cats Confuse Reasoning LLM: Query Agnostic Adversarial Triggers for Reasoning Modelscited by 23
  14. 2021Catala: A Programming Language for the Lawcited by 18
  15. 2024Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoningcited by 17
  16. 2024NLP Verification: Towards a General Methodology for Certifying Robustnesscited by 14
  17. 2025VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoningcited by 12
  18. 2024HYBRIDMIND: Meta Selection of Natural Language and Symbolic Language for Enhanced LLM Reasoningcited by 11
  19. 2022Interactive configurator with FO(.) and IDP-Z3cited by 2

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 1; 2026: 7.

8 papers.

  1. 2025VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generationcited by 4
  2. 2026Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verificationcited by 4
  3. 2026MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agentscited by 3
  4. 2026FregeLogic at SemEval 2026 Task 11: A Hybrid Neuro-Symbolic Architecture for Content-Robust Syllogistic Validity Predictioncited by 1
  5. 2026LLMs + Security = Troublecited by 0
  6. 2026Neurosymbolic Auditing of Natural-Language Software Requirementscited by 0
  7. 2026Managing Uncertainty in LLM-Generated Procedural Knowledge for Virtual Laboratory Planningcited by 0
  8. 2026Verifiable Checks for Business Rule Consistencycited by 0