Searcharxiv⌕ Search

arXiv subjects

Jian Fang

Publications and source records attributed to Jian Fang.

At least 19 recordsLinked to original sources
arXiv2026

SenseNova-U1.5: Towards Native Unified Visual Intelligence

We launch SenseNova-U1.5, an 8B-MoT native unified multimodal model that understands, reasons about, and generates visual content within an encoder-free and VAE-free architecture. We strengthen its visual interface through spatially coherent patch reconstruction and scale its training with carefully curated generation and editing data, improved task formulation, structural prompt enhancement, and native resolutions of up to 4K. For post-training, we optimize specialized experts for visual aesthetics, bilingual text rendering, infographic generation, and image editing, and consolidate their capabilities through multi-expert on-policy distillation. Across extensive evaluations, SenseNova-U1.5 largely advances image fidelity, text rendering, complex composition, multi-reference editing, and interleaved generation, while improving instruction following and preserving subject identity, geometry, and unmodified regions. Despite limited exposure to structured formats in its generation data, SenseNova-U1.5 generalizes effectively to long, complex, and structured visual instructions, further proving that multimodal understanding can transfer to visual planning and creation. Together, these findings position native unified modelling as a promising path towards systems that perceive, reason and create within a fully end-to-end framework. We will open-source training code, including supervised fine-tuning, reinforcement learning, and on-policy distillation.

cs.CV↗
arXiv2026

Extraction and Search in Rocq: Theorems, Definitions and Their dependencies

Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven theorems to assist the current proof process. However, the current search command is limited to the environment of imported modules and cannot search for theorems outside of this scope. Furthermore, tool developers and researchers may want to obtain detailed information about theorems, such as theorem's names, statements, and dependencies. But there are currently no user-friendly and efficient tools available for extracting comprehensive information from Rocq projects. We introduce a Rocq theorem extraction and analysis tool, TheoremExtr, which is capable of analyzing theorem composition and extracting theorems, dependencies, and definitions from both parsing phase and runtime. We extracted 71,795 theorems and their dependencies from 32 open-source projects from the Rocq community. In addition, we extracted 27,481 definitions and their types among these projects. We also developed a website that supports cross-project similarity search for theorems and definitions. The tool is available at https://github.com/Rw1nd/TheoremExtr, and the search website is available at https://lemmasearch.com.

cs.SE↗
arXiv2026

Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover

Generating code from natural-language requirements has become a primary route for LLM-assisted software development. Although LLMs can successfully complete small programming tasks, generating an entire complex project remains unreliable because subtle errors may survive compilation and testing. Verified programming can reduce this risk by requiring generated implementations to satisfy machine-checked specifications. Existing explorations mostly target verification-oriented languages and toolchains such as Dafny and Frama-C, but directly generating project-scale verified code with these systems remains difficult. This paper studies whether interactive theorem provers (ITPs) can support large-scale software generation. Because ITPs handle pure total functions but not effects such as I/O, our agent separates effectful code from pure logic: it implements the effects in the target language, proves the pure logic in an ITP, and extracts it for integration into the final project. We study this route through the fully automatic development of a CPU interpreter for all 47 instructions of the unprivileged RISC-V RV32I base: after the requirements are supplied, no human intervenes in synthesis, proof repair, extraction, or integration. With Rocq as the backend, the agent completes the project within 30 minutes, producing 1,859 lines of verified Rocq and extracting 2,848 lines of C++. The resulting interpreter passes all 265 LLM-generated tests covering the 47 instructions and exhibits zero crashes and zero hangs during 12 hours of AFL++ fuzzing. Under the same configuration, a Dafny-based backend fails to complete verification. Our observation is that Rocq exposes a concrete proof state when a proof attempt fails, giving the agent actionable feedback for repair. These results provide empirical evidence that ITP-based verified programming is a feasible route for LLM-generated software projects.

cs.SE↗
arXiv2026

Mixing plant for JUNO liquid scintillator: Design, construction, installation and commissioning

