Cette page résume et organise les publications en intelligence artificielle du monde entier. Les contenus sont synthétisés grâce à Google Gemini et le service est proposé à but non lucratif. Les droits d'auteur des articles appartiennent à leurs auteurs ou institutions respectives ; en cas de partage, il suffit d'en mentionner la source.
Seed-Prover : Raisonnement approfondi et large pour la démonstration automatisée de théorèmes
Created by
Haebom
Auteur
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, Thomas Hanwen Zhu
Contour
Cet article propose un nouveau modèle, appelé Seed-Prover, pour améliorer les capacités de raisonnement mathématique des modèles de langage à grande échelle (LLM). Seed-Prover s'appuie sur Lean, un langage de vérification formelle, pour améliorer itérativement le processus de preuve par apprentissage par renforcement. Nous concevons trois stratégies d'inférence pour résoudre les problèmes de niveau IMO. Notre modèle prouve 78,1 % des problèmes IMO antérieurs, atteint des performances de pointe sur le jeu de données MiniF2F et surpasse PutnamBench de plus de 50 %. Cela surpasse considérablement les méthodes existantes. De plus, pour pallier le manque de prise en charge géométrique de Lean, nous avons également développé un moteur d'inférence géométrique appelé Seed-Geometry, prouvant avec succès cinq des six problèmes du défi IMO 2025. Cela représente une avancée significative dans le domaine du raisonnement mathématique automatisé exploitant la vérification formelle et la réflexion à long terme.
Takeaways, Limitations
•
Takeaways:
◦
De grands progrès ont été réalisés dans le domaine de la démonstration de théorèmes mathématiques à l’aide de LLM.
◦
Nous avons démontré l’efficacité de l’apprentissage par renforcement en utilisant des langages formels tels que Lean.
◦
Seed-Prover et Seed-Geometry surpassent considérablement les systèmes d'inférence mathématique automatisés existants.
◦
La praticabilité du modèle a été vérifiée par une participation réelle à l’OMI 2025.
•
Limitations:
◦
Il présente une forte dépendance aux langages Lean. Des recherches sont nécessaires pour explorer son extensibilité à d'autres langages formels.
◦
Des extensions de prise en charge de la géométrie, notamment Seed-Geometry, sont requises.
◦
Vous ne pourrez peut-être pas résoudre tous les problèmes mathématiques, et vous serez peut-être fort dans certains types de problèmes.
◦
Il y a un manque d’analyse de la complexité informatique et du temps de traitement.
