7 papers · 1 filter
The Minimum Q-Order of BFGS with Exact Line Search Is One
Benqi Liu, Chenyi Li, Zaiwen Wen
Powell asked whether the smoothness assumptions underlying classical superlinear convergence force a fixed power law between adjacent iterates of exact-line-search variable-metric…
ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System
Yutong He, Daibo Li, Guohong Li +15
Recent advances in Large Language Models have fueled autonomous AI agents capable of tackling complex scientific tasks, yet existing automated research systems remain predominantly…
MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures
Wentao Long, Yunfei Zhang, Chenyi Li +1
Automatically constructing well-specified and valuable mathematical conjectures remains a central challenge in AI-assisted mathematical discovery. Many existing open problems and c…
CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
Wentao Long, Yunfei Zhang, Chenyi Li +3
Formal theorem-proving benchmarks enable mechanically verifiable evaluation of mathematical reasoning in large language models. However, existing benchmarks mainly focus on Olympia…
Teacher-Feature Drifting: One-Step Diffusion Distillation with Pretrained Diffusion Representations
Yuan Zhang, Chenyi Li, Haodong Yu +8
Sampling from pretrained diffusion and flow-matching models typically requires many forward passes to generate diverse and high-fidelity images. Existing distillation methods often…
OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
Chenyi Li, Yanchen Nie, Zhenyu Ming +3
Recent advances in formal theorem proving have focused on Olympiad-level mathematics, leaving undergraduate domains largely unexplored. Optimization, fundamental to machine learnin…
Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
Bowen Yang, Yi Yuan, Chenyi Li +5
Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of decl…