arXiv subjects

Bin Dong

Publications and source records attributed to Bin Dong.

At least 37 records · Page 2Linked to original sources

arXiv2026

Connected Theorems: A Graph-Based Approach to Evaluating Mathematical Results

The evaluation of mathematical results plays a central role in assessing researchers' contributions and shaping the direction of the field. Currently, such evaluations rely primarily on human judgment, whether through journal peer review or committees at research institutions. To complement these traditional processes, we propose a data-driven approach. We construct a hierarchical graph linking conjectures, theorems, papers, authors and fields to capture their citation relationships. We then introduce a PageRank-style algorithm to compute influence scores for these entities. Using these scores, we analyze the evolution of field rankings over time and quantify the impact between fields. We hope this framework can contribute to the development of more advanced, quantitative methods for evaluating mathematical research and serve as a complement to expert assessment.

cs.SI↗

arXiv2026

Robust topological BIC nanocavities for upconversion directional emission

Photonic bound states in the continuum (BICs) provide a revolutionary paradigm for boosting light-matter interactions in integrated nanocavity systems. Nevertheless, precise manipulation of open cavity-emitter architectures still faces critical challenges, especially in realizing deterministic directional radiation and suppressing the perturbation of intrinsic cavity modes induced by emitters as local impurities. Conventional investigations on cavity-emitter coupling are predominantly based on ensemble measurements, which inevitably mask the intrinsic physics underlying individual light-matter interactions. Here, we propose a robust strategy to control the upconversion and emission of a single-particle emitter using a topological plasmonic cavity with broken σh mirror symmetry. This structured design enables the transition from symmetry-protected BICs to a multi-BIC regime with finite but ultrahigh confinement, where nontrivial phase evolution and hybridization of transverse electric and magnetic modes open a well-defined far-field radiation channel for directional emission. Leveraging this scheme, we experimentally demonstrate dramatically enhanced radiation intensity from a single point-like emitter, together with uniform and deterministic directional emission, while achieving excellent structural robustness against local perturbations. This work establishes a general framework for engineering coherent directional light emission at the nanoscale, which lays a solid foundation for high-performance chip-scale integrated nanophotonic applications.

physics.optics↗

arXiv2026

FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels

Recent advances in large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, particularly on contest-based mathematical benchmarks like the IMO. However, these contests do not reflect the depth, breadth, and abstraction of modern mathematical research. To bridge this gap, we introduce FATE (Formal Algebra Theorem Evaluation), a new benchmark series in formal algebra designed to chart a course toward advanced mathematical reasoning. We present two new components, FATE-H and FATE-X, each with 100 problems in abstract and commutative algebra. The FATE series spans a difficulty spectrum from undergraduate exercises to problems exceeding PhD qualifying exams. Notably, FATE-X is the first formal benchmark to surpass both PhD-level exam difficulty and the coverage of the Mathlib library. Our evaluations of state-of-the-art LLM provers on this new benchmark reveal a stark performance gap compared to contest math: the best model achieves only 3% (pass@64) accuracy on FATE-H and 0% on FATE-X. Our two-stage evaluation reveals that models' natural-language reasoning is notably more accurate than their ability to formalize this reasoning. We systematically classify the common errors that arise during this formalization process. Furthermore, a comparative study shows that a specialized prover can exhibit less effective reflection than general-purpose models, reducing its accuracy at the natural-language stage. We believe FATE provides a robust and challenging benchmark that establishes essential checkpoints on the path toward research-level formal mathematical reasoning.

cs.LG↗

arXiv2026

From Atoms to Trees: Building a Structured Feature Forest with Hierarchical Sparse Autoencoders

