arXiv subjects

Zaiwen Wen

Publications and source records attributed to Zaiwen Wen.

At least 37 records · Page 2Linked to original sources

arXiv2026

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

Formal theorem-proving benchmarks enable mechanically verifiable evaluation of mathematical reasoning in large language models. However, existing benchmarks mainly focus on Olympiad-style problems and algebraic domains, leaving computational and applied mathematics underrepresented. We introduce CAM-Bench, a Lean 4 theorem-proving benchmark of 1,000 Lean proof targets in computational and applied mathematics, with coverage spanning optimization, numerical linear algebra, and numerical analysis. These problems are adapted from textbook exercises and often depend on locally introduced definitions, notation, algorithms, and elementary results. To construct CAM-Bench, we develop a dependency-recovery pipeline that reconstructs the local textbook context needed to state each problem faithfully. It then normalizes each problem into a standalone informal theorem and translates it into a Lean target. We validate the resulting formal problems through Lean compilation and semantic review, checking both formal correctness and semantic alignment with the original exercises. For each problem, we release the raw exercise, recovered context, normalized informal theorem, and final Lean target. CAM-Bench complements existing formal mathematics benchmarks by targeting applied mathematics problems that rely on textbook concepts and elementary theorems, many of which are not directly available as standard Mathlib4 lemmas. We evaluate widely used large language models and formalization agents on CAM-Bench, and analyze common failure modes in tracking local assumptions, applying elementary results, decomposing proofs, and maintaining long-horizon control in Lean.

cs.AI↗

arXiv2026

Nyström Approximation on Manifolds

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 reduce the computational costs and preserve the benign properties of tangent operators, we develop the Riemannian Nyström approximation on manifolds, a low-rank approximation of tangent operators through subspace projections onto the tangent space. The developed approximation is intrinsically constructed and inherits desirable properties from the classical Nyström approximation, e.g., positive semidefiniteness and approximation errors. Instead of the Gaussian sketching, we introduce the Haar--Grassmann sketching condition with a coordinate-free representation, which remains compatible under isometric vector transport across tangent spaces. Moreover, we propose a randomized Newton-type method for optimization on manifolds in which the linear system is constructed via the Riemannian Nyström approximation. Numerical experiments on the SPD and Grassmann manifolds, together with principal geodesic analysis on real data, illustrate that the proposed approximation reduces the computational cost of operators while maintaining comparable accuracy.

math.NA↗

arXiv2026

PEARL: Solver-in-the-Loop Interactive Optimization Modeling from Natural Language

Optimization modeling is the process of translating real-world decision problems, often described in natural language, into formal mathematical formulations and executable solver code. While recent advances in large language models have shown promise in automating this process, most existing approaches remain one-shot: a model produces a formulation once, without executing it, conditioning on solver feedback, or iteratively revising errors. This stands in sharp contrast to real-world optimization modeling, which is inherently interactive and proceeds through repeated solve-debug-revise cycles. We introduce PEARL, a system for interactive optimization modeling that uses Python execution and mathematical programming solvers inside this loop. Rather than relying on a fixed repair workflow, PEARL learns when to test partial models, how to revise from solver diagnostics, and when to stop. It operates in a multi-turn tool-integrated setting where intermediate execution results, feasibility signals, and solution checks are used to improve both formulations and solver code before finalization. Across diverse optimization benchmarks, PEARL substantially improves verified solve rates over strong one-shot and tool-augmented baselines; notably, our PEARL-Qwen3-\textbf{4B} model outperforms the much larger DeepSeek-V3.2-\textbf{685B} in both macro- and micro-averaged accuracy on optimization modeling tasks.

cs.AI↗

arXiv2026

MM-OptBench: A Solver-Grounded Benchmark for Multimodal Optimization Modeling

