Use instruction-tuned code model for reliable XML answers

README.md

@@ -17,6 +17,6 @@ This Space powers the “Try it yourself” panel on the
 It accepts a standard C* program, applies the selected benchmark intervention,
 loads the corresponding formal semantics from the
 [PLSemanticsBench dataset](https://huggingface.co/datasets/EngineeringSoftware/PLSemanticsBench),
-and runs `deepseek-ai/DeepSeek-R1-Distill-Qwen-1.5B` on ZeroGPU.
+and runs `Qwen/Qwen2.5-Coder-3B-Instruct` on ZeroGPU.
 
 The named Gradio API endpoint is `/predict`.

app.py

@@ -18,7 +18,7 @@ from cstar import (
     build_predstate_prompt,
 )
 
-MODEL_ID = "deepseek-ai/DeepSeek-R1-Distill-Qwen-1.5B"
+MODEL_ID = "Qwen/Qwen2.5-Coder-3B-Instruct"
 DEFAULT_PROGRAM = """int a;
 int b;
 int ans;
@@ -115,7 +115,7 @@ def predict(
     with torch.inference_mode():
         generated = MODEL.generate(
             **model_inputs,
-            max_new_tokens=1024,
+            max_new_tokens=512,
             do_sample=False,
             pad_token_id=TOKENIZER.eos_token_id,
         )