# Neurosymbolic Auditing of Natural-Language Software Requirements

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 34 references that are in the map.
- First posted on arXiv 13 May 2026.

## Builds on (most cited first, 16 of 16)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [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)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [HumanEvalComm: Benchmarking the Communication Competence of Code Generation for LLMs and LLM Agent](https://mlsanity.com/paper/2406.00215/) (2024)
- [Unsupervised Evaluation of Code LLMs with Round-Trip Correctness](https://mlsanity.com/paper/2402.08699/) (2024)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [Large Language Models Based Automatic Synthesis of Software Specifications](https://mlsanity.com/paper/2304.09181/) (2023)
- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [Can Code Language Models Learn Clarification-Seeking Behaviors?](https://mlsanity.com/paper/2504.16331/) (2025)
- [Supporting Software Formal Verification with Large Language Models: An Experimental Study](https://mlsanity.com/paper/2507.04857/) (2025)
- [VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generation](https://mlsanity.com/paper/2512.14744/) (2025)
- [Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.10704/) (2025)
- [Multi-agent Self-triage System with Medical Flowcharts](https://mlsanity.com/paper/2511.12439/) (2025)

## Abstract (arXiv)

Natural-language software requirements are often ambiguous, inconsistent, and underspecified; in safety-critical domains, these defects propagate into formal models that verify the wrong specification and into implementations that ship unsafe behavior. We show that large language models, equipped with an SMT solver, can audit such requirements: translating them into formal logic, detecting ambiguity through stochastic variation in the generated formalization, and exposing inconsistency, vacuousness, and safety violations through solver queries on the resulting specification. We present VERIMED, a neurosymbolic pipeline that operationalizes this idea for medical-device software requirements, and report two findings. First, stochastic variation across independent formalizations is a signal of ambiguity: requirements that admit multiple plausible interpretations produce SMT-inequivalent formalizations, and bidirectional SMT equivalence checking turns this disagreement into a solver-checkable test. Second, the usefulness of symbolic feedback depends on its granularity: in counterexample-guided repair on a hemodialysis question-answering benchmark, concrete SMT counterexamples raise verified accuracy from 55.4% to 98.5%. Over an extensive experimental evaluation on open-source hemodialysis safety requirements, we show that the LLM-based approach in VERIMED successfully reduces ambiguity-sensitive requirements and enables rigorous auditing of software requirements through SMT-based queries.