Optimization modeling translates real decision-making problems into mathematical optimization models and solver-executable implementations. Although language models are increasingly used to generate optimization formulations and solver code, existing benchmarks are almost entirely text-only. This omits many optimization-modeling tasks that arise in operational practice, where requirements are described in text but instance information is conveyed through visual artifacts such as tables, graphs, maps, schedules, and dashboards. We introduce multimodal optimization modeling, a benchmark setting in which models must construct both a mathematical formulation and executable solver code from a text-and-visual problem specification. To evaluate this setting, we develop a solver-grounded framework that generates structured optimization instances, verifies each with an exact solver, and builds both the model-facing inputs and hidden reference files from the same verified source. We instantiate the framework as MM-OptBench, a benchmark of 780 solver-verified instances spanning 6 optimization families, 26 subcategories, and 3 structural difficulty levels. We evaluate 9 multimodal large language models (MLLMs), including 6 frontier general-purpose models and 3 math-specialized models, with aggregate, family-level, difficulty-level, and failure-mode analyses. The results show that the task remains far from solved: the best two models reach 52.1% and 51.3% pass@1, while on average across the six general-purpose MLLMs, pass@1 is 43.4% on easy instances and 15.9% on hard instances. All three math-specialized MLLMs solve 0/780 instances. Failure attribution shows that errors arise both when extracting instance data from text and visuals and when turning extracted data into solver-correct formulations and code. MM-OptBench provides a testbed for solver-grounded, decision-oriented multimodal intelligence.

cs.AI↗

arXiv2026

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

Recent advances in formal theorem proving have focused on Olympiad-level mathematics, leaving undergraduate domains largely unexplored. Optimization, fundamental to machine learning, operations research, and scientific computing, remains underserved by existing provers. Its reliance on domain-specific formalisms (convexity, optimality conditions, and algorithmic analysis) creates significant distribution shift, making naive domain transfer ineffective. We present OptProver, a trained model that achieves robust transfer from Olympiad to undergraduate optimization. Starting from a strong Olympiad-level prover, our pipeline mitigates distribution shift through two key innovations. First, we employ large-scale optimization-focused data curation via expert iteration. Second, we introduce a specialized preference learning objective that integrates perplexity-weighted optimization with a mechanism to penalize valid but non-progressing proof steps. This not only addresses distribution shifts but also guides the search toward efficient trajectories. To enable rigorous evaluation, we construct a novel benchmark in Lean 4 focused on optimization. On this benchmark, OptProver achieves state-of-the-art Pass@1 and Pass@32 among comparably sized models while maintaining competitive performance on general theorem-proving tasks, demonstrating effective domain transfer without catastrophic forgetting.

cs.LG↗

arXiv2026

Learning to Solve the Quadratic Assignment Problem with Warm-Started MCMC Finetuning

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 QAP solvers still struggle to achieve consistently competitive performance across structurally diverse real-world instances. To bridge this performance gap, we propose PLMA, an innovative permutation learning framework. PLMA features an efficient warm-started MCMC finetuning procedure to enhance deployment-time performance, leveraging short Markov chains to anchor the adaptation to the promising regions previously explored. For rapid exploration via MCMC over the permutation space, we design an additive energy-based model (EBM) that enables an $O(1)$-time 2-swap Metropolis-Hastings sampling step. Moreover, the neural network used to parameterize the EBM incorporates a scalable and flexible cross-graph attention mechanism to model interactions between facilities and locations in the QAP. Extensive experiments demonstrate that PLMA consistently outperforms state-of-the-art baselines across various benchmarks. In particular, PLMA achieves a near-zero average optimality gap on QAPLIB, exhibits remarkably superior robustness on the notoriously difficult Taixxeyy instances, and also serves as an effective QAP solver in bandwidth minimization.

cs.LG↗

arXiv2026

LMask: Learn to Solve Constrained Routing Problems with Lazy Masking

