arXiv subjects

Junyu Lai

Publications and source records attributed to Junyu Lai.

10 recordsLinked to original sources

arXiv2026

Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving

Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation. These two paradigms represent opposite granularities for constructing supervised training data: the former provides dense local signals but may fragment coherent proof processes, while the latter preserves global structure but requires complex end-to-end generation. In this paper, we revisit supervision granularity as a training set construction problem over proof trajectories and propose segment-level supervision, a training data construction strategy that extracts locally coherent proof segments for training policy models. We further reuse the same strategy at inference time to trigger short rollouts for existing step-level models. When trained with segment-level supervision on STP, LeanWorkbook, and NuminaMath-LEAN, the resulting policy models achieve proof success rates of 64.84%, 60.90%, and 66.31% on miniF2F, respectively, consistently outperforming both step-level and whole-proof baselines. Goal-aware rollout further improves existing step-level provers while reducing inference costs. It increases the proof success rate of BFS-Prover-V2-7B from 68.77% to 70.74% and that of InternLM2.5-StepProver from 59.59% to 60.33%, showing that appropriate supervision granularity better aligns model learning with proof structure and search. Code and models are available at https://github.com/NJUDeepEngine/SEG-ATP.

cs.AI↗

arXiv2025

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of $60.74\%$ on MiniF2F and $21.18\%$ on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.

cs.AI↗

arXiv2024

Executing Arithmetic: Fine-Tuning Large Language Models as Turing Machines

Large Language Models (LLMs) have demonstrated remarkable capabilities across a wide range of natural language processing and reasoning tasks. However, their performance in the foundational domain of arithmetic remains unsatisfactory. When dealing with arithmetic tasks, LLMs often memorize specific examples rather than learning the underlying computational logic, limiting their ability to generalize to new problems. In this paper, we propose a Composable Arithmetic Execution Framework (CAEF) that enables LLMs to learn to execute step-by-step computations by emulating Turing Machines, thereby gaining a genuine understanding of computational logic. Moreover, the proposed framework is highly scalable, allowing composing learned operators to significantly reduce the difficulty of learning complex operators. In our evaluation, CAEF achieves nearly 100% accuracy across seven common mathematical operations on the LLaMA 3.1-8B model, effectively supporting computations involving operands with up to 100 digits, a level where GPT-4o falls short noticeably in some settings.

cs.AI↗

arXiv2024

MeteoRA: Multiple-tasks Embedded LoRA for Large Language Models

The pretrain+fine-tune paradigm is foundational for deploying large language models (LLMs) across various downstream applications. Within this framework, Low-Rank Adaptation (LoRA) stands out for its parameter-efficient fine-tuning (PEFT), producing numerous reusable task-specific LoRA adapters. However, this approach requires explicit task intention selection, posing challenges for autonomous task sensing and switching during inference with multiple existing LoRA adapters embedded in a single LLM. In this work, we introduce MeteoRA (Multiple-tasks embedded LoRA), a scalable and efficient framework that reuses multiple task-specific LoRA adapters into the base LLM via a full-mode Mixture-of-Experts (MoE) architecture. This framework also includes novel MoE forward acceleration strategies to address the efficiency challenges of traditional MoE implementations. Our evaluation, using the LlaMA2-13B and LlaMA3-8B base models equipped with 28 existing LoRA adapters through MeteoRA, demonstrates equivalent performance with the traditional PEFT method. Moreover, the LLM equipped with MeteoRA achieves superior performance in handling composite tasks, effectively solving ten sequential problems in a single inference pass, thereby demonstrating the framework's enhanced capability for timely adapter switching.

cs.CL↗

arXiv2024

XPS analysis of molecular contamination and sp2 amorphous carbon on oxidized (100) diamond

The efficacy of oxygen (O) surface terminations on diamond is an important factor for the performance and stability for diamond-based quantum sensors and electronics. Given the wide breadth of O-termination techniques, it can be difficult to discern which method would yield the highest and most consistent O coverage. Furthermore, the interpretation of surface characterization techniques is complicated by surface morphology and purity, which if not accounted for will yield inconsistent determination of the oxygen coverage. We present a comprehensive approach to consistently prepare and analyze oxygen termination of surfaces on (100) single-crystalline diamond. We report on X-ray Photoelectron Spectroscopy (XPS) characterization of diamond surfaces treated with six oxidation methods that include various wet chemical oxidation techniques, photochemical oxidation with UV illumination, and steam oxidation using atomic layer deposition (ALD). Our analysis entails a rigorous XPS peak-fitting procedure for measuring the functionalization of O-terminated diamond. The findings herein have provided molecular-level insights on oxidized surfaces in (100) diamond, including the demonstration of clear correlation between the measured oxygen atomic percentage and the presence of molecular contaminants containing nitrogen, silicon, and sulfur. We also provide a comparison of the sp2 carbon content with the O1s atomic percentage and discern a correlation with the diamond samples treated with dry oxidation which eventually tapers off at a max O1s atomic percentage value of 7.09 +/- 0.40%. Given these results, we conclude that the dry oxidation methods yield some of the highest oxygen amounts, with the ALD water vapor technique proving to be the cleanest technique out of all the oxidation methods explored in this work.

cond-mat.mtrl-sci↗

arXiv2024

Advancing Transformer Architecture in Long-Context Large Language Models: A Comprehensive Survey

