Generating Bounded Linear Temporal Logic in Systems Biology with Large Language Models

In computational modeling, Bounded Linear Temporal Logic (BLTL) is a valuable formalism for describing and verifying the temporal behavior of biological systems. However, translating natural language (NL) descriptions of system behaviors into accurate BLTL properties remains a labor-intensive task, requiring deep expertise in both logic syntax and semantic translation. With the advent of large language models (LLMs), automating this translation has become a promising direction. In this work, we propose an accurate and flexible NL-BLTL transformation framework based on transfer learning. Our approach consists of three stages: 1) Synthetic data generation, where we construct a large-scale NL-BLTL dataset. 2) Pre-training, where we fine-tune LLMs on the synthetic dataset to enhance their ability to characterize logical structure and BLTL specifications. 3) Fine-tuning, where we adapt the pre-trained models to a naive T-cell dataset with manual NL-BLTL annotations. We evaluate the fine-tuned models on the naive T-cell test set and further assess their generalizability on an unseen NL-BLTL dataset in the context of the pancreatic cancer environment, using comprehensive metrics. Experimental results show that models pre-trained on the synthetic data and fine-tuned on real-world annotations outperform both out-of-the-box LLMs, such as GPT-4, and models trained directly on the naive T-cell dataset without pre-training, demonstrating the effectiveness of our framework.