9 papers
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…
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…