Sparse autoencoders (SAEs) have proven effective for extracting monosemantic features from large language models (LLMs), yet these features are typically identified in isolation. However, broad evidence suggests that LLMs capture the intrinsic structure of natural language, where the phenomenon of "feature splitting" in particular indicates that such structure is hierarchical. To capture this, we propose the Hierarchical Sparse Autoencoder (HSAE), which jointly learns a series of SAEs and the parent-child relationships between their features. HSAE strengthens the alignment between parent and child features through two novel mechanisms: a structural constraint loss and a random feature perturbation mechanism. Extensive experiments across various LLMs and layers demonstrate that HSAE consistently recovers semantically meaningful hierarchies, supported by both qualitative case studies and rigorous quantitative metrics. At the same time, HSAE preserves the reconstruction fidelity and interpretability of standard SAEs across different dictionary sizes. Our work provides a powerful, scalable tool for discovering and analyzing the multi-scale conceptual structures embedded in LLM representations.

cs.AI↗

arXiv2026

PaperRegister: Boosting Flexible-grained Paper Search via Hierarchical Register Indexing

As researchers delve more deeply into their work, paper search requirements may become more flexible, sometimes involving specific details such as module configuration rather than being limited to coarse-grained topics. However, previous paper search systems are unable to meet these flexible-grained requirements, as previous systems mainly collect paper abstract to construct corpus index, which lacks detailed information to support retrieval by some finer-grained queries. In this work, we propose PaperRegister, which transforms traditional abstract-based index into a hierarchical index tree, thereby supporting queries at flexible granularity. Experiments on paper search tasks across a range of granularity demonstrate that PaperRegister achieves the SOTA performance, and particularly excels in the fine-grained scenarios, highlighting good potential as an effective solution for flexible-grained paper search in real-world applications. https://github.com/Li-Z-Q/PaperRegister.

cs.IR↗

arXiv2025

Translating Informal Proofs into Formal Proofs Using a Chain of States

We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach is grounded in two key insights. First, informal proofs tend to proceed via a sequence of logical transitions - often implications or equivalences - without explicitly specifying intermediate results or auxiliary lemmas. In contrast, formal systems like Lean require an explicit representation of each proof state and the tactics that connect them. Second, each informal reasoning step can be viewed as an abstract transformation between proof states, but identifying the corresponding formal tactics often requires nontrivial domain knowledge and precise control over proof context. To bridge this gap, we propose a two stage framework. Rather than generating formal tactics directly, we first extract a Chain of States (CoS), a sequence of intermediate formal proof states aligned with the logical structure of the informal argument. We then generate tactics to transition between adjacent states in the CoS, thereby constructing the full formal proof. This intermediate representation significantly reduces the complexity of tactic generation and improves alignment with informal reasoning patterns. We build dedicated datasets and benchmarks for training and evaluation, and introduce an interactive framework to support tactic generation from formal states. Empirical results show that our method substantially outperforms existing baselines, achieving higher proof success rates.

cs.LO↗

arXiv2025

Design and Construction of a Dedicated Radiolucent 8-element Flexible Radiofrequency (RF) Torso Coil for the 1.0T Australian MRI-Linac System

Magnetic resonance imaging-guided linear accelerators (MRI-Linacs) are an emerging treatment technology that enable online soft-tissue visualisation and adaptive radiotherapy. The Australian 1.0 T MRI-Linac employs a fixed, inline beamline, with treatment angles achieved via patient couch rotation, and currently relies on a radiolucent whole-body radiofrequency (RF) coil. However, the large coil-patient separation limits signal-to-noise ratio (SNR) and constrains the fast imaging required for real-time tumour tracking. Here, we show the design and validation of a dedicated, flexible 8-element receive-only RF torso array tailored to the geometry and beam access requirements of the Australian MRI-Linac. Electromagnetic simulations, bench measurements, and phantom imaging demonstrate approximately three-fold SNR improvement at the centre and eight-fold improvement at superficial regions compared with the whole-body coil. In vivo abdominal imaging confirms enhanced anatomical detail and sharper tissue boundaries, and the increased SNR enables parallel imaging with GRAPPA acceleration factors up to three without severe artefacts. Dosimetry measurements and dynamic beam-on noise analysis confirm that the coil array is effectively radiolucent, with dose differences below 1% and no measurable degradation in image noise. This work demonstrates a practical RF solution for accelerated, high-SNR imaging compatible with patient rotation and beam delivery on the Australian MRI-Linac.

