arXiv subjects

Shuai Lu

Publications and source records attributed to Shuai Lu.

At least 55 records · Page 3Linked to original sources

arXiv2025

A Recursive Algorithm for Multi-Coefficient Inversion in Nonlinear Helmholtz Equations

We present a recursive algorithm for multi-coefficient inversion in nonlinear Helmholtz equations with polynomial-type nonlinearities, utilizing the linearized Dirichlet-to-Neumann map as measurement data. To achieve effective recursive decoupling and simultaneous recovery of multiple coefficients, we develop a novel Fourier-based approach that combines the principle of inclusion-exclusion with carefully constructed complex exponential solutions. This methodology not only ensures unique identifiability but also yields progressively increasing stability with enhanced wavenumbers. Comprehensive numerical experiments demonstrate the algorithm's computational efficiency and excellent reconstruction accuracy.

math.AP↗

arXiv2025

AutoVerus: Automated Proof Generation for Rust Code

Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLMs to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.

cs.SE↗

arXiv2025

UrbanSense:A Framework for Quantitative Analysis of Urban Streetscapes leveraging Vision Large Language Models

Urban cultures and architectural styles vary significantly across cities due to geographical, chronological, historical, and socio-political factors. Understanding these differences is essential for anticipating how cities may evolve in the future. As representative cases of historical continuity and modern innovation in China, Beijing and Shenzhen offer valuable perspectives for exploring the transformation of urban streetscapes. However, conventional approaches to urban cultural studies often rely on expert interpretation and historical documentation, which are difficult to standardize across different contexts. To address this, we propose a multimodal research framework based on vision-language models, enabling automated and scalable analysis of urban streetscape style differences. This approach enhances the objectivity and data-driven nature of urban form research. The contributions of this study are as follows: First, we construct UrbanDiffBench, a curated dataset of urban streetscapes containing architectural images from different periods and regions. Second, we develop UrbanSense, the first vision-language-model-based framework for urban streetscape analysis, enabling the quantitative generation and comparison of urban style representations. Third, experimental results show that Over 80% of generated descriptions pass the t-test (p less than 0.05). High Phi scores (0.912 for cities, 0.833 for periods) from subjective evaluations confirm the method's ability to capture subtle stylistic differences. These results highlight the method's potential to quantify and interpret urban style evolution, offering a scientifically grounded lens for future design.

cs.CV↗

arXiv2025

ArchiLense: A Framework for Quantitative Analysis of Architectural Styles Based on Vision Large Language Models

Architectural cultures across regions are characterized by stylistic diversity, shaped by historical, social, and technological contexts in addition to geograph-ical conditions. Understanding architectural styles requires the ability to describe and analyze the stylistic features of different architects from various regions through visual observations of architectural imagery. However, traditional studies of architectural culture have largely relied on subjective expert interpretations and historical literature reviews, often suffering from regional biases and limited ex-planatory scope. To address these challenges, this study proposes three core contributions: (1) We construct a professional architectural style dataset named ArchDiffBench, which comprises 1,765 high-quality architectural images and their corresponding style annotations, collected from different regions and historical periods. (2) We propose ArchiLense, an analytical framework grounded in Vision-Language Models and constructed using the ArchDiffBench dataset. By integrating ad-vanced computer vision techniques, deep learning, and machine learning algo-rithms, ArchiLense enables automatic recognition, comparison, and precise classi-fication of architectural imagery, producing descriptive language outputs that ar-ticulate stylistic differences. (3) Extensive evaluations show that ArchiLense achieves strong performance in architectural style recognition, with a 92.4% con-sistency rate with expert annotations and 84.5% classification accuracy, effec-tively capturing stylistic distinctions across images. The proposed approach transcends the subjectivity inherent in traditional analyses and offers a more objective and accurate perspective for comparative studies of architectural culture.

cs.CV↗

arXiv2025

FloorplanMAE:A self-supervised framework for complete floorplan generation from partial inputs

In the architectural design process, floorplan design is often a dynamic and iterative process. Architects progressively draw various parts of the floorplan according to their ideas and requirements, continuously adjusting and refining throughout the design process. Therefore, the ability to predict a complete floorplan from a partial one holds significant value in the design process. Such prediction can help architects quickly generate preliminary designs, improve design efficiency, and reduce the workload associated with repeated modifications. To address this need, we propose FloorplanMAE, a self-supervised learning framework for restoring incomplete floor plans into complete ones. First, we developed a floor plan reconstruction dataset, FloorplanNet, specifically trained on architectural floor plans. Secondly, we propose a floor plan reconstruction method based on Masked Autoencoders (MAE), which reconstructs missing parts by masking sections of the floor plan and training a lightweight Vision Transformer (ViT). We evaluated the reconstruction accuracy of FloorplanMAE and compared it with state-of-the-art benchmarks. Additionally, we validated the model using real sketches from the early stages of architectural design. Experimental results show that the FloorplanMAE model can generate high-quality complete floor plans from incomplete partial plans. This framework provides a scalable solution for floor plan generation, with broad application prospects.

