arXiv subjects

Qiming Dai

Publications and source records attributed to Qiming Dai.

4 recordsLinked to original sources

arXiv2026

The multiplier step size in classical two-block ADMM: convergence and counterexamples

How large can the multiplier step be in the classical two-block alternating direction method of multipliers (ADMM)? We keep the penalty fixed and use the usual primal updates. We consider finite-dimensional problems with closed proper convex objectives. We assume that a Karush-Kuhn-Tucker point exists and that each block subproblem attains its minimum at every step. Under these assumptions, the constraint images and the multiplier converge for a range of factors that extends beyond the golden ratio. The constraint matrices may be rank deficient. For larger steps, we construct two fixed compact polytopes and give an explicit threshold below two. The polytopes admit an infeasible periodic orbit for every factor at or above this threshold. At that threshold, ADMM can cycle even for smooth strongly convex objectives. This gives a negative answer to Glowinski's question about the full interval from zero to two. A different pair of piecewise-quadratic objectives gives geometrically growing residuals. For the general convex class, we locate the endpoint of the uniform convergence interval near 1.88688256. A convergence certificate on the unit circle gives the lower bound, while a separate periodic orbit gives the upper bound. Exact arithmetic verifies that the two bounds differ by less than 0.000000174.

math.OC↗

arXiv2026

FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence

Large language models can now generate complex, multi-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical challenge. Existing evaluation approaches largely depend on model-based natural-language judgments, which often overlook local reasoning gaps. While formal theorem provers like Lean offer a path to rigorous verification, using them to evaluate informal text requires solving locality and semantic mismatches: a prover might bypass a local flaw by proving an overly broad target, or validate an auto-formalized statement that drifts from the original mathematical intent. To address this, we introduce FaithSieve, a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs. FaithSieve decomposes coarse proof steps into local reasoning units, extracts typed proof obligations, and verifies them through a formal evaluation agent. Formal validation is gated by semantic alignment scoring, so Lean evidence is incorporated only when the formal statement faithfully preserves the context, objects, and logical form of the original claim. We construct two expert-verified datasets, ProofLoc-Olympiad and ProofLoc-University, to benchmark first-error localization. On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43% exact first-error accuracy, outperforming the direct-judging baseline of 72.29%. Furthermore, on the 200-problem ProofLoc-University benchmark spanning six advanced domains, FaithSieve reaches 84.5% exact accuracy, compared to 75.0% for the direct judge. Our work demonstrates that decomposing proofs into fine-grained units and grounding them with faithful formal evidence significantly improves reliable evaluation of natural-language reasoning.

cs.AI↗

arXiv2026

Non-Asymptotic Global Convergence of PPO-Clip

Reinforcement learning has gained attention for modern Large Language Model post-training. The actor-only variants of Proximal Policy Optimization (PPO) are widely applied for their efficiency. These algorithms incorporate a clipping mechanism to improve stability. Besides, a regularization term, such as the reverse KL-divergence or a more general $f$-divergence, is introduced to control excessive deviation from a reference policy. Despite their empirical success, a rigorous theoretical understanding of the problem and the algorithm's properties is limited. This paper advances the theoretical foundations of the PPO-Clip algorithm by analyzing a deterministic actor-only PPO algorithm within the general RL setting with $f$-divergence regularization under the softmax policy parameterization. We derive a non-uniform Lipschitz smoothness condition and a Łojasiewicz inequality for the considered problem. Based on these properties, we establish non-asymptotic global linear convergence in value gap for the forward KL regularizer. For the reverse KL regularizer, we derive global linear convergence from any finite softmax initialization in both value gap and squared policy distance.

math.OC↗

arXiv2024

A new perspective from hypertournaments to tournaments

A $k$-tournament $H$ on $n$ vertices is a pair $(V, A)$ for $2\leq k\leq n$, where $V(H)$ is a set of vertices, and $A(H)$ is a set of all possible $k$-tuples of vertices, such that for any $k$-subset $S$ of $V$, $A(H)$ contains exactly one of the $k!$ possible permutations of $S$. In this paper, we investigate the relationship between a hyperdigraph and its corresponding normal digraph. Particularly, drawing on a result from Gutin and Yeo, we establish an intrinsic relationship between a strong $k$-tournament and a strong tournament, which enables us to provide an alternative (more straightforward and concise) proof for some previously known results and get some new results.

math.CO↗