arXiv subjects

Zhengfeng Yang

Publications and source records attributed to Zhengfeng Yang.

At least 19 recordsLinked to original sources

arXiv2026

A Proof of the Dittert Conjecture in Dimension 4 via an Exact Constrained Sum-of-Squares Certificate

The Dittert conjecture states that the Dittert functional on nonnegative $n\times n$ matrices whose entries sum to $n$ is uniquely maximized by the uniform matrix. We prove the conjecture in dimension $4$. More precisely, let $K_4$ be the simplex of nonnegative $4\times4$ real matrices whose entries sum to $4$, let $U_4$ be the uniform matrix, and let $\phi$ denote the Dittert functional. We establish $\frac{61}{32}-\phi(A)\ge \frac{1}{52}\|A-U_4\|_F^2$ for every $A\in K_4$. Consequently, $U_4$ is the unique maximizer of $\phi$ on $K_4$. The proof reduces the problem to an exact certification of the nonnegativity of a structured quartic polynomial in sixteen variables on a simplex. We develop a symbolic-numeric procedure for constructing an exact rational constrained sum-of-squares certificate. The procedure combines adaptive template selection with sequential rational recovery to handle singular Gram matrices and coupled SOS blocks arising from the constraint structure. The final certificate consists of a main SOS with $152$ positively weighted rational squares and $136$ smaller SOS blocks, each containing $16$ such squares. Exact $LDL^T$ decompositions and coefficient comparison over $\mathbb{Q}$ certify the polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.

cs.SC↗

arXiv2026

Richer Representations for Neural Algorithmic Reasoning via Auxiliary Reconstruction

Neural algorithmic reasoning has emerged as a popular research direction. It aims to train neural networks to mimic the step-by-step behavior of classical rule-based algorithms. More specifically, the execution of such algorithms can be abstracted as a sequence of states, where each state represents the intermediate outcome after an execution step. The training objective is to generate state sequences that replicate the underlying algorithmic process. A common framework for this task adopts an encoder-processor-decoder architecture, where the encoder learns representations of states, the processor simulates algorithmic steps, and the decoder reconstructs output states. While prior work has focused on improving the processor, the role of the encoder in representation learning has received little attention. Most methods rely on simple MLP encoders, raising the question of whether such representations are sufficiently informative for supporting algorithmic reasoning. This paper investigates how to improve encoder representations for neural algorithmic reasoning. We propose a reconstruction module that aims to recover the input state from its encoded representation. This auxiliary reconstruction task encourages the encoder to retain critical information about the input. We demonstrate that incorporating this task during training improves the performance of existing neural architectures on standard benchmarks. Furthermore, we observe that current encoders often underutilize the correlations among features within a state. To address this, we draw inspiration from self-supervised learning and design an enhanced variant of the auxiliary task that encourages the encoder to capture intra-state feature dependencies. Experimental results show that our method enables the encoder to learn richer representations, thereby enhancing the performance of existing processors on algorithmic reasoning tasks.

cs.LG↗

arXiv2026

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.

cs.AI↗

arXiv2026

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.

cs.LG↗

arXiv2025

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

Neurosymbolic approaches integrating large language models with formal reasoning have recently achieved human-level performance on mathematics competition problems in algebra, geometry and number theory. In comparison, combinatorics remains a challenging domain, characterized by a lack of appropriate benchmarks and theorem libraries. To address this gap, we introduce CombiBench, a comprehensive benchmark comprising 100 combinatorial problems, each formalized in Lean~4 and paired with its corresponding informal statement. The problem set covers a wide spectrum of difficulty levels, ranging from middle school to IMO and university level, and span over ten combinatorial topics. CombiBench is suitable for testing IMO solving capabilities since it includes all IMO combinatorial problems since 2000 (except IMO 2004 P3 as its statement contain an images). Furthermore, we provide a comprehensive and standardized evaluation framework, dubbed Fine-Eval (for $\textbf{F}$ill-in-the-blank $\textbf{in}$ L$\textbf{e}$an Evaluation), for formal mathematics. It accommodates not only proof-based problems but also, for the first time, the evaluation of fill-in-the-blank questions. Using Fine-Eval as the evaluation method and Kimina Lean Server as the backend, we benchmark several LLMs on CombiBench and observe that their capabilities for formally solving combinatorial problems remain limited. Among all models tested (none of which has been trained for this particular task), Kimina-Prover attains the best results, solving 7 problems (out of 100) under both ``with solution'' and ``without solution'' scenarios. We open source the benchmark dataset alongside with the code of the proposed evaluation method at https://github.com/MoonshotAI/CombiBench/.

cs.AI↗

arXiv2025

Automated Proof of Polynomial Inequalities via Reinforcement Learning