Routing problems are canonical combinatorial optimization tasks with wide-ranging applications in logistics, transportation, and supply chain management. However, solving these problems becomes significantly more challenging when complex constraints are involved. In this paper, we propose LMask, a novel learning framework that utilizes dynamic masking to generate high-quality feasible solutions for constrained routing problems. LMask introduces the LazyMask decoding method, which lazily refines feasibility masks with the backtracking mechanism. In addition, it employs the refinement intensity embedding to encode the search trace into the model, mitigating representation ambiguities induced by backtracking. To further reduce sampling cost, LMask sets a backtracking budget during decoding, while constraint violations are penalized in the loss function during training to counteract infeasibility caused by this budget. We provide theoretical guarantees for the validity and probabilistic optimality of our approach. Extensive experiments on the traveling salesman problem with time windows (TSPTW) and TSP with draft limits (TSPDL) demonstrate that LMask achieves state-of-the-art feasibility rates and solution quality, outperforming existing neural methods.

math.OC↗

arXiv2026

Accelerating LLM Pre-Training through Flat-Direction Dynamics Enhancement

Pre-training Large Language Models requires immense computational resources, making optimizer efficiency essential. The optimization landscape is highly anisotropic, with loss reduction driven predominantly by progress along flat directions. While matrix-based optimizers such as Muon and SOAP leverage fine-grained curvature information to outperform AdamW, their updates tend toward isotropy -- relatively conservative along flat directions yet potentially aggressive along sharp ones. To address this limitation, we first establish a unified Riemannian Ordinary Differential Equation (ODE) framework that elucidates how common adaptive algorithms operate synergistically: the preconditioner induces a Riemannian geometry that mitigates ill-conditioning, while momentum serves as a Riemannian damping term that promotes convergence. Guided by these insights, we propose LITE, a generalized acceleration strategy that enhances training dynamics by applying larger Hessian damping coefficients and learning rates along flat trajectories. Extensive experiments demonstrate that LITE significantly accelerates both Muon and SOAP across diverse architectures (Dense, MoE), parameter scales (130M--1.3B), datasets (C4, Pile), and learning-rate schedules (cosine, warmup-stable-decay). Theoretical analysis confirms that LITE facilitates faster convergence along flat directions in anisotropic landscapes, providing a principled approach to efficient LLM pre-training. The code is available at https://github.com/SHUCHENZHU/LITE.

cs.LG↗

arXiv2026

M2F: Automated Formalization of Mathematical Literature at Scale

Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.

cs.AI↗

arXiv2026

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of declarative propositions, often neglecting the task of explicitly synthesizing solutions. This limitation is particularly acute in applied mathematics domains, where the goal is frequently to derive concrete values or executable algorithms rather than solely proving theorems. To address this, we introduce a Lean 4 framework that enforces a construction-verification workflow, compelling the agent to define explicit solutions before proving their correctness. We curate a comprehensive benchmark AMBER (Applied Mathematics BEnchmark for Reasoning) spanning core domains of applied mathematics, including convex analysis, optimization, numerical algebra, and high-dimensional probability. Aside from theorem proving, our benchmark features complex tasks such as evaluation, algorithm design, and representation transformation. Experiments reveal that current models face significant difficulties with these constructive tasks. Notably, we observe that general-purpose reasoning models consistently outperform specialized theorem provers. We attribute this to a degradation of instruction following capabilities in specialized models. Fine-tuning on proof corpora appears to induce ``tactical overfitting", compromising the ability to adhere to complex constructive requirements, whereas general models retain the versatility needed for multi-task formal reasoning.

cs.LO↗

arXiv2025

