arXiv subjects

Zhaoyu Li

Publications and source records attributed to Zhaoyu Li.

31 records · Page 2Linked to original sources

arXiv2024

Autoformalizing Euclidean Geometry

Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformalization. In this paper, we introduce a neuro-symbolic framework for autoformalizing Euclidean geometry, which combines domain knowledge, SMT solvers, and large language models (LLMs). One challenge in Euclidean geometry is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. To address this issue, we use theorem provers to fill in such diagrammatic information automatically, so that the LLM only needs to autoformalize the explicit textual steps, making it easier for the model. We also provide automatic semantic evaluation for autoformalized theorem statements. We construct LeanEuclid, an autoformalization benchmark consisting of problems from Euclid's Elements and the UniGeo dataset formalized in the Lean proof assistant. Experiments with GPT-4 and GPT-4V show the capability and limitations of state-of-the-art LLMs on autoformalizing geometry problems. The data and code are available at https://github.com/loganrjmurphy/LeanEuclid.

cs.LG↗

arXiv2024

G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

Graph neural networks (GNNs) have recently emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT), offering potential alternatives to traditional backtracking or local search SAT solvers. However, despite the growing volume of literature in this field, there remains a notable absence of a unified dataset and a fair benchmark to evaluate and compare existing approaches. To address this crucial gap, we present G4SATBench, the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. In G4SATBench, we meticulously curate a large and diverse set of SAT datasets comprising 7 problems with 3 difficulty levels and benchmark a broad range of GNN models across various prediction tasks, training objectives, and inference algorithms. To explore the learning abilities and comprehend the strengths and limitations of GNN-based SAT solvers, we also compare their solving processes with the heuristics in search-based SAT solvers. Our empirical results provide valuable insights into the performance of GNN-based SAT solvers and further suggest that existing GNN models can effectively learn a solving strategy akin to greedy local search but struggle to learn backtracking search in the latent space. Our codebase is available at https://github.com/zhaoyu-li/G4SATBench.

cs.LG↗

arXiv2024

Insight into the Galactic Bulge Chemodynamical Properties from Gaia DR3

We explore the chemodynamical properties of the Galaxy in the azimuthal velocity $V_ϕ$ and metallicity [Fe/H] space using red giant stars from Gaia Data Release 3. The row-normalized $V_ϕ$-[Fe/H] maps form a coherent sequence from the bulge to the outer disk, clearly revealing the thin/thick disk and the Splash. The metal-rich stars display bar-like kinematics while the metal-poor stars show dispersion-dominated kinematics. The intermediate-metallicity population ($-1<$[Fe/H]$<-0.4$) can be separated into two populations, one that is bar-like, i.e. dynamically cold ($σ_{V_R}\sim80$ $\rm km\ s^{-1}$) and fast rotating ($V_ϕ\gtrsim100$ $\rm km\ s^{-1}$), and the Splash, which is dynamically hot ($σ_{V_R}\sim110$ $\rm km\ s^{-1}$) and slow rotating ($V_ϕ\lesssim100$ $\rm km\ s^{-1}$). We compare the observations in the bulge region with an Auriga simulation where the last major merger event occurred $\sim10$ Gyr ago: only stars born around the time of the merger reveal a Splash-like feature in the $V_ϕ$-[Fe/H] space, suggesting that the Splash is likely merger-induced, predominantly made-up of heated disk stars and the starburst associated with the last major merger. Since the Splash formed from the proto-disk, its lower metallicity limit coincides with that of the thick disk. The bar formed later from the dynamically hot disk with [Fe/H] $>-1$ dex, with the Splash not participating in the bar formation and growth. Moreover, with a set of isolated evolving $N$-body disk simulations, we confirm that a non-rotating classical bulge can be spun up by the bar and develop cylindrical rotation, consistent with the observation for the metal-poor stars.

astro-ph.GA↗

arXiv2024

The Jiao Tong University Spectroscopic Telescope Project

The Jiao Tong University Spectroscopic Telescope (JUST) is a 4.4-meter f/6.0 segmentedmirror telescope dedicated to spectroscopic observations. The JUST primary mirror is composed of 18 hexagonal segments, each with a diameter of 1.1 m. JUST provides two Nasmyth platforms for placing science instruments. One Nasmyth focus fits a field of view of 10 arcmin and the other has an extended field of view of 1.2 deg with correction optics. A tertiary mirror is used to switch between the two Nasmyth foci. JUST will be installed at a site at Lenghu in Qinghai Province, China, and will conduct spectroscopic observations with three types of instruments to explore the dark universe, trace the dynamic universe, and search for exoplanets: (1) a multi-fiber (2000 fibers) medium-resolution spectrometer (R=4000-5000) to spectroscopically map galaxies and large-scale structure; (2) an integral field unit (IFU) array of 500 optical fibers and/or a long-slit spectrograph dedicated to fast follow-ups of transient sources for multimessenger astronomy; (3) a high-resolution spectrometer (R~100000) designed to identify Jupiter analogs and Earth-like planets, with the capability to characterize the atmospheres of hot exoplanets.