cs.AI↗

arXiv2025

FloorPlan-DeepSeek (FPDS): A multimodal approach to floorplan generation using vector-based next room prediction

In the architectural design process, floor plan generation is inherently progressive and iterative. However, existing generative models for floor plans are predominantly end-to-end generation that produce an entire pixel-based layout in a single pass. This paradigm is often incompatible with the incremental workflows observed in real-world architectural practice. To address this issue, we draw inspiration from the autoregressive 'next token prediction' mechanism commonly used in large language models, and propose a novel 'next room prediction' paradigm tailored to architectural floor plan modeling. Experimental evaluation indicates that FPDS demonstrates competitive performance in comparison to diffusion models and Tell2Design in the text-to-floorplan task, indicating its potential applicability in supporting future intelligent architectural design.

cs.CL↗

arXiv2025

A Cascading Cooperative Multi-agent Framework for On-ramp Merging Control Integrating Large Language Models

Traditional Reinforcement Learning (RL) suffers from replicating human-like behaviors, generalizing effectively in multi-agent scenarios, and overcoming inherent interpretability issues.These tasks are compounded when deep environment understanding, agent coordination and dynamic optimization are required. While Large Language Model (LLM) enhanced methods have shown promise in generalization and interoperability, they often neglect necessary multi-agent coordination. Therefore, we introduce the Cascading Cooperative Multi-agent (CCMA) framework, integrating RL for individual interactions, a fine-tuned LLM for regional cooperation, a reward function for global optimization, and the Retrieval-augmented Generation mechanism to dynamically optimize decision-making across complex driving scenarios. Our experiments demonstrate that the CCMA outperforms existing RL methods, demonstrating significant improvements in both micro and macro-level performance in complex driving environments.

cs.CV↗

arXiv2025

Alleviating CoD in Renewable Energy Profile Clustering Using an Optical Quantum Computer

The traditional clustering problem of renewable energy profiles is typically formulated as a combinatorial optimization that suffers from the Curse of Dimensionality (CoD) on classical computers. To address this issue, this paper first proposed a kernel-based quantum clustering method. More specifically, the kernel-based similarity between profiles with minimal intra-group distance is encoded into the ground-state of the Hamiltonian in the form of an Ising model. Then, this NP-hard problem can be reformulated into a Quadratic Unconstrained Binary Optimization (QUBO), which a Coherent Ising Machine (CIM) can naturally solve with significant improvement over classical computers. The test results from a real optical quantum computer verify the validity of the proposed method. It also demonstrates its ability to address CoD in an NP-hard clustering problem.

quant-ph↗

arXiv2025

ArchShapeNet:An Interpretable 3D-CNN Framework for Evaluating Architectural Shapes

In contemporary architectural design, the growing complexity and diversity of design demands have made generative plugin tools essential for quickly producing initial concepts and exploring novel 3D forms. However, objectively analyzing the differences between human-designed and machine-generated 3D forms remains a challenge, limiting our understanding of their respective strengths and hindering the advancement of generative tools. To address this, we built ArchForms-4000, a dataset containing 2,000 architect-designed and 2,000 Evomass-generated 3D forms; Proposed ArchShapeNet, a 3D convolutional neural network tailored for classifying and analyzing architectural forms, incorporating a saliency module to highlight key spatial features aligned with architectural reasoning; And conducted comparative experiments showing our model outperforms human experts in distinguishing form origins, achieving 94.29% accuracy, 96.2% precision, and 98.51% recall. This study not only highlights the distinctive advantages of human-designed forms in spatial organization, proportional harmony, and detail refinement but also provides valuable insights for enhancing generative design tools in the future.

cs.CV↗

arXiv2025

A highly scalable numerical framework for reservoir simulation on UG4 platform

The modeling and simulation of multiphase fluid flow receive significant attention in reservoir engineering. Many time discretization schemes for multiphase flow equations are either explicit or semi-implicit, relying on the decoupling between the saturation equation and the pressure equation. In this study, we delve into a fully coupled and fully implicit framework for simulating multiphase flow in heterogeneous porous media, considering gravity and capillary effects. We utilize the Vertex-Centered Finite Volume Method for spatial discretization and propose an efficient implementation of interface conditions for heterogeneous porous media within the current scheme. Notably, we introduce the Linearly Implicit Extrapolation Method (LIMEX) with an error estimator, adapted for the first time to multiphase flow problems. To solve the resulting linear system, we employ the BiCGSTAB method with the Geometric Multigrid (GMG) preconditioner. The implementations of models and methods are based on the open-source software: UG4. The results from parallel computations on the supercomputer demonstrate that the scalability of our proposed framework is sufficient, supporting a scale of thousands of processors with Degrees of Freedom (DoF) extending up to billions.

