BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Lihong Zhi

Lihong Zhi appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
math.OCmath.NAmath.OANumerical AnalysisSystems and ControlMachine Learningmath-phmath.AGmath.FAmath.MP

Catalog footprint

What is connected

13works
10topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

13 published item(s)

preprint2026arXiv

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberger (WZ) method can achieve a mechanized proof of combinatorial identities by constructing special auxiliary functions and demonstrating that they satisfy specific recurrence relations. We propose WZ-LLM, a neuro-symbolic framework that turns WZ proof plans into executable proof sketches in Lean 4 and uses an LLM-based prover to discharge the resulting machine-checkable subgoals. We also train a dedicated WZ-Prover via a Lean-kernel-verified bootstrapping loop with expert-verified iteration, followed by DAPO-based refinement. Experiments show that WZ-LLM achieves a 34% proof success rate on LCI-Test (100 classic combinatorial identities), outperforming strong baselines such as DeepSeek-V3 and Goedel-Prover-V2, and delivering consistent gains on CombiBench and PutnamBench-Comb. These results indicate that our framework provides two complementary strengths: improved direct proving for identities beyond the scope of WZ, and substantially higher end-to-end success when WZ sketches guide a specialized prover.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Extensions of S-Lemma for Noncommutative Polynomials

We consider the problem of extending the classical S-lemma from commutative case to noncommutative cases. We show that a symmetric quadratic homogeneous matrix-valued polynomial is positive semidefinite if and only if its coefficient matrix is positive semidefinite. Then we extend the S-lemma to three kinds of noncommutative polynomials: noncommutative polynomials whose coefficients are real numbers, matrix-valued noncommutative polynomials and hereditary polynomials.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Synthesizing Invariant Clusters for Polynomial Programs by Semidefinite Programming

In this paper, we present a novel approach to synthesize invariant clusters for polynomial programs. An invariant cluster is a set of program invariants that share a common structure, which could, for example, be used to save the needs for repeatedly synthesizing new invariants when the specifications and programs are evolving. To that end, we search for sets of parameters $R_k$ w.r.t. a parameterized multivariate polynomial $I(a, x)$ (i.e. a template) such that $I(a, x) \leq 0$ is a valid program invariant for all $a \in R_k$. Instead of using time-consuming symbolic routines such as quantifier eliminations, we show that such sets of parameters can be synthesized using a hierarchy of semidefinite programming (SDP). Moreover, we show that, under some standard non-degenerate assumptions, almost all possible valid parameters can be included in the synthesized sets. Such kind of completeness result has previously only been provided by symbolic approaches. Further extensions such as using semialgebraic and general algebraic templates (instead of polynomial ones) and allowing non-polynomial continuous functions in programs are also discussed.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

On quantum Strassen's theorem

Strassen's theorem circa 1965 gives necessary and sufficient conditions on the existence of a probability measure on two product spaces with given support and two marginals. In the case where each product space is finite Strassen's theorem is reduced to a linear programming problem which can be solved using flow theory. A density matrix of bipartite quantum system is a quantum analog of a probability matrix on two finite product spaces. Partial traces of the density matrix are analogs of marginals. The support of the density matrix is its range. The analog of Strassen's theorem in this case can be stated and solved using semidefinite programming. The aim of this paper is to give analogs of Strassen's theorem to density trace class operators on a product of two separable Hilbert spaces, where at least one of the Hilbert spaces is infinite dimensional.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Symmetric Tensor Decompositions On Varieties

This paper discusses the problem of symmetric tensor decomposition on a given variety $X$: decomposing a symmetric tensor into the sum of tensor powers of vectors contained in $X$. In this paper, we first study geometric and algebraic properties of such decomposable tensors, which are crucial to the practical computations of such decompositions. For a given tensor, we also develop a criterion for the existence of a symmetric decomposition on $X$. Secondly and most importantly, we propose a method for computing symmetric tensor decompositions on an arbitrary $X$. As a specific application, Vandermonde decompositions for nonsymmetric tensors can be computed by the proposed algorithm.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Lifts of Non-compact Convex Sets and Cone Factorizations

In this paper we generalize the factorization theorem of Gouveia, Parrilo and Thomas to a broader class of convex sets. Given a general convex set, we define a slack operator associated to the set and its polar according to whether the convex set is full dimensional, whether it is a translated cone and whether it contains lines. We strengthen the condition of a cone lift by requiring not only the convex set is the image of an affine slice of a given closed convex cone, but also its recession cone is the image of the linear slice of the closed convex cone. We show that the generalized lift of a convex set can also be characterized by the cone factorization of a properly defined slack operator.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Semidefinite representations of non-compact convex sets

