Математическият ИИ daVinci-Prover реши 97,1% от задачите в MiniF2F чрез компресиране на разсъжденията

Математическият изкуствен интелект daVinci-Prover постигна 97,1% успеваемост на теста MiniF2F чрез поетапна проверка на доказателствата в Lean 4 и периодично компресиране на историята на собствените си разсъждения. Системата постигна почти безпогрешен резултат на стандартния тест благодарение на неочакван похват: съкращаване на собствената си история на разсъжденията. В разработката daVinci-Prover моделът Qwen3.5 с 9 млрд. параметъра […]