Polynomial inequality proving is fundamental to many mathematical disciplines and finds wide applications in diverse fields. Current traditional algebraic methods are based on searching for a polynomial positive definite representation over a set of basis. However, these methods are limited by truncation degree. To address this issue, this paper proposes an approach based on reinforcement learning to find a {Krivine-basis} representation for proving polynomial inequalities. Specifically, we formulate the inequality proving problem as a linear programming (LP) problem and encode it as a basis selection problem using reinforcement learning (RL), achieving a non-negative {Krivine basis}. Moreover, a fast multivariate polynomial multiplication method based on Fast Fourier Transform (FFT) is employed to enhance the efficiency of action space search. Furthermore, we have implemented a tool called {APPIRL} (Automated Proof of Polynomial Inequalities via Reinforcement Learning). Experimental evaluation on benchmark problems demonstrates the feasibility and effectiveness of our approach. In addition, {APPIRL} has been successfully applied to solve the maximum stable set problem.

cs.LG↗

arXiv2025

A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation

Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone of mathematics, provides essential tools for analyzing discrete structures and solving optimization problems. However, its inherent complexity makes it particularly challenging for automated theorem proving (ATP) for combinatorial identities. To address this, we manually construct LeanComb, combinatorial identities benchmark in Lean, which is, to our knowledge, the first formalized theorem proving benchmark built for combinatorial identities. We develop an Automated Theorem Generator for Combinatorial Identities, ATG4CI, which combines candidate tactics suggested by a self-improving large language model with a Reinforcement Learning Tree Search approach for tactic prediction. By utilizing ATG4CI, we generate a LeanComb-Enhanced dataset comprising 260K combinatorial identities theorems, each with a complete formal proof in Lean, and experimental evaluations demonstrate that models trained on this dataset can generate more effective tactics, thereby improving success rates in automated theorem proving for combinatorial identities.

cs.AI↗

arXiv2025

CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization

Automated theorem proving (ATP) is one of the most challenging mathematical reasoning tasks for Large Language Models (LLMs). Most existing LLM-based ATP methods rely on supervised fine-tuning, which results in a limited alignment between the theorem proving process and human preferences. Direct Preference Optimization (DPO), which aligns LLMs with human preferences, has shown positive effects for certain tasks. However, the lack of high-quality preference data for theorem proving presents a significant challenge. In this paper, we innovatively apply DPO to formal automated theorem proving and introduces a Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP) method. Specifically, we propose a method for constructing preference data which utilizes LLMs and existing theorem proving data to enhance the diversity of the preference data while reducing the reliance on human preference annotations. We then integrate this preference data construction method with curriculum learning to iteratively fine-tune the theorem proving model through DPO. Experimental results on the MiniF2F and ProofNet datasets demonstrate the effectiveness of the proposed method.

cs.AI↗

arXiv2024

Open-Book Neural Algorithmic Reasoning

Neural algorithmic reasoning is an emerging area of machine learning that focuses on building neural networks capable of solving complex algorithmic tasks. Recent advancements predominantly follow the standard supervised learning paradigm -- feeding an individual problem instance into the network each time and training it to approximate the execution steps of a classical algorithm. We challenge this mode and propose a novel open-book learning framework. In this framework, whether during training or testing, the network can access and utilize all instances in the training dataset when reasoning for a given instance. Empirical evaluation is conducted on the challenging CLRS Algorithmic Reasoning Benchmark, which consists of 30 diverse algorithmic tasks. Our open-book learning framework exhibits a significant enhancement in neural reasoning capabilities. Further, we notice that there is recent literature suggesting that multi-task training on CLRS can improve the reasoning accuracy of certain tasks, implying intrinsic connections between different algorithmic tasks. We delve into this direction via the open-book framework. When the network reasons for a specific task, we enable it to aggregate information from training instances of other tasks in an attention-based manner. We show that this open-book attention mechanism offers insights into the inherent relationships among various tasks in the benchmark and provides a robust tool for interpretable multi-task training.

cs.LG↗

arXiv2024

A Context-Enhanced Framework for Sequential Graph Reasoning

The paper studies sequential reasoning over graph-structured data, which stands as a fundamental task in various trending fields like automated math problem solving and neural graph algorithm learning, attracting a lot of research interest. Simultaneously managing both sequential and graph-structured information in such tasks presents a notable challenge. Over recent years, many neural architectures in the literature have emerged to tackle the issue. In this work, we generalize the existing architectures and propose a context-enhanced framework. The crucial innovation is that the reasoning of each step does not only rely on the outcome of the preceding step but also leverages the aggregation of information from more historical outcomes. The idea stems from our observation that in sequential graph reasoning, each step's outcome has a much stronger inner connection with each other compared to traditional seq-to-seq tasks. We show that the framework can effectively integrate with the existing methods, enhancing their reasoning abilities. Empirical evaluations are conducted on the challenging CLRS Reasoning Benchmark, and the results demonstrate that the proposed framework significantly improves the performance of existing architectures, yielding state-of-the-art results across the majority of the datasets within the benchmark.