The most challenging part of building the Jiangmen Underground Neutrino Observatory (JUNO) is the production of 20 kilotons of ultra pure Liquid Scintillator (LS). This paper presents the design, construction, installation, and commissioning of the LS Mixing Plant, a core facility dedicated to blending the primary organic solvent (LAB) with essential functional solutes (PPO, bis-MSB, and BHT). The main purpose of the Mixing Plant is to prepare and purify the concentrated Master Solution (MS) to achieve a low radioactive contamination background. The amount of radioactive contaminants in the MS are lowered by approximately two orders of magnitude after acid and water extraction, followed by a multi-stage filtration procedure. The purified MS is mixed with LAB and then diluted into the LS for JUNO experiments. Commissioning results of the LS verify that the Mixing Plant achieved its design goal, delivering ultra pure LS that satisfies the stringent radiopurity requirements for neutrino physics.

physics.ins-det↗
arXiv2026

A Learning Method for Symbolic Systems Using Large Language Models

Automated theorem proving is essential for the formal verification of safety-critical systems. As the corpus of formal proofs grows, a natural paradigm is to learn from existing proofs. However, current learning-based approaches predominantly train Large Language Models (LLMs) as end-to-end provers, which yields resource-intensive, opaque systems. Conversely, while traditional symbolic provers are computationally efficient, how to automatically improve these solvers from data remains an open challenge. This paper bridges this gap by proposing LLM2Ltac, the first approach that leverages the reasoning power of LLMs not as end-to-end provers, but as intelligent synthesizers to mine purely symbolic tactics from data. Given a corpus of formal proofs, LLM2Ltac asks an LLM to identify latent proof strategies and formalize them into reusable tactics. These tactics are verified for validity and generalizability, and finally integrated into symbolic provers to enhance their automated proving capabilities without the runtime cost of LLMs. We implement LLM2Ltac on Rocq 8.20.0 and mine tactics from 11,725 theorems in the standard library. We evaluate our approach on 6,199 theorems from four large real-world verification projects, namely, compcert, Coq-Art, Ext-Lib, and VFA. Results show that the mined tactics improve CoqHammer to prove 23.87% more theorems, and when integrating the improved CoqHammer with Claude Code, the overall proved theorems increases by 9.90%, indicating the effectiveness of LLM2Ltac.

cs.SE↗
arXiv2025

Fisher-KPP waves and the minimal speed on hexagonal lattice

The hexagonal structure is ubiquitous in nature. The propagation phenomena occurring in a media with a hexagonal structure remain to be explored. One way of exploring this question is to formulate lattice dynamical systems and analyze the propagation dynamics. In this paper, we propose a lattice differential equation model featuring a discrete diffusion operator with the hexagonal structure, and a monostable nonlinear term known as the Fisher-KPP mechanism in modeling population growth. A rigorous analysis is conducted on the traveling waves, thoroughly establishing the existence and uniqueness (up to translation) of the traveling waves. Moreover, the periodicity and monotonicity of the minimal wave speed concerning an angle are demonstrated, which is different from the existing results of the minimal wave speed in $\mathbb{R}^2$ and $\mathbb{Z}^2$. Numerical results validate theoretical analysis and further suggest that the minimal wave speed is also the spreading speed of solutions with compactly supported initial values.

math.DS↗
arXiv2025

Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

One important approach to software verification is interactive theorem proving. However, writing formal proofs often requires substantial human effort, making proof automation highly important. Traditionally, proof automation has relied on symbolic provers. Recently, large language models (LLMs) have demonstrated strong capabilities in theorem proving, complementing symbolic provers. Nonetheless, prompting LLMs can be expensive and may pose security risks for confidential codebases. As a result, purely symbolic approaches remain important even in the LLM era, as they are cost-effective, secure, and complement the strengths of LLMs. Motivated by these considerations, we pose a new research question: can the internal proof strategies of LLMs be extracted to enhance the capabilities of symbolic provers? As an initial step, we introduce Strat2Rocq. In an offline stage, Strat2Rocq extracts proof strategies from LLMs and formalizes them as lemmas in Rocq. In an online stage, given a theorem to be proved, Strat2Rocq augments the proof context with these extracted lemmas, enabling CoqHammer to leverage the LLM-derived strategies for more effective automated proving. Our evaluation demonstrates that, on open-source Rocq projects for software verification, Strat2Rocq enhances the success rate of CoqHammer by 13.41%. A side discovery is that the extracted lemmas are also beneficial to LLM proof agents, improving the success rate of an LLM proof agent by 4.00%.

cs.LO↗
arXiv2025

The Lost-K and Shorter-J Phenomenon in Non-Standard Ballistocardiography Data

