arXiv subjects

Bingyu Xia

Publications and source records attributed to Bingyu Xia.

5 recordsLinked to original sources

arXiv2026

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.

cs.AI↗

arXiv2025

MASS: Muli-agent simulation scaling for portfolio construction

The application of LLM-based agents in financial investment has shown significant promise, yet existing approaches often require intermediate steps like predicting individual stock movements or rely on predefined, static workflows. These limitations restrict their adaptability and effectiveness in constructing optimal portfolios. In this paper, we introduce the Multi-Agent Scaling Simulation (MASS), a novel framework that leverages multi-agent simulation for direct, end-to-end portfolio construction. At its core, MASS employs a backward optimization process to dynamically learn the optimal distribution of heterogeneous agents, enabling the system to adapt to evolving market regimes. A key finding enabled by our framework is the exploration of the scaling effect for portfolio construction: we demonstrate that as the number of agents increases exponentially (up to 512), the aggregated decisions yield progressively higher excess returns. Extensive experiments on a challenging, self-collected dataset from the 2023 Chinese A-share market show that MASS consistently outperforms seven state-of-the-art baselines. Further backtesting, stability analyses and the experiment on data leakage concerns validate its enhanced profitability and robustness. We have open-sourced our code, dataset, and training snapshots at https://github.com/gta0804/MASS/ to foster further research.

cs.AI↗

arXiv2021

Decorated sheaves and morphisms in tilted hearts

We identify limit stable pairs and stable framed sheaves as epimorphisms and monomorphisms, respectively, in tilts of the standard heart, under suitable conditions. We then identify the moduli spaces with the corresponding Quot spaces, obtaining the projectivity of the Quot spaces in these cases. We also prove a formula in a motivic Hall algebra relating the Quot spaces under a tilt.

math.AG↗

arXiv2018

Bridgeland stability conditions on surfaces with curves of negative self-intersection

Let $X$ be a smooth complex projective variety. In 2002, Bridgeland defined a notion of stability for the objects in $D^b(X)$, the bounded derived category of coherent sheaves on $X$, which generalized the notion of slope stability for vector bundles on curves. There are many nice connections between stability conditions on $X$ and the geometry of the variety. We construct new stability conditions for surfaces containing a curve $C$ whose self-intersection is negative. We show that these stability conditions lie on a wall of the geometric chamber of ${\rm Stab}(X)$, the stability manifold of $X$. We then construct the moduli space $M_σ(\mathcal{O}_X)$ of $σ$-semistable objects of class $[\mathcal{O}_X]$ in $K_0(X)$ after wall-crossing.

math.AG↗

arXiv2016

Hilbert scheme of twisted cubics as simple wall-crossing

We study the Hilbert scheme of twisted cubics in the three-dimensional projective space by using Bridgeland stability conditions. We use wall-crossing techniques to describe its geometric structure and singularities, which reproves the classical result of Piene and Schlessinger.

math.AG↗