arXiv subjects

Haozhe Sun

Publications and source records attributed to Haozhe Sun.

18 recordsLinked to original sources

arXiv2026

Potassium-40 geoneutrinos detection and the Earth's large-scale structures imaging by directional geoneutrino detection

Geoneutrinos, the electron (anti)neutrinos generated in decays or decay chains of radioactive elements within the Earth, primarily K-40, U-238, and Th-232, serve as a unique probe of the Earth's inner chemical composition. A directional geoneutrino detection method with a Cherenkov liquid scintillator is investigated in this work. Neutrino-electron elastic scattering in the Cherenkov scintillator is employed to detect geoneutrinos. The direction reconstruction resolution for neutrinos is studied. The radioactive and solar neutrino backgrounds are taken into account. The intrinsic neutrino background from the Sun is suppressed with an optimized solar angle cut. The required exposure to reach a 3 sigma sensitivity to discover geoneutrinos in a potassium-dominated energy region is 6.9 kiloton-years. The potential to image Earth's large-scale structures using directional geoneutrino information is also studied. The required exposure to reject a uniform terrestrial angle distribution of geoneutrinos at the 3 sigma level exceeds 27 kiloton-years.

hep-ex↗

arXiv2026

The Research and Development of New Electronics System and its Testing on the JNE-1ton Prototype Detector

The Jinping Neutrino Experiment (JNE), a next-generation neutrino observatory under construction at the China Jinping Underground Laboratory II (CJPL-II), requires high-precision waveform-based event reconstruction, imposing stringent demands on its readout electronics. To meet these requirements, we have developed a high-performance readout system featuring 1 GSa/s real-time sampling, 14-bit physical resolution with an effective number of bits (ENOB) of 10.6, a total data throughput of 64 Gbps, and a deterministic zero-delay clock distribution architecture. The new single-crate 64-channel system (PDS1500) was validated through bench tests and deployment on the upgraded JNE-1ton prototype detector. Its performance was further evaluated against a commercial reference system. The results demonstrate that all key metrics meet the JNE experimental requirements: zero data loss within a 1000 ns acquisition window, baseline noise reduced to one-third of the reference level, timing drift limited to 0.3 ns across power cycles, and an energy threshold as low as 0.1 MeV, enabling the detection of low-energy solar neutrinos. While the 14-bit physical resolution provides significantly higher waveform fidelity, the overall energy resolution in this test remains dominated by the intrinsic limitations of the JNE-1ton detector, as expected. Furthermore, the modular architecture provides the throughput and scalability required to support the full-scale 3000-channel JNE detector. These results collectively demonstrate that the newly developed electronics system fully satisfies the technical requirements of the future JNE experiment.

physics.ins-det↗

arXiv2026

Mountain Muography for China Jinping Underground Laboratory

The China Jinping Underground Laboratory (CJPL), located $\sim 2,400$~m beneath Jinping Mountain, is one of the world's deepest and largest ($\sim 300{,}000~\mathrm{m}^3$) underground facilities, hosting dark matter, nuclear astrophysics, and neutrino experiments. We report the first muon radiography (muography) conducted at this extraordinary depth. Cosmic muons detected by a one-ton prototype developed for the Jinping Neutrino Experiment were used to perform non-invasive subsurface density mapping over a 3~km lateral range. The 1.3~m diameter detector provides nearly isotropic acceptance and an angular resolution of $\sim 4.5^\circ$. By correlating the predicted surface muon flux distributions with the underground measurements, we reconstruct a directional opacity map that constrains the density structure of the overburden and shows excellent agreement with satellite-derived terrain models. This work demonstrates the feasibility of muography at extreme depths with kilometer-scale overburden and establishes a robust methodology for future geophysical applications and large-scale facilities, such as the full Jinping Neutrino Experiment. Based on this validated overburden model, we further predict the total muon fluxes for the eight experimental halls in CJPL-II, providing essential input for their physics programs.

hep-ex↗

arXiv2026

Molecular structure, electric property, and scintillation and quenching of liquid scintillators