Non-standard ballistocardiogram(BCG) data generally do not have prominent J peaks. This paper introduces two phenomena that reduce the prominence of Jpeaks: the shorter-J phenomenon and the lost-K phenomenon, both of which are commonly observed in non-standard BCG signals . This paper also proposes three signal transformation methods that effectively improve the lost-K and shorter-J phenomena. The methods were evaluated on a time-aligned ECG-BCG dataset with 40 subjects. The results show that based on the transformed signal, simple J-peak-based methods using only the detection of local maxima or minima show better performance in locating J-peaks and extracting BCG cycles, especially for non-standard BCG data.

eess.SP↗
arXiv2025

Perspective-Invariant 3D Object Detection

With the rise of robotics, LiDAR-based 3D object detection has garnered significant attention in both academia and industry. However, existing datasets and methods predominantly focus on vehicle-mounted platforms, leaving other autonomous platforms underexplored. To bridge this gap, we introduce Pi3DET, the first benchmark featuring LiDAR data and 3D bounding box annotations collected from multiple platforms: vehicle, quadruped, and drone, thereby facilitating research in 3D object detection for non-vehicle platforms as well as cross-platform 3D detection. Based on Pi3DET, we propose a novel cross-platform adaptation framework that transfers knowledge from the well-studied vehicle platform to other platforms. This framework achieves perspective-invariant 3D detection through robust alignment at both geometric and feature levels. Additionally, we establish a benchmark to evaluate the resilience and robustness of current 3D detectors in cross-platform scenarios, providing valuable insights for developing adaptive 3D perception systems. Extensive experiments validate the effectiveness of our approach on challenging cross-platform tasks, demonstrating substantial gains over existing adaptation methods. We hope this work paves the way for generalizable and unified 3D perception systems across diverse and complex environments. Our Pi3DET dataset, cross-platform benchmark suite, and annotation toolkit have been made publicly available.

cs.CV↗
arXiv2025

The contribution of dilatational motion to energy flux in homogeneous compressible turbulence

We analyze the energy flux in compressible turbulence by generalizing the exact decomposition recently proposed by Johnson (Phys. Rev. Lett., vol. 124, 2020. 104501) to study incompressible turbulent flows. This allows us to characterize the effect of dilatational motion on the inter-scale energy transfer in three-dimensional compressible turbulence. Our analysis reveals that the contribution of dilatational motion to energy transfer is due to three different physical mechanisms: the interaction between dilatation and strain, between dilatation and vorticity, and the self-interaction of dilatational motion across scales. By analyzing numerical simulations of flows at moderate turbulent Mach numbers ($Ma_t \lesssim 0.3$), we validate our theoretical derivations and provide a quantitative description of the role of dilatational motion in energy transfer. In particular, we determine the scaling dependence of the dilatational contributions on the turbulent Mach number. Moreover, our findings reveal that the eddy-viscosity assumption often used in large-eddy simulations, in the spirit of the approach used for incompressible flows, effectively neglects the interaction between solenoidal-dilatational energy transfer and overestimate dilatational effects.

physics.flu-dyn↗
arXiv2025

PDM-SSD: Single-Stage Three-Dimensional Object Detector With Point Dilation

Current Point-based detectors can only learn from the provided points, with limited receptive fields and insufficient global learning capabilities for such targets. In this paper, we present a novel Point Dilation Mechanism for single-stage 3D detection (PDM-SSD) that takes advantage of these two representations. Specifically, we first use a PointNet-style 3D backbone for efficient feature encoding. Then, a neck with Point Dilation Mechanism (PDM) is used to expand the feature space, which involves two key steps: point dilation and feature filling. The former expands points to a certain size grid centered around the sampled points in Euclidean space. The latter fills the unoccupied grid with feature for backpropagation using spherical harmonic coefficients and Gaussian density function in terms of direction and scale. Next, we associate multiple dilation centers and fuse coefficients to obtain sparse grid features through height compression. Finally, we design a hybrid detection head for joint learning, where on one hand, the scene heatmap is predicted to complement the voting point set for improved detection accuracy, and on the other hand, the target probability of detected boxes are calibrated through feature fusion. On the challenging Karlsruhe Institute of Technology and Toyota Technological Institute (KITTI) dataset, PDM-SSD achieves state-of-the-art results for multi-class detection among single-modal methods with an inference speed of 68 frames. We also demonstrate the advantages of PDM-SSD in detecting sparse and incomplete objects through numerous object-level instances. Additionally, PDM can serve as an auxiliary network to establish a connection between sampling points and object centers, thereby improving the accuracy of the model without sacrificing inference speed. Our code will be available at https://github.com/AlanLiangC/PDM-SSD.git.

