16 papers
Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
Jihao Liu, Guoxiong Gao, Zeming Sun +8
Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, sca…
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
Hanyu Wang, Ruohan Xie, Yutong Wang +3
Accurate auto-formalization of theorem statements is essential for advancing automated discovery and verification of research-level mathematics, yet remains a major bottleneck for…
From Search to Synthesis: Training LLMs as Zero-Shot Workflow Generators
Gan Luo, Zihan Qin, Bin Dong +1
Large language models (LLMs) excel across a wide range of tasks, yet their instance-specific solutions often lack the structural consistency needed for reliable deployment. Workflo…
Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning
Ruoran Xu, Haoyu Cheng, Bin Dong +1
Geometric problem solving, as a typical multimodal reasoning problem, has attracted much attention and made great progress recently, however most of works focus on plane geometry w…
Automated Conjecture Resolution with Formal Verification
Haocheng Ju, Guoxiong Gao, Jiedong Jiang +13
Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capa…
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
Guoxiong Gao, Zeming Sun, Jiedong Jiang +5
Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof -- a task we call global premise retrieval. Existing…