Model-checking (MC) of refinement propositions over reactive programs, characterised by complete lattice theories, can suffer from state-explosion due to exponential complexity. Leveraging Large Language Models (LLMs) in formal verification could potentially counter this problem, however, the high-quality training data necessary for such models is not available. Presently, we are synthesising a novel dataset, of refinements of reactive programs, which we will use in the fine-tuning of a chosen LLM for application in a guided MC approach. We will evaluate the approach against benchmark examples and the chosen LLM(s) against well-established metrics within the field.