NL2BLTL: Automated Generation of Bounded Linear Temporal Logic from Natural Language for Systems Biology

Motivation: Translating natural language biological discoveries into formal temporal logic specifications for model verification demands expertise most experimentalists lack. Bounded Linear Temporal Logic (BLTL), which attaches explicit time bounds to temporal operators, is well suited for capturing biological dynamics. However, no automated solution exists for this translation, limiting the broader adoption of statistical model checking in systems biology. Results: We present NL2BLTL, the first framework to automate natural language to BLTL translation for systems biology. NL2BLTL combines a synthetic dataset of 5,000 NL-BLTL pairs built via grammar-guided generation, Chain-of-Thought preprocessing to resolve linguistic ambiguity in biological hypotheses, and grammar-constrained decoding to enforce syntactic validity and prevent hallucinated variables or time bounds. Evaluated on a newly curated biomedical NL-BLTL dataset drawn from published T cell and pancreatic cancer models, NL2BLTL framework achieves 84.62% exact match and 100% syntactic validity, outperforming GPT-4 by over 16 points and improving 14 points over the base fine-tuned model.