LLM World Models for Efficient Exploration in Automated Theorem Proving

Jason Liu, Wensen Mao, and He Zhu

Automated theorem proving is a fundamental goal in artificial intelligence. Here, we finetuned Qwen2.5-Math-7B to suggest tactics and estimate distance from success, given a partial proof in LEAN. We use a best first search method using the estimated distance as a heuristic, which we show leads to promising performance.

Maternal genetic variants in kinesin motor domains prematurely increase egg aneuploidy

Leelati Biswas et al. including Jason Liu and Jinchuan Xing

In this study we show that KIF genes are associated with aneuploidy in human eggs. Analysis using my module identification methods prioritized these genes as candidates.

Systematic Assessment of Active Module Identification Algorithms

In this study we systematically compared the performance of four active module identification algorithms across four datasets.

We also introduce the Earth Mover's Distance as a metric to compute module similarity. Using this, we show that high performing algorithms produce complementary outputs.

We therefore introduce an algorithm that uses spectral clustering to combine the outputs of the four algorithms.

Identification and Prioritization of Candidate Genes Associated with Aneuploidy using PGT-A Data

In this study we develop a computational pipeline to identify candidate genes for aneuploidy using GWAS data.

Identifying modules in biological networks

In this study, the PAPER (Preferential Attachment Plus Erdos Renyi) model was implemented to partition biological networks into the underlying processes.

We show that our algorithm outperforms other leading methods.

Using machine learning to predict disease risk

Jason Liu, Siqi Sun, and Jinchuan Xing

In this study, a machine learning classifier was trained to predict patient aneuploidy risk.

Candidate genes were identified using a novel approach.