arXiv subjects

Yihang Xia

Publications and source records attributed to Yihang Xia.

3 recordsLinked to original sources

arXiv2026

Search for invisible decays of light mesons via $J/\psi \to VP$ $(V=\omega/\phi,P=\eta/\eta')$ decays at STCF

We present a preliminary feasibility study of searches for invisible decays of light mesons via $J/\psi \to VP$ $(V=\omega/\phi,P=\eta/\eta')$ using a traditional analytical method at the proposed Super $\tau$-Charm facility (STCF) which is expected to accumulate $3.4\times10^{12}$ $J/\psi$ events per year, based on an inclusive Monte Carlo sample of $1.3 \times 10^{9}$ $J/\psi$ events. The upper limits on the invisible decay branching fractions at the 90\% confidence level are set as $\mathcal{B}(\omega \to invisible) < 3.7 \times 10^{-7}$, $\mathcal{B}(\phi \to invisible) < 8.9 \times 10^{-7}$, $\mathcal{B}(\eta \to invisible) < 1.8 \times 10^{-7}$ and $\mathcal{B}(\eta' \to invisible) < 4.1 \times 10^{-7}$, respectively, using a projected toy data corresponding to the expected STCF statistics. By using the machine learning technique such as Deep Learning, the upper limit may be further improved to approach theoretical predictions for light dark matter.

hep-ex↗

arXiv2025

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

LLMs have demonstrated strong mathematical reasoning abilities by leveraging reinforcement learning with long chain-of-thought, yet they continue to struggle with theorem proving due to the lack of clear supervision signals when solely using natural language. Dedicated domain-specific languages like Lean provide clear supervision via formal verification of proofs, enabling effective training through reinforcement learning. In this work, we propose \textbf{Seed-Prover}, a lemma-style whole-proof reasoning model. Seed-Prover can iteratively refine its proof based on Lean feedback, proved lemmas, and self-summarization. To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning. Seed-Prover proves $78.1\%$ of formalized past IMO problems, saturates MiniF2F, and achieves over 50\% on PutnamBench, outperforming the previous state-of-the-art by a large margin. To address the lack of geometry support in Lean, we introduce a geometry reasoning engine \textbf{Seed-Geometry}, which outperforms previous formal geometry engines. We use these two systems to participate in IMO 2025 and fully prove 5 out of 6 problems. This work represents a significant advancement in automated mathematical reasoning, demonstrating the effectiveness of formal verification with long chain-of-thought reasoning.

cs.AI↗

arXiv2025

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving. While prior work has focused on generation and compilation success, little attention has been paid to the critic phase-the evaluation of whether generated formalizations truly capture the semantic intent of the original problem. In this paper, we introduce CriticLean, a novel critic-guided reinforcement learning framework that elevates the role of the critic from a passive validator to an active learning component. Specifically, first, we propose the CriticLeanGPT, trained via supervised fine-tuning and reinforcement learning, to rigorously assess the semantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench, a benchmark designed to measure models' ability to distinguish semantically correct from incorrect formalizations, and demonstrate that our trained CriticLeanGPT models can significantly outperform strong open- and closed-source baselines. Building on the CriticLean framework, we construct FineLeanCorpus, a dataset comprising over 285K problems that exhibits rich domain diversity, broad difficulty coverage, and high correctness based on human evaluation. Overall, our findings highlight that optimizing the critic phase is essential for producing reliable formalizations, and we hope our CriticLean will provide valuable insights for future advances in formal mathematical reasoning.

cs.CL↗