SoS1 : Les modèles de langage à raisonnement de type O1 et R1 sont des solveurs de sommes de carrés.

SoS1: O1 and R1-Like Reasoning LLMs are Sum-of-Square Solvers

February 27, 2025

Auteurs: Kechen Li, Wenqi Zhu, Coralia Cartis, Tianbo Ji, Shiwei Liu

cs.AI

Résumé

Les modèles de langage de grande taille (LLMs) ont atteint un niveau de compétence comparable à celui des humains pour une variété de tâches, mais leur capacité à résoudre des problèmes mathématiques rigoureux reste un défi ouvert. Dans ce travail, nous étudions un problème fondamental mais computationnellement insoluble : déterminer si un polynôme multivarié donné est non négatif. Ce problème, étroitement lié au dix-septième problème de Hilbert, joue un rôle crucial dans l'optimisation globale des polynômes et trouve des applications dans divers domaines. Tout d'abord, nous présentons SoS-1K, un ensemble de données soigneusement constitué d'environ 1 000 polynômes, accompagné d'instructions de raisonnement conçues par des experts et basées sur cinq critères progressivement plus difficiles. En évaluant plusieurs LLMs de pointe, nous constatons que, sans guidance structurée, tous les modèles ne performent que légèrement au-dessus du seuil de hasard de 50 %. Cependant, des instructions de raisonnement de haute qualité améliorent significativement la précision, augmentant les performances jusqu'à 81 %. De plus, notre modèle de 7B, SoS-7B, affiné sur SoS-1K pendant seulement 4 heures, surpasse en précision le DeepSeek-V3 de 671B et le GPT-4o-mini, tout en ne nécessitant respectivement que 1,8 % et 5 % du temps de calcul requis pour les lettres. Nos résultats mettent en lumière le potentiel des LLMs pour repousser les limites du raisonnement mathématique et s'attaquer à des problèmes NP-difficiles.

English

Large Language Models (LLMs) have achieved human-level proficiency across diverse tasks, but their ability to perform rigorous mathematical problem solving remains an open challenge. In this work, we investigate a fundamental yet computationally intractable problem: determining whether a given multivariate polynomial is nonnegative. This problem, closely related to Hilbert's Seventeenth Problem, plays a crucial role in global polynomial optimization and has applications in various fields. First, we introduce SoS-1K, a meticulously curated dataset of approximately 1,000 polynomials, along with expert-designed reasoning instructions based on five progressively challenging criteria. Evaluating multiple state-of-the-art LLMs, we find that without structured guidance, all models perform only slightly above the random guess baseline 50%. However, high-quality reasoning instructions significantly improve accuracy, boosting performance up to 81%. Furthermore, our 7B model, SoS-7B, fine-tuned on SoS-1K for just 4 hours, outperforms the 671B DeepSeek-V3 and GPT-4o-mini in accuracy while only requiring 1.8% and 5% of the computation time needed for letters, respectively. Our findings highlight the potential of LLMs to push the boundaries of mathematical reasoning and tackle NP-hard problems.