cs.CV↗
arXiv2024

SGCCNet: Single-Stage 3D Object Detector With Saliency-Guided Data Augmentation and Confidence Correction Mechanism

The single-stage point-based 3D object detectors have attracted widespread research interest due to their advantages of lightweight and fast inference speed. However, they still face challenges such as inadequate learning of low-quality objects (ILQ) and misalignment between localization accuracy and classification confidence (MLC). In this paper, we propose SGCCNet to alleviate these two issues. For ILQ, SGCCNet adopts a Saliency-Guided Data Augmentation (SGDA) strategy to enhance the robustness of the model on low-quality objects by reducing its reliance on salient features. Specifically, We construct a classification task and then approximate the saliency scores of points by moving points towards the point cloud centroid in a differentiable process. During the training process, SGCCNet will be forced to learn from low saliency features through dropping points. Meanwhile, to avoid internal covariate shift and contextual features forgetting caused by dropping points, we add a geometric normalization module and skip connection block in each stage. For MLC, we design a Confidence Correction Mechanism (CCM) specifically for point-based multi-class detectors. This mechanism corrects the confidence of the current proposal by utilizing the predictions of other key points within the local region in the post-processing stage. Extensive experiments on the KITTI dataset demonstrate the generality and effectiveness of our SGCCNet. On the KITTI \textit{test} set, SGCCNet achieves $80.82\%$ for the metric of $AP_{3D}$ on the \textit{Moderate} level, outperforming all other point-based detectors, surpassing IA-SSD and Fast Point R-CNN by $2.35\%$ and $3.42\%$, respectively. Additionally, SGCCNet demonstrates excellent portability for other point-based detectors

cs.CV↗
arXiv2024

Proving Functional Program Equivalence via Directed Lemma Synthesis

Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about algebraic data types (ADTs) and compositions of structural recursions. Modern theorem provers address this problem by applying structural induction, which is insufficient for proving many equivalence theorems. In such cases, one has to invent a set of lemmas, prove these lemmas by additional induction, and use these lemmas to prove the original theorem. There is, however, a lack of systematic understanding of what lemmas are needed for inductive proofs and how these lemmas can be synthesized automatically. This paper presents directed lemma synthesis, an effective approach to automating equivalence proofs by discovering critical lemmas using program synthesis techniques. We first identify two induction-friendly forms of propositions that give formal guarantees to the progress of the proof. We then propose two tactics that synthesize and apply lemmas, thereby transforming the proof goal into induction-friendly forms. Both tactics reduce lemma synthesis to a specialized class of program synthesis problems with efficient algorithms. Experimental results demonstrate the effectiveness of our approach: Compared to state-of-the-art equivalence checkers employing heuristic-based lemma enumeration, directed lemma synthesis saves 95.47% runtime on average and solves 38 more tasks over an extended version of the standard benchmark set.

cs.PL↗
arXiv2024

A practical approach of measuring $^{238}$U and $^{232}$Th in liquid scintillator to sub-ppq level using ICP-MS

Liquid scintillator (LS) is commonly utilized in experiments seeking rare events due to its high light yield, transparency, and radiopurity. The concentration of $^{238}$U and $^{232}$Th in LS consistently remains below 1 ppq (10$^{-15}$ g/g), and the current screening result is based on a minimum 20-ton detector. Inductively coupled plasma mass (ICP-MS) spectroscopy is well-regarded for its high sensitivity to trace $^{238}$U and $^{232}$Th. This study outlines a method for detecting $^{238}$U and $^{232}$Th in LS at the sub-ppq level using ICP-MS, involving the enrichment of $^{238}$U/$^{232}$Th from the LS through acid extraction. With meticulous cleanliness control, $^{238}$U/$^{232}$Th in approximately 2 kg of LS is concentrated by acid extraction with 0.4 (0.3) pg $^{238}$U ($^{232}$Th) contamination. Three standard adding methods are employed to assess recovery efficiency, including radon daughter, 2,5-diphenyloxazole (PPO), and natural non-existent $^{233}$U/$^{229}$Th. The method detection limit at a 99% confidence level of this approach can reach approximately 0.2-0.3 ppq for $^{238}$U/$^{232}$Th with nearly 100% recovery efficiency.

