arXiv subjects

Jianlin Wang

Publications and source records attributed to Jianlin Wang.

11 recordsLinked to original sources

arXiv2026

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.

cs.AI↗

arXiv2026

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberger (WZ) method can achieve a mechanized proof of combinatorial identities by constructing special auxiliary functions and demonstrating that they satisfy specific recurrence relations. We propose WZ-LLM, a neuro-symbolic framework that turns WZ proof plans into executable proof sketches in Lean 4 and uses an LLM-based prover to discharge the resulting machine-checkable subgoals. We also train a dedicated WZ-Prover via a Lean-kernel-verified bootstrapping loop with expert-verified iteration, followed by DAPO-based refinement. Experiments show that WZ-LLM achieves a 34% proof success rate on LCI-Test (100 classic combinatorial identities), outperforming strong baselines such as DeepSeek-V3 and Goedel-Prover-V2, and delivering consistent gains on CombiBench and PutnamBench-Comb. These results indicate that our framework provides two complementary strengths: improved direct proving for identities beyond the scope of WZ, and substantially higher end-to-end success when WZ sketches guide a specialized prover.

cs.LG↗

arXiv2025

A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation

Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone of mathematics, provides essential tools for analyzing discrete structures and solving optimization problems. However, its inherent complexity makes it particularly challenging for automated theorem proving (ATP) for combinatorial identities. To address this, we manually construct LeanComb, combinatorial identities benchmark in Lean, which is, to our knowledge, the first formalized theorem proving benchmark built for combinatorial identities. We develop an Automated Theorem Generator for Combinatorial Identities, ATG4CI, which combines candidate tactics suggested by a self-improving large language model with a Reinforcement Learning Tree Search approach for tactic prediction. By utilizing ATG4CI, we generate a LeanComb-Enhanced dataset comprising 260K combinatorial identities theorems, each with a complete formal proof in Lean, and experimental evaluations demonstrate that models trained on this dataset can generate more effective tactics, thereby improving success rates in automated theorem proving for combinatorial identities.

cs.AI↗

arXiv2025

CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization

Automated theorem proving (ATP) is one of the most challenging mathematical reasoning tasks for Large Language Models (LLMs). Most existing LLM-based ATP methods rely on supervised fine-tuning, which results in a limited alignment between the theorem proving process and human preferences. Direct Preference Optimization (DPO), which aligns LLMs with human preferences, has shown positive effects for certain tasks. However, the lack of high-quality preference data for theorem proving presents a significant challenge. In this paper, we innovatively apply DPO to formal automated theorem proving and introduces a Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP) method. Specifically, we propose a method for constructing preference data which utilizes LLMs and existing theorem proving data to enhance the diversity of the preference data while reducing the reliance on human preference annotations. We then integrate this preference data construction method with curriculum learning to iteratively fine-tune the theorem proving model through DPO. Experimental results on the MiniF2F and ProofNet datasets demonstrate the effectiveness of the proposed method.

cs.AI↗

arXiv2023

Robust room temperature ferromagnetism in an itinerant van der Waals antiferromagnet

The coexistence of antiferromagnetic and ferromagnetic order at room temperature in single-phase van der Waals materials, particularly within the two-dimensional limit, has attracted significant research interest. Nonetheless, such materials are rare. In this work, we introduce an itinerant van der Waals antiferromagnet (Fe0.56Co0.44)5GeTe2, where the ferromagnetic order of its exfoliated flakes remains discernible up to room temperature, extending down to the monolayer limit. A notable phenomenon observed is the evident odd-even layer-number effect at high temperature (e.g., T = 150 K). Such behaviour can be expounded by a linear-chain model. Of particular interest is the robust ferromagnetic order observed in even-layer flakes at low temperature (e.g., T = 2 K), which could potentially be attributed to spin-polarized defects. The intricate interplay among magnetic field strength, layer number, and temperature gives rise to a diverse array of phenomena, holding promise not only for new physics but also for practical applications.

cond-mat.str-el↗

arXiv2022

DC-SPP-YOLO: Dense Connection and Spatial Pyramid Pooling Based YOLO for Object Detection

Although the YOLOv2 method is extremely fast on object detection, its detection accuracy is restricted due to the low performance of its backbone network and the underutilization of multi-scale region features. Therefore, a dense connection (DC) and spatial pyramid pooling (SPP) based YOLO (DC-SPP-YOLO) method for ameliorating the object detection accuracy of YOLOv2 is proposed in this paper. Specifically, the dense connection of convolution layers is employed in the backbone network of YOLOv2 to strengthen the feature extraction and alleviate the vanishing-gradient problem. Moreover, an improved spatial pyramid pooling is introduced to pool and concatenate the multi-scale region features, so that the network can learn the object features more comprehensively. The DC-SPP-YOLO model is established and trained based on a new loss function composed of MSE (mean square error) loss and cross-entropy loss. The experimental results indicated that the mAP (mean Average Precision) of DC-SPP-YOLO is higher than that of YOLOv2 on the PASCAL VOC datasets and the UA-DETRAC datasets. The effectiveness of DC-SPP-YOLO method proposed is demonstrated.

cs.CV↗

arXiv2022

Brachial Plexus Nerve Trunk Segmentation Using Deep Learning: A Comparative Study with Doctors' Manual Segmentation