Liquid scintillators are widely used in particle and nuclear physics. Understanding the scintillation and quenching mechanisms is a fundamental issue in designing a high-light-yield liquid scintillator. In this work, the basic scintillation process for two-component liquid scintillators is discussed, highlighting the processes of excitation, ionization, and anion-cation recombination. A molecule's polar group, polarization characteristics, and the corresponding material's dielectric constant are found to be correlated with a liquid scintillator's scintillation efficiency. Polar groups and high relative dielectric constant (permittivity) can cause quenching and should be avoided. The tellurium loading scheme in the liquid scintillator of the SNO+ experiment, TeBD, is discussed. The hydroxyl groups introduce polar structures in the TeBD, and for the first time, the relative dielectric constant of TeBD is measured to be $16\pm1$. These discussions explain part of the quenching of the TeBD liquid scintillator.

physics.ins-det↗

arXiv2026

Investigating Production of TeV-scale Muons in Extensive Air Shower at 2400 Meters Underground

Deep underground experiments present a new avenue to probe the first interactions in extensive air showers or hadronic interactions in the extreme forward phase space. The China Jinping Underground Laboratory, characterized by a vertical rock overburden of 2,400~m, provides an exceptionally effective shield against cosmic muons with energies below 3~TeV. The surviving high-energy muons, produced in the first interactions of extensive air showers, open a unique observational window into primary cosmic rays from tens of TeV up to the PeV scale and beyond. This distinctive feature also enables detailed studies of charged hadron production in the earliest stages of shower development. Using 1,338.6 live days of data collected with a one-ton prototype detector for the Jinping Neutrino Experiment, we measured the underground muon flux originating from air showers. The results show discrepancies of about 40\% corresponding to significances of more than 2$σ$, relative to predictions from several leading hadronic interaction models. We interpret these findings from two complementary perspectives: (i) by adopting the expected cosmic-ray spectra, we constrain the modeling of the first hadronic interactions in air showers and provide novel insights into resolving the long-standing \textit{muon puzzle}; and (ii) by assuming specific hadronic interaction models, we infer the mass composition of cosmic rays, and our data favor a lighter component in the corresponding energy range. Our study demonstrates the potential of deep underground laboratories to provide new experimental insights into air shower physics and cosmic rays.

hep-ex↗

arXiv2026

Automated Formalization via Conceptual Retrieval-Augmented LLMs

Interactive theorem provers (ITPs) require manual formalization, which is labor-intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hallucination (e.g., undefined predicates, symbol misuse, and version incompatibility) and the semantic gap caused by ambiguous or missing premises in natural language descriptions. To address these issues, we propose CRAMF, a Concept-driven Retrieval-Augmented Mathematical Formalization framework. CRAMF enhances LLM-based autoformalization by retrieving formal definitions of core mathematical concepts, providing contextual grounding during code generation. However, applying retrieval-augmented generation (RAG) in this setting is non-trivial due to the lack of structured knowledge bases, the polymorphic nature of mathematical concepts, and the high precision required in formal retrieval. We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4, the standard mathematical library for the Lean 4 theorem prover, indexing over 26,000 formal definitions and 1,000+ core mathematical concepts. To address conceptual polymorphism, we propose contextual query augmentation with domain- and application-level signals. In addition, we design a dual-channel hybrid retrieval strategy with reranking to ensure accurate and relevant definition retrieval. Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers, yielding consistent improvements in translation accuracy, achieving up to 62.1% and an average of 29.9% relative improvement.

cs.AI↗

arXiv2025

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification

Automated Theorem Proving (ATP) represents a core research direction in artificial intelligence for achieving formal reasoning and verification, playing a significant role in advancing machine intelligence. However, current large language model (LLM)-based theorem provers suffer from limitations such as restricted domain coverage and weak generalization in mathematical reasoning. To address these issues, we propose MSC-180, a benchmark for evaluation based on the MSC2020 mathematical subject classification. It comprises 180 formal verification problems, 3 advanced problems from each of 60 mathematical branches, spanning from undergraduate to graduate levels. Each problem has undergone multiple rounds of verification and refinement by domain experts to ensure formal accuracy. Evaluations of state-of-the-art LLM-based theorem provers under the pass@32 setting reveal that the best model achieves only an 18.89% overall pass rate, with prominent issues including significant domain bias (maximum domain coverage 41.7%) and a difficulty gap (significantly lower pass rates on graduate-level problems). To further quantify performance variability across mathematical domains, we introduce the coefficient of variation (CV) as an evaluation metric. The observed CV values are 4-6 times higher than the statistical high-variability threshold, indicating that the models still rely on pattern matching from training corpora rather than possessing transferable reasoning mechanisms and systematic generalization capabilities. MSC-180, together with its multi-dimensional evaluation framework, provides a discriminative and systematic benchmark for driving the development of next-generation AI systems with genuine mathematical reasoning abilities.

cs.AI↗

arXiv2025

An exploratory study of a tellurium-loaded liquid scintillator based on water and p-dioxane

Tellurium-loaded liquid scintillators are critical for neutrinoless double-beta decay experiments. However, conventional organic scintillators are constrained by the limited solubility of organic tellurium compounds compared with that of inorganic ones in water, whereas water-based scintillators are likely constrained by the destabilization of surfactants caused by inorganic tellurium compounds. In this work, a surfactant-free water-containing route is explored, in which an aqueous telluric acid solution is introduced into a water-miscible organic scintillator comprising p-dioxane, naphthalene, and PPO. The phase behavior of this system is mapped to delineate homogeneous-mixture domains and to estimate practical upper bounds on tellurium loading. Optical properties are characterized by UV-visible absorption spectroscopy and fluorescence spectroscopy. The scintillation light yield is obtained with a relative method that compares to a reference LAB-PPO scintillator. The measurements demonstrate scintillation quenching induced by water and by tellurium acid. These results provide benchmarks for water-containing and surfactant-free formulations and support the development of high-loading liquid scintillators for future detector design.

physics.ins-det↗

arXiv2025

Autoformalization in the Era of Large Language Models: A Survey

Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field.

cs.AI↗

arXiv2025

Lossless, Non-Volatile Post-Fabrication Trimming of PICs via On-Chip High-Temperature Annealing of Undercut Waveguides

Limited by equipment precision, manufacturing deviations in waveguide width, etch depth, and layer thickness inevitably occur in photonic integrated circuits (PICs). These variations cause initial phase errors, compromising the reliability of phase-sensitive devices such as Mach-Zehnder Interferometers (MZI) and microring resonators. To overcome this, we report a nonvolatile, near-lossless post-trimming method utilizing sufficient high-temperature thermal treatment for undercut waveguides, reported here for the first time to the best of our knowledge. This CMOS-compatible approach requires no additional processes or equipment, enables simple electrical heating for trimming, and retains long-term stability after high-temperature removal, ensuring high energy efficiency. Transmission electron microscopy indicates that high-temperature thermal treatment induces irreversible lattice expansion in silicon waveguides, leading to a reduction in the real refractive index and enabling compensation for process errors. Experimental results using MZIs confirm a permanent refractive index reduction of 0.0173 and high-resolution tuning up to 5.25 bits, effective across a broadband spectrum and stable for over 218 days after final trimming. Furthermore, 15 MZIs on a single wafer are precisely calibrated to BAR, CROSS, or orthogonal states, demonstrating the method universality. This practical and scalable technique enables reliable post-fabrication trimming for next-generation low-cost, energy-efficient PIC applications such as optical switches and optical computing.

physics.optics↗

arXiv2024

Study of neutron production for 360 GeV cosmic muons

