1 citations · 1 across the 17 of their papers we have counts for
18 papers
FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
Ziyu Wang, Qiming Dai, Yishan Wu +1
Large language models can now generate complex, multi-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical ch…
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…
A Unified Framework for Formalizing Matrix Decomposition Proofs
Wanli Ma, Zichen Wang, Zaiwen Wen
Existence proofs for many matrix decompositions share a recursive routine: a local transformation prepares the matrix, a slice is selected, a recursive solution is obtained, and th…
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…
Nyström Approximation on Manifolds
Hantao Nie, Bin Gao, Andi Han +3
Computations on a manifold often involve constructing an operator on the tangent space and computing its inverse, which can be time-consuming in many applications. In order to redu…
MM-OptBench: A Solver-Grounded Benchmark for Multimodal Optimization Modeling
Zhong Li, Qi Huang, Yuxuan Zhu +6
Optimization modeling translates real decision-making problems into mathematical optimization models and solver-executable implementations. Although language models are increasingl…
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…
Learning to Solve the Quadratic Assignment Problem with Warm-Started MCMC Finetuning
Yicheng Pan, Ruisong Zhou, Haijun Zou +2
The quadratic assignment problem (QAP) is a fundamental NP-hard task that poses significant challenges for both traditional heuristics and modern learning-based solvers. Existing Q…
A Learning Method with Gap-Aware Generation for Heterogeneous DAG Scheduling
Ruisong Zhou, Haijun Zou, Li Zhou +2
Efficient scheduling of directed acyclic graphs (DAGs) is a core problem in large-scale data-intensive computing systems, where query plans, data-processing workloads, and computat…
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…
Translating Informal Proofs into Formal Proofs Using a Chain of States
Ziyu Wang, Bowen Yang, Chenyi Li +4
We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach…
SITA: A Framework for Structure-to-Instance Theorem Autoformalization
Chenyi Li, Wanli Ma, Zichen Wang +1
While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structur…
Accelerating Optimization via Differentiable Stopping Time
Zhonglin Xie, Yiman Fong, Haoran Yuan +1
Optimization is an important module of modern machine learning applications. Tremendous efforts have been made to accelerate optimization algorithms. A common formulation is achiev…
Accelerated Natural Gradient Method for Parametric Manifold Optimization
Chenyi Li, Shuchen Zhu, Zhonglin Xie +1
Parametric manifold optimization problems frequently arise in various machine learning tasks, where state functions are defined on infinite-dimensional manifolds. We propose a unif…
OptMATH: A Scalable Bidirectional Data Synthesis Framework for Optimization Modeling
Hongliang Lu, Zhonglin Xie, Yaoyu Wu +3
Despite the rapid development of large language models (LLMs), a fundamental challenge persists: the lack of high-quality optimization modeling datasets hampers LLMs' robust modeli…
ODE-based Learning to Optimize
Zhonglin Xie, Wotao Yin, Zaiwen Wen
Recent years have seen a growing interest in understanding acceleration methods through the lens of ordinary differential equations (ODEs). Despite the theoretical advancements, tr…
Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization
Chenyi Li, Ziyu Wang, Wanyi He +3
The convergence rate of various first-order optimization algorithms is a pivotal concern within the numerical optimization community, as it directly reflects the efficiency of thes…