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

Zhengfeng Yang

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

ResearcherUnclaimed source record
Symbolic ComputationSoftware Engineeringmath.OCArtificial IntelligenceMachine Learning

Catalog footprint

What is connected

7works
5topics
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

7 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
preprint2026arXiv

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Domain-of-Attraction Estimation for Uncertain Non-polynomial Systems

In this paper, we consider the problem of computing estimates of the domain-of-attraction for non-polynomial systems. A polynomial approximation technique, based on multivariate polynomial interpolation and error analysis for remaining functions, is applied to compute an uncertain polynomial system, whose set of trajectories contains that of the original non-polynomial system. Experiments on the benchmark non-polynomial systems show that our approach gives better estimates of the domain-of-attraction.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Exact Safety Verification of Interval Hybrid Systems Based on Symbolic-Numeric Computation

In this paper, we address the problem of safety verification of interval hybrid systems in which the coefficients are intervals instead of explicit numbers. A hybrid symbolic-numeric method, based on SOS relaxation and interval arithmetic certification, is proposed to generate exact inequality invariants for safety verification of interval hybrid systems. As an application, an approach is provided to verify safety properties of non-polynomial hybrid systems. Experiments on the benchmark hybrid systems are given to illustrate the efficiency of our method.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation

In this paper, we address the problem of safety verification of nonlinear hybrid systems. A hybrid symbolic-numeric method is presented to compute exact inequality invariants of hybrid systems efficiently. Some numerical invariants of a hybrid system can be obtained by solving a bilinear SOS programming via PENBMI solver or iterative method, then the modified Newton refinement and rational vector recovery techniques are applied to obtain exact polynomial invariants with rational coefficients, which {\it exactly} satisfy the conditions of invariants. Experiments on some benchmarks are given to illustrate the efficiency of our algorithm.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Exact Safety Verification of Hybrid Systems Using Sums-Of-Squares Representation

In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is deployed to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Generating Loop Invariants by Computing Vanishing Ideals of Sample Points

Loop invariants play a very important role in proving correctness of programs. In this paper, we address the problem of generating invariants of polynomial loop programs. We present a new approach, for generating polynomial equation invariants of polynomial loop programs through computing vanishing ideals of sample points. We apply rational function interpolation, based on early termination technique, to generate invariants of loop programs with symbolic initial values. Our approach avoids first-order quantifier elimination and cylindrical algebraic decomposition(CAD). An algorithm for generating polynomial invariants is proposed and some examples are given to illustrate the algorithm. Furthermore, we demonstrate on a set of loop programs with symbolic initial values that our algorithm can yield polynomial invariants with degrees high up to 15.

0 citations0 reviewsNo code linkedOpen access