The China Jinping underground Laboratory (CJPL) is an excellent location for studying solar, terrestrial, and supernova neutrinos due to its 2400-meter vertical rock overburden. Its unparalleled depth gives an opportunity to investigate the cosmic-ray muons with exceptionally high average energy at $\sim360$ GeV. This paper details a study of muon-related backgrounds based on 1178 days of data collected by the 1-ton prototype neutrino detector used for the Jinping Neutrino Experiment (JNE) since 2017. The apparent effects for the leakage of muons' secondary particles due to detector's finite size on the measured neutron yield are first discussed in detail. The analysis of 493 cosmic-ray muon candidates and $13.6\pm5.7$ cosmogenic neutron candidates, along with a thorough evaluation of detection efficiency and uncertainties, gives a muon flux of $(3.56\pm0.16_{\mathrm{stat.}}\pm0.10_{\mathrm{syst.}})\times10^{-10}~\mathrm{cm}^{-2}\mathrm{s^{-1}}$ and a cosmogenic neutron yield of $(3.37\pm 1.41_{\mathrm{stat.}}\pm 0.31_{\mathrm{syst.}}) \times 10^{-4}~\mathrmμ^{-1} \mathrm{g}^{-1} \mathrm{cm}^{2}$ in LAB-based liquid scintillator.

hep-ex↗

arXiv2023

Modularity in Deep Learning: A Survey

Modularity is a general principle present in many fields. It offers attractive advantages, including, among others, ease of conceptualization, interpretability, scalability, module combinability, and module reusability. The deep learning community has long sought to take inspiration from the modularity principle, either implicitly or explicitly. This interest has been increasing over recent years. We review the notion of modularity in deep learning around three axes: data, task, and model, which characterize the life cycle of deep learning. Data modularity refers to the observation or creation of data groups for various purposes. Task modularity refers to the decomposition of tasks into sub-tasks. Model modularity means that the architecture of a neural network system can be decomposed into identifiable modules. We describe different instantiations of the modularity principle, and we contextualize their advantages in different deep learning sub-fields. Finally, we conclude the paper with a discussion of the definition of modularity and directions for future research.

cs.LG↗

arXiv2023

RRR-Net: Reusing, Reducing, and Recycling a Deep Backbone Network

It has become mainstream in computer vision and other machine learning domains to reuse backbone networks pre-trained on large datasets as preprocessors. Typically, the last layer is replaced by a shallow learning machine of sorts; the newly-added classification head and (optionally) deeper layers are fine-tuned on a new task. Due to its strong performance and simplicity, a common pre-trained backbone network is ResNet152.However, ResNet152 is relatively large and induces inference latency. In many cases, a compact and efficient backbone with similar performance would be preferable over a larger, slower one. This paper investigates techniques to reuse a pre-trained backbone with the objective of creating a smaller and faster model. Starting from a large ResNet152 backbone pre-trained on ImageNet, we first reduce it from 51 blocks to 5 blocks, reducing its number of parameters and FLOPs by more than 6 times, without significant performance degradation. Then, we split the model after 3 blocks into several branches, while preserving the same number of parameters and FLOPs, to create an ensemble of sub-networks to improve performance. Our experiments on a large benchmark of $40$ image classification datasets from various domains suggest that our techniques match the performance (if not better) of ``classical backbone fine-tuning'' while achieving a smaller model size and faster inference speed.

cs.LG↗

arXiv2023

Meta-Album: Multi-domain Meta-Dataset for Few-Shot Image Classification

We introduce Meta-Album, an image classification meta-dataset designed to facilitate few-shot learning, transfer learning, meta-learning, among other tasks. It includes 40 open datasets, each having at least 20 classes with 40 examples per class, with verified licences. They stem from diverse domains, such as ecology (fauna and flora), manufacturing (textures, vehicles), human actions, and optical character recognition, featuring various image scales (microscopic, human scales, remote sensing). All datasets are preprocessed, annotated, and formatted uniformly, and come in 3 versions (Micro $\subset$ Mini $\subset$ Extended) to match users' computational resources. We showcase the utility of the first 30 datasets on few-shot learning problems. The other 10 will be released shortly after. Meta-Album is already more diverse and larger (in number of datasets) than similar efforts, and we are committed to keep enlarging it via a series of competitions. As competitions terminate, their test data are released, thus creating a rolling benchmark, available through OpenML.org. Our website https://meta-album.github.io/ contains the source code of challenge winning methods, baseline methods, data loaders, and instructions for contributing either new datasets or algorithms to our expandable meta-dataset.