physics.med-ph↗

arXiv2025

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL-Prover, a new open-source stepwise theorem prover for Lean 4 to push this boundary. This prover, based on our fine-tuned large language model (REAL-Prover-v1) and integrated with a retrieval system (Leansearch-PS), notably boosts performance on solving college-level mathematics problems. To train REAL-Prover-v1, we developed HERALD-AF, a data extraction pipeline that converts natural language math problems into formal statements, and a new open-source Lean 4 interactive environment (Jixia-interactive) to facilitate synthesis data collection. In our experiments, our prover using only supervised fine-tune achieves competitive results with a 23.7% success rate (Pass@64) on the ProofNet dataset-comparable to state-of-the-art (SOTA) models. To further evaluate our approach, we introduce FATE-M, a new benchmark focused on algebraic problems, where our prover achieves a SOTA success rate of 56.7% (Pass@64).

cs.CL↗

arXiv2025

SciAgent: A Unified Multi-Agent System for Generalistic Scientific Reasoning

Recent advances in large language models have enabled AI systems to achieve expert-level performance on domain-specific scientific tasks, yet these systems remain narrow and handcrafted. We introduce SciAgent, a unified multi-agent system designed for generalistic scientific reasoning-the ability to adapt reasoning strategies across disciplines and difficulty levels. SciAgent organizes problem solving as a hierarchical process: a Coordinator Agent interprets each problem's domain and complexity, dynamically orchestrating specialized Worker Systems, each composed of interacting reasoning Sub-agents for symbolic deduction, conceptual modeling, numerical computation, and verification. These agents collaboratively assemble and refine reasoning pipelines tailored to each task. Across mathematics and physics Olympiads (IMO, IMC, IPhO, CPhO), SciAgent consistently attains or surpasses human gold-medalist performance, demonstrating both domain generality and reasoning adaptability. Additionally, SciAgent has been tested on the International Chemistry Olympiad (IChO) and selected problems from the Humanity's Last Exam (HLE) benchmark, further confirming the system's ability to generalize across diverse scientific domains. This work establishes SciAgent as a concrete step toward generalistic scientific intelligence-AI systems capable of coherent, cross-disciplinary reasoning at expert levels.

cs.AI↗

arXiv2025

MorphoBench: A Benchmark with Difficulty Adaptive to Model Reasoning

With the advancement of powerful large-scale reasoning models, effectively evaluating the reasoning capabilities of these models has become increasingly important. However, existing benchmarks designed to assess the reasoning abilities of large models tend to be limited in scope and lack the flexibility to adapt their difficulty according to the evolving reasoning capacities of the models. To address this, we propose MorphoBench, a benchmark that incorporates multidisciplinary questions to evaluate the reasoning capabilities of large models and can adjust and update question difficulty based on the reasoning abilities of advanced models. Specifically, we curate the benchmark by selecting and collecting complex reasoning questions from existing benchmarks and sources such as Olympiad-level competitions. Additionally, MorphoBench adaptively modifies the analytical challenge of questions by leveraging key statements generated during the model's reasoning process. Furthermore, it includes questions generated using simulation software, enabling dynamic adjustment of benchmark difficulty with minimal resource consumption. We have gathered over 1,300 test questions and iteratively adjusted the difficulty of MorphoBench based on the reasoning capabilities of models such as o3 and GPT-5. MorphoBench enhances the comprehensiveness and validity of model reasoning evaluation, providing reliable guidance for improving both the reasoning abilities and scientific robustness of large models. The code has been released in https://github.com/OpenDCAI/MorphoBench.

cs.AI↗

arXiv2025

PDE Solvers Should Be Local: Fast, Stable Rollouts with Learned Local Stencils

