Tool-using large language models (LLMs) have improved at producing executable API calls, but reliable tool use requires coordinating semantic intent with executable invocation, especially in multi-step settings. Existing tool-learning objectives and traces collapse these two roles into a single homogeneous generation stream, so the learning signal cannot distinguish a flawed plan from a flawed call. We propose Dual-Mode Unified Policy Optimization (DUPO), a typed trajectory optimization framework that represents each step with a PLAN span for the current subgoal and a TOOL span for the API invocation. DUPO follows a PLAN-to-TOOL rollout factorization, optimizes the two modes with mode-separated policy ratios, and introduces Chain-Aware Upstream Advantage, so that early planning errors, which propagate through the rest of the trajectory, receive stronger credit than later steps. To support this optimization, we introduce PlanArena, a human-annotated dataset of 20,646 trajectories across 7,941 scenarios with explicit PLAN–TOOL supervision. Experiments on BFCL, API-Bank, and Tau2 show that DUPO improves tool-use performance, with gains concentrated in multi-step settings. Our code and dataset will be released upon publication.

Recent advancements in the application of Large Language Models (LLMs) to formal theorem proving in Lean have unveiled new prospects in complex logical reasoning scenarios. Acknowledging that the difficulty across reasoning steps in a formal theorem proof is not uniform, prior proof search algorithms have not systematically investigated which proof steps are more crucial to explore. This paper introduces Entropy-Based Best-First Search (EBFS), an entropy-inspired heuristic tree search algorithm that enhances the efficiency of proof generation models to explore proof trees, thereby increasing the probability of finding the correct proof. We also introduce a reinforcement fine-tuning approach specifically for proof tree search. Using EBFS during the generation stage further boosts the model’s performance in proof generation. Evaluations demonstrate that our fine-tuned EBFS model achieves consistent improvements over the baseline models. Under the same sample budget, it outperforms whole proof generation by 3.2% on the ProofNet testset, with further gains of 1.9% on MiniF2F and 1.5% on ProverBench.

To alleviate the hallucination problem of large language model (LLM), retrieval-augmented generation (RAG) has been proposed and widely adopted. Due to the limitations in cross-chunk summarization task of naive RAG, graph-based RAG has emerged as a promising solution. However, a close study reveals several flaws in these works. First, most graph-based RAGs suffer from less efficient indexing process, which leads to information loss and expensive costs. Second, they heavily rely on LLM for retrieval thus inference slowly, which hinders their application in industry. To build a more efficient and effective RAG, we propose the multi-semantic RAG (MS-RAG). In this work, we combine knowledge graphs with dense vector to build a multi-semantic RAG. To be specific, (i) at indexing stage, we create multiple semantic-level indexes, including chunk-level, relation-level, and entity-level, to leverage the merits of dense vector and knowledge graph. (ii) at retrieval stage, unlike the previous LLM-empowered entity extraction, we propose a novel mix recall algorithm. Finally, we employ a multi-semantic rerank module to purify the results. Extensive experiments show that MS-RAG achieves superior performance. In terms of retrieval effect, MS-RAG achieves state-of-the-art performance, which is about 10%-30% improvement than the existing methods. In terms of question-answering effect, MS-RAG still achieves promising results with faster inference speed. More analysis and experiments are provided in Appendix.