Towards auto-shot learning of Temporal Constraints in LLMs

Large Language Models (LLMs) perform strongly on many NLP tasks, yet their reliability on formal temporal reasoning remains unclear. We present a formally grounded evaluation framework for the past-time fragment of Linear Temporal Logic (LTL) that measures an LLM's ability to interpret and reconstruct temporal constraints with semantic fidelity. The pipeline integrates constraint-guided synthesis, automata-theoretic verification, symbol-free obfuscation, grammar-constrained reconstruction, and counterexample-driven repair within a unified loop. Equivalence is checked via language inclusion, and shortest counterexamples provide graded feedback. The experiments across five instruction-tuned models (Llama-3.2-1B, Qwen2.5-7B, Gemma-3-4B, DeepSeek-Math-7B, Mathstral-7B) show a consistent positive association between fidelity and understanding for the obfuscator, and a monotone relationship between fidelity and intelligence for the player. Covariance analysis indicates that variability is higher for the player, suggesting that reconstruction behavior contributes more to performance variance than obfuscation. This highlights the significance of improving grammar-constrained decoding, CKB-guided beam scoring, and counterexample-driven repair, which deliver larger gains than refining obfuscation alone. The framework provides a reproducible basis for diagnosing and improving temporal reasoning in LLMs.