Independent re-evaluation by the Zurich formal methods group reproduced 51.8% on the held-out set with a clean-room rebuild of Kestrel-7

open — nothing has been offered for or against it · what this means

no sources · falsifiability unrated

0 ◎ brunner_fm (15) · 2 months ago · reproducibility, formal-verification

Brunner, Sahakyan & Oyelaran (2026) retrained the Kestrel architecture from the published recipe on their own Mathlib snapshot and evaluated on the same 300 held-out problems under identical compute budget, obtaining 51.8% pass@64. The 2.3-point shortfall was traced to a smaller synthetic-proof corpus (9M vs 14M states).

rate this claim

Accurate 0
Falsifiable 0
Clear 0
Novel 0
Important 0

evidence

cited by (1)

[+0] Held-out contamination audit found miniF2F-Lean4 gains persist at 54% on 300 freshly authored problems never posted online discuss machine-learning

this claim

opposes (0)

no opposing evidence yet

whole evidence graph shown depth 1 2 3 both pro con full

what the marks mean

supports · opposes · cites this claim · the claim you are reading
[+9] net votes on the evidence link — whether this is good evidence here, not whether the claim itself is true
Af··· accurate, falsifiable, clear, novel, important — a capital is established, lowercase weak, unrated; no strip at all where nothing has been rated yet
[?] no score has been computed for that claim yet
field shown only where a claim's fields differ from the one above it, so a field marks where the argument crosses into another

respondeo

Loading responses… open them

Independent re-evaluation by the Zurich formal methods group reproduced 51.8% on the held-out set with a clean-room rebuild of Kestrel-7

evidence

respondeo

discussion