Diffusion language models (LMs) enable parallel decoding, but still lag behind autoregressive (AR) LMs in accuracy, and behind multi-token prediction (MTP) methods in efficiency. This raises three questions: should diffusion LMs compete with AR LMs or be harmonized with them; can diffusion provide a stronger acceleration mechanism than MTP; and does diffusion decoding have sufficient long-term potential to justify further exploration? We study these questions through Nemotron-Labs-Diffusion, a tri-mode LM that unifies three decoding modes—AR, diffusion, and self-speculation (diffusion drafts, AR verifies)—within a single model to sustain high throughput across all concurrency levels. Our study shows that (1) AR and diffusion objectives are mutually beneficial rather than competing, (2) diffusion-based self-speculation achieves higher acceptance lengths and better system vs. per-user throughput trade-offs than MTP baselines, and (3) diffusion decoding shows strong potential for parallel decoding under an optimal sampler in a speed-of-light analysis. Based on these insights, we develop the Nemotron-Labs-Diffusion family at 3B, 8B, and 14B scales. Our models outperform state-of-the-art open-source AR and diffusion LMs in both accuracy and speed, e.g., achieving 6x tokens per forward over Qwen3-8B with comparable benchmark accuracy, translating to 4x throughput on SPEED-Bench measured with SGLang on an NVIDIA GB200 GPU.

Recent advances in neural theorem-proving resort to large language models and tree searches. When proving a theorem, a language model advises single-step actions based on the current proving state and the tree search finds a sequence of correct steps using actions given by the language model. However, prior works often conduct constant computation efforts for each proving state while ignoring that the hard states often need more exploration than easy states. Moreover, they evaluate and guide the proof search solely depending on the current proof state instead of considering the whole proof trajectory as human reasoning does. Here, to accommodate general theorems, we propose a novel Dynamic-Tree Driven Theorem Solver (DT-Solver) by guiding the search procedure with state confidence and proof-level values. Specifically, DT-Solver introduces a dynamic-tree Monte-Carlo search algorithm, which dynamically allocates computing budgets for different state confidences, guided by a new proof-level value function to discover proof states that require substantial exploration. Experiments on two popular theorem-proving datasets, PISA and Mathlib, show significant performance gains by our DT-Solver over the state-of-the-art approaches, with a 6.65% improvement on average in terms of success rate. And especially under low computing resource settings (11.03% improvement on average).