violetxi/Qwen3.5-9B-EquationalTheories-Proof-nl-eval
Qwen3.5-9B base: Equational Theories prose-proof evaluation Accuracy: 42.73% (282/660 correct). Single-turn natural-language proof correctness, graded by GPT-5.6-sol. These are model-judged results; generated proofs were not checked by the Lean kernel. Model Accuracy Correct / total Change vs base Base (this dataset) 42.73% 282/660 +0.00 pp 1M 38.64% 255/660 -4.09 pp 3M 44.85% 296/660 +2.12 pp 10M 43.64% 288/660 +0.91 pp The default dataset viewer now shows… See the full description on the dataset page: https://huggingface.co/datasets/violetxi/Qwen3.5-9B-EquationalTheories-Proof-nl-eval.
Qwen3.5-9B base: Equational Theories prose-proof evaluation
Accuracy: 42.73% (282/660 correct).
Single-turn natural-language proof correctness, graded by GPT-5.6-sol. These are model-judged results; generated proofs were not checked by the Lean kernel.
The default dataset viewer now shows this performance comparison: performance / summary. It contains four aggregate rows, one per model, with overall and per-split accuracies. For individual attempts, select single_turn_proof; correct and verdict are the first columns.
All scores count all 660 tasks, including empty and truncated outputs. change_vs_base_pp is the difference in percentage points from Base.
Unmodified base Qwen3.5-9B.
One completion per problem, Lean theorem input and natural-language proof output. No tools, notes, or reference proofs were supplied to the solver. GPT-5.6-sol graded final proofs against trusted Lean references. These are model-judged scores; generated proofs were not checked by the Lean kernel.
final: general magmas; final_finite: finite magmas; final_equivalence: 208 directions forming 104 equivalence pairs; final_duality: opposite-operation dualities. The four splits together cover all 660 tasks.
Reading the trajectories
transcript renders the full solver conversation, including generated reasoning. messages contains the system, user, and assistant messages, with reasoning stored separately on the assistant. reasoning and final_output expose the generated fields directly. finish_reason records token-budget termination. assistant_tokens includes generated reasoning. verdict, correct, and grader_explanation contain the recorded grade. attempt_json preserves the original attempt except the private reference proof; grade_json preserves the original grade and usage. Private reference proofs and certificates are omitted.
from datasets import load_dataset, concatenate_datasets
ds = load_dataset("violetxi/Qwen3.5-9B-EquationalTheories-Proof-nl-eval", "single_turn_proof")
all_660 = concatenate_datasets([ds[s] for s in ["final", "final_finite", "final_equivalence", "final_duality"]])Reproducibility
The solver uses temperature 0.6, top-p 0.95, thinking enabled, and a total completion budget of 16,384 tokens. Seeds, input messages, task IDs, and splits match across all four models. Only the final proof is graded; generated reasoning is retained for inspection. Grader: gpt-5.6-sol, requested reasoning effort high, maximum completion tokens 8,000. Solver prompts and the grader system prompt are in prompts/. provenance.json records the pinned base revision, checkpoint hashes, training settings, decoding, and source hashes. Base serving used 131,072 context and 48 workers; trained runs used 32,768 context and 72 workers. Every input plus the completion budget fits both context limits.