arXiv subjects

Zeyu Zheng

Publications and source records attributed to Zeyu Zheng.

At least 73 records · Page 4Linked to original sources

arXiv2025

Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

The integration of Large Language Models (LLMs) into automated theorem proving has shown immense promise, yet is fundamentally constrained by challenges in scaling up both training-time reinforcement learning (RL) and inference-time compute. This paper introduces \texttt{BFS-Prover-V2}, a system designed to address this dual scaling problem. We present two primary innovations. The first is a novel multi-turn off-policy RL framework for continually improving the performance of LLM step-prover at training time. This framework, inspired by the principles of AlphaZero, utilizes a multi-stage expert iteration pipeline featuring adaptive tactic-level data filtering and periodic retraining to surmount the performance plateaus that typically curtail long-term RL in LLM-based agents. The second innovation is a planner-enhanced multi-agent search architecture that scales reasoning capabilities at inference time. This architecture employs a general reasoning model as a high-level planner to iteratively decompose complex theorems into a sequence of simpler subgoals. This hierarchical approach substantially reduces the search space, enabling a team of parallel prover agents to collaborate efficiently by leveraging a shared proof cache. We demonstrate that this dual approach to scaling yields state-of-the-art results on established formal mathematics benchmarks. \texttt{BFS-Prover-V2} achieves 95.08\% and 41.4\% on the MiniF2F and ProofNet test sets respectively. While demonstrated in the domain of formal mathematics, the RL and inference techniques presented in this work are of broader interest and may be applied to other domains requiring long-horizon multi-turn reasoning and complex search.

cs.AI↗

arXiv2025

An Energy-Efficient Edge Coprocessor for Neural Rendering with Explicit Data Reuse Strategies

Neural radiance fields (NeRF) have transformed 3D reconstruction and rendering, facilitating photorealistic image synthesis from sparse viewpoints. This work introduces an explicit data reuse neural rendering (EDR-NR) architecture, which reduces frequent external memory accesses (EMAs) and cache misses by exploiting the spatial locality from three phases, including rays, ray packets (RPs), and samples. The EDR-NR architecture features a four-stage scheduler that clusters rays on the basis of Z-order, prioritize lagging rays when ray divergence happens, reorders RPs based on spatial proximity, and issues samples out-of-orderly (OoO) according to the availability of on-chip feature data. In addition, a four-tier hierarchical RP marching (HRM) technique is integrated with an axis-aligned bounding box (AABB) to facilitate spatial skipping (SS), reducing redundant computations and improving throughput. Moreover, a balanced allocation strategy for feature storage is proposed to mitigate SRAM bank conflicts. Fabricated using a 40 nm process with a die area of 10.5 mmX, the EDR-NR chip demonstrates a 2.41X enhancement in normalized energy efficiency, a 1.21X improvement in normalized area efficiency, a 1.20X increase in normalized throughput, and a 53.42% reduction in on-chip SRAM consumption compared to state-of-the-art accelerators.

eess.IV↗

arXiv2025

Joint Optimization and Statistical Inference for Zero-th Order Simulation Optimization

We consider stochastic optimization problems with the dual tasks of (i) effectively finding the optimizer and (ii) reliably conducting statistical inference for the optimal objective function value. We find that classical simulation optimization and stochastic optimization algorithms, despite of their fast convergence rates to the optimizer under strong convexity assumptions, may not come with a valid central limit theorem (CLT) with a vanishing bias. This non-vanishing bias can harm statistical inference and the construction of asymptotically valid confidence intervals. We fix this issue by providing a new stochastic optimization algorithm that on one hand maintains the same fast convergence rate and on the other hand permits the establishment of a valid CLT with vanishing bias. We discuss practical implementations of the proposed algorithm and conduct numerical experiments to illustrate the theoretical findings.

stat.ME↗

arXiv2025

OpenVision 2: A Family of Generative Pretrained Visual Encoders for Multimodal Learning

This paper provides a simplification on OpenVision's architecture and loss design for enhancing its training efficiency. Following the prior vision-language pretraining works CapPa and AIMv2, as well as modern multimodal designs like LLaVA, our changes are straightforward: we remove the text encoder (and therefore the contrastive loss), retaining only the captioning loss as a purely generative training signal. We name this new version OpenVision 2. The initial results are promising: despite this simplification, OpenVision 2 competitively matches the original model's performance on a broad set of multimodal benchmarks while substantially cutting both training time and memory consumption. For example, with ViT-L/14, it reduces training time by about 1.5x (from 83h to 57h), and memory usage by about 1.8x (from 24.5GB to 13.8GB, equivalently allowing the maximum batch size to grow from 2k to 8k). This superior training efficiency also allows us to scale far beyond the largest vision encoder used in OpenVision, reaching more than 1 billion parameters. We hold a strong belief that this lightweight, generative-only paradigm is compelling for future vision encoder development in multimodal foundation models.

