Add interactive C* ZeroGPU demo

README.md

@@ -1,13 +1,22 @@
 ---
 title: PLSemanticsBench
-emoji: 🏃
-colorFrom: gray
-colorTo: indigo
+emoji: 🧭
+colorFrom: blue
+colorTo: yellow
 sdk: gradio
-sdk_version: 6.29.1
-python_version: '3.12'
+python_version: 3.12.12
 app_file: app.py
-pinned: false
+suggested_hardware: zero-a10g
+license: mit
 ---
 
-Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference
+# PLSemanticsBench interactive demo
+
+This Space powers the “Try it yourself” panel on the
+[PLSemanticsBench project page](https://engineeringsoftware.github.io/PLSemanticsBench/).
+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.
+
+The named Gradio API endpoint is `/predict`.

app.py

@@ -0,0 +1,172 @@
+"""ZeroGPU Gradio app for the PLSemanticsBench interactive demo."""
+
+from __future__ import annotations
+
+import re
+import time
+
+import spaces
+import gradio as gr
+import torch
+from datasets import load_dataset
+from transformers import AutoModelForCausalLM, AutoTokenizer
+
+from cstar import (
+    DATASET_ID,
+    INTERVENTIONS,
+    SemanticsSpec,
+    build_predstate_prompt,
+)
+
+MODEL_ID = "deepseek-ai/DeepSeek-R1-Distill-Qwen-1.5B"
+DEFAULT_PROGRAM = """int a;
+int b;
+int ans;
+a = 10;
+b = 3;
+ans = (a + b);"""
+
+
+def _load_semantics() -> dict[tuple[str, str], SemanticsSpec]:
+    specs: dict[tuple[str, str], SemanticsSpec] = {}
+    for formalization in ("S", "K"):
+        standard_split = load_dataset(
+            DATASET_ID,
+            "predstate",
+            split=f"{formalization}_Standard_Human_Written",
+        )
+        standard = standard_split[0]
+        specs[(formalization, "Standard")] = SemanticsSpec(
+            syntax=standard["syntax"],
+            semantics=standard["semantics"],
+        )
+
+        nonstandard_split_name = f"{formalization}_NonStandard_Human_Written"
+        nonstandard_split = load_dataset(
+            DATASET_ID,
+            "predstate",
+            split=nonstandard_split_name,
+        )
+        for intervention in ("KeywordSwap", "KeywordObf"):
+            record = next(
+                (
+                    row
+                    for row in nonstandard_split
+                    if row["mutation-pattern"] == intervention
+                ),
+                None,
+            )
+            if record is None:
+                raise RuntimeError(
+                    f"{intervention} is missing from {nonstandard_split_name}."
+                )
+            specs[(formalization, intervention)] = SemanticsSpec(
+                syntax=record["syntax"],
+                semantics=record["semantics"],
+            )
+    return specs
+
+
+SEMANTICS_SPECS = _load_semantics()
+TOKENIZER = AutoTokenizer.from_pretrained(MODEL_ID)
+MODEL = AutoModelForCausalLM.from_pretrained(
+    MODEL_ID,
+    torch_dtype=torch.bfloat16,
+).to("cuda")
+MODEL.eval()
+
+
+def _extract_answer(response: str) -> str:
+    matches = re.findall(r"<answer>.*?</answer>", response, flags=re.DOTALL)
+    return matches[-1].strip() if matches else response.strip()
+
+
+@spaces.GPU(duration=30)
+def predict(
+    program: str,
+    intervention: str,
+    formalization: str,
+) -> tuple[str, str, str, str]:
+    """Run one benchmark-style PredState request on ZeroGPU."""
+    started = time.perf_counter()
+    prompt, transformed_program = build_predstate_prompt(
+        program=program,
+        intervention=intervention,
+        formalization=formalization,
+        specs=SEMANTICS_SPECS,
+    )
+    messages = [{"role": "user", "content": prompt}]
+    model_inputs = TOKENIZER.apply_chat_template(
+        messages,
+        add_generation_prompt=True,
+        return_tensors="pt",
+    ).to("cuda")
+
+    with torch.inference_mode():
+        generated = MODEL.generate(
+            model_inputs,
+            max_new_tokens=512,
+            do_sample=False,
+            pad_token_id=TOKENIZER.eos_token_id,
+        )
+
+    response = TOKENIZER.decode(
+        generated[0, model_inputs.shape[-1] :],
+        skip_special_tokens=True,
+    ).strip()
+    answer = _extract_answer(response)
+    elapsed = time.perf_counter() - started
+    run_details = (
+        f"{MODEL_ID} · {intervention} · {formalization} · {elapsed:.1f}s"
+    )
+    return answer, response, transformed_program, run_details
+
+
+with gr.Blocks(title="PLSemanticsBench · Try C*") as demo:
+    gr.Markdown(
+        """
+# Try C* under counterfactual semantics
+
+Enter a standard C* program. The app applies the selected PLSemanticsBench
+intervention, supplies the corresponding formal semantics to the model, and
+asks it to predict the final state.
+"""
+    )
+    with gr.Row():
+        intervention_input = gr.Radio(
+            choices=list(INTERVENTIONS),
+            value="Standard",
+            label="Semantic intervention",
+        )
+        formalization_input = gr.Dropdown(
+            choices=["Small-step (S)", "K semantics"],
+            value="Small-step (S)",
+            label="Formalization",
+        )
+    program_input = gr.Code(
+        value=DEFAULT_PROGRAM,
+        language="c",
+        label="Standard C* program",
+        lines=12,
+    )
+    run_button = gr.Button("Run model", variant="primary")
+    answer_output = gr.Code(label="Predicted final state", language="html")
+    with gr.Accordion("Program after intervention", open=True):
+        transformed_output = gr.Code(language="c")
+    with gr.Accordion("Raw model output", open=False):
+        raw_output = gr.Textbox(lines=10)
+    details_output = gr.Textbox(label="Run details", interactive=False)
+
+    run_button.click(
+        fn=predict,
+        inputs=[program_input, intervention_input, formalization_input],
+        outputs=[
+            answer_output,
+            raw_output,
+            transformed_output,
+            details_output,
+        ],
+        api_name="predict",
+    )
+
+demo.queue(default_concurrency_limit=1).launch()

cstar.py

@@ -0,0 +1,170 @@
+"""C* source transformations and prompt construction for the interactive demo."""
+
+from __future__ import annotations
+
+import re
+from dataclasses import dataclass
+from typing import Mapping
+
+DATASET_ID = "EngineeringSoftware/PLSemanticsBench"
+MAX_PROGRAM_CHARS = 6_000
+
+INTERVENTIONS = {
+    "Standard": {},
+    "KeywordSwap": {
+        "+": "-",
+        "-": "+",
+        "*": "/",
+        "/": "*",
+        "<": ">",
+        ">": "<",
+        "<=": ">=",
+        ">=": "<=",
+        "==": "!=",
+        "!=": "==",
+        "&&": "||",
+        "||": "&&",
+    },
+    "KeywordObf": {
+        "+": "𐕐",
+        "-": "𐕙",
+        "*": "𐕊",
+        "/": "𐕏",
+        "%": "𐕖",
+        "=": "𐕂",
+        "<": "𐔳",
+        ">": "𐕃",
+        "<=": "𐔷",
+        ">=": "𐕛",
+        "==": "𐕟",
+        "!=": "𐕀",
+        "&&": "𐕜",
+        "||": "𐔻",
+        "!": "𐔰",
+        "break": "𐔾",
+        "if": "𐔸",
+        "else": "𐕎",
+        "while": "𐕕",
+        "halt": "𐔱",
+        "continue": "𐔲",
+    },
+}
+
+FORMALIZATIONS = {
+    "Small-step (S)": "S",
+    "K semantics": "K",
+}
+
+_TOKEN_PATTERN = re.compile(
+    r"""
+    "(?:\\.|[^"\\])*"             | # string literal
+    '(?:\\.|[^'\\])*'             | # character literal
+    //[^\n]*                       | # line comment
+    /\*.*?\*/                      | # block comment
+    <=|>=|==|!=|&&|\|\|            | # multi-character operators
+    [+\-*/%=<>!]                   | # single-character operators
+    [A-Za-z_][A-Za-z0-9_]*           # identifiers and keywords
+    """,
+    re.DOTALL | re.MULTILINE | re.VERBOSE,
+)
+
+
+@dataclass(frozen=True)
+class SemanticsSpec:
+    syntax: str
+    semantics: str
+
+
+def validate_program(program: str) -> str:
+    program = program.strip()
+    if not program:
+        raise ValueError("Enter a C* program before running the model.")
+    if len(program) > MAX_PROGRAM_CHARS:
+        raise ValueError(
+            f"Keep the program under {MAX_PROGRAM_CHARS:,} characters for this demo."
+        )
+    return program
+
+
+def transform_program(program: str, intervention: str) -> str:
+    """Apply the benchmark's lexical intervention to standard C* source."""
+    try:
+        replacements = INTERVENTIONS[intervention]
+    except KeyError as exc:
+        raise ValueError(f"Unknown semantic intervention: {intervention}") from exc
+
+    if not replacements:
+        return program
+
+    def replace_token(match: re.Match[str]) -> str:
+        token = match.group(0)
+        if token.startswith(('"', "'", "//", "/*")):
+            return token
+        return replacements.get(token, token)
+
+    return _TOKEN_PATTERN.sub(replace_token, program)
+
+
+def build_predstate_prompt(
+    *,
+    program: str,
+    intervention: str,
+    formalization: str,
+    specs: Mapping[tuple[str, str], SemanticsSpec],
+) -> tuple[str, str]:
+    """Build the benchmark-style PredState prompt and transformed source."""
+    program = validate_program(program)
+    try:
+        formalization_key = FORMALIZATIONS[formalization]
+    except KeyError as exc:
+        raise ValueError(f"Unknown formalization: {formalization}") from exc
+
+    transformed_program = transform_program(program, intervention)
+    try:
+        spec = specs[(formalization_key, intervention)]
+    except KeyError as exc:
+        raise ValueError(
+            f"No semantics found for {formalization} / {intervention}."
+        ) from exc
+
+    if formalization_key == "S":
+        formalization_intro = f"""Here is the C* syntax in EBNF:
+```
+{spec.syntax}
+```
+
+Here is the complete small-step operational semantics:
+```
+{spec.semantics}
+```"""
+        termination_note = (
+            "Execution finishes at one of the terminal configurations "
+            "〈ε, σ, χ〉, 〈halt, σ, χ〉, or 〈ERROR, σ, χ〉."
+        )
+    else:
+        formalization_intro = f"""Here is the complete K-framework formalization:
+```
+{spec.semantics}
+```"""
+        termination_note = ""
+
+    prompt = f"""You are an interpreter for C*. Use only the supplied formal
+semantics, even when a symbol conflicts with its conventional meaning. Assume
+the supplied rules are correct.
+
+{formalization_intro}
+
+Here is the C* program:
+```
+{transformed_program}
+```
+
+Predict the values of every declared variable after execution.
+{termination_note}
+- If execution does not terminate, return <answer>##timeout##</answer>.
+- If execution has an error or undefined behavior, return <answer>##error##</answer>.
+- Otherwise, put every variable in its own XML tag inside <answer>.
+
+Return only the <answer> XML block. Do not include reasoning or commentary."""
+
+    return prompt, transformed_program

requirements.txt

@@ -0,0 +1,4 @@
+datasets>=4.0,<5
+spaces>=0.45
+torch==2.8.0
+transformers>=4.51,<6