arXiv subjects

Yuxuan Xiao

Publications and source records attributed to Yuxuan Xiao.

At least 19 recordsLinked to original sources

arXiv2026

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.

cs.AI↗

arXiv2026

Beyond Facial Consistency: Personalized Person Image Generation with Holistic Identity Preservation

Personalized person image generation requires preserving subject identity across both local facial details and broader appearance cues. Existing methods typically emphasize only one level of identity information, leading to an inherent trade-off between facial fidelity and overall appearance consistency. To address this, we first propose a simple dual-branch baseline that unifies global appearance control and local facial control within a shared generation framework. This simple combination of different branches yields promising results, but suffers from instability in practice due to uncoordinated branch contributions. To this end, we propose Dynamic Balancing Scaling (DBS), a fine-tuning strategy for improving face and appearance identity coordination. DBS consists of two components: adaptive temporal gating, which dynamically modulates branch contributions along the denoising trajectory, and region-aware optimization, which improves the coordination of facial, appearance, and global supervision. Together, these designs alleviate persistent face-branch over-dominance and encourage more effective appearance-aware guidance. We also introduce Pexels-100, a benchmark for evaluating holistic identity consistency in personalized person generation. Experiments show that DBS achieves a better trade-off between facial fidelity and appearance consistency than existing open-source baselines, while providing a controllable basic framework for holistic identity modeling.

cs.CV↗

arXiv2026

Schanuel Integration and Euler Characteristic of Semi-algebraic Sets

We extend the Schanuel integration framework, originally introduced for finite unions of convex sets, to arbitrary semi-algebraic sets. We prove that the resulting Schanuel integral of indicator functions is independent of the choice of ordered linear bases and therefore defines a well-defined Euler characteristic in the semi-algebraic category. We further show that this Schanuel--Euler characteristic coincides with the classical Euler characteristic defined via Borel--Moore homology and cylindrical algebraic decomposition. The recursive fiberwise structure of Schanuel integration provides an elementary and geometric interpretation of Euler characteristic and yields simplified proofs of several classical properties, including invariance under semi-algebraic isomorphisms.

math.AG↗

arXiv2026

A Double Bind: Gendered Funding, Research Topics, and Academic Performance in the Social Sciences

While female representation in social sciences is increasing, systemic gender disparities may persist in research funding and academic performance. Some argue that female scholars now receive equal opportunities, yet evidence suggests that gender imbalances remain, particularly in specific research areas. This study examines 12,945 National Science Foundation (NSF)-funded principal investigators in social sciences from 2000 to 2019 to assess gender disparities in grant allocation, research topics, and post-award academic performance. Findings reveal a dual imbalance. First, despite similar overall funding success rates, female scholars remain underrepresented in high-impact and traditionally male-dominated research topics. Male recipients are more represented in most funded topics, especially technology- and methodology-related ones, whereas female recipients are more concentrated in a smaller set of topics related to children, family, cognition, and health. Second, post-award performance patterns suggest that females outperform males in male-dominated fields, whereas males excel in female-dominated ones, undermining any presumed advantage of female scholars in their own research areas. These patterns may be associated with gendered constraints in academic career trajectories. Furthermore, early-career experiences shape these outcomes asymmetrically. In male-dominated topics, postdoctoral experience is associated with lower publication and citation performance for women but higher publication and citation performance for men. In female-dominated topics, postdoctoral experience is positively associated with women's publications and citations and with men's publication output. These findings suggest that policy discussions should consider not just overall funding equality, but also gendered disparities across research topics and career trajectories.

cs.DL↗

arXiv2026

How Proposal Novelty, Topical Diversity, and Theory-Practice Balance Shape Scholarly Outcomes in Funded Education Research