Translating Informal Proofs into Formal Proofs Using a Chain of States

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 is grounded in two key insights. First, informal proofs tend to proceed via a sequence of logical transitions - often implications or equivalences - without explicitly specifying intermediate results or auxiliary lemmas. In contrast, formal systems like Lean require an explicit representation of each proof state and the tactics that connect them. Second, each informal reasoning step can be viewed as an abstract transformation between proof states, but identifying the corresponding formal tactics often requires nontrivial domain knowledge and precise control over proof context. To bridge this gap, we propose a two stage framework. Rather than generating formal tactics directly, we first extract a Chain of States (CoS), a sequence of intermediate formal proof states aligned with the logical structure of the informal argument. We then generate tactics to transition between adjacent states in the CoS, thereby constructing the full formal proof. This intermediate representation significantly reduces the complexity of tactic generation and improves alignment with informal reasoning patterns. We build dedicated datasets and benchmarks for training and evaluation, and introduce an interactive framework to support tactic generation from formal states. Empirical results show that our method substantially outperforms existing baselines, achieving higher proof success rates.

cs.LO↗

arXiv2025

Extended parameter shift rules with minimal derivative variance for parameterized quantum circuits

Parameter shift rules (PSRs) are useful methods for computing arbitrary-order derivatives of the cost function in parameterized quantum circuits. The basic idea of PSRs is to evaluate the cost function at different parameter shifts, then use specific coefficients to combine them linearly to obtain the exact derivatives. In this work, we propose an extended parameter shift rule (EPSR) which generalizes a broad range of existing PSRs and has the following two advantages. First, EPSR offers an infinite number of possible parameter shifts, allowing the selection of the optimal parameter shifts to minimize the final derivative variance and thereby obtaining the more accurate derivative estimates with limited quantum resources. Second, EPSR extends the scope of the PSRs in the sense that EPSR can handle arbitrary Hermitian operator $H$ in gate $U(x) = \exp (iHx)$ in the parameterized quantum circuits, while existing PSRs are valid only for simple Hermitian generators $H$ such as simple Pauli words. Additionally, we show that the widely used ``general PSR'', introduced by Wierichs et al. (2022), is a special case of our EPSR, and we prove that it yields globally optimal shifts for minimizing the derivative variance under the weighted-shot scheme. Finally, through numerical simulations, we demonstrate the effectiveness of EPSR and show that the usage of the optimal parameter shifts indeed leads to more accurate derivative estimates.

quant-ph↗

arXiv2025

SITA: A Framework for Structure-to-Instance Theorem Autoformalization

While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete settings. With the goal of auto-formalizing mathematical results at the research level, we develop a framework for structure-to-instance theorem autoformalization (SITA), which systematically bridges the gap between abstract mathematical theories and their concrete applications in Lean proof assistant. Formalized abstract structures are treated as modular templates that contain definitions, assumptions, operations, and theorems. These templates serve as reusable guides for the formalization of concrete instances. Given a specific instantiation, we generate corresponding Lean definitions and instance declarations, integrate them using Lean's typeclass mechanism, and construct verified theorems by checking structural assumptions. We incorporate LLM-based generation with feedback-guided refinement to ensure both automation and formal correctness. Experiments on a dataset of optimization problems demonstrate that SITA effectively formalizes diverse instances grounded in abstract structures.

cs.AI↗

arXiv2025

The Augmented Lagrangian Methods: Overview and Recent Advances

Large-scale constrained optimization is pivotal in modern scientific, engineering, and industrial computation, often involving complex systems with numerous variables and constraints. This paper provides a unified and comprehensive perspective on constructing augmented Lagrangian functions (based on Hestenes-Powell-Rockafellar augmented Lagrangian) for various optimization problems, including nonlinear programming and convex and nonconvex composite programming. We present the augmented Lagrangian method (ALM), covering its theoretical foundations in both convex and nonconvex cases, and discuss several successful examples and applications. Recent advancements have extended ALM's capabilities to handle nonconvex constraints and ensure global convergence to first and second-order stationary points. For nonsmooth convex problems, ALM utilizes proximal operations, preserving desirable properties such as locally linear convergence rates. Furthermore, recent progress has refined the complexity analysis for ALM and tackled challenging integer programming instances. This review aims to offer a thorough understanding of ALM's benefits and limitations, exploring different ALM variants designed to enhance convergence and computational performance. We also illustrate effective algorithms for ALM subproblems across different types of optimization problems and highlight practical implementations in several fields.