astro-ph.IM↗

arXiv2023

Learning Reliable Logical Rules with SATNet

Bridging logical reasoning and deep learning is crucial for advanced AI systems. In this work, we present a new framework that addresses this goal by generating interpretable and verifiable logical rules through differentiable learning, without relying on pre-specified logical structures. Our approach builds upon SATNet, a differentiable MaxSAT solver that learns the underlying rules from input-output examples. Despite its efficacy, the learned weights in SATNet are not straightforwardly interpretable, failing to produce human-readable rules. To address this, we propose a novel specification method called "maximum equality", which enables the interchangeability between the learned weights of SATNet and a set of propositional logical rules in weighted MaxSAT form. With the decoded weighted MaxSAT formula, we further introduce several effective verification techniques to validate it against the ground truth rules. Experiments on stream transformations and Sudoku problems show that our decoded rules are highly reliable: using exact solvers on them could achieve 100% accuracy, whereas the original SATNet fails to give correct solutions in many cases. Furthermore, we formally verify that our decoded logical rules are functionally equivalent to the ground truth ones.

cs.AI↗

arXiv2023

On the Migration Origin of the Hercules Moving Group with GAIA, LAMOST, APOGEE, and GALAH Surveys

Using Gaia DR3 data and the wavelet transformation technique, we study the substructures of the Hercules moving group (HMG): Hercules 1 (H1) and Hercules 2 (H2). Spectroscopic survey data from LAMOST, APOGEE, and GALAH are used to obtain metallicities and ages of stars belonging to the HMG. Our analysis leads to several key findings as follows: ($a$) the HMG is on average richer in metallicity than the Galactic disk, with H2 being metal richer than H1; ($b$) the HMG likely has a radial metallicity gradient distinct from that of the disk; ($c$) the HMG is on average older than the disk, with H2 being older than H1; ($d$) the HMG likely has a radial age gradient distinct from that of the disk; and ($e$) the metallicity and age distributions of the HMG depend mainly on the Galactic radius but show no dependence on the azimuthal velocity. Taken all together, we conclude that the HMG is composed primarily of stars undergoing radial migration. We suggest that the HMG is associated with a higher-order dynamical resonance of the bar of the Galaxy.

astro-ph.GA↗

arXiv2023

A Monolithic Graphene-Functionalized Microlaser for Multispecies Gas Detection

Optical microcavity enhanced light-matter interaction offers a powerful tool to develop fast and precise sensing techniques, spurring applications in the detection of biochemical targets ranging from cells, nanoparticles, and large molecules. However, the intrinsic inertness of such pristine microresonators limits their spread in new fields such as gas detection. Here, a functionalized microlaser sensor is realized by depositing graphene in an erbium-doped over-modal microsphere. By using a 980 nm pump, multiple laser lines excited in different mode families of the microresonator are co-generated in a single device. The interference between these splitting mode lasers produce beat notes in the electrical domain (0.2-1.1 MHz) with sub-kHz accuracy, thanks to the graphene-induced intracavity backward scattering. This allows for multispecies gas identification from a mixture, and ultrasensitive gas detection down to individual molecule.

physics.optics↗

arXiv2022

NSNet: A General Neural Probabilistic Framework for Satisfiability Problems

We present the Neural Satisfiability Network (NSNet), a general neural framework that models satisfiability problems as probabilistic inference and meanwhile exhibits proper explainability. Inspired by the Belief Propagation (BP), NSNet uses a novel graph neural network (GNN) to parameterize BP in the latent space, where its hidden representations maintain the same probabilistic interpretation as BP. NSNet can be flexibly configured to solve both SAT and #SAT problems by applying different learning objectives. For SAT, instead of directly predicting a satisfying assignment, NSNet performs marginal inference among all satisfying solutions, which we empirically find is more feasible for neural networks to learn. With the estimated marginals, a satisfying assignment can be efficiently generated by rounding and executing a stochastic local search. For #SAT, NSNet performs approximate model counting by learning the Bethe approximation of the partition function. Our evaluations show that NSNet achieves competitive results in terms of inference accuracy and time efficiency on multiple SAT and #SAT datasets.

cs.AI↗

arXiv2022