cs.CV↗

arXiv2022

Lessons learned from the NeurIPS 2021 MetaDL challenge: Backbone fine-tuning without episodic meta-learning dominates for few-shot learning image classification

Although deep neural networks are capable of achieving performance superior to humans on various tasks, they are notorious for requiring large amounts of data and computing resources, restricting their success to domains where such resources are available. Metalearning methods can address this problem by transferring knowledge from related tasks, thus reducing the amount of data and computing resources needed to learn new tasks. We organize the MetaDL competition series, which provide opportunities for research groups all over the world to create and experimentally assess new meta-(deep)learning solutions for real problems. In this paper, authored collaboratively between the competition organizers and the top-ranked participants, we describe the design of the competition, the datasets, the best experimental results, as well as the top-ranked methods in the NeurIPS 2021 challenge, which attracted 15 active teams who made it to the final phase (by outperforming the baseline), making over 100 code submissions during the feedback phase. The solutions of the top participants have been open-sourced. The lessons learned include that learning good representations is essential for effective transfer learning.

cs.LG↗

arXiv2022

LTU Attacker for Membership Inference

We address the problem of defending predictive models, such as machine learning classifiers (Defender models), against membership inference attacks, in both the black-box and white-box setting, when the trainer and the trained model are publicly released. The Defender aims at optimizing a dual objective: utility and privacy. Both utility and privacy are evaluated with an external apparatus including an Attacker and an Evaluator. On one hand, Reserved data, distributed similarly to the Defender training data, is used to evaluate Utility; on the other hand, Reserved data, mixed with Defender training data, is used to evaluate membership inference attack robustness. In both cases classification accuracy or error rate are used as the metric: Utility is evaluated with the classification accuracy of the Defender model; Privacy is evaluated with the membership prediction error of a so-called "Leave-Two-Unlabeled" LTU Attacker, having access to all of the Defender and Reserved data, except for the membership label of one sample from each. We prove that, under certain conditions, even a "naïve" LTU Attacker can achieve lower bounds on privacy loss with simple attack strategies, leading to concrete necessary conditions to protect privacy, including: preventing over-fitting and adding some amount of randomness. However, we also show that such a naïve LTU Attacker can fail to attack the privacy of models known to be vulnerable in the literature, demonstrating that knowledge must be complemented with strong attack strategies to turn the LTU Attacker into a powerful means of evaluating privacy. Our experiments on the QMNIST and CIFAR-10 datasets validate our theoretical results and confirm the roles of over-fitting prevention and randomness in the algorithms to protect against privacy attacks.

cs.LG↗

arXiv2022

OmniPrint: A Configurable Printed Character Synthesizer

We introduce OmniPrint, a synthetic data generator of isolated printed characters, geared toward machine learning research. It draws inspiration from famous datasets such as MNIST, SVHN and Omniglot, but offers the capability of generating a wide variety of printed characters from various languages, fonts and styles, with customized distortions. We include 935 fonts from 27 scripts and many types of distortions. As a proof of concept, we show various use cases, including an example of meta-learning dataset designed for the upcoming MetaDL NeurIPS 2021 competition. OmniPrint is available at https://github.com/SunHaozhe/OmniPrint.

cs.CV↗

arXiv2021

Effectiveness of Optimization Algorithms in Deep Image Classification

Adam is applied widely to train neural networks. Different kinds of Adam methods with different features pop out. Recently two new adam optimizers, AdaBelief and Padam are introduced among the community. We analyze these two adam optimizers and compare them with other conventional optimizers (Adam, SGD + Momentum) in the scenario of image classification. We evaluate the performance of these optimization algorithms on AlexNet and simplified versions of VGGNet, ResNet using the EMNIST dataset. (Benchmark algorithm is available at \hyperref[https://github.com/chuiyunjun/projectCSC413]{https://github.com/chuiyunjun/projectCSC413}).

cs.CV↗