cs.CV↗

arXiv2025

Controllable Coupled Image Generation via Diffusion Models

We provide an attention-level control method for the task of coupled image generation, where "coupled" means that multiple simultaneously generated images are expected to have the same or very similar backgrounds. While backgrounds coupled, the centered objects in the generated images are still expected to enjoy the flexibility raised from different text prompts. The proposed method disentangles the background and entity components in the model's cross-attention modules, attached with a sequence of time-varying weight control parameters depending on the time step of sampling. We optimize this sequence of weight control parameters with a combined objective that assesses how coupled the backgrounds are as well as text-to-image alignment and overall visual quality. Empirical results demonstrate that our method outperforms existing approaches across these criteria.

cs.CV↗

arXiv2025

Efficient Fine-Grained Guidance for Diffusion Model Based Symbolic Music Generation

Developing generative models to create or conditionally create symbolic music presents unique challenges due to the combination of limited data availability and the need for high precision in note pitch. To address these challenges, we introduce an efficient Fine-Grained Guidance (FGG) approach within diffusion models. FGG guides the diffusion models to generate music that aligns more closely with the control and intent of expert composers, which is critical to improve the accuracy, listenability, and quality of generated music. This approach empowers diffusion models to excel in advanced applications such as improvisation, and interactive music creation. We derive theoretical characterizations for both the challenges in symbolic music generation and the effects of the FGG approach. We provide numerical experiments and subjective evaluation to demonstrate the effectiveness of our approach. We have published a demo page to showcase performances, which enables real-time interactive generation.

cs.SD↗

arXiv2025

IDA-Bench: Evaluating LLMs on Interactive Guided Data Analysis

Large Language Models (LLMs) show promise as data analysis agents, but existing benchmarks overlook the iterative nature of the field, where experts' decisions evolve with deeper insights of the dataset. To address this, we introduce IDA-Bench, a novel benchmark evaluating LLM agents in multi-round interactive scenarios. Derived from complex Kaggle notebooks, tasks are presented as sequential natural language instructions by an LLM-simulated user. Agent performance is judged by comparing its final numerical output to the human-derived baseline. Initial results show that even state-of-the-art coding agents (like Claude-3.7-thinking) succeed on < 50% of the tasks, highlighting limitations not evident in single-turn tests. This work underscores the need to improve LLMs' multi-round capabilities for building more reliable data analysis agents, highlighting the necessity of achieving a balance between instruction following and reasoning.

cs.CL↗

arXiv2025

The generalized trifference problem

We study the problem of finding the largest number $T(n, m)$ of ternary vectors of length $n$ such that for any three distinct vectors there are at least $m$ coordinates where they pairwise differ. For $m = 1$, this is the classical trifference problem which is wide open. We prove upper and lower bounds on $T(n, m)$ for various ranges of the parameter $m$ and determine the phase transition threshold on $m=m(n)$ where $T(n, m)$ jumps from constant to exponential in $n$. By relating the linear version of this problem to a problem on blocking sets in finite geometry, we give explicit constructions and probabilistic lower bounds. We also compute the exact values of this function and its linear variation for small parameters.

math.CO↗

arXiv2025

A Regeneration-based a Posteriori Error Bound for a Markov Chain Stationary Distribution Truncation Algorithm

When the state space of a discrete state space positive recurrent Markov chain is infinite or very large, it becomes necessary to truncate the state space in order to facilitate numerical computation of the stationary distribution. This paper develops a new approach for bounding the truncation error that arises when computing approximations to the stationary distribution. This rigorous a posteriori error bound exploits the regenerative structure of the chain and assumes knowledge of a Lyapunov function. Because the bound is a posteriori (and leverages the computations done to calculate the stationary distribution itself), it tends to be much tighter than a priori bounds. The bound decomposes the regenerative cycle into a random number of excursions from a set $K$ defined in terms of the Lyapunov function into the complement of the truncation set $A$. The bound can be easily computed, and does not (for example) involve a linear program, as do some other error bounds.

math.PR↗

arXiv2025

Approximation of Markov Chain Expectations and the Key Role of Stationary Distribution Convergence