Ultrasound-guided nerve block anesthesia (UGNB) is a high-tech visual nerve block anesthesia method that can observe the target nerve and its surrounding structures, the puncture needle's advancement, and local anesthetics spread in real-time. The key in UGNB is nerve identification. With the help of deep learning methods, the automatic identification or segmentation of nerves can be realized, assisting doctors in completing nerve block anesthesia accurately and efficiently. Here, we establish a public dataset containing 320 ultrasound images of brachial plexus (BP). Three experienced doctors jointly produce the BP segmentation ground truth and label brachial plexus trunks. We design a brachial plexus segmentation system (BPSegSys) based on deep learning. BPSegSys achieves experienced-doctor-level nerve identification performance in various experiments. We evaluate BPSegSys' performance in terms of intersection-over-union (IoU), a commonly used performance measure for segmentation experiments. Considering three dataset groups in our established public dataset, the IoU of BPSegSys are 0.5238, 0.4715, and 0.5029, respectively, which exceed the IoU 0.5205, 0.4704, and 0.4979 of experienced doctors. In addition, we show that BPSegSys can help doctors identify brachial plexus trunks more accurately, with IoU improvement up to 27%, which has significant clinical application value.

eess.IV↗

arXiv2021

Spin-glass state induced by Mn-doping into a moderate gap layered semiconductor SnSe$_2$

Various types of magnetism can appear in emerging quantum materials such as van der Waals layered ones. Here, we report the successful doping of manganese atoms into a post-transition metal dichalcogenide semiconductor: SnSe$_2$. We synthesized a single crystal Sn$_{1-x}$Mn$_x$Se$_{2}$ with $\textit{x}$ = 0.04 by the chemical vapor transport (CVT) method and characterized it by x-ray diffraction (XRD) and energy-dispersive x-ray spectroscopy (EDS). The magnetic properties indicated a competition between coexisting ferromagnetic and antiferromagnetic interactions, from the temperature dependence of the magnetization, together with magnetic hysteresis loops. This means that magnetic clusters having ferromagnetic interaction within a cluster form and the short-range antiferromagnetic interaction works between the clusters; a spin-glass state appears below ~ 60 K. Furthermore, we confirmed by $\textit{ab initio}$ calculations that the ferromagnetic interaction comes from the 3$\textit{d}$ electrons of the manganese dopant. Our results offer a new material platform to understand and utilize the magnetism in the van der Waals layered materials.

cond-mat.mtrl-sci↗

arXiv2020

The Lightest 2D Nanomaterial: Freestanding Ultrathin Li Nanosheets by in-situ Electron Microscopy

Lithium (Li) is the simplest metal and the lightest solid element. Here we report the first demonstration of controlled growth of two-dimensional (2D) ultrathin Li nanosheets with large lateral dimensions up to several hundreds of nanometres and thickness limited to just a few nanometres by in-situ transmission electron microscopy (TEM). The nanoscale dynamics of nanosheets growth were unravelled by real-time TEM imaging, which, in combination with density function theory (DFT) calculations indicates that the growth of bcc structured Li into 2D nanosheets is a consequence of kinetic control as mediated by preferential oxidization of the (111) surfaces due to the trace amount of O2 (~10-6 Pa) within TEM chamber. The plasmonic optical properties of the as-grown Li nanosheets were probed by cathodoluminescence (CL) spectroscopy equipped within TEM, and a broadband visible emission was observed that contains contributions of both in-plane and out-of-plane plasmon resonance modes.

physics.chem-ph↗

arXiv2020

Fermi liquid behavior and colossal magnetoresistance in layered MoOCl2

A characteristic of a Fermi liquid is the T^2 dependence of its resistivity, sometimes referred to as the Baber law. However, for most metals, this behavior is only restricted to very low temperatures, usually below 20 K. Here, we experimentally demonstrate that for the single-crystal van der Waals layered material MoOCl2, the Baber law holds in a wide temperature range up to ~120 K, indicating that the electron-electron scattering plays a dominant role in this material. Combining with the specific heat measurement, we find that the modified Kadowaki-Woods ratio of the material agrees well with many other strongly correlated metals. Furthermore, in the magneto-transport measurement, a colossal magneto-resistance is observed, which reaches ~350% at 9 T and displays no sign of saturation. With the help of first-principles calculations, we attribute this behavior to the presence of open orbits on the Fermi surface. We also suggest that the dominance of electron-electron scattering is related to an incipient charge density wave state of the material. Our results establish MoOCl2 as a strongly correlated metal and shed light on the underlying physical mechanism, which may open a new path for exploring the effects of electron-electron interaction in van der Waals layered structures.

cond-mat.mtrl-sci↗

arXiv2019

Direct Imaging Revealing Halved Ferromagnetism in Tensile-Strained LaCoO3 Thin Films

The enigma of the emergent ferromagnetic state in tensile-strained LaCoO3 thin films remains to be explored because of the lack of a well agreed explanation. The direct magnetic imaging technique using a low-temperature magnetic force microscope (MFM) is critical to reveal new aspects of the ferromagnetism by investigating the lateral magnetic phase distribution. Here we show the experimental demonstration of the rare halved occupation of the ferromagnetic state in tensile-strained LaCoO3 thin films on SrTiO3 substrates using the MFM. The films have uniformly strained lattice structure and minimal oxygen vacancies (less than 2%) beyond the measurement limit. It is found that percolated ferromagnetic regions with typical sizes between 100 nm and 200 nm occupy about 50% of the entire film, even down to the lowest achievable temperature of 4.5 K and up to the largest magnetic field of 13.4 T. Preformed ferromagnetic droplets were still observed when the temperature is 20 K above the Curie temperature indicating the existence of possible Griffiths phase. Our study demonstrated a sub-micron level phase separation in high quality LaCoO3 thin films, which has substantial implications in revealing the intrinsic nature of the emergent ferromagnetism.

cond-mat.str-el↗