Source-linked AI summary
Stratified Consistency Distillation for Natural Language Formalization
Zhichao Hou, Ferhat Erata, Joe Lilien, MohamadAli Torkamani
TL;DR
The paper targets inaccurate natural-language-to-logical-formula translation and the cost and limited adaptability of frontier LLMs. It proposes Stratified Consistency Distillation, which clusters multiple teacher translations, selects pseudo-labels by entropy, and fine-tunes a smaller model. Experiments report improved translation performance and lower inference latency than larger models.
Problem
Natural-language-to-formula translation remains difficult, while frontier LLMs are costly to run and generally unavailable for fine-tuning.
Method
The method clusters multiple frontier-LLM translations by semantic equivalence, stratifies examples by entropy, selects pseudo-labels, and fine-tunes a smaller student model.
Results
SCD achieves the best Pass@10 at 55.208%, exceeding Qwen3-14B by 12.500 percentage points and vanilla distillation by 4.861 percentage points.
Takeaways & Limitations
The approach improves logical translation accuracy while transferring frontier-model capabilities to a smaller model with substantially lower inference latency.
Takeaways & Limitations
The approach assumes access to frontier LLMs for generating teacher translations, although those models are typically closed-source and available through black-box APIs.
Abstract
from arXiv · showhide
Neurosymbolic reasoning has shown promising success in addressing complex reasoning tasks by combining large language models (LLMs) and symbolic solvers. While this approach shows promise, a fundamental challenge remains: improving the accuracy of translations from natural language to logical formulas. Current methods predominantly rely on prompt engineering, which is difficult to scale across different domains and input formats. Drawing inspiration from the success of fine-tuning in other model adaptation and alignment applications, we propose a fine-tuning-based Stratified Consistency Distillation approach: (1) We generate K logical translations per input using a frontier LLM and cluster them by semantic equivalence (2) Based on the entropy level, we apply majority voting (low entropy), LLM-as-a-Judge (medium entropy), or unification/abstention (high entropy), and (3) fine-tune a smaller model using the selected pseudo-labels. Our experiments show significant and consistent improvements in both Pass@K and our novel Equivalent Logical Similarity metrics, demonstrating the potential of advancing logical translation through consistency distillation.
1 Introduction
The paper addresses reliable natural-language-to-logic translation for verifiable reasoning, especially where chatbot errors carry high stakes. It proposes distilling frontier-LLM capabilities into a smaller open-source model through Stratified Consistency Distillation.
- High-stakes chatbot hallucinations can contradict authoritative policies and cause financial, legal, or reputational harm.
- The central question is whether LLMs can translate human-written natural language into formulas that symbolic solvers can verify.
- 70B-to-over-500B frontier models impose high latency and computational cost, while closed black-box access prevents fine-tuning.
- Stratified Consistency Distillation transfers frontier-LLM reasoning and translation capabilities to a smaller, more efficient open-source model.
- The framework combines synthetic policy-document data, entropy-based distillation, and evaluation across multiple policy-driven reasoning benchmarks.
2 Preliminary
The paper formulates NL2SMT as generating SMT-LIB completions that capture natural-language semantics and evaluates both exact equivalence and graded logical similarity. Its data pipeline creates aligned question-answer and SMT-LIB pairs from policy documents.
- Synthetic dataset generation: The synthetic-data pipeline extracts semantic context from policy documents before generating grounded natural-language question-answer pairs.
- Synthetic dataset generation: Each generated example is organized as a natural-language prompt paired with an SMT-LIB completion for model training.
- NL2SMT problem setup: NL2SMT maps a natural-language prompt p to an SMT-LIB completion t that accurately captures its logical semantics.
- NL2SMT problem setup: The training objective maximizes expected similarity between the model-generated translation and the ground-truth SMT-LIB translation.
- Equivalence measurements: Evaluation combines Z3-based binary equivalence with a continuous similarity score to measure exact and partial logical alignment.
3 Stratified Consistency Distillation
Stratified Consistency Distillation generates and clusters multiple frontier-LLM translations, estimates semantic entropy, and selects supervision according to uncertainty before fine-tuning a smaller student model.
- Framework overview: The pipeline generates frontier-LLM translations, clusters them by logical equivalence, selects pseudo-labels, and distills them into a smaller student model.
- Equivalent clustering and entropy: Semantic-equivalence clustering uses Z3-based checks to group translations, while semantic entropy summarizes the probability distribution over clusters.
- Stratified selection: The strategy is designed to allocate supervision based on the uncertainty of generated translations rather than applying one selection rule universally.
- Stratified selection: Low-entropy inputs use the largest cluster, medium-entropy inputs use an LLM judge over the top two clusters, and high-entropy inputs are unified or abstained.
- Knowledge distillation: Fine-tuning a smaller student model, such as Qwen2.5-7B, transfers knowledge from the frontier teacher.
4 Experiment
Experiments evaluate NL2SMT translation on FOLIO using Pass@K, similarity scores, latency percentiles, and cluster-selection analyses. Stratified consistency distillation improves translation performance while retaining practical efficiency, and entropy-aware clustering supports candidate selection.
- Evaluation setup: Experiments evaluate NL2SMT translation on FOLIO using Pass@K and continuous similarity metrics, with Qwen2.5-7B-Instruct as the primary student model.Comparisons include pretrained, fine-tuned, distilled, and several open-source and proprietary models.
- FOLIO translation: 55.208% Pass@10 is achieved by SCD, exceeding Qwen3-14B by 12.500 percentage points and vanilla distillation by 4.861 percentage points.Vanilla distillation reaches 50.347%, compared with 21.875% for few-shot Qwen2.5-7B-Instruct.
- Per-example analysis: Fine-tuning and consistency distillation broaden correct-translation coverage and shift similarity heatmaps toward higher logical alignment than pretrained models.The visualizations compare per-example Pass@10 outcomes and continuous similarity scores across model and training configurations.
- Efficiency: 4.040 seconds P50 latency for fine-tuned Qwen2.5-7B-Instruct is approximately 4.1× faster than Claude Sonnet 3.7 at 16.680 seconds.The advantage also appears at P90 and P99, with 5.074 versus 28.042 seconds and 5.651 versus 29.425 seconds, respectively.
- Cluster selection: Top@2 approaches the Pass@10 oracle upper bound, indicating that the correct translation is usually contained in one of the two largest semantic-equivalence clusters.Top@1 also outperforms random candidate selection, while increasing entropy makes the largest cluster less reliable.
- Ablation analysis: Stratified SCD achieves the highest or tied-highest Pass@K performance across the ablation results, outperforming single entropy-regime strategies.Low-entropy samples consistently outperform high-entropy samples, suggesting more consistent teacher predictions provide stronger supervision.
5 Related Works
Prior work has improved LLM reasoning through prompting, while autoformalization converts informal language into machine-verifiable representations for mathematical and verification settings.
- Improving Logical Reasoning of LLMs: Prompting strategies such as Chain-of-Thought have been used to improve pretrained LLMs’ logical reasoning capabilities.
- Automalization of LLMs: Autoformalization converts informal natural language into verifiable formal representations.
- Automalization of LLMs: In mathematics, autoformalization translates human-written proofs into machine-checkable formats for proof assistants including Coq, Lean, and Isabelle.
6 Conclusion
The paper presents NL2SMT and Stratified Consistency Distillation to make LLM-generated logical translations verifiable, accurate, efficient, and more practical for high-stakes domains.
- NL2SMT translates natural language into verifiable SMT-LIB formulas for automated checking with symbolic solvers.
- Stratified Consistency Distillation transfers a frontier model’s logical translation capability to a smaller open-source model according to translation uncertainty.
- Experiments on FOLIO show improved translation accuracy over pretrained and vanilla-distillation baselines, matching or exceeding substantially larger models.
- The distilled model offers considerably lower inference latency, supporting more practical deployment.
A Prompt for Translation Generation
The prompt instructs an expert model to translate natural-language premises and conclusions into pure SMT-LIB assertions using only the supplied declarations and logical operators.
- The prompt frames the task as translating natural-language logical reasoning into SMT-LIB format.
- The model must analyze declared variables, types, and descriptions before translating the premises and conclusion.
- The output must use only constants and functions from the declarations, with each assertion wrapped in (assert ...).
- The prompt specifies SMT-LIB operators including and, or, not, =>, xor, forall, and exists.
- The prompt prohibits XML tags and markdown formatting in the final output.
- The worked example supplies premises, a conclusion, declarations, and pure SMT-LIB assertions as the expected translation format.