Consider a sequence $P_n$ of positive recurrent transition matrices or kernels that approximate a limiting infinite state matrix or kernel $P_{\infty}$. Such approximations arise naturally when one truncates an infinite state Markov chain and replaces it with a finite state approximation. It also describes the situation in which $P_{\infty}$ is a simplified limiting approximation to $P_n$ when $n$ is large. In both settings, it is often verified that the approximation $P_n$ has the characteristic that its stationary distribution $π_n$ converges to the stationary distribution $π_{\infty}$ associated with the limit. In this paper, we show that when the state space is countably infinite, this stationary distribution convergence implies that $P_n^m$ can be approximated uniformly in $m$ by $P_{\infty}^m$ when n is large. We show that this ability to approximate the marginal distributions at all time scales $m$ fails in continuous state space, but is valid when the convergence is in total variation or when we have weak convergence and the kernels are suitably Lipschitz. When the state space is discrete (as in the truncation setting), we further show that stationary distribution convergence also implies that all the expectations that are computable via first transition analysis (e.g. mean hitting times, expected infinite horizon discounted rewards) converge to those associated with the limit $P_{\infty}$. Simply put, we show that once one has established stationary distribution convergence, one immediately can infer convergence for a huge range of other expectations.

math.PR↗

arXiv2025

Collaborative Bayesian Optimization via Wasserstein Barycenters

Motivated by the growing need for black-box optimization and data privacy, we introduce a collaborative Bayesian optimization (BO) framework that addresses both of these challenges. In this framework agents work collaboratively to optimize a function they only have oracle access to. In order to mitigate against communication and privacy constraints, agents are not allowed to share their data but can share their Gaussian process (GP) surrogate models. To enable collaboration under these constraints, we construct a central model to approximate the objective function by leveraging the concept of Wasserstein barycenters of GPs. This central model integrates the shared models without accessing the underlying data. A key aspect of our approach is a collaborative acquisition function that balances exploration and exploitation, allowing for the optimization of decision variables collaboratively in each iteration. We prove that our proposed algorithm is asymptotically consistent and that its implementation via Monte Carlo methods is numerically accurate. Through numerical experiments, we demonstrate that our approach outperforms other baseline collaborative frameworks and is competitive with centralized approaches that do not consider data privacy.

cs.LG↗

arXiv2025

Improving LLM Interpretability and Performance via Guided Embedding Refinement for Sequential Recommendation

The fast development of Large Language Models (LLMs) offers growing opportunities to further improve sequential recommendation systems. Yet for some practitioners, integrating LLMs to their existing base recommendation systems raises questions about model interpretability, transparency and related safety. To partly alleviate challenges from these questions, we propose guided embedding refinement, a method that carries out a guided and interpretable usage of LLM to enhance the embeddings associated with the base recommendation system. Instead of directly using LLMs as the backbone of sequential recommendation systems, we utilize them as auxiliary tools to emulate the sales logic of recommendation and generate guided embeddings that capture domain-relevant semantic information on interpretable attributes. Benefiting from the strong generalization capabilities of the guided embedding, we construct refined embedding by using the guided embedding and reduced-dimension version of the base embedding. We then integrate the refined embedding into the recommendation module for training and inference. A range of numerical experiments demonstrate that guided embedding is adaptable to various given existing base embedding models, and generalizes well across different recommendation tasks. The numerical results show that the refined embedding not only improves recommendation performance, achieving approximately $10\%$ to $50\%$ gains in Mean Reciprocal Rank (MRR), Recall rate, and Normalized Discounted Cumulative Gain (NDCG), but also enhances interpretability, as evidenced by case studies.

cs.IR↗

arXiv2025

On the number of edges in saturated partial embeddings of maximal planar graphs

We investigate the extremal properties of saturated partial plane embeddings of maximal planar graphs. For a planar graph $G$, the plane-saturation number $\mathrm{sat}_{\mathcal{P}}(G)$ denotes the minimum number of edges in a plane subgraph of $G$ such that the addition of any edge either violates planarity or results in a graph that is not a subgraph of $G$. We focus on maximal planar graphs and establish an upper bound on $\mathrm{sat}_{\mathcal{P}}(G)$ by showing there exists a universal constant $ε> 0$ such that $\mathrm{sat}_{\mathcal{P}}(G) < (3-ε)v(G)$ for any maximal planar graph $G$ with $v(G) \geq 16$. This answers a question posed by Clifton and Simon. Additionally, we derive lower bound results and demonstrate that for maximal planar graphs with sufficiently large number of vertices, the minimum ratio $\mathrm{sat}_{\mathcal{P}}(G)/e(G)$ lies within the interval $(1/16, 1/9 + o(1)]$.

math.CO↗

arXiv2025

Reinforcement-Learning Portfolio Allocation with Dynamic Embedding of Market Information

