A Neurosymbolic Approach to Natural Language Formalization and Verification

• URL: http://arxiv.org/abs/2511.09008v1
• Date: Thu, 13 Nov 2025 01:25:51 GMT
• Title: A Neurosymbolic Approach to Natural Language Formalization and Verification
• Authors: Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Marc Hudak, Dejan Jovanović, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamarić, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, Jianan Yao,
• Abstract summary: Large Language Models perform well at natural language interpretation and reasoning, but their inherentity limits their adoption in regulated industries like finance and healthcare.<n>We present a two-stage neurosymbolic framework that uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process.<n>Our benchmarks demonstrate that our approach exceeds 99% soundness, indicating a near-zero false positive rate in identifying logical validity.
• Score: 4.697939947463767
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large Language Models perform well at natural language interpretation and reasoning, but their inherent stochasticity limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we present a two-stage neurosymbolic framework 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. When correctness is paramount, we perform multiple redundant formalization steps at inference time, cross checking the formalizations for semantic equivalence. Our benchmarks demonstrate that our approach exceeds 99% soundness, indicating a near-zero false positive rate in identifying logical validity. Our approach produces auditable logical artifacts that substantiate the verification outcomes and can be used to improve the original text.

Related papers

• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• Structured Decomposition for LLM Reasoning: Cross-Domain Validation and Semantic Web Integration [0.0]
  Rule-based reasoning arises in domains where decisions must be auditable and justifiable.<n>Applying rules to such inputs demands both interpretive flexibility and formal guarantees.<n>This paper presents an integration pattern that combines these strengths.
  arXiv  Detail & Related papers  (2026-01-04T17:19:20Z)
• Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
  Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models.<n>This paper explores the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements.<n>Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs.
  arXiv  Detail & Related papers  (2025-11-14T19:45:17Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like reasoning: efficiency.<n>We propose a framework for assessing LM reasoning efficiency through the lens of logic programming.
  arXiv  Detail & Related papers  (2025-10-29T15:30:31Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Explainable Rule Application via Structured Prompting: A Neural-Symbolic Approach [0.0]
  Large Language Models (LLMs) excel in complex reasoning tasks but struggle with consistent rule application, exception handling, and explainability.<n>This paper introduces a structured prompting framework that decomposes reasoning into three verifiable steps: entity identification, property extraction, and symbolic rule application.
  arXiv  Detail & Related papers  (2025-06-19T14:14:01Z)
• Learning to Reason via Mixture-of-Thought for Logical Reasoning [56.24256916896427]
  Mixture-of-Thought (MoT) is a framework that enables LLMs to reason across three complementary modalities: natural language, code, and truth-table.<n>MoT adopts a two-phase design: (1) self-evolving MoT training, which jointly learns from filtered, self-generated rationales across modalities; and (2) MoT inference, which fully leverages the synergy of three modalities to produce better predictions.
  arXiv  Detail & Related papers  (2025-05-21T17:59:54Z)
• Mitigating Content Effects on Reasoning in Language Models through Fine-Grained Activation Steering [14.298418197820912]
  Large language models (LLMs) frequently demonstrate reasoning limitations, often conflating content plausibility with logical validity.<n>This can result in biased inferences, where plausible arguments are incorrectly deemed logically valid or vice versa.<n>This paper investigates the problem of mitigating content biases on formal reasoning through activation steering.
  arXiv  Detail & Related papers  (2025-05-18T01:34:34Z)
• PEIRCE: Unifying Material and Formal Reasoning via LLM-Driven Neuro-Symbolic Refinement [13.042323420379187]
  PEIRCE is a neuro-symbolic framework designed to unify material and formal inference through an iterative conjecture-criticism process.<n>We demonstrate its capabilities in the domain of natural language explanation generation.
  arXiv  Detail & Related papers  (2025-04-05T09:04:47Z)
• Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection [44.31755414036022]
  We introduce Natural Language to First-Order Logic (NL2FOL), a framework to autoformalize natural language to FOL step by step using Large Language Models (LLMs)<n>Our approach addresses key challenges in this translation process, including the integration of implicit background knowledge.<n>Being neurosymbolic, our approach also provides interpretable insights into the reasoning process and demonstrates robustness without requiring model fine-tuning or labeled training data.
  arXiv  Detail & Related papers  (2024-04-18T00:20:48Z)
• Language Models as Inductive Reasoners [125.99461874008703]
  We propose a new paradigm (task) for inductive reasoning, which is to induce natural language rules from natural language facts. We create a dataset termed DEER containing 1.2k rule-fact pairs for the task, where rules and facts are written in natural language. We provide the first and comprehensive analysis of how well pretrained language models can induce natural language rules from natural language facts.
  arXiv  Detail & Related papers  (2022-12-21T11:12:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.