physics.comp-ph↗

arXiv2025

Integrating Building Thermal Flexibility Into Distribution System: A Privacy-Preserved Dispatch Approach

The inherent thermal storage capacity of buildings brings considerable thermal flexibility to the heating/cooling loads, which are promising demand response resources for power systems. It is widely believed that integrating the thermal flexibility of buildings into the distribution system can improve the operating economy and reliability of the system. However, the private information of the buildings needs to be transferred to the distribution system operator (DSO) to achieve a coordinated optimization, bringing serious privacy concerns to users. Given this issue, we propose a novel privacy-preserved optimal dispatch approach for the distribution system incorporating buildings. Using it, the DSO can exploit the thermal flexibility of buildings without accessing their private information, such as model parameters and indoor temperature profiles. Specifically, we first develop an optimal dispatch model for the distribution system integrating buildings, which can be extended to other storage-like flexibility resources. Second, we reveal that the privacy-preserved integration of buildings is a joint privacy preservation problem for both parameters and state variables and then design a privacy-preserved algorithm based on transformation-based encryption, constraint relaxation, and constraint extension techniques. Besides, we implement a detailed privacy analysis for the proposed method, considering both semi-honest adversaries and external eavesdroppers. Case studies demonstrate the accuracy, privacy-preserved performance, and computational efficiency of the proposed method.

eess.SY↗

arXiv2025

Unveiling a young thick disk in the Milky Way

The thickness of a galaxy's disk provides a valuable probe of its formation and evolution history. Observations of the Milky Way and local galaxies have revealed an ubiquitous disk structure with two distinctive components: an old thick disk and a relatively young thin disk. The formation of this dual-disk structure and the mechanisms that develop the thickness of the disk are still unclear. Whether the disk thickness inherit from the birth environment or is established through secular dynamical heating after formation is under debate. In this work we identify a relatively young ($\sim$6.6 billion years old) geometric thick disk in the Milky Way, with a scale height of $0.64$ kpc at the Solar Circle. This young thick component exhibits comparable thickness and flaring strength to the canonical old thick disk but is more radially extended and systematically younger. We also identify thin disk components that formed before and after this young thick disk. Detailed analysis of the solar vicinity structure suggests that the young thick disk marks the onset of a new phase of upside-down disk formation. These findings strongly discount the role of secular dynamical heating and support a turbulent, bursty birth environment as the primary mechanism behind thick disk formation. The existence of two thick disk components suggests that the Milky Way has undergone at least two episodes of turbulent and bursty star formation, likely triggered by galaxy mergers.

astro-ph.GA↗

arXiv2025

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves a 2.47% absolute performance gain on the out-of-distribution miniF2F benchmark based on the synthetic data.To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.

cs.AI↗

arXiv2025

Dinomaly: The Less Is More Philosophy in Multi-Class Unsupervised Anomaly Detection

Recent studies highlighted a practical setting of unsupervised anomaly detection (UAD) that builds a unified model for multi-class images. Despite various advancements addressing this challenging task, the detection performance under the multi-class setting still lags far behind state-of-the-art class-separated models. Our research aims to bridge this substantial performance gap. In this paper, we introduce a minimalistic reconstruction-based anomaly detection framework, namely Dinomaly, which leverages pure Transformer architectures without relying on complex designs, additional modules, or specialized tricks. Given this powerful framework consisted of only Attentions and MLPs, we found four simple components that are essential to multi-class anomaly detection: (1) Foundation Transformers that extracts universal and discriminative features, (2) Noisy Bottleneck where pre-existing Dropouts do all the noise injection tricks, (3) Linear Attention that naturally cannot focus, and (4) Loose Reconstruction that does not force layer-to-layer and point-by-point reconstruction. Extensive experiments are conducted across popular anomaly detection benchmarks including MVTec-AD, VisA, and Real-IAD. Our proposed Dinomaly achieves impressive image-level AUROC of 99.6%, 98.7%, and 89.3% on the three datasets respectively, which is not only superior to state-of-the-art multi-class UAD methods, but also achieves the most advanced class-separated UAD records.

cs.CV↗

arXiv2025

IllustrisTNG Insights: Factors Affecting the Presence of Bars in Disk Galaxies