We develop a portfolio allocation framework that leverages deep learning techniques to address challenges arising from high-dimensional, non-stationary, and low-signal-to-noise market information. Our approach includes a dynamic embedding method that reduces the non-stationary, high-dimensional state space into a lower-dimensional representation. We design a reinforcement learning (RL) framework that integrates generative autoencoders and online meta-learning to dynamically embed market information, enabling the RL agent to focus on the most impactful parts of the state space for portfolio allocation decisions. Empirical analysis based on the top 500 U.S. stocks demonstrates that our framework outperforms common portfolio benchmarks and the predict-then-optimize (PTO) approach using machine learning, particularly during periods of market stress. Traditional factor models do not fully explain this superior performance. The framework's ability to time volatility reduces its market exposure during turbulent times. Ablation studies confirm the robustness of this performance across various reinforcement learning algorithms. Additionally, the embedding and meta-learning techniques effectively manage the complexities of high-dimensional, noisy, and non-stationary financial data, enhancing both portfolio performance and risk management.

q-fin.PM↗

arXiv2025

Black-box Optimization with Simultaneous Statistical Inference for Optimal Performance

Black-box optimization is often encountered for decision-making in complex systems management, where the knowledge of system is limited. Under these circumstances, it is essential to balance the utilization of new information with computational efficiency. In practice, decision-makers often face the dual tasks of optimization and statistical inference for the optimal performance, in order to achieve it with a high reliability. Our goal is to address the dual tasks in an online fashion. Wu et al (2022) [arXiv preprint: 2210.06737] point out that the sample average of performance estimates generated by the optimization algorithm needs not to admit a central limit theorem. We propose an algorithm that not only tackles this issue, but also provides an online consistent estimator for the variance of the performance. Furthermore, we characterize the convergence rate of the coverage probabilities of the asymptotic confidence intervals.

stat.CO↗

arXiv2024

Structured Diffusion Models with Mixture of Gaussians as Prior Distribution

We propose a class of structured diffusion models, in which the prior distribution is chosen as a mixture of Gaussians, rather than a standard Gaussian distribution. The specific mixed Gaussian distribution, as prior, can be chosen to incorporate certain structured information of the data. We develop a simple-to-implement training procedure that smoothly accommodates the use of mixed Gaussian as prior. Theory is provided to quantify the benefits of our proposed models, compared to the classical diffusion models. Numerical experiments with synthetic, image and operational data are conducted to show comparative advantages of our model. Our method is shown to be robust to mis-specifications and in particular suits situations where training resources are limited or faster training in real time is desired.

cs.LG↗

arXiv2024

A Simple and Optimal Policy Design with Safety against Heavy-Tailed Risk for Stochastic Bandits

We study the stochastic multi-armed bandit problem and design new policies that enjoy both worst-case optimality for expected regret and light-tailed risk for regret distribution. Specifically, our policy design (i) enjoys the worst-case optimality for the expected regret at order $O(\sqrt{KT\ln T})$ and (ii) has the worst-case tail probability of incurring a regret larger than any $x>0$ being upper bounded by $\exp(-Ω(x/\sqrt{KT}))$, a rate that we prove to be best achievable with respect to $T$ for all worst-case optimal policies. Our proposed policy achieves a delicate balance between doing more exploration at the beginning of the time horizon and doing more exploitation when approaching the end, compared to standard confidence-bound-based policies. We also enhance the policy design to accommodate the "any-time" setting where $T$ is unknown a priori, and prove equivalently desired policy performances as compared to the "fixed-time" setting with known $T$. Numerical experiments are conducted to illustrate the theoretical findings. We find that from a managerial perspective, our new policy design yields better tail distributions and is preferable than celebrated policies especially when (i) there is a risk of under-estimating the volatility profile, or (ii) there is a challenge of tuning policy hyper-parameters. We conclude by extending our proposed policy design to the stochastic linear bandit setting that leads to both worst-case optimality in terms of expected regret and light-tailed risk on the regret distribution.

stat.ML↗

arXiv2024

Normalization and effective learning rates in reinforcement learning

Normalization layers have recently experienced a renaissance in the deep reinforcement learning and continual learning literature, with several works highlighting diverse benefits such as improving loss landscape conditioning and combatting overestimation bias. However, normalization brings with it a subtle but important side effect: an equivalence between growth in the norm of the network parameters and decay in the effective learning rate. This becomes problematic in continual learning settings, where the resulting effective learning rate schedule may decay to near zero too quickly relative to the timescale of the learning problem. We propose to make the learning rate schedule explicit with a simple re-parameterization which we call Normalize-and-Project (NaP), which couples the insertion of normalization layers with weight projection, ensuring that the effective learning rate remains constant throughout training. This technique reveals itself as a powerful analytical tool to better understand learning rate schedules in deep reinforcement learning, and as a means of improving robustness to nonstationarity in synthetic plasticity loss benchmarks along with both the single-task and sequential variants of the Arcade Learning Environment. We also show that our approach can be easily applied to popular architectures such as ResNets and transformers while recovering and in some cases even slightly improving the performance of the base model in common stationary benchmarks.

cs.LG↗