arXiv subjects

Yuanhong Wang

Publications and source records attributed to Yuanhong Wang.

At least 19 recordsLinked to original sources

arXiv2026

Weighted First-Order Model Counting over Ordered Domains

The Weighted First-Order Model Counting Problem (WFOMC) asks for the weighted sum of models of a first-order logical sentence over a domain. It is a fundamental problem in statistical relational learning, with applications extending to enumerative combinatorics and graph polynomials. Computing WFOMC for the three-variable fragment is $\mathsf{\#P}_1$-hard, whereas polynomial-time algorithms exist for the two-variable fragment and its extensions by cardinality constraints and counting quantifiers. In this work, we explore computing WFOMC in polynomial time over linearly ordered domains, enabling tractable reasoning across inference scenarios and combinatorial problems involving sequences. Because encoding a linear order in standard first-order logic requires three variables, negating our polynomial-time aspirations, we add a linear order axiom directly to the language. This forces one predicate to impose a total ordering on domain elements. We first prove that WFOMC with the linear order axiom can be solved in time polynomial in the domain size. We then extend this result to ordered domains with access to successor relations. While this holds when successors are explicitly defined via the linear order, we demonstrate an alternative implicit approach where successor relations are part of the axiom. This implicit method exhibits significantly better performance on all tested instances, sometimes providing exponential runtime improvements. Finally, we analyze scenarios with two distinct linear orders. We show that WFOMC over the two-variable fragment with two linear orders is $\mathsf{\#P}_1$-hard. However, we develop a polynomial-time algorithm for WFOMC with one linear order and a successor relation of another, pushing the intractability barrier further, yet still leaving the question of how close to a second full linear order one can get.

cs.LO↗

arXiv2026

CombEval: A Framework for Evaluating Combinatorial Counting in Large Language Models

We present CombEval, a dynamic benchmark for evaluating combinatorial counting in large language models. CombEval represents each problem as a typed Cofola specification over entities, combinatorial objects, object dependencies, and constraints, enabling controlled generation of natural-language counting problems with exact solver-verified answers. Unlike static collections, CombEval supports systematic variation of object type, entity scale, constraint count, and reasoning depth. We evaluate 11 LLMs under direct and code-augmented settings and find that models remain brittle on ordered objects, indistinguishable elements, relatively positional constraints, and nested object dependencies. Error analysis further identifies failures in constraint interpretation and counting principles. CombEval provides a diagnostic testbed for studying when and why LLMs fail at combinatorial reasoning. The code and generated benchmark suites are publicly available at \url{https://github.com/YuxuZhou-CN/combination-problem-generation}.

cs.AI↗

arXiv2026

Solving Combinatorial Counting Problems with Weighted First-Order Model Counting

Combinatorial counting problems pervade artificial intelligence, statistics, and discrete mathematics. Whether the task is enumerating subsets, multisets, permutations, partitions, or compositions under structural and arithmetic constraints, solving it remains a stubbornly manual exercise. Closed-form derivations are powerful but brittle, while naive encodings to propositional model counting or constraint satisfaction destroy the exchangeability that makes counting tractable in the first place. We present Cofola (COmbinatorial counting LAnguage with First-Order logic), a typed declarative language whose primitives are the combinatorial objects that recur in everyday counting questions, including sets, bags, tuples, sequences, circles, partitions, and compositions, together with natural relational and arithmetic constraints over them. A denotational semantics maps every Cofola program to a well-defined combinatorial counting problem, and a three-phase compilation pipeline (preprocessing, decomposition, and symmetry-preserving encoding) reduces this problem to a weighted first-order model counting (WFOMC) instance augmented with coefficient-extraction constraints. To stay inside known domain-liftable fragments whenever possible, the encoding groups indistinguishable entities, breaks the symmetry of unordered groupings lexicographically, and encodes sequences and circles via order axioms. On a suite of representative combinatorial counting problems, ranging from textbook math problems to multi-object scenarios that the closest prior framework cannot express, Cofola produces concise specifications and a uniform solving pipeline that is practical end-to-end.

cs.AI↗

arXiv2026

On Knowledge Compilation For Two-Variable First-Order Logic

Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO2, the two-variable fragment of first-order logic over finite domains. Given an FO2 sentence and a domain of size n, its grounding yields a propositional theory over ground atoms. We ask whether such theories admit compact representations in DNNF-based and related knowledge compilation languages, and whether these can be constructed efficiently, both with respect to the domain size n for a fixed sentence. We show first that compact compilation is impossible in general: there exists an FO2 sentence whose grounding over a domain of size n requires DNNF size $2^{\Omega(n)}$. On the positive side, we develop a two-stage compiler that exploits the symmetries inherent in the propositional groundings of FO2 sentences. It branches on unary and binary types rather than individual ground atoms, in a similar spirit to lifted inferences for probabilistic relational models. Moreover, it optimizes the compilation process by efficiently identifying and caching residual subproblems that are equivalent with respect to future extensions. Experiments show the practical efficiency of our approach, which often produces smaller circuits and compiles faster than straightforward grounding-based baselines.

cs.LO↗

arXiv2026

A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers

Weighted first-order model counting (WFOMC) is a central task in lifted probabilistic inference: It asks for the weighted sum of all models of a first-order sentence over a finite domain. A long line of work has identified domain-liftable fragments of first-order logic, that is, syntactic classes for which WFOMC can be solved in time polynomial in the domain size. Among them, the two-variable fragment with counting quantifiers, $\mathbf{C}^2$, is one of the most expressive known liftable fragments. Existing algorithms for $\mathbf{C}^2$, however, establish tractability through multi-stage reductions that eliminate counting quantifiers via cardinality constraints, which introduces substantial practical overhead as the domain size grows. In this paper, we introduce IncrementalWFOMC3, a lifted algorithm for WFOMC on $\mathbf{C}^2$ and its modulo counting extension, $\mathbf{C}^2_{\text{mod}}$. Instead of relying on reduction techniques, IncrementalWFOMC3 operates directly on a Scott normal form that retains counting quantifiers throughout inference. This direct treatment yields two main results. First, we derive a tighter data-complexity bound for WFOMC in $\mathbf{C}^2$, reducing the degree of the polynomial from quadratic to linear in the counting parameters. Second, we prove that $\mathbf{C}^2_{\text{mod}}$ is domain-liftable, extending tractability from $\mathbf{C}^2$ to a richer fragment with native modulo counting support. Finally, our empirical evaluation shows that IncrementalWFOMC3 delivers orders-of-magnitude runtime improvements and better scalability than both existing WFOMC algorithms and state-of-the-art propositional model counters.

cs.LO↗

arXiv2026

Verifiable Counterfactual Supervision for Process Reward Models

Process reward models (PRMs) require supervision that identifies not only whether a reasoning trajectory is correct, but also where the reasoning process first becomes unsupported by its prefix. We frame this requirement as verifiable counterfactual process supervision with paired correct and erroneous trajectories in which the first invalid transition is known, the error mechanism is controlled, and the downstream continuation remains coherent under the corrupted state. Starting from a verified symbolic reasoning chain, our method injects a template-aware error at a selected intermediate step, recomputes all subsequent steps under the corrupted state, and verifies that the injected step is not derivable from its original prefix. The resulting trajectories provide prefix-valid first-error annotations and are translated into aligned natural-language processes for PRM training and evaluation. Experiments show that the synthesized data improve Best-of-8 reranking on logical reasoning benchmarks and show preliminary transfer to mathematical process evaluation.

cs.AI↗

arXiv2025

FFTrainer: Fast Failover in Large-Language Model Training with Almost-Free State Management

Recent developments in large language models (LLMs) have introduced new requirements for efficient and robust training. As LLM clusters scale, node failures, lengthy recoveries, and bulky checkpoints erode efficiency. Infrequent asynchronous checkpoints trigger costly rollbacks, yet higher frequencies add prohibitive overhead. To address these challenges, we propose FFTrainer, a system designed for robust LLM training. FFTrainer leverages surplus network capacity to quickly save and load states, thereby preventing rollbacks and accelerating recovery. Compared with prior checkpointing approaches, FFTrainer reduces recovery time by up to 98% and mitigates GPU utilization loss by up to 68% without hindering normal training.

cs.DC↗

arXiv2025

Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. Conditioning WFOMC on evidence -- fixing the truth values of a set of ground literals -- has been shown impossible in time polynomial in the domain size (unless $\mathsf{\#P \subseteq FP}$) even for fragments of logic that are otherwise tractable for WFOMC without evidence. In this work, we address the barrier by restricting the binary evidence to the case where the underlying Gaifman graph has bounded treewidth. We present a polynomial-time algorithm in the domain size for computing WFOMC for the two-variable fragments $\text{FO}^2$ and $\text{C}^2$ conditioned on such binary evidence. Furthermore, we show the applicability of our algorithm in combinatorial problems by solving the stable seating arrangement problem on bounded-treewidth graphs of bounded degree, which was an open problem. We also conducted experiments to show the scalability of our algorithm compared to the existing model counting solvers.

cs.LO↗

arXiv2025

Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. The boundary between fragments for which WFOMC can be computed in polynomial time relative to the domain size lies between the two-variable fragment ($\text{FO}^2$) and the three-variable fragment ($\text{FO}^3$). It is known that WFOMC for \FOthree{} is $\mathsf{\#P_1}$-hard while polynomial-time algorithms exist for computing WFOMC for $\text{FO}^2$ and $\text{C}^2$, possibly extended by certain axioms such as the linear order axiom, the acyclicity axiom, and the connectedness axiom. All existing research has concentrated on extending the fragment with axioms on a single distinguished relation, leaving a gap in understanding the complexity boundary of axioms on multiple relations. In this study, we explore the extension of the two-variable fragment by axioms on two relations, presenting both negative and positive results. We show that WFOMC for $\text{FO}^2$ with two linear order relations and $\text{FO}^2$ with two acyclic relations are $\mathsf{\#P_1}$-hard. Conversely, we provide an algorithm in time polynomial in the domain size for WFOMC of $\text{C}^2$ with a linear order relation, its successor relation and another successor relation.

cs.LO↗

arXiv2025

Faster Lifting for Ordered Domains with Predecessor Relations

We investigate lifted inference on ordered domains with predecessor relations, where the elements of the domain respect a total (cyclic) order, and every element has a distinct (clockwise) predecessor. Previous work has explored this problem through weighted first-order model counting (WFOMC), which computes the weighted sum of models for a given first-order logic sentence over a finite domain. In WFOMC, the order constraint is typically encoded by the linear order axiom introducing a binary predicate in the sentence to impose a linear ordering on the domain elements. The immediate and second predecessor relations are then encoded by the linear order predicate. Although WFOMC with the linear order axiom is theoretically tractable, existing algorithms struggle with practical applications, particularly when the predecessor relations are involved. In this paper, we treat predecessor relations as a native part of the axiom and devise a novel algorithm that inherently supports these relations. The proposed algorithm not only provides an exponential speedup for the immediate and second predecessor relations, which are known to be tractable, but also handles the general k-th predecessor relations. The extensive experiments on lifted inference tasks and combinatorics math problems demonstrate the efficiency of our algorithm, achieving speedups of a full order of magnitude.

cs.AI↗

arXiv2025

Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables ($FO^2$). Specifically, given an $FO^2$ sentence $\Gamma$ and a positive integer $n$, how can one enumerate all the models of $\Gamma$ over a domain of size $n$? In this paper, we devise a novel algorithm to address this problem. The delay complexity, the time required between producing two consecutive models, of our algorithm is quadratic in the given domain size $n$ (up to logarithmic factors) when the sentence is fixed. This complexity is almost optimal since the interpretation of binary predicates in any model requires at least $\Omega(n^2)$ bits to represent.

cs.LO↗

arXiv2024

Searches for exotic spin-dependent interactions with spin sensors

Numerous theories have postulated the existence of exotic spin-dependent interactions beyond the Standard Model of particle physics. Spin-based quantum sensors, which utilize the quantum properties of spins to enhance measurement precision, emerge as powerful tools for probing these exotic interactions. These sensors encompass a wide range of technologies, such as optically pumped magnetometers, atomic comagnetometers, spin masers, nuclear magnetic resonance, spin amplifiers, and nitrogen-vacancy centers. These technologies stand out for their ultrahigh sensitivity, compact tabletop design, and cost-effectiveness, offering complementary approaches to the large-scale particle colliders and astrophysical observations. This article reviews the underlying physical principles of various spin sensors and highlights the recent theoretical and experimental progress in the searches for exotic spin-dependent interactions with these quantum sensors. Investigations covered include the exotic interactions of spins with ultralight dark matter, exotic spin-dependent forces, electric dipole moment, spin-gravity interactions, and among others. Ongoing and forthcoming experiments using advanced spin-based sensors to investigate exotic spin-dependent interactions are discussed.

quant-ph↗

arXiv2024

Search for New Particles with Flying Quantum Sensors in Space

Recent advancements in space science and technologies offer exciting prospects for investigating novel research that is unattainable within terrestrial laboratories. Here we propose the implementation of space-based quantum sensing to explore ultralight new particles beyond the standard model. The central idea involves probing long-range interactions between spin ensembles of space quantum sensors and the particles residing within Earth, mediated by ultralight particles. We show that such interactions can be substantially enhanced in space platforms and thus increase the search sensitivity. In contrast to their terrestrial counterparts, space-based quantum searches exhibit remarkable velocity enhancements, approaching the first cosmic speed, and thus enables the exploration of unexplored parameter space concerning ultralight new particles. Furthermore, the substantial abundance of electrons and nucleons within Earth plays a crucial role in extending the scope of our mission. Our projected search sensitivity can surpass the sensitivities of both terrestrial experiments and proposals by up to approximately 7 orders of magnitude. We also briefly discuss other space mission, including ``space-ground integrated" network of quantum sensors for dark matter searches.

quant-ph↗

arXiv2024

Bridging Weighted First Order Model Counting and Graph Polynomials

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as $C^2$. This polynomial-time complexity is known to be retained when extending $C^2$ by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from $C^2$. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having $k$ connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials.

cs.LO↗

arXiv2024

Femtotesla Atomic Magnetometer for Zero- and Ultralow-field Nuclear Magnetic Resonance

Zero- and ultralow-field nuclear magnetic resonance (ZULF NMR) has experienced rapid development and provides an excellent tool for diverse research fields ranging from materials science, quantum information processing to fundamental physics. The detection of ZULF NMR signals in samples with natural abundance remains a challenging endeavor, due to the limited sensitivity of NMR detectors and thermal polarization. In this work, we demonstrate a femtotesla potassium spin-exchange relaxation-free (SERF) magnetometer designed for ZULF NMR detection. A potassium vapor cell with high buffer gas pressure and high atomic number density is used in the magnetometer. With absorption spectroscopy and SERF effect, the key parameters of the vapor cell are characterized and applied to optimize the magnetometer sensitivity. To combine our SERF magnetometer and ZULF NMR detection, a custom-made vacuum chamber is employed to keep NMR sample close to the magnetometer cell and protect the sample from undesired heating effects. Gradiometric measurement is performed to greatly reduce the magnetic noise. With the phase calibration applied, the gradiometric measurement achieves 7-fold enhancement in magnetic-field sensitivity compared to the single channel and has a magnetic noise floor of 1.2 fT/Hz$^{1/2}$. Our SERF magnetometer exhibits high sensitivity and is promising to realize ZULF NMR detection of samples with natural abundance.

quant-ph↗

arXiv2024

ForestColl: Throughput-Optimal Collective Communications on Heterogeneous Network Fabrics

As modern DNN models grow ever larger, collective communications between the accelerators (allreduce, etc.) emerge as a significant performance bottleneck. Designing efficient communication schedules is challenging, given today's heterogeneous and diverse network fabrics. We present ForestColl, a tool that generates throughput-optimal schedules for any network topology. ForestColl constructs broadcast/aggregation spanning trees as the communication schedule, achieving theoretical optimality. Its schedule generation runs in polynomial time and is highly scalable. ForestColl supports any network fabric, including both switching fabrics and direct accelerator connections. We evaluated ForestColl on AMD MI250 and NVIDIA DGX A100 & H100 clusters. ForestColl showed significant improvements over the vendors' own optimized communication libraries across various settings and in LLM training. ForestColl also outperformed other state-of-the-art schedule generation techniques with both more efficient generated schedules and substantially faster generation speed.

cs.NI↗

arXiv2023

Cooperative Spin Amplification

Quantum amplification is recognized as a key resource for precision measurements. However, most conventional paradigms employ an ensemble of independent particles that usually limit the performance of quantum amplification in gain, spectral linewidth, etc. Here we demonstrate a new signal amplification using cooperative 129Xe nuclear spins embedded within a feedback circuit, where the noble-gas spin coherence time is enhanced by at least one order of magnitude. Using such a technique, magnetic field can be substantially pre-enhanced by more than three orders and is in situ readout with an embedded 87Rb magnetometer. We realize an ultrahigh magnetic sensitivity of 4.0 fT/Hz$^{1/2}$ that surpasses the photon-shot noise and even below the spin-projection noise of the embedded atomic magnetometer, allowing for exciting applications including searches for dark matter with sensitivity well beyond supernova constraints. Our findings extend the physics of quantum amplification to cooperative spin systems and can be generalized to a wide variety of existing sensors, enabling a new class of cooperative quantum sensors.

quant-ph↗

arXiv2023

Enhanced quantum sensing with amplification and deamplification

Quantum sensing is a fundamental building block of modern technology that employs quantum resources and creates new opportunities for precision measurements. However, previous methods usually have a common assumption that detection noise levels should be below the intrinsic sensitivity provided by quantum resources. Here we report the first demonstration of Fano resonance between coupled alkali-metal and noble gases through rapid spin-exchange collisions. The Fano resonance gives rise to two intriguing phenomena: spin amplification and deamplification, which serve as crucial resources for enhanced sensing. Further we develop a novel scheme of quantum sensing enhanced by amplification and deamplification, with relaxed requirements on the detection noise. The coupled systems of alkali-metal and noble gases act as amplifiers or de-amplifiers, enabling to extract small signals above the detection noise before final detection. We demonstrate magnetic-field measurement about 54 decibels below the photon-shot noise, which outperforms the state-of-the-art squeezed-light technology and realizes femtotesla-level sensitivity. Our work opens new avenues to applications in searches for ultralight dark matter with sensitivity well beyond the supernova-observation constraints.

quant-ph↗