formalmathatepfl/qwen3-4b-feedback-evluator

Qwen3-4B Feedback Evaluator

Given a Lean 4 program, this model generates the program annotated with predicted compiler feedback. To obtain a binary validity prediction, check the generated feedback blocks for an error marker using a regex.

Input and output

Input: unannotated Lean source, including any imports and declarations needed by the program. Format the prompt as source_code.rstrip() + "\n\n". Use plain text, without a chat template, instructions, or Markdown code fences.

Output: Lean source annotated with inline feedback comments, such as /- <feedback> ... </feedback> -/.

Example input:

example : False := by
  trivial

Illustrative output (the exact generated feedback may vary):

example : False := by
  trivial
/- <feedback>
-- type: error, msg: tactic 'trivial' failed
⊢ False
</feedback> -/

Generate feedback

Install the inference dependencies:

pip install torch 'transformers>=4.51.0' accelerate

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "formalmathatepfl/qwen3-4b-feedback-evluator"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id,
    torch_dtype=torch.bfloat16,
    device_map="auto",
)
model.eval()

source_code = """example : False := by
  trivial
"""
prompt = source_code.rstrip() + "\n\n"
inputs = tokenizer(prompt, return_tensors="pt", add_special_tokens=False).to(model.device)

with torch.inference_mode():
    output_ids = model.generate(
        **inputs,
        max_new_tokens=4096,
        do_sample=False,
        pad_token_id=tokenizer.eos_token_id,
    )

# Decode only the generated annotation, excluding the input prompt.
feedback = tokenizer.decode(
    output_ids[0, inputs["input_ids"].shape[1]:],
    skip_special_tokens=True,
)
print(feedback)

Allow enough output tokens for the model to reproduce the source and add feedback. If generation reaches the token limit, increase the budget before classifying it.

Classify the generated feedback

Search inside the generated <feedback> ... </feedback> blocks for -- type: error:

import re

FEEDBACK_BLOCK_RE = re.compile(
    r"<feedback>(.*?)</feedback>", re.DOTALL | re.IGNORECASE
)
ERROR_RE = re.compile(r"--\s*type\s*:\s*error\b", re.IGNORECASE)


def predict_validity(feedback: str) -> bool:
    return not any(
        ERROR_RE.search(block)
        for block in FEEDBACK_BLOCK_RE.findall(feedback)
    )


predicted_valid = predict_validity(feedback)
print({"predicted_valid": predicted_valid})

• An error marker in any feedback block gives False.
• No error marker in the feedback blocks gives True; warning and info messages alone do not count as errors.

The Boolean is computed from the generated feedback. Direct lean_verified True/False prediction and parsing an explicit \lean4_valid{True|False} verdict belong to the older method and are not used here.

This is a model prediction of compiler feedback; actual verification requires running the program through Lean.