Neural operator models for solving partial differential equations (PDEs) often rely on global mixing mechanisms-such as spectral convolutions or attention-which tend to oversmooth sharp local dynamics and introduce high computational cost. We present FINO, a finite-difference-inspired neural architecture that enforces strict locality while retaining multiscale representational power. FINO replaces fixed finite-difference stencil coefficients with learnable convolutional kernels and evolves states via an explicit, learnable time-stepping scheme. A central Local Operator Block leverage a differential stencil layer, a gating mask, and a linear fuse step to construct adaptive derivative-like local features that propagate forward in time. Embedded in an encoder-decoder with a bottleneck, FINO captures fine-grained local structures while preserving interpretability. We establish (i) a composition error bound linking one-step approximation error to stable long-horizon rollouts under a Lipschitz condition, and (ii) a universal approximation theorem for discrete time-stepped PDE dynamics. (iii) Across six benchmarks and a climate modelling task, FINO achieves up to 44\% lower error and up to around 2\times speedups over state-of-the-art operator-learning baselines, demonstrating that strict locality with learnable time-stepping yields an accurate and scalable foundation for neural PDE solvers.

cs.LG↗

arXiv2025

Multimodal Reasoning for Science: Technical Report and 1st Place Solution to the ICML 2025 SeePhys Challenge

Multimodal reasoning remains a fundamental challenge in artificial intelligence. Despite substantial advances in text-based reasoning, even state-of-the-art models such as GPT-o3 struggle to maintain strong performance in multimodal scenarios. To address this gap, we introduce a caption-assisted reasoning framework that effectively bridges visual and textual modalities. Our approach achieved 1st place in the ICML 2025 AI for Math Workshop \& Challenge 2: SeePhys, highlighting its effectiveness and robustness. Furthermore, we validate its generalization on the MathVerse benchmark for geometric reasoning, demonstrating the versatility of our method. Our code is publicly available at https://github.com/OpenDCAI/SciReasoner.

cs.CL↗

arXiv2025

Compact Attention: Exploiting Structured Spatio-Temporal Sparsity for Fast Video Generation

The computational demands of self-attention mechanisms pose a critical challenge for transformer-based video generation, particularly in synthesizing ultra-long sequences. Current approaches, such as factorized attention and fixed sparse patterns, fail to fully exploit the inherent spatio-temporal redundancies in video data. Through systematic analysis of video diffusion transformers (DiT), we uncover a key insight: Attention matrices exhibit structured, yet heterogeneous sparsity patterns, where specialized heads dynamically attend to distinct spatiotemporal regions (e.g., local pattern, cross-shaped pattern, or global pattern). Existing sparse attention methods either impose rigid constraints or introduce significant overhead, limiting their effectiveness. To address this, we propose Compact Attention, a hardware-aware acceleration framework featuring three innovations: 1) Adaptive tiling strategies that approximate diverse spatial interaction patterns via dynamic tile grouping, 2) Temporally varying windows that adjust sparsity levels based on frame proximity, and 3) An automated configuration search algorithm that optimizes sparse patterns while preserving critical attention pathways. Our method achieves 1.6~2.5x acceleration in attention computation on single-GPU setups while maintaining comparable visual quality with full-attention baselines. This work provides a principled approach to unlocking efficient long-form video generation through structured sparsity exploitation. Project Page: https://yo-ava.github.io/Compact-Attention.github.io/

cs.CV↗

arXiv2025

Dynamics of chiral phase transition in a $N_f=2+1$ soft-wall AdS/QCD model

We investigate the real-time dynamics of the chiral phase transition in a soft-wall AdS/QCD model, of which the mass plane phase diagram from equilibrium calculation is qualitatively consistent with the so-called Columbia plot. By directly solving the non-equilibrium evolution of the order parameter of the chiral phase transition, i.e. the chiral condensate, we study the thermalization of the QCD matter in different regions of the quark mass plane. It is shown that, when the system is close to the transition region, the thermalization process will show non-trivial behavior in the intermediate time region.

hep-ph↗

arXiv2025

State-observation augmented diffusion model for nonlinear assimilation with unknown dynamics

