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.