NEAR a utilisé DeepSeek pour résoudre 600 problèmes de mathématiques et s'efforce de rendre l’audit du code on-chain aussi abordable que possible.

Auteur : 长安, DeepTechFlow

Résumé DeepTech : 672 problèmes issus des plus prestigieux concours de mathématiques universitaires nord-américains ont tous été résolus par l'équipe NEAR AI à l'aide d'un Agent. Le coût total s’est élevé à environ 111 dollars, soit 0,17 dollar par question. L'équipe NEAR AI a fait appel au modèle open source chinois DeepSeek V4 pour réaliser ce test. Il ne s’agit pas seulement d’une simple compétition d’intelligence d’IA, mais d’une entreprise d’infrastructure visant à démocratiser la "vérification formelle" des smart contracts, traditionnellement coûteuse.

Les données de test d’un référentiel open source révèlent clairement le coût de résolution de problèmes par les grands modèles d’IA.

Récemment, selon les données publiées par Alex Skidanov, cofondateur de NEAR Protocol, ainsi que par la branche officielle, l’Agent NEAR AI a résolu les 672 problèmes mathématiques de PutnamBench.

Pour les lecteurs moins familiers, PutnamBench n’est pas une base de problèmes ordinaire. Il s’agit d’un benchmark composé des énoncés formalisés des concours universitaires de mathématiques les plus prestigieux des États-Unis (William Lowell Putnam).

En d’autres termes, il s’agit de demander à une IA d’effectuer des raisonnements mathématiques rigoureux pour vérifier si elle peut résoudre de manière autonome les problèmes. Pour venir à bout de tous les exercices, NEAR AI a dépensé environ 111,85 dollars. Cela représente un coût moyen de 0,17 dollar par problème.

À titre de comparaison, les autres solutions ayant obtenu le score maximal sont de loin beaucoup plus onéreuses.

Selon les données compilées par MSBIntel, utiliser le GPT-5.6 d’OpenAI revient à 44,5 dollars par problème ; utiliser le Claude Opus 5 d’Anthropic coûte 3,52 dollars par exercice.

Dans ce test spécifique, NEAR a choisi la solution DeepSeek V4, ramenant le coût à un 250e de celui de GPT-5.6.

Une blockchain qui résout des problèmes de maths : un objectif bien au-delà de l’éducation

L’effort fourni par une équipe blockchain pour résoudre des problèmes mathématiques ne vise pas le marché éducatif.

L'exigence centrale du test PutnamBench est la vérifiabilité machine : les réponses de l’IA ne doivent pas être de simples textes, mais des codes de démonstration strictement rédigés en Lean 4 (un langage assistant de preuve reconnu dans le domaine).

Ces codes ne doivent présenter aucune faille syntaxique, ne peuvent passer aucune étape du raisonnement, et doivent être validés à 100% par la machine. Ce principe correspond en informatique à une technique clé : la vérification formelle.

Dans l'industrie crypto, les smart contracts manipulent des centaines de millions voire des dizaines de milliards de dollars. Les audits de code traditionnels reposent sur l’analyse humaine pour détecter les failles, tandis que la vérification formelle consiste à démontrer, ligne par ligne, via des raisonnements mathématiques rigoureux, que le code ne produira jamais d’erreur dans toutes les situations possibles.

Depuis longtemps, le défaut majeur de la vérification formelle réside dans son coût élevé et sa lenteur. Elle nécessite des experts de sécurité de haut niveau et des délais souvent longs, généralement accessibles uniquement aux projets les mieux financés.

Ce test de NEAR AI démontre la faisabilité de générer en masse des preuves mathématiques fiables à l’aide de modèles open source, et surtout, la possibilité de le faire à très faible coût.

Une infrastructure abordable pour la sécurité on-chain

Faire passer le seuil de la vérification formelle à quelques dizaines de centimes, c'est le véritable objectif sur lequel NEAR travaille actuellement.

À ce jour, l'ensemble du code reliant DeepSeek et Lean 4 a été entièrement mis en open source. Le prochain objectif déclaré par NEAR est d’appliquer directement cet outil bon marché à la vérification de la sécurité des smart contracts centraux ainsi que du protocole NEAR lui-même.

On peut donc interpréter cela comme une démocratisation technologique, ou plus simplement, comme une preuve concrète que les équipes de projet passent à l’action dans la vague de l’IA.

Si l’IA open source peut produire de façon stable des preuves de sécurité de code vérifiables par machine, cela signifie que tout développeur ordinaire ou petite équipe pourrait, pour quelques dizaines de centimes, effectuer une vérification formelle avant de déployer son contrat. Cela réduirait largement le risque de bugs sur les smart contracts.

Cependant, il faut noter que cela n’a pas d’impact direct sur le cours du token NEAR à court terme. Mais dans la compétition de fond entre blockchains, dépenser quelques dizaines de centimes pour prévenir plutôt que des millions en interventions correctives confère une utilité commerciale bien réelle.