用确定性流程把自然语言需求转为逻辑代码，确保可审计、可复现。
VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline
- 通过指令微调模型+双向校验，实现高可靠翻译
- 在SatBench上正确率达94.46%，回译相似度87.73%
- 支持调试与回归测试，适合可靠性关键场景
VeriTrans是一种以可靠性为核心的机器学习系统，将自然语言需求编译为求解器可用的逻辑表达式，并通过验证器门控保障可靠性。该流程集成指令微调的自然语言到逻辑翻译器、用于高精度接受判断的往返重建（逻辑→自然语言），以及标准的逻辑→合取范式编译，所有操作均采用固定API配置（温度=0；微调使用种子=42）和逐项结果记录（提示、输出、哈希值），支持可审计性和重放调试。在包含2,100个规范的SatBench数据集上，VeriTrans实现94.46%的SAT/UNSAT正确率和87.73%的中位数往返相似度。对100–150个精选样本进行紧凑微调可提升约1–1.5个百分点的保真度，且不增加延迟（在201个规范的运行子集上平均耗时25.8秒/规范）。基于往返得分阈值的接受策略揭示了可靠性与覆盖范围之间的权衡：当阈值τ=75时，约68%的项目被保留，接受集合上的正确率约为94%。验证器开销占端到端运行时间不足15%，所有提示、响应及时间元数据均被记录，支持重放驱动的调试与回归测试。通过分离学习型翻译与符号验证，并强制执行确定性、验证器门控的接受机制，VeriTrans使自然语言到逻辑的前端组件成为可审计、可复现的可靠性关键工作流组成部分。
原文摘要 · Abstract (English)
\textbf{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$\!\to\!$PL translator, round-trip reconstruction (PL$\!\to\!$NL) used as a high-precision acceptance gate, and canonical PL$\!\to\!$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 \textbf{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 $\sim$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$\!\to\!$logic front-ends into auditable, reproducible components for reliability-critical workflows.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。