Training tool-use agents typically relies on outcome-based filtering: Supervised Fine-Tuning (SFT) on successful trajectories and Reinforcement Learning (RL) on pass-rate-selected tasks. However, this paradigm ignores interaction dynamics—successful trajectories may lack error recovery or exhibit redundancy, while pass rates fail to distinguish structurally informative tasks from trivial ones. To bridge this gap, we propose TopoCurate, an interaction-aware framework that shifts the paradigm from linear outcome filtering to topological interaction modeling. By projecting multi-trial rollouts into a unified semantic quotient topology within the same task, we construct a structured manifold that explicitly captures the divergence between success and failure pathways across tool invocations and environmental responses. Leveraging this representation, we introduce a dual-selection mechanism: for SFT, we prioritize trajectories demonstrating reflective recovery, semantic efficiency, and strategic diversity to mitigate covariate shift and mode collapse; for RL, we select tasks with high error branch ratios and strategic heterogeneity, maximizing gradient Signal-to-Noise Ratio to address vanishing signals in sparse-reward settings. Evaluations on BFCLv3 and Tau2 Bench show that TopoCurate achieves consistent gains of 4.2% (SFT) and 6.9% (RL) over state-of-the-art baselines.

Current Large Language Model (LLM) agents struggle with long-horizon reasoning tasks, such as competition-level mathematics, where sustaining precision over hundreds of steps is critical. A primary bottleneck is the reliance on natural language context or summaries to track progress; these linguistic representations are inherently "lossy," introducing semantic drift and accumulating errors that derail the reasoning chain. To address this, we propose Structured Strategy Folding (SSF), a novel paradigm that shifts the agent’s memory mechanism from linguistic description to computational verification. Instead of compressing history into text, SSF "folds" the reasoning trajectory into a sequence of Executable Symbolic States (ESS). Each ESS serves as a verifiable anchor—comprising either executed code artifacts or formally judged symbolic lemmas—generated through a dual-pathway validation mechanism. By interacting with these rigorous state artifacts rather than raw textual history, the agent effectively eliminates ambiguity and prevents error propagation. Experiments on challenging mathematical benchmarks demonstrate that SSF significantly outperforms standard Chain-of-Thought and existing summarization baselines, achieving substantial accuracy improvements while maintaining robust performance over extended reasoning horizons.

Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities with applications in various areas. However, their effectiveness in complex mathematical reasoning involving multi-step FOL deductions is still under-researched. While LLMs perform competitively on established mathematical reasoning benchmarks, they struggle with multi-step FOL tasks, as demonstrated by Deepseek-Prover-V2-7B’s low accuracy (4.2%) on our proposed theorem proving dataset. This issue arises from the limited exploration of diverse proof strategies and the potential for early reasoning mistakes to undermine entire proofs. To address these issues, we propose DREAM, a self-adaptive solution that enhances the Diversity and REAsonability of LLMs’ generation strategies. DREAM incorporates an Axiom-Driven Strategy Diversification mechanism to promote varied strategic outcomes and a Sub-Proposition Error Feedback to help LLMs reflect on and correct their proofs. Our contributions include pioneering advancements in LLMs’ mathematical reasoning through FOL theorem proving, introducing a novel inference stage solution that improves performance by 0.6% to 6.4%, and providing a curated dataset of 447 mathematical theorems in Lean 4 format for evaluation.