A Neurosymbolic Approach to Natural Language Formalization and Verification
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.
Keywords
Cite
@article{arxiv.2511.09008,
title = {A Neurosymbolic Approach to Natural Language Formalization and Verification},
author = {Sam Bayless and Stefano Buliani and Darion Cassel and Byron Cook and Duncan Clough and Rémi Delmas and Nafi Diallo and Ferhat Erata and Nick Feng and Dimitra Giannakopoulou and Aman Goel and Aditya Gokhale and Joe Hendrix and Marc Hudak and Dejan Jovanović and Andrew M. Kent and Benjamin Kiesl-Reiter and Jeffrey J. Kuna and Nadia Labai and Joseph Lilien and Divya Raghunathan and Zvonimir Rakamarić and Niloofar Razavi and Michael Tautschnig and Ali Torkamani and Nathaniel Weir and Michael W. Whalen and Jianan Yao},
journal= {arXiv preprint arXiv:2511.09008},
year = {2025}
}
Comments
20 pages, 12 figures