Dynamical Origin for the Collinder 132-Gulliver 21 Stream: A Mixture of three Co-Moving Populations with an Age Difference of 250 Myr

We use Gaia DR3 data to study the Collinder 132-Gulliver 21 region via the machine learning algorithm StarGO, and find eight subgroups of stars (ASCC 32, Collinder 132 gp 1--6, Gulliver 21) located in close proximity. Three co-moving populations were identified among these eight subgroups: (i) a coeval 25 Myr-old moving group (Collinder 132); (ii) an intermediate-age (50--100 Myr) group; and (iii) the 275 Myr-old dissolving cluster Gulliver 21. These three populations form parallel diagonal stripe-shape over-densities in the U--V distribution, which differ from open clusters and stellar groups in the solar neighborhood. We name this kinematic structure the Collinder 132-Gulliver 21 stream, as it extends over 270 pc in the 3D space. The oldest population Gulliver21 is spatially surrounded by the Collinder 132 moving group and the intermediate-age group. Stars in the Collinder 132-Gulliver 21 stream have an age difference up to 250 Myr. Metallicity information shows a variation of 0.3 dex between the youngest and oldest populations. The formation of the Collinder132-Gulliver 21 stream involves both star formation and dynamical heating. The youngest population (Collinder 132 moving group) with homogeneous metallicity is probably formed through filamentary star formation. The intermediate-age and the oldest population were then scatted by the Galactic bar or spiral structure resonance to intercept Collinder 132's orbit. Without mutual interaction between each population, the three populations are flying by each other currently and will become distinct three groups again in approximately ~50Myr.

astro-ph.GA↗

arXiv2021

Multimodal Emotion-Cause Pair Extraction in Conversations

Emotion cause analysis has received considerable attention in recent years. Previous studies primarily focused on emotion cause extraction from texts in news articles or microblogs. It is also interesting to discover emotions and their causes in conversations. As conversation in its natural form is multimodal, a large number of studies have been carried out on multimodal emotion recognition in conversations, but there is still a lack of work on multimodal emotion cause analysis. In this work, we introduce a new task named Multimodal Emotion-Cause Pair Extraction in Conversations, aiming to jointly extract emotions and their associated causes from conversations reflected in multiple modalities (text, audio and video). We accordingly construct a multimodal conversational emotion cause dataset, Emotion-Cause-in-Friends, which contains 9,272 multimodal emotion-cause pairs annotated on 13,509 utterances in the sitcom Friends. We finally benchmark the task by establishing a baseline system that incorporates multimodal features for emotion-cause pair extraction. Preliminary experimental results demonstrate the potential of multimodal information fusion for discovering both emotions and causes in conversations.

cs.CL↗

arXiv2021

Graph Contrastive Pre-training for Effective Theorem Reasoning

Interactive theorem proving is a challenging and tedious process, which requires non-trivial expertise and detailed low-level instructions (or tactics) from human experts. Tactic prediction is a natural way to automate this process. Existing methods show promising results on tactic prediction by learning a deep neural network (DNN) based model from proofs written by human experts. In this paper, we propose NeuroTactic, a novel extension with a special focus on improving the representation learning for theorem proving. NeuroTactic leverages graph neural networks (GNNs) to represent the theorems and premises, and applies graph contrastive learning for pre-training. We demonstrate that the representation learning of theorems is essential to predict tactics. Compared with other methods, NeuroTactic achieves state-of-the-art performance on the CoqGym dataset.

cs.LG↗

arXiv2013

Parallelizing Probabilistic Inference: Some Early Explorations

We report on an experimental investigation into opportunities for parallelism in beliefnet inference. Specifically, we report on a study performed of the available parallelism, on hypercube style machines, of a set of randomly generated belief nets, using factoring (SPI) style inference algorithms. Our results indicate that substantial speedup is available, but that it is available only through parallelization of individual conformal product operations, and depends critically on finding an appropriate factoring. We find negligible opportunity for parallelism at the topological, or clustering tree, level.

cs.AI↗

arXiv2013

An efficient approach for finding the MPE in belief networks

Given a belief network with evidence, the task of finding the I most probable explanations (MPE) in the belief network is that of identifying and ordering the I most probable instantiations of the non-evidence nodes of the belief network. Although many approaches have been proposed for solving this problem, most work only for restricted topologies (i.e., singly connected belief networks). In this paper, we will present a new approach for finding I MPEs in an arbitrary belief network. First, we will present an algorithm for finding the MPE in a belief network. Then, we will present a linear time algorithm for finding the next MPE after finding the first MPE. And finally, we will discuss the problem of finding the MPE for a subset of variables of a belief network, and show that the problem can be efficiently solved by this approach.

cs.AI↗