Education research occupies a distinctive position in public science because it is expected to advance scholarly knowledge while also informing learning, teaching, participation, and workforce development. This study examines how the intellectual characteristics of NSF-funded education proposals are associated with the subsequent academic performance of funded scholars. Linking 8,715 NSF education awards from 1990 to 2020 with 84,519 publications by principal investigators, the analysis focuses on four major NSF education divisions that collectively span undergraduate and graduate levels, formal and informal learning environments, and inclusive educational initiatives. Proposal novelty is measured as semantic distance from prior funded projects within the same division, topical diversity as breadth across latent research themes, and intellectual orientation as theoretical, practical, or balanced. The results show that NSF education funding is consistently associated with higher publication output across divisions. However, this increase is not accompanied by stronger citation performance or higher journal-level visibility; citation and CiteScore estimates are often negative, particularly in later decades. Proposal novelty shows limited and uneven associations with post-award outcomes, whereas topical diversity is more clearly related to publication growth in some divisions but weaker citation-based performance in others. Balanced proposals that integrate theoretical and practical aims display the most favourable overall profile, combining positive publication associations with fewer negative citation-based patterns. These findings highlight the importance of evaluating education research funding through multiple academic outcomes and division-specific research contexts.

cs.DL↗

arXiv2026

Diffusion Attention Expert Model for Predicting and Semi-automatic Localizing STAS in Lung Cancer Histopathological Images

Accurate intraoperative and postoperative diagnosis of spread through air spaces (STAS) is essential for guiding surgical decisions and postoperative management in lung cancer. However, histopathological assessment is labor-intensive and is prone to missed or incorrect diagnoses. We propose a Diffusion Attention Expert Model (DAEM) to detect STAS in frozen sections (FSs) and paraffin sections (PSs). Its diffusion attention expert module leverages full attention aggregation to learn multi-scale features from histopathological images, while a dual-branch architecture strengthens multi-scale feature representation. On an internal dataset, DAEM achieves AUCs of 0.8946 for FSs and 0.9112 for PSs. Validation on external multi-center datasets from eight institutions demonstrates strong generalizability and interpretability. Using tumor microenvironment (TME) features in PSs, we further enable semi-automatic measurement of STAS location and its distance from the primary tumor. Several quantitative TME metrics are identified as potential biomarkers for STAS, including micropapillary-type STAS. Overall, DAEM offers a clinically actionable framework for STAS assessment by enabling accurate and interpretable detection on FSs and PSs, supporting postoperative risk stratification through quantitative TME-based analysis.

cs.CV↗

arXiv2026

Head Similarity: Modeling Structured Whole-Head Appearance Beyond Face Recognition

Many vision applications require identity consistency beyond strict biometric recognition, especially under non-frontal views or when facial cues are missing. However, conventional face recognition models enforce intra-identity invariance, collapsing appearance variations such as hairstyle or styling changes into a single representation, limiting their use in appearance-sensitive scenarios. To address this limitation, we introduce Head Similarity, a new formulation that extends identity-centric recognition to structured whole-head similarity modeling. Our approach explicitly captures intra-identity appearance variation and enforces hierarchical similarity ordering across identity and appearance states, enabling meaningful comparison even under occlusion or rear-view conditions. We construct a large-scale benchmark from long-form videos with weakly-supervised appearance states, covering diverse poses, occlusions, and temporal changes. As a first step, we develop a simple yet effective framework that jointly models identity discrimination and appearance-sensitive similarity through hierarchical supervision and identity-aware distillation. Experiments show that conventional face recognition models fail to capture appearance-dependent similarity, while our approach demonstrates the feasibility of structured whole-head similarity modeling.

cs.CV↗

arXiv2026

Rethinking Multi-Label Node Classification: Do Tuned Classic GNNs Suffice?

