Subiect: #Matematică
Kimina-Prover: Revoluția în Demonstrația Automată de Teoreme prin Căutare RL în Timpul Testării
Kimina-Prover-72B stabilește un nou standard în demonstrația automată de teoreme, atingând o rată de succes de 92.2% pe benchmark-ul miniF2F. Inovația sa principală, cadrul TTRL Search, permite modelului să descopere și combine recursiv leme, transformând procesul dintr-o simplă generare într-o căutare agentică strategică și profundă.
Kimina-Prover-RL: O nouă eră în demonstrarea automată a teoremelor prin învățare prin întărire
Echipa Kimina lansează kimina-prover-rl, un pipeline open-source de învățare prin întărire pentru demonstrarea teoremelor în Lean 4, care utilizează un paradigmă de raționament structurat și un mecanism inovator de corecție a erorilor, obținând performanțe de top pentru modelele de dimensiuni mici.
Axiom Math și revoluția AI în matematică: Un instrument gratuit promite să democratizeze descoperirea științifică
Startup-ul Axiom Math lansează Axplorer, un instrument AI gratuit care rulează pe un PC personal, promițând să democratizeze cercetarea matematică și să accelereze descoperirea de noi tipare, dincolo de simpla rezolvare a problemelor existente.
DeepMath: Un agent ușor de raționament matematic, construit cu smolagents
DeepMath este un agent inovator de raționament matematic bazat pe modelul Qwen3-4B, care utilizează fragmente de cod Python executate într-un mediu securizat pentru a reduce erorile și lungimea output-ului cu până la 66%, demonstrând că modelele mici pot depăși limitările tradiționale ale LLM-urilor prin antrenament GRPO și arhitecturi hibride.