We consider the problem of the semidefinite representation of a class of non-compact basic semialgebraic sets. We introduce the conditions of pointedness and closedness at infinity of a semialgebraic set and show that under these conditions our modified hierarchies of nested theta bodies and Lasserre's relaxations converge to the closure of the convex hull of $S$. Moreover, if the PP-BDR property is satisfied, our theta body and Lasserre's relaxation are exact when the order is large enough; if the PP-BDR property does not hold, our hierarchies convergent uniformly to the closure of the convex hull of $S$ restricted to every fixed ball centered at the origin. We illustrate through a set of examples that the conditions of pointedness and closedness are essential to ensure the convergence. Finally, we provide some strategies to deal with cases where the conditions of pointedness and closedness are violated.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

A certificate for semidefinite relaxations in computing positive dimensional real varieties

For an ideal I with a positive dimensional real variety, based on moment relaxations, we study how to compute a Pommaret basis which is simultaneously a Groebner basis of an ideal J generated by the kernel of a truncated moment matrix and nesting between I and its real radical ideal. We provide a certificate consisting of a condition on coranks of moment matrices for terminating the algorithm. For a generic delta-regular coordinate system, we prove that the condition is satisfiable in a large enough order of moment relaxations.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Certificates of Impossibility of Hilbert-Artin Representations of a Given Degree for Definite Polynomials and Functions

We deploy numerical semidefinite programming and conversion to exact rational inequalities to certify that for a positive semidefinite input polynomial or rational function, any representation as a fraction of sums-of-squares of polynomials with real coefficients must contain polynomials in the denominator of degree no less than a given input lower bound. By Artin's solution to Hilbert's 17th problems, such representations always exist for some denominator degree. Our certificates of infeasibility are based on the generalization of Farkas's Lemma to semidefinite programming. The literature has many famous examples of impossibility of SOS representability including Motzkin's, Robinson's, Choi's and Lam's polynomials, and Reznick's lower degree bounds on uniform denominators, e.g., powers of the sum-of-squares of each variable. Our work on exact certificates for positive semidefiniteness allows for non-uniform denominators, which can have lower degree and are often easier to convert to exact identities. Here we demonstrate our algorithm by computing certificates of impossibilities for an arbitrary sum-of-squares denominator of degree 2 and 4 for some symmetric sextics in 4 and 5 variables, respectively. We can also certify impossibility of base polynomials in the denominator of restricted term structure, for instance as in Landau's reduction by one less variable.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Verified Error Bounds for Isolated Singular Solutions of Polynomial Systems

In this paper, we generalize the algorithm described by Rump and Graillat, as well as our previous work on certifying breadth-one singular solutions of polynomial systems, to compute verified and narrow error bounds such that a slightly perturbed system is guaranteed to possess an isolated singular solution within the computed bounds. Our new verification method is based on deflation techniques using smoothing parameters. We demonstrate the performance of the algorithm for systems with singular solutions of multiplicity up to hundreds.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Verified Error Bounds for Isolated Singular Solutions of Polynomial Systems: Case of Breadth One

In this paper we describe how to improve the performance of the symbolic-numeric method in (Li and Zhi,2009, 2011) for computing the multiplicity structure and refining approximate isolated singular solutions in the breadth one case. By introducing a parameterized and deflated system with smoothing parameters, we generalize the algorithm in (Rump and Graillat, 2009) to compute verified error bounds such that a slightly perturbed polynomial system is guaranteed to have a breadth-one multiple root within the computed bounds.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Computing Isolated Singular Solutions of Polynomial Systems: Case of Breadth One

We present a symbolic-numeric method to refine an approximate isolated singular solution $\hat{\mathbf{x}}=(\hat{x}_{1}, ..., \hat{x}_{n})$ of a polynomial system $F=\{f_1, ..., f_n\}$ when the Jacobian matrix of $F$ evaluated at $\hat{\mathbf{x}}$ has corank one approximately. Our new approach is based on the regularized Newton iteration and the computation of approximate Max Noether conditions satisfied at the approximate singular solution. The size of matrices involved in our algorithm is bounded by $n \times n$. The algorithm converges quadratically if $\hat{\xx}$ is close to the isolated exact singular solution.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

The Minimum-Rank Gram Matrix Completion via Modified Fixed Point Continuation Method

The problem of computing a representation for a real polynomial as a sum of minimum number of squares of polynomials can be casted as finding a symmetric positive semidefinite real matrix (Gram matrix) of minimum rank subject to linear equality constraints. In this paper, we propose algorithms for solving the minimum-rank Gram matrix completion problem, and show the convergence of these algorithms. Our methods are based on the modified fixed point continuation (FPC) method. We also use the Barzilai-Borwein (BB) technique and a specific linear combination of two previous iterates to accelerate the convergence of modified FPC algorithms. We demonstrate the effectiveness of our algorithms for computing approximate and exact rational sum of squares (SOS) decompositions of polynomials with rational coefficients.

0 citations0 reviewsNo code linkedOpen access