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

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 29 references that are in the map.
- First posted on arXiv 11 Apr 2026.

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

- [A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions](https://mlsanity.com/paper/2311.05232/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools](https://mlsanity.com/paper/2404.11891/) (2024)
- [SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas](https://mlsanity.com/paper/2505.14615/) (2025)
- [Learning to Reason via Mixture-of-Thought for Logical Reasoning](https://mlsanity.com/paper/2505.15817/) (2025)
- [A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters](https://mlsanity.com/paper/2406.00284/) (2024)
- [Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite](https://mlsanity.com/paper/2507.00877/) (2025)
- [Adaptive Selection of Symbolic Languages for Improving LLM Logical Reasoning](https://mlsanity.com/paper/2510.10703/) (2025)
- [Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs](https://mlsanity.com/paper/2509.22338/) (2025)
- [Fine-Tuned Large Language Models for Logical Translation: Reducing Hallucinations with Lang2Logic](https://mlsanity.com/paper/2512.02987/) (2025)

## Built on by (most cited first, 2 of 2)

- [Provably Secure Agent Guardrail](https://mlsanity.com/paper/2605.29251/) (2026)
- [Auto-Formalizing Neuro-Symbolic Predictors](https://mlsanity.com/paper/2610.01519/) (2026)

## Abstract (arXiv)

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.