VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline

arXiv:2604.10341v1 Announce Type: new Abstract: extbf{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!o!PL translator, round-trip reconstruction (PL!o!NL) used as a high-precision acceptance gate, and canonical PL!o!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 extbf{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 au{=}75, roughly 68% of items are retained with sim94% 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!o!logic front-ends into auditable, reproducible components for reliability-critical workflows.

Related

• SymptomWise: A Deterministic Reasoning Layer for Reliable and Efficient AI Systems
• Probabilistic Language Tries: A Unified Framework for Compression, Decision Policies, and Execution Reuse
• Multi-Modal Learning meets Genetic Programming: Analyzing Alignment in Latent Space Optimization
• ChipSeek: Optimizing Verilog Generation via EDA-Integrated Reinforcement Learning

Source: arXiv cs.AI | 2026-04-14