Transformer-based Large Language Models (LLMs) have been applied in diverse areas such as knowledge bases, human interfaces, and dynamic agents, and marking a stride towards achieving Artificial General Intelligence (AGI). However, current LLMs are predominantly pretrained on short text snippets, which compromises their effectiveness in processing the long-context prompts that are frequently encountered in practical scenarios. This article offers a comprehensive survey of the recent advancement in Transformer-based LLM architectures aimed at enhancing the long-context capabilities of LLMs throughout the entire model lifecycle, from pre-training through to inference. We first delineate and analyze the problems of handling long-context input and output with the current Transformer-based models. We then provide a taxonomy and the landscape of upgrades on Transformer architecture to solve these problems. Afterwards, we provide an investigation on wildly used evaluation necessities tailored for long-context LLMs, including datasets, metrics, and baseline models, as well as optimization toolkits such as libraries, frameworks, and compilers to boost the efficacy of LLMs across different stages in runtime. Finally, we discuss the challenges and potential avenues for future research. A curated repository of relevant literature, continuously updated, is available at https://github.com/Strivin0311/long-llms-learning.

cs.CL↗

arXiv2022

Transient Characteristics of $β$-Ga$_2$O$_3$ Nanomembrane Schottky Barrier Diodes on Various Substrates

In this paper, a transient delayed rising and fall time of $β$-Ga$_2$O$_3$ NMs Schottky barrier diodes (SBDs) formed on four different substrates (diamond, Si, sapphire, and polyimide) were measured using a sub-micron second resolution time-resolved electrical measurement system under a different temperature condition. The devices exhibited noticeably less-delayed turn-on-/off- the transient time when $β$-Ga$_2$O$_3$ NMs SBDs were transfer-printed on a high-k substrate. Furthermore, a relationship between the $β$-Ga$_2$O$_3$ NM thicknesses and their transient characteristics were systematically investigated and found that phonon scattering plays an important role in heat dissipation as the thickness of $β$-Ga$_2$O$_3$ NMs get thinner which is also verified by the Multiphysics simulator. Overall, our result reveals the impact of various substrates with different thermal properties and different \b{eta}- Ga2O3 NMs thickness with the performance of $β$-Ga$_2$O$_3$ NMs based devices. Hence, these results can guide further efforts us to optimize the performance of future $β$-Ga$_2$O$_3$ devices by maximizing heat dissipation from the $β$-Ga$_2$O$_3$ layer.

physics.app-ph↗

arXiv2021

Electrical and Thermal Property of Si/GaAs Heterojunction Formed by Ultra-Thin Oxide Interfacial Layer

We have successfully demonstrated Si/GaAs p-n heterostructures using Al2O3 ultra-thin oxide interfacial layers. The band diagram and band offsets were investigated using X-ray photoelectron spectroscopy and confirm a small discontinuity in the conduction band (0.03 eV) at the interface. The interface defect density (Dit) values of the heterointerface with different ultra-thin oxide (UO) thicknesses ranged from 0.35 nm to 3.5 nm and were also characterized based on a metal-oxide-semiconductor capacitor (MOSCAP) structure using a capacitance-voltage measurement. The results revealed that a thin UO interfacial layer (around 1 nm) maximizes carrier transport property due to better surface passivation and efficient tunneling properties. Thermal property investigation also shows that the Al2O3 UO interfacial layer offers a good tunneling layer but also facilitates phonon transport across the interface. Finally, the electrical characterization of Si/GaAs heterojunction p-n diodes confirms reliable rectifying behavior with an extremely low ideality factor; thus, heterogeneous integration using the UO approach offers a robust way to create more types of heterojunctions between dissimilar semiconductors.

cond-mat.mtrl-sci↗

arXiv2021

Investigation of the Imperfect Interface at the Si/GaAs Heterojunction Formed by Ultra-Thin Oxide Interfacial Layer

The structure property of non-ideal Si/GaAs heterostructures that were integrated with the ultra-thin oxide (UO) tunneling interfacial layer has been systematically investigated. Si nanomembranes (NMs) were oxidized in different time periods prior to the hetero-integration process to create the non-ideal single-side passivated Si/GaAs heterostructure. The atomic level oxygen distribution and the degree of oxygen content in Si NM and GaAs were carefully investigated using the atom probe tomography (APT) and X-ray photoelectron spectroscopy (XPS) to trace the changes in chemical composition and reactional mechanism across the UO interface when the surface of Si NM was exposed to air for different period of time. The negatively induced charges at the UO layer caused the oxygen diffusion to GaAs layer and formed the unwanted GaAs oxide layer. This native oxide stack noticeably degraded the thermal properties of the Si/GaAs heterostructure as Si NMs were more oxidized. This study revealed that the poor surface passivation on the one side of the heterointerface leads to a both-side oxidation, thus severely deteriorating the transport properties across the heterojunction that is formed with the UO layer.

cond-mat.mtrl-sci↗

arXiv2021

Theoretical Prediction of Heterogeneous Integration of Dissimilar Semiconductor with Various Ultra-Thin Oxides and 2D Materials

In this paper, we have built a numerical p-n Si/GaAs heterojunction model using a quantum-mechanical tunneling theory with various quantum tunneling interfacial materials including two-dimensional semiconductors such as hexagonal boron nitride (h-BN) and graphene and ALD-enabled oxide materials such as HfO2, Al2O3, and SiO2. Their tunneling efficiencies and tunneling current with different thicknesses were systematically calculated and compared. Multiphysics modeling was used with the aforementioned tunneling interfacial materials to analyze changes in strain under different temperature conditions. Considering the transport properties and thermal-induced strain analysis, Al2O3 among three oxide materials and graphene in 2D materials are favorable material choices that offer the highest heterojunction quality. Overall, our results offer the viable route to guide the selection of quantum tunneling materials for myriad possible combinations of new heterostructures that can be obtained via remote epitaxy and the UO method.

cond-mat.mes-hall↗