math.OC↗

arXiv2025

An Augmented Lagrangian Value Function Method for Lower-level Constrained Stochastic Bilevel Optimization

Recently, lower-level constrained bilevel optimization has attracted increasing attention. However, existing methods mostly focus on either deterministic cases or problems with linear constraints. The main challenge in stochastic cases with general constraints is the bias and variance of the hyper-gradient, arising from the inexact solution of the lower-level problem. In this paper, we propose a novel stochastic augmented Lagrangian value function method for solving stochastic bilevel optimization problems with nonlinear lower-level constraints. Our approach reformulates the original bilevel problem using an augmented Lagrangian-based value function and then applies a penalized stochastic gradient method that carefully manages the noise from stochastic oracles. We establish an equivalence between the stochastic single-level reformulation and the original constrained bilevel problem and provide a non-asymptotic rate of convergence for the proposed method. The rate is further enhanced by employing variance reduction techniques. Extensive experiments on synthetic problems and real-world applications demonstrate the effectiveness of our approach.

math.OC↗

arXiv2025

SSNCVX: A primal-dual semismooth Newton method for convex composite optimization problem

In this paper, we propose a uniform semismooth Newton-based algorithmic framework called SSNCVX for solving a broad class of convex composite optimization problems. By exploiting the augmented Lagrangian duality, we reformulate the original problem into a saddle point problem and characterize the optimality conditions via a semismooth system of nonlinear equations. The nonsmooth structure is handled internally without requiring problem specific transformation or introducing auxiliary variables. This design allows easy modifications to the model structure, such as adding linear, quadratic, or shift terms through simple interface-level updates. The proposed method features a single loop structure that simultaneously updates the primal and dual variables via a semismooth Newton step. Extensive numerical experiments on benchmark datasets show that SSNCVX outperforms state-of-the-art solvers in both robustness and efficiency across a wide range of problems.

math.OC↗

arXiv2025

Numerical Optimization for Tensor Disentanglement

Tensor networks provide compact and scalable representations of high-dimensional data, enabling efficient computation in fields such as quantum physics, numerical partial differential equations (PDEs), and machine learning. This paper focuses on tensor disentangling, the task of identifying transformations that reduce bond dimensions by exploiting gauge freedom in the network. We formulate this task as an optimization problem over orthogonal matrices acting on a single tensor's indices, aiming to minimize the rank of its matricized form. We present Riemannian optimization methods and a joint optimization framework that alternates between optimizing the orthogonal transformation for a fixed low-rank approximation and optimizing the low-rank approximation for a fixed orthogonal transformation, offering a competitive alternative when the target rank is known. To seek the often unknown optimal rank, we introduce a binary search strategy integrated with the disentangling procedure. Numerical experiments on random tensors and tensors in an approximate isometric tensor network state are performed to compare different optimization methods and explore the possibility of combining different methods in a hybrid approach.

math.NA↗

arXiv2025

Accelerating Optimization via Differentiable Stopping Time

Optimization is an important module of modern machine learning applications. Tremendous efforts have been made to accelerate optimization algorithms. A common formulation is achieving a lower loss at a given time. This enables a differentiable framework with respect to the algorithm hyperparameters. In contrast, its dual, minimizing the time to reach a target loss, is believed to be non-differentiable, as the time is not differentiable. As a result, it usually serves as a conceptual framework or is optimized using zeroth-order methods. To address this limitation, we propose a differentiable stopping time and theoretically justify it based on differential equations. An efficient algorithm is designed to backpropagate through it. As a result, the proposed differentiable stopping time enables a new differentiable formulation for accelerating algorithms. We further discuss its applications, such as online hyperparameter tuning and learning to optimize. Our proposed methods show superior performance in comprehensive experiments across various problems, which confirms their effectiveness.

cs.LG↗