Ayon sa 1M AI News , ang koponan ng Meituan LongCat ay nag-open source ang LongCat-Flash-Prover, isang MoE model na may 560 bilyong parameter na espesyalisado sa mga gawain ng matematikal na pag-iisip para sa formang pagsasalaysay ng teorema na Lean4. Ang mga timbang ng model ay inilabas sa ilalim ng MIT license at nasa GitHub, Hugging Face, at ModelScope na ngayon.
Ang modelo ay naghihiwalay ang pormal na pag-iisip sa tatlong hiwalay na kakayahan: awtomatikong pormalisasyon (pagsasalin ng natural na wika sa matematikal na problema sa mga pormal na pahayag ng Lean4), pagbuo ng sketsa (paglikha ng mga framework ng patotoo na estilo ng lemma), at pagbuo ng kompletong patotoo. Ang lahat ng tatlong kakayahan ay pinagpapatotohanan sa real-time sa pamamagitan ng integrasyon ng mga kasangkapan ng Agent sa pag-iisip (TIR) at ang Lean4 compiler.
Sa aspeto ng pagtuturo, ang koponan ay nagmungkahi ng Hybrid-Experts Iteration Framework upang lumikha ng cold-start data, at sa pagkakaroon ng reinforcement learning, ipinakilala ang HisPO algorithm upang mapanatili ang katatagan ng pagtuturo ng malalayong gawain sa MoE model, samantalang idinagdag ang mga mekanismo ng pagsubok sa pagkakatugma at kawastuhan ng teorema upang maiwasan ang reward hacking.
Ang benchmark ay nagpapakita na ang LongCat-Flash-Prover ay nag-set ng bagong SOTA sa automatic formalization at theorem proving sa mga open-source weight models. Nakamit ang 97.1% pass rate sa MiniF2F-Test gamit ang 72 inference lamang, at 70.8% at 41.5% sa ProverBench at PutnamBench, kasama ang hindi hihigit sa 220 inference bawat tanong.