minif2f-824721bb·3 events·first seen Aliases: MiniF2F
Mistral AI released Leanstral 1.5, an Apache-2.0 licensed mixture-of-experts model with 119B total and 6B active parameters, specialized for formal verification in Lean 4. The model saturates miniF2F (100%), solves 587/672 PutnamBench problems, and achieves new state-of-the-art results on FATE-H (87%) and FATE-X (34%), while costing roughly $4 per problem versus ~$300 for comparable systems. Trained via mid-training, supervised fine-tuning, and reinforcement learning with CISPO, it demonstrates strong test-time scaling and practical code verification capabilities, uncovering 5 previously unknown bugs across 57 open-source repositories.
A new arXiv preprint introduces the signal-coverage matrix, a 2×2 framework that crosses Lean elaborator pass/fail with semantic-equivalence judgments to decompose autoformalization errors into four distinct cells rather than a single type-correctness scalar. The authors evaluate four methods (Vanilla, Lean-Retry, Sample-Filter, and Stratified Autoformalization) on ProofNet# and MiniF2F-test using DeepSeek V4-Pro, finding that headline TC% gains mask flat semantic-only error recovery and that symbolic and LLM judges diverge by 26–37 percentage points on elaborator-feedback outputs. The work argues that TC% improvements should be credited by which error cell moved, not by the aggregate scalar alone.
Goedel-Architect is an agentic framework for formal theorem proving in Lean 4 that uses blueprint generation — a dependency graph of definitions and lemmas — rather than recursive decomposition, enabling parallel lemma closure and global refinement. Built on DeepSeek-V4-Flash (284B-A13B), it achieves 99.2% pass@1 on MiniF2F-test and 75.6% on PutnamBench, scaling to 100% on MiniF2F, 88.8% on PutnamBench, and 4/6 on IMO 2025 when seeded with natural-language proofs. The authors claim state-of-the-art performance for an open-source pipeline at up to 500x lower cost than comparable systems.