10 papers
What Did the Agent Actually Do? Evidence-Grounded Oversight for Long-Horizon Agents
Zhongxiang Sun, Jiahao Yan, Hongkang Zhao +5
As agents take on long-horizon tasks, users shift from making individual decisions to overseeing autonomous execution. Yet the volume of agent activity and the fragmentation of sup…
Argus: A General-Purpose Agentic Reasoning Runtime for Long-Horizon Tasks
Boxiu Li, Zimo Wen, Yijia Fan +24
Long-horizon reasoning requires an agentic runtime that can persist when evidence supports its current approach and pivot when measurements reveal failure, hidden constraints, or a…
Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
Linbin Tang, Jingyan You, Zilin Kang +8
Recent formal reasoning systems have reached IMO-level performance, yet they leave a fragmented landscape: algebra and number theory are handled in Lean, while geometry still relie…
Post-Trained MoE Can Skip Half Experts via Self-Distillation
Xingtai Lv, Li Sheng, Kaiyan Zhang +12
Mixture-of-Experts (MoE) scales language models efficiently through sparse expert activation, and its dynamic variant further reduces computation by adjusting the activated experts…
STAR-PólyaMath: Multi-Agent Reasoning under Persistent Meta-Strategic Supervision
Jiaao Wu, Xian Zhang, Hanzhang Liu +3
Frontier AI models and multi-agent systems have led to significant improvements in mathematical reasoning. However, for problems requiring extended, long-horizon reasoning, existin…
Vibe Reasoning: Eliciting Frontier AI Mathematical Capabilities -- A Case Study on IMO 2025 Problem 6
Jiaao Wu, Xian Zhang, Fan Yang +1
We introduce Vibe Reasoning, a human-AI collaborative paradigm for solving complex mathematical problems. Our key insight is that frontier AI models already possess the knowledge r…
TrainVerify: Equivalence-Based Verification for Distributed LLM Training
Yunchi Lu, Youshan Miao, Cheng Tan +4
Training large language models (LLMs) at scale requires parallel execution across thousands of devices, incurring enormous computational costs. Yet, these costly distributed traini…
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
Chenrui Cao, Liangcheng Song, Zenan Li +4
Recent advancements, such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B, demonstrate a prevailing trend in leveraging reinforcement learning (RL)-based large-scale train…
REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Ziju Shen, Naohao Huang, Fanyi Yang +11
Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this pa…
Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
Zenan Li, Zhaoyu Li, Wen Tang +6
Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tact…