Data assimilation has become a key technique for combining physical models with observational data to estimate state variables. However, classical assimilation algorithms often struggle with the high nonlinearity present in both physical and observational models. To address this challenge, a novel generative model, termed the State-Observation Augmented Diffusion (SOAD) model is proposed for data-driven assimilation. The marginal posterior associated with SOAD has been derived and then proved to match the true posterior distribution under mild assumptions, suggesting its theoretical advantages over previous score-based approaches. Experimental results also indicate that SOAD may offer improved performance compared to existing data-driven methods.

cs.LG↗

arXiv2025

Meta-DSP: A Meta-Learning Approach for Data-Driven Nonlinear Compensation in High-Speed Optical Fiber Systems

Nonlinear effects in high-speed optical fiber systems fundamentally limit channel capacity. While traditional Digital Backward Propagation (DBP) with adaptive filters addresses these effects, its computational complexity remains impractical. Data-driven solutions like Filtered DBP (FDBP) reduce complexity but critically lack inherent generalization: Their nonlinear compensation capability cannot be naturally extended to new transmission rates or WDM channel counts without retraining on newly collected data. We propose Meta-DSP, a novel signal processing pipeline combining: (1) Meta-DBP, a meta-learning-based DBP model that generalizes across transmission parameters without retraining, and (2) XPM-ADF, a carefully engineered adaptive filter designed to address multi-channel nonlinear distortions. The system demonstrates strong generalization, learning from 40 Gbaud single-channel data and successfully applying this knowledge to higher rates (80/160 Gbaud) and multi-channel configurations (up to 21 channels). Experimental results show Meta-DSP improves Q-factor by 0.55 dB over CDC in challenging scenarios while reducing computational complexity 10$\times$ versus DBP. This work provides a scalable solution for nonlinear compensation in dynamic optical networks, balancing performance with practical computational constraints.

eess.SP↗

arXiv2025

RainFusion: Adaptive Video Generation Acceleration via Multi-Dimensional Visual Redundancy

Video generation using diffusion models is highly computationally intensive, with 3D attention in Diffusion Transformer (DiT) models accounting for over 80\% of the total computational resources. In this work, we introduce {\bf RainFusion}, a novel training-free sparse attention method that exploits inherent sparsity nature in visual data to accelerate attention computation while preserving video quality. Specifically, we identify three unique sparse patterns in video generation attention calculations--Spatial Pattern, Temporal Pattern and Textural Pattern. The sparse pattern for each attention head is determined online with negligible overhead (\textasciitilde\,0.2\%) with our proposed {\bf ARM} (Adaptive Recognition Module) during inference. Our proposed {\bf RainFusion} is a plug-and-play method, that can be seamlessly integrated into state-of-the-art 3D-attention video generation models without additional training or calibration. We evaluate our method on leading open-sourced models including HunyuanVideo, OpenSoraPlan-1.2 and CogVideoX-5B, demonstrating its broad applicability and effectiveness. Experimental results show that RainFusion achieves over {\bf 2$\times$} speedup in attention computation while maintaining video quality, with only a minimal impact on VBench scores (-0.2\%).

cs.CV↗

arXiv2025

MIRB: Mathematical Information Retrieval Benchmark

Mathematical Information Retrieval (MIR) is the task of retrieving information from mathematical documents and plays a key role in various applications, including theorem search in mathematical libraries, answer retrieval on math forums, and premise selection in automated theorem proving. However, a unified benchmark for evaluating these diverse retrieval tasks has been lacking. In this paper, we introduce MIRB (Mathematical Information Retrieval Benchmark) to assess the MIR capabilities of retrieval models. MIRB includes four tasks: semantic statement retrieval, question-answer retrieval, premise retrieval, and formula retrieval, spanning a total of 12 datasets. We evaluate 13 retrieval models on this benchmark and analyze the challenges inherent to MIR. We hope that MIRB provides a comprehensive framework for evaluating MIR systems and helps advance the development of more effective retrieval models tailored to the mathematical domain.

cs.IR↗