Bars are important in the secular evolution of galaxies. This study is aimed at exploring the reasons why some galaxies have bars at redshift $z=0$ while others do not. We use ellipse fitting to measure the properties and evolution of bars in the IllustrisTNG cosmological simulation. By using the K-S two-sample test and tracing their evolutionary changes, we analyze the parameter differences between barred and unbarred galaxies. The properties of galaxies with short bars are also studied. When tracing all disk galaxies at $z=0$ back to $z=1$, all of them show similar bar features at $z=1$. The fraction of bars increases in barred and short-bar galaxies but decreases in unbarred galaxies during $z=1-0$. In the case of disk galaxies with stellar mass log$(M_*/M_\odot)> 10.8$, nurture (mainly mergers) plays the most important role in suppressing or destroying bars. Bars are more likely to endure in galaxies that experience fewer mergers, which can be quantified by smaller stellar halos and ex-situ mass fractions. Approximately 60\% of the unbarred galaxies in the local Universe once had a bar. In contrast, the lack of responsiveness to bar instabilities (a larger Toomre-Q parameter) due to a less compact nature plays an important role in generating unbarred disk galaxies with stellar mass log$(M_*/M_\odot)<10.8$. Moreover, short bars generally form at a similar time to normal bars, during which they either grow mildly or contract significantly. The fact that IllustrisTNG simulations produce too many galaxies with short bars indicates that the dynamical properties of the central regions in IllustrisTNG galaxies are less affected by external factors, such as mergers and gas inflows.

astro-ph.GA↗

arXiv2025

Fast Critical Clearing Time Calculation for Power Systems with Synchronous and Asynchronous Generation

The increasing penetration of renewables is replacing traditional synchronous generation in modern power systems with low-inertia asynchronous converter-interfaced generators (CIGs). This penetration threatens the dynamic stability of the modern power system. To assess the latter, we resort to the critical clearing time (CCT) as a stability index, which is typically computed through a large number of time-domain simulations. This is especially true for CIG-embedded power systems, where the complexity of the model is further increased. To alleviate the computing burden, we developed a trajectory sensitivity-based method for assessing the CCT in power systems with synchronous and asynchronous generators. This allows us to obtain the CCT cost-effectively. The simulation results reveal the excellent performance of the proposed method.

eess.SY↗

arXiv2025

TSCnet: A Text-driven Semantic-level Controllable Framework for Customized Low-Light Image Enhancement

Deep learning-based image enhancement methods show significant advantages in reducing noise and improving visibility in low-light conditions. These methods are typically based on one-to-one mapping, where the model learns a direct transformation from low light to specific enhanced images. Therefore, these methods are inflexible as they do not allow highly personalized mapping, even though an individual's lighting preferences are inherently personalized. To overcome these limitations, we propose a new light enhancement task and a new framework that provides customized lighting control through prompt-driven, semantic-level, and quantitative brightness adjustments. The framework begins by leveraging a Large Language Model (LLM) to understand natural language prompts, enabling it to identify target objects for brightness adjustments. To localize these target objects, the Retinex-based Reasoning Segment (RRS) module generates precise target localization masks using reflection images. Subsequently, the Text-based Brightness Controllable (TBC) module adjusts brightness levels based on the generated illumination map. Finally, an Adaptive Contextual Compensation (ACC) module integrates multi-modal inputs and controls a conditional diffusion model to adjust the lighting, ensuring seamless and precise enhancements accurately. Experimental results on benchmark datasets demonstrate our framework's superior performance at increasing visibility, maintaining natural color balance, and amplifying fine details without creating artifacts. Furthermore, its robust generalization capabilities enable complex semantic-level lighting adjustments in diverse open-world environments through natural language interactions.

cs.CV↗

arXiv2025

PromptLNet: Region-Adaptive Aesthetic Enhancement via Prompt Guidance in Low-Light Enhancement Net

Learning and improving large language models through human preference feedback has become a mainstream approach, but it has rarely been applied to the field of low-light image enhancement. Existing low-light enhancement evaluations typically rely on objective metrics (such as FID, PSNR, etc.), which often result in models that perform well objectively but lack aesthetic quality. Moreover, most low-light enhancement models are primarily designed for global brightening, lacking detailed refinement. Therefore, the generated images often require additional local adjustments, leading to research gaps in practical applications. To bridge this gap, we propose the following innovations: 1) We collect human aesthetic evaluation text pairs and aesthetic scores from multiple low-light image datasets (e.g., LOL, LOL2, LOM, DCIM, MEF, etc.) to train a low-light image aesthetic evaluation model, supplemented by an optimization algorithm designed to fine-tune the diffusion model. 2) We propose a prompt-driven brightness adjustment module capable of performing fine-grained brightness and aesthetic adjustments for specific instances or regions. 3) We evaluate our method alongside existing state-of-the-art algorithms on mainstream benchmarks. Experimental results show that our method not only outperforms traditional methods in terms of visual quality but also provides greater flexibility and controllability, paving the way for improved aesthetic quality.

cs.CV↗