Natural language (NL) requirements are widely used in system design, but their ambiguity makes formal verification difficult. Translating NL requirements into Computation Tree Logic (CTL) is challenging because generated formulas must be both semantically appropriate and compatible with concrete verification models. Although large language models (LLMs) provide a promising basis for NL-to-CTL(NL2CTL) translation, their outputs are often unstable and prone to parsing, typing, and grounding errors.
To address these issues, we propose GenCTL, a prompt-based framework for effective and model-aware NL2CTL translation without task-specific fine-tuning. GenCTL combines structured prompting, retrieval-enhanced few-shot examples, atomic-proposition (AP) grounding from nuXmv models, multi-candidate generation with frequency-first selection and length-normalized log-likelihood tie-breaking, and interactive refinement through an explanation dictionary.
Experimental results demonstrate the effectiveness of the proposed framework in both model-agnostic and model-aware settings. On a generated NL--CTL dataset, the best automatically selected translation achieves 68% accuracy, which increases to 92% after one round of user refinement. On 150 NL requirements grounded in three nuXmv models, AP-list prompting yields 139/150 directly checkable formulas, increasing to 149/150 after lightweight normalization. These results show that GenCTL improves the reliability and practical checkability of LLM-generated CTL specifications.
Ran Tao· Poster Volume 0007 The 2026...· 0 citations
For scale-invariant deep networks, Hyperball-style optimizers have shown strong performance in large-scale training by fixing the norms of matrix-valued parameters and normalizing updates. However, the source of their advantage remains unclear. Starting from the angular displacement between consecutive parameter states, we derive an angular effective learning rate that accounts for the parameter-update angle, parameter norm, and update norm. We also show that the conventional norm-based measure is a special case under parameter-update orthogonality. We then decompose optimizer updates into radial and tangential components and analyze how radial updates affect one-step angular displacement. Under the training configurations considered, numerical results show that the radial component has only a limited direct effect on the angular effective learning rate. It therefore cannot explain why MuonH converges more slowly than MuonWD early in training but overtakes it later. To further isolate the underlying mechanism, we devise a heuristic experiment that modifies only the learning-rate schedule so that the dynamics of each optimizer reproduce those of the other. The results suggest that their main difference stems from the evolution of the effective step size rather than an intrinsically superior update direction induced by Hyperball. Our pretraining experiments further show that more aggressive learning-rate decay can accelerate MuonH early in training but may impair its later performance. Thus, maintaining a constant angular velocity does not eliminate the learning-rate-scheduling problem; careful scheduling remains essential to realizing the potential of Hyperball-style optimizers. Our code is publicly available at https://github.com/mangocrazz/hyperball-may-not-be-a-free-lunch.
Yihao Xiao, Jialong Sun, Zitian Gao et al.· 2 citations
On-policy distillation (OPD) transfers teacher capabilities by supervising trajectories sampled from the student's own policy, yet its generalization behavior remains poorly understood, as most studies evaluate OPD on a single domain and on benchmarks close to the training data. We present a controlled study that varies one generalization factor at a time, from in-domain distribution shifts to cross-domain transfer and the multi-teacher setting. We find that OPD transfers a teacher's reasoning behavior rather than its answers to particular problems: training difficulty barely matters, and even problems the teacher never solves are useful. Transfer depends strongly on the origin relationship between teacher and student: same-origin pairs bring the student close to the teacher across languages, reasoning horizons, and even other domains, whereas cross-origin pairs mostly fit the trained distribution. This broad reach is a double-edged sword: since routing prompts to domain experts cannot confine each teacher's influence, combining them yields a mixture-dependent seesaw among their capabilities. These results clarify when OPD generalizes and offer a useful perspective for diagnosing multi-teacher OPD.
Zhaoyi Li, Deyang Kong, Yuan Wei et al.· 0 citations
This work presents a unified black-box RL framework for stable and scalable optimization of general agents through complex harnesses, supporting unified training across heterogeneous execution systems.
Huatong Song, Fei Bai, Ming Yang et al.· 0 citations
This work presents LoopCoder pre-trained on 12T+ code and general tokens, along with LoopCoder-Thinking and LoopCoder-Instruct variants, the first large-scale looped transformer for code, achieving comparable performance to standard dense architectures with more parameters.
Jian Yang, Wei Zhang, Shawn Guo et al.· 0 citations