A Neurosymbolic Approach to Natural Language Formalization and Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915612876341248 |
|---|---|
| author | Bayless, Sam Buliani, Stefano Cassel, Darion Cook, Byron Clough, Duncan Delmas, Rémi Diallo, Nafi Erata, Ferhat Feng, Nick Giannakopoulou, Dimitra Goel, Aman Gokhale, Aditya Hendrix, Joe Hudak, Marc Jovanović, Dejan Kent, Andrew M. Kiesl-Reiter, Benjamin Kuna, Jeffrey J. Labai, Nadia Lilien, Joseph Raghunathan, Divya Rakamarić, Zvonimir Razavi, Niloofar Tautschnig, Michael Torkamani, Ali Weir, Nathaniel Whalen, Michael W. Yao, Jianan |
| author_facet | Bayless, Sam Buliani, Stefano Cassel, Darion Cook, Byron Clough, Duncan Delmas, Rémi Diallo, Nafi Erata, Ferhat Feng, Nick Giannakopoulou, Dimitra Goel, Aman Gokhale, Aditya Hendrix, Joe Hudak, Marc Jovanović, Dejan Kent, Andrew M. Kiesl-Reiter, Benjamin Kuna, Jeffrey J. Labai, Nadia Lilien, Joseph Raghunathan, Divya Rakamarić, Zvonimir Razavi, Niloofar Tautschnig, Michael Torkamani, Ali Weir, Nathaniel Whalen, Michael W. Yao, Jianan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_09008 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Neurosymbolic Approach to Natural Language Formalization and Verification Bayless, Sam Buliani, Stefano Cassel, Darion Cook, Byron Clough, Duncan Delmas, Rémi Diallo, Nafi Erata, Ferhat Feng, Nick Giannakopoulou, Dimitra Goel, Aman Gokhale, Aditya Hendrix, Joe Hudak, Marc Jovanović, Dejan Kent, Andrew M. Kiesl-Reiter, Benjamin Kuna, Jeffrey J. Labai, Nadia Lilien, Joseph Raghunathan, Divya Rakamarić, Zvonimir Razavi, Niloofar Tautschnig, Michael Torkamani, Ali Weir, Nathaniel Whalen, Michael W. Yao, Jianan Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science 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. |
| title | A Neurosymbolic Approach to Natural Language Formalization and Verification |
| topic | Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2511.09008 |