physics.ins-det↗
arXiv2023

Does generalization performance of $l^q$ regularization learning depend on $q$? A negative example

$l^q$-regularization has been demonstrated to be an attractive technique in machine learning and statistical modeling. It attempts to improve the generalization (prediction) capability of a machine (model) through appropriately shrinking its coefficients. The shape of a $l^q$ estimator differs in varying choices of the regularization order $q$. In particular, $l^1$ leads to the LASSO estimate, while $l^{2}$ corresponds to the smooth ridge regression. This makes the order $q$ a potential tuning parameter in applications. To facilitate the use of $l^{q}$-regularization, we intend to seek for a modeling strategy where an elaborative selection on $q$ is avoidable. In this spirit, we place our investigation within a general framework of $l^{q}$-regularized kernel learning under a sample dependent hypothesis space (SDHS). For a designated class of kernel functions, we show that all $l^{q}$ estimators for $0< q < \infty$ attain similar generalization error bounds. These estimated bounds are almost optimal in the sense that up to a logarithmic factor, the upper and lower bounds are asymptotically identical. This finding tentatively reveals that, in some modeling contexts, the choice of $q$ might not have a strong impact in terms of the generalization capability. From this perspective, $q$ can be arbitrarily specified, or specified merely by other no generalization criteria like smoothness, computational complexity, sparsity, etc..

cs.LG↗
arXiv2023

Direct numerical simulation of inflow boundary-layer turbulence effects on cavity flame stabilisation in a model scramjet combustor

Supersonic lean premixed hydrogen/air combustion stabilised by a cavity-flame holder within a model scramjet, characterized by a Mach 1.5 inflow at 1000 K and 50 kPa, is investigated via direct numerical simulation. By separately implementing wall-bounded turbulent and laminar inlet conditions, this work analysis various physical processes of flame stabilization and turbulence-flame interactions to study the influence of inflow boundary layer conditions. Findings indicate that combustion occurred within the cavity shear layer in both cases and propagated downstream along the lower wall. Also, the server impingement at the rear wall in the case with laminar inflow leads to greater cavity resistance. Furthermore, the studies on gas exchange and transport process indicates that with laminar inflow the entered gas accumulates in the back part of the cavity via the intensive mass exchange process and weaker interaction between the primary and secondary vortices. Flame stretch and thickness are further investigated to shed light into turbulence-flame interaction in supersonic flows. Findings indicates that the case with inflow wall-bounded turbulence show similar behaviours compared to previous studies, whereas the observed phenomena in front part of cavity shear layer are differ due to the presence of roll-up vortices in the case with laminar inflow. Overall, the influence of tangential strain rate and curvature are consistent with the preceding results and the evolution of flame thickness is caused by the combined effect of the two factors in both cases.

physics.flu-dyn↗
arXiv2022

NNPred: A Predictor Library to Deploy Neural Networks in Computational Fluid Dynamics software

A neural-networks predictor library has been developed to deploy machine learning (ML) models into computational fluid dynamics (CFD) codes. The pointer-to-implementation strategy is adopted to isolate the implementation details in order to simplify the implementation to CFD solvers. The library provides simplified model-managing functions by encapsulating the TensorFlow C library, and it maintains self-belonging data containers to deal with data type casting and memory layouts in the input/output (I/O) functions interfacing with CFD solvers. On the language level, the library provides application programming interfaces (APIs) for C++ and Fortran, the two commonly used programming languages in the CFD community. High-level customized modules are developed for two open-source CFD codes, OpenFOAM and CFL3D, written with C++ and Fortran, respectively. The basic usage of the predictor is demonstrated in a simple data-driven heat transfer problem as the first tutorial case. Another tutorial case of modeling the effect of turbulence in channel flow using the library is implemented in both OpenFOAM and CFL3D codes. The developed ML predictor library provides a powerful tool for the deployment of ML models in CFD solvers.

physics.flu-dyn↗
arXiv2022

Low-order moments of the velocity gradient in homogeneous compressible turbulence

We derive from first principles analytic relations for the second and third order moments of the velocity gradient mij = dui/dxj in compressible turbulence, which generalize known relations in incompressible flows. These relations, although derived for homogeneous flows, hold approximately for a mixing layer. We also discuss how to apply these relations to determine all the second and third moments of the velocity gradient experimentally.

physics.flu-dyn↗