cs.AI↗

arXiv2024

Learning to Select Cutting Planes in Mixed Integer Linear Programming Solving

Cutting planes (cuts) are crucial for solving Mixed Integer Linear Programming (MILP) problems. Advanced MILP solvers typically rely on manually designed heuristic algorithms for cut selection, which require much expert experience and cannot be generalized for different scales of MILP problems. Therefore, learning-based methods for cut selection are considered a promising direction. State-of-the-art learning-based methods formulate cut selection as a sequence-to-sequence problem, easily handled by sequence models. However, the existing sequence models need help with the following issues: (1) the model only captures cut information while neglecting the Linear Programming (LP) relaxation; (2) the sequence model utilizes positional information of the input sequence, which may influence cut selection. To address these challenges, we design a novel learning model HGTSM for better select cuts. We encode MILP problem state as a heterogeneous tripartite graph, utilizing heterogeneous graph networks to fully capture the underlying structure of MILP problems. Simultaneously, we propose a novel sequence model whose architecture is tailored to handle inputs in different orders. Experimental results demonstrate that our model outperforms heuristic methods and learning-based baselines on multiple challenging MILP datasets. Additionally, the model exhibits stability and the ability to generalize to different types of problems.

math.OC↗

arXiv2024

Algebraic Curve Interpolation for Intervals via Symbolic-Numeric Computation

Algebraic curve interpolation is described by specifying the location of N points in the plane and constructing an algebraic curve of a function f that should pass through them. In this paper, we propose a novel approach to construct the algebraic curve that interpolates a set of data (points or neighborhoods). This approach aims to search the polynomial with the smallest degree interpolating the given data. Moreover, the paper also presents an efficient method to reconstruct the algebraic curve of integer coefficients with the smallest degree and the least monomials that interpolates the provided data. The problems are converted into optimization problems and are solved via Lagrange multipliers methods and symbolic computation. Various examples are presented to illustrate the proposed approaches.

math.GM↗

arXiv2022

Efficient and Accurate Quantized Image Super-Resolution on Mobile NPUs, Mobile AI & AIM 2022 challenge: Report

Image super-resolution is a common task on mobile and IoT devices, where one often needs to upscale and enhance low-resolution images and video frames. While numerous solutions have been proposed for this problem in the past, they are usually not compatible with low-power mobile NPUs having many computational and memory constraints. In this Mobile AI challenge, we address this problem and propose the participants to design an efficient quantized image super-resolution solution that can demonstrate a real-time performance on mobile NPUs. The participants were provided with the DIV2K dataset and trained INT8 models to do a high-quality 3X image upscaling. The runtime of all models was evaluated on the Synaptics VS680 Smart Home board with a dedicated edge NPU capable of accelerating quantized neural networks. All proposed solutions are fully compatible with the above NPU, demonstrating an up to 60 FPS rate when reconstructing Full HD resolution images. A detailed description of all models developed in the challenge is provided in this paper.

eess.IV↗

arXiv2017

Layered material GeSe and vertical GeSe/MoS2 p-n heterojunctions

Group-IV monochalcogenides are emerging as a new class of layered materials beyond graphene, transition metal dichalcogenides (TMDCs), and black phosphorus (BP). In this paper, we report experimental and theoretical investigations of the band structure and transport properties of GeSe and its heterostructures. We find that GeSe exhibits a markedly anisotropic electronic transport, with maximum conductance along the armchair direction. Density functional theory calculations reveal that the effective mass is 2.7 times larger along the zigzag direction than the armchair direction; this mass anisotropy explains the observed anisotropic conductance. The crystallographic orientation of GeSe is confirmed by angleresolved polarized Raman measurements, which are further supported by calculated Raman tensors for the orthorhombic structure. Novel GeSe/MoS2 p-n heterojunctions are fabricated, combining the natural p-type doping in GeSe and n-type doping in MoS2. The temperature dependence of the measured junction current reveals that GeSe and MoS2 have a type-II band alignment with a conduction band offset of ~0.234 eV. The anisotropic conductance of GeSe may enable the development of new electronic and optoelectronic devices, such as high-efficiency thermoelectric devices and plasmonic devices with resonance frequency continuously tunable through light polarization direction. The unique GeSe/MoS2 p-n junctions with type-II alignment may become essential building blocks of vertical tunneling field-effect transistors for low-power applications. The novel p-type layered material GeSe can also be combined with n-type TMDCs to form heterogeneous complementary metal oxide semiconductor (CMOS) circuits.

cond-mat.mes-hall↗

arXiv2013

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.

cs.SC↗

arXiv2013

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.

cs.SC↗

arXiv2012

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.

cs.SE↗