Multi-label node classification (MLNC) has recently been addressed by increasingly complex label-aware designs that explicitly model node-label interactions and inter-label dependencies.However, it remains unclear whether the advantages of these methods truly stem from their specialized designs, or simply from insufficiently optimized baselines. In this paper, we revisit MLNC from a strong-baseline perspective and investigate whether carefully tuned classic full-graph GNNs can already serve as strong solutions to this task. We systematically study several representative backbones, including GCN, SSGConv, and GCNII, and optimize them using standard yet effective techniques such as normalization, dropout, and residual connections. Experiments on five representative benchmark datasets show that our tuned baselines outperform representative specialized methods on four datasets and achieve state-of-the-art performance in multiple settings. These results indicate that careful tuning of classic backbones is a highly influential but often overlooked factor in MLNC, and highlight the need for more rigorous strong-baseline evaluation in future research on multi-label graph learning.

cs.LG↗

arXiv2026

CORP: A Multi-Modal Dataset for Campus-Oriented Roadside Perception Tasks

Numerous roadside perception datasets have been introduced to propel advancements in autonomous driving and intelligent transportation systems research and development. However, it has been observed that the majority of their concentrates is on urban arterial roads, inadvertently overlooking residential areas such as parks and campuses that exhibit entirely distinct characteristics. In light of this gap, we propose CORP, which stands as the first public benchmark dataset tailored for multi-modal roadside perception tasks under campus scenarios. Collected in a university campus, CORP consists of over 205k images plus 102k point clouds captured from 18 cameras and 9 LiDAR sensors. These sensors with different configurations are mounted on roadside utility poles to provide diverse viewpoints within the campus region. The annotations of CORP encompass multi-dimensional information beyond 2D and 3D bounding boxes, providing extra support for 3D seamless tracking and instance segmentation with unique IDs and pixel masks for identifying targets, to enhance the understanding of objects and their behaviors distributed across the campus premises. Unlike other roadside datasets about urban traffic, CORP extends the spectrum to highlight the challenges for multi-modal perception in campuses and other residential areas.

cs.CV↗

arXiv2026

Formalizing Wu-Ritt Method in Lean 4

We formalize the Wu-Ritt characteristic set method for the triangular decomposition of polynomial systems in the Lean 4 theorem prover. Our development includes the core algebraic notions of the method, such as polynomial initials, orders, pseudo-division, pseudo-remainders with respect to a polynomial or a triangular set, and standard and weak ascending sets. On this basis, we formalize algorithms for computing basic sets, characteristic sets, and zero decompositions, and prove their termination and correctness. In particular, we formalize the well-ordering principle relating a polynomial system to its characteristic set and verify that zero decomposition expresses the zero set of the original system as a union of zero sets of triangular sets away from the zeros of the corresponding initials. This work provides a machine-checked verification of Wu-Ritt's method in Lean 4 and establishes a foundation for certified polynomial system solving and geometric theorem proving.

math.AC↗

arXiv2024

SoccerNet 2024 Challenges Results

The SoccerNet 2024 challenges represent the fourth annual video understanding challenges organized by the SoccerNet team. These challenges aim to advance research across multiple themes in football, including broadcast video understanding, field understanding, and player understanding. This year, the challenges encompass four vision-based tasks. (1) Ball Action Spotting, focusing on precisely localizing when and which soccer actions related to the ball occur, (2) Dense Video Captioning, focusing on describing the broadcast with natural language and anchored timestamps, (3) Multi-View Foul Recognition, a novel task focusing on analyzing multiple viewpoints of a potential foul incident to classify whether a foul occurred and assess its severity, (4) Game State Reconstruction, another novel task focusing on reconstructing the game state from broadcast videos onto a 2D top-view map of the field. Detailed information about the tasks, challenges, and leaderboards can be found at https://www.soccer-net.org, with baselines and development kits available at https://github.com/SoccerNet.

cs.CV↗

arXiv2024

Unconventional Field-Like Spin-Torques in CrPt$_3$

