VeriTrans is a reliability-first ML system that compiles natural-language requirements into solver-ready logic with validator-gated reliability. The pipeline integrates an instruction-tuned NL→PL translator, round-trip reconstruction (PL→NL) used as a high-precision acceptance gate, and canonical PL→CNF compilation, all executed via fixed API configuration (temperature=0; fine-tuning runs use seed=42) and per-item artifact logging (prompts, outputs, hashes) to support auditability and replay-driven debugging. On SatBench (2{,}100 specifications), VeriTrans achieves 94.46% SAT/UNSAT correctness and 87.73% median round-trip similarity. Compact fine-tuning on 100--150 curated examples improves fidelity by about 1--1.5,pp without increasing latency (mean 25.8,s/spec on our 201-spec runtime subset). A thresholded acceptance policy on the round-trip score exposes a reliability--coverage knob: at τ=75, roughly 68% of items are retained with ∼94% correctness on the accepted set. Validator overhead contributes <15% of end-to-end runtime, and all prompts/responses and timing metadata are logged to enable replay-driven debugging and regression testing. By separating learned translation from symbolic verification and enforcing deterministic, validator-gated acceptance, VeriTrans turns NL→logic front-ends into auditable, reproducible components for reliability-critical workflows.
Figures & tables
Figure 1. Hybrid neural–symbolic VeriTrans pipeline. The LLM performs NL → PL translation; validators enforce linguistic and structural consistency; deterministic PL → CNF conversion and SAT solving provide reproducible verification.
Threshold
Count
Proportion
≥75%
1422
0.677
Table 1. High-consistency mass at τ=75% .
Model
Mean Sim. (%)
Median Sim. (%)
Mean Runtime (s)
SAT/UNSAT Correctness (%)
Baseline
80.2
79.4
25.81
91.8
FT-50
85.1
86.3
37.96
93.9
FT-100
87.2
88.1
28.24
94.5
FT-150
87.7
88.4
23.38
94.5
FT-300
87.6
88.2
19.27
94.3
Table 2. Summary of fine-tuning performance on the 201-spec subset. All values are averaged per item.
τ Range
Support
Equiv. Rate
Notes
≥90
800
98.3%
Ultra-high fidelity
[ 80, 90)
471
95.6%
High confidence
[ 70, 80)
277
85.2%
Moderate
<70
552
54.1%
Low fidelity
Table 3. CNF equivalence breakdown by similarity threshold bin.
Model
Median Δ (%)
p -value
Cliff’s δ
FT-50
+0.9
<10−5
0.35 (small)
FT-100
+1.4
<10−5
0.42 (medium)
FT-150
+1.6
<10−5
0.44 (medium)
Table 4. Wilcoxon signed-rank test comparing fine-tuned models with baseline.
Model
Mean Δ (%)
95% CI (BCa)
FT-50
+0.9
[ +0.6 , +1.2 ]
FT-100
+1.4
[ +1.1 , +1.7 ]
FT-150
+1.6
[ +1.2 , +1.9 ]
Table 5. BCa bootstrap (10 000 resamples) 95% confidence intervals for mean similarity gain.
A standard pipeline for symbolic reasoning over natural-language problems translates them into first-order logic and invokes a theorem prover. The translation step is the bottleneck: swap "every" for "some" and every inference that follows is corrupted. Yet today's metrics often score more broken translations higher than less broken ones, because BLEU, BERTScore, and Smatch++ reward surface overlap that the worst errors happen to preserve. We introduce SIV, which derives two kinds of probes from the target formula and uses a theorem prover to verify the candidate translation against each. Positive probes are statements the candidate must entail, which detect translations that drop content; contrastive probes are statements the candidate must not entail, which detect translations that assert more than the original. On a controlled pool of perturbed FOLIO translations, the severity of the error accounts for 80% of SIV's score variance, compared with at most 17% for any prior metric. Across six error classes on a disjoint pool, SIV scores the reference above the perturbed candidate in over 99% of pairs. Because each probe is labeled with what it tests, the failure pattern also supplies a labeled error trace, recovering the perturbation class at macro-F1 0.638, nearly double the score-only baseline. On 434 expert-audited real LLM translations, SIV attains the top AUC, uniquely detects and grades expert-labeled major errors, and abstains, rather than mis-scoring, on out-of-vocabulary translations.
Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28% semantic equivalence with reference specifications while ensuring 86% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.
Accurate translation from Natural Language to First-Order Logic (NL-to-FOL) underpins neurosymbolic AI systems and Natural Language Inference (NLI), making the quality of NL-to-FOL benchmarks essential---yet these datasets have never been rigorously audited. Our first contribution is to present a systematic human inspection of the validation split of FOLIO and a subset of MALLS test instances, finding that approximately 42.5% and 42% of entries, respectively, contain incorrect FOL formalizations (i.e., ground truth labels), with additional rates of ambiguous NL sentences (17.8% and 51%) and incorrect NLI labels in FOLIO (8.4%). Our second contribution is to develop and release corrected ground truths for such datasets, showing that annotation errors distort model evaluation on a reference benchmark task: testing three state-of-the-art LLMs (Gemma~4 31B-it, Qwen3-30B-A3B, and GPT-4o-mini) with the corrected ground truths yields accuracy gains from +11 to +23 percentage points. Motivated by these findings, we propose an LLM-based framework to support humans in manual reviewing NL-to-FOL datasets. By directing reviewers toward the most error-prone instances, we empirically show that it is possible to achieve 90% dataset accuracy after reviewing fewer than 20% of instances, compared to over 76% required by unguided review. We release all human-verified annotations and the code for our framework.