The DSR Formalizer was created by applying LoRA fine-tuning to Qwen2.5-7B-Instruct with the training dataset. The instruction used for fine-tuning is as follows. To ensure model performance, please use the same instruction for inference. Please translate the natural language component into Lean4 code, and then parse it into a structured operator tree in JSON format. Use 'formal_content' for the operator logic (with ' ' as placeholders) and 'children' for the nested arguments.\nComponent: {text}\nTag: {tag}