The topological semimetal CrPt$_3$ has potential for generating unconventional spin torques due to its ferrimagnetic ordering, topological band structure, and high anomalous Hall effect. CrPt$_3$ exhibits ferrimagnetic behavior only in its chemically ordered phase and is paramagnetic in its chemically disordered phase. By controlling the growth and annealing temperatures, epitaxial films of both chemically ordered and disordered phases of CrPt$_3$ are prepared allowing us to investigate the role of magnetic ordering on unconventional torque generation. We use angle dependent spin-torque ferromagnetic resonance and second harmonic Hall measurements to probe the spin torques generated from epitaxial CrPt$_3$ in CrPt$_3$/Cu/Ni$_{81}$Fe$_{19}$ heterostructures. With current applied along specific directions with respect to the crystal order we reveal unconventional spin torques in both ordered and disordered films. When current flows parallel to the $[1\overline{1}1]$ and $[\overline{1}11]$ directions we observe an unconventional field-like torque that is opposite in sign for the two directions. Our calculations reveal that this unconventional torque originates from an indirect nonlocal spin-orbit torque due to spin scattering at the CrPt$_3$/Cu interface, in addition to symmetry breaking at this interface.

cond-mat.mtrl-sci↗

arXiv2024

CalibFormer: A Transformer-based Automatic LiDAR-Camera Calibration Network

The fusion of LiDARs and cameras has been increasingly adopted in autonomous driving for perception tasks. The performance of such fusion-based algorithms largely depends on the accuracy of sensor calibration, which is challenging due to the difficulty of identifying common features across different data modalities. Previously, many calibration methods involved specific targets and/or manual intervention, which has proven to be cumbersome and costly. Learning-based online calibration methods have been proposed, but their performance is barely satisfactory in most cases. These methods usually suffer from issues such as sparse feature maps, unreliable cross-modality association, inaccurate calibration parameter regression, etc. In this paper, to address these issues, we propose CalibFormer, an end-to-end network for automatic LiDAR-camera calibration. We aggregate multiple layers of camera and LiDAR image features to achieve high-resolution representations. A multi-head correlation module is utilized to identify correlations between features more accurately. Lastly, we employ transformer architectures to estimate accurate calibration parameters from the correlation information. Our method achieved a mean translation error of $0.8751 \mathrm{cm}$ and a mean rotation error of $0.0562 ^{\circ}$ on the KITTI dataset, surpassing existing state-of-the-art methods and demonstrating strong robustness, accuracy, and generalization capabilities.

cs.CV↗

arXiv2023

Local control of a single nitrogen-vacancy center by nanoscale engineered magnetic domain wall motions

Effective control and readout of qubits form the technical foundation of next-generation, transformative quantum information sciences and technologies. The nitrogen-vacancy (NV) center, an intrinsic three-level spin system, is naturally relevant in this context due to its excellent quantum coherence, high fidelity of operations, and remarkable functionality over a broad range of experimental conditions. It is an active contender for the development and implementation of cutting-edge quantum technologies. Here, we report magnetic domain wall motion driven local control and measurements of NV spin properties. By engineering the local magnetic field environment of an NV center via nanoscale reconfigurable domain wall motions, we show that NV photoluminescence, spin level energies, and coherence time can be reliably controlled and correlated to the magneto-transport response of a magnetic device. Our results highlight the electrically tunable dipole interaction between NV centers and nanoscale magnetic structures, providing an attractive platform to realize interactive information transfer between spin qubits and non-volatile magnetic memory in hybrid quantum spintronic systems.

cond-mat.mes-hall↗

arXiv2023

Nanoscale magnetic domains in polycrystalline Mn3Sn films imaged by a scanning single-spin magnetometer

Noncollinear antiferromagnets with novel magnetic orders, vanishingly small net magnetization and exotic spin related properties hold enormous promise for developing next-generation, transformative spintronic applications. A major ongoing research focus of this community is to explore, control, and harness unconventional magnetic phases of this emergent material system to deliver state-of-the-art functionalities for modern microelectronics. Here we report direct imaging of magnetic domains of polycrystalline Mn3Sn films, a prototypical noncollinear antiferromagnet, using nitrogen-vacancy-based single-spin scanning microscopy. Nanoscale evolution of local stray field patterns of Mn3Sn samples are systematically investigated in response to external driving forces, revealing the characteristic "heterogeneous" magnetic switching behaviors in polycrystalline textured Mn3Sn films. Our results contribute to a comprehensive understanding of inhomogeneous magnetic orders of noncollinear antiferromagnets, highlighting the potential of nitrogen-vacancy centers to study microscopic spin properties of a broad range of emergent condensed matter systems.

cond-mat.mes-hall↗

arXiv2022

Quantum sensing and imaging of spin-orbit-torque-driven spin dynamics in noncollinear antiferromagnet Mn3Sn

Novel noncollinear antiferromagnets with spontaneous time-reversal symmetry breaking, nontrivial band topology, and unconventional transport properties have received immense research interest over the past decade due to their rich physics and enormous promise in technological applications. One of the central focuses in this emerging field is exploring the relationship between the microscopic magnetic structure and exotic material properties. Here, the nanoscale imaging of both spin-orbit-torque-induced deterministic magnetic switching and chiral spin rotation in noncollinear antiferromagnet Mn3Sn films using nitrogen-vacancy (NV) centers is reported. Direct evidence of the off-resonance dipole-dipole coupling between the spin dynamics in Mn3Sn and proximate NV centers is also demonstrated with NV relaxometry measurements. These results demonstrate the unique capabilities of NV centers in accessing the local information of the magnetic order and dynamics in these emergent quantum materials and suggest new opportunities for investigating the interplay between topology and magnetism in a broad range of topological magnets.

cond-mat.mes-hall↗

arXiv2021

Spin Pumping of an Easy-Plane Antiferromagnet Enhanced by Dzyaloshinskii-Moriya Interaction

Recently, antiferromagnets have received revived interest due to their significant potential for developing next-generation ultrafast magnetic storage. Here we report dc spin pumping by the acoustic resonant mode in a canted easy-plane antiferromagnet α-Fe2O3 enabled by the Dzyaloshinskii-Moriya interaction. Systematic angle and frequency dependent measurements demonstrate that the observed spin pumping signals arise from resonance-induced spin injection and inverse spin Hall effect in α-Fe2O3/metal heterostructures, mimicking the behavior of spin pumping in conventional ferromagnet/nonmagnet systems. The pure spin current nature is further corroborated by reversal of the polarity of spin pumping signals when the spin detector is switched from platinum to tungsten which has an opposite sign of the spin Hall angle. Our results highlight the potential opportunities offered by the low-frequency acoustic resonant mode in canted easy-plane antiferromagnets for developing next-generation, functional spintronic devices.

cond-mat.mtrl-sci↗

arXiv2021

Large Spin-to-Charge Conversion in Ultrathin Gold-Silicon Multilayers

Investigation of the spin Hall effect in gold has triggered increasing interest over the past decade, since gold combines the properties of a large bulk spin diffusion length and strong interfacial spin-orbit coupling. However, discrepancies between the values of the spin Hall angle of gold reported in the literature have brought into question the microscopic origin of the spin Hall effect in Au. Here, we investigate the thickness dependence of the spin-charge conversion efficiency in single Au films and ultrathin Au/Si multilayers by non-local transport and spin-torque ferromagnetic resonance measurements. We show that the spin-charge conversion efficiency is strongly enhanced in ultrathin Au/Si multilayers, reaching exceedingly large values of 0.99 +/- 0.34 when the thickness of the individual Au layers is scaled down to 2 nm. These findings reveal the coexistence of a strong interfacial spin-orbit coupling effect which becomes dominant in ultrathin Au, and bulk spin Hall effect with a relatively low bulk spin Hall angle of 0.012 +/- 0.005. Our experimental results suggest the key role of the Rashba-Edelstein effect in the spin-to-charge conversion in ultrathin Au.

cond-mat.mtrl-sci↗