Auteur : Chang'an, Shenchao TechFlow
Guide de Shenchao : L'équipe NEAR AI a résolu les 672 problèmes du concours de mathématiques universitaires nord-américain le plus prestigieux, en dépensant environ 111 dollars américains, soit 0,17 dollar par problème en moyenne. L'équipe NEAR AI a utilisé le modèle open source chinois DeepSeek V4 pour effectuer ce test. Il ne s'agit pas simplement d'une compétition d'intelligence des grands modèles ; derrière la facture de calcul se cache un projet d'infrastructure visant à démocratiser la « vérification formelle » coûteuse des contrats intelligents.
Données de test d'un dépôt de code ouvert, qui ont révélé le coût de résolution des problèmes par les grands modèles.
Récemment, selon les données publiées par Alex Skidanov, cofondateur de NEAR Protocol, et les canaux officiels, l'agent NEAR AI a résolu les 672 problèmes mathématiques sur PutnamBench.
Pour les lecteurs non familiers, PutnamBench n'est pas une simple base de questions ; c'est un benchmark formelisé à partir des sujets du concours de mathématiques universitaires les plus prestigieux d'Amérique du Nord, le William Lowell Putnam.
En termes simples, cela signifie faire effectuer à l’IA une déduction mathématique rigoureuse pour voir si elle peut résoudre les problèmes de manière autonome. Pour accomplir l’ensemble des solutions, NEAR AI a dépensé environ 111,85 dollars américains. En moyenne, le coût par problème est de 0,17 dollar américain.
En comparaison, les autres propositions ayant obtenu la note maximale sont beaucoup plus coûteuses.
Selon les données compilées par MSBIntel, l'utilisation de GPT-5.6 d'OpenAI coûte en moyenne 44,50 $ par question ; l'utilisation de Claude Opus 5 d'Anthropic coûte également 3,52 $ par question.
Lors de ce test spécifique, NEAR a réduit les coûts à un deux-cent-cinquantième du coût de GPT-5.6 en adoptant la solution DeepSeek V4.
Les chaînes publiques résolvent des problèmes mathématiques, mais l'intention du buveur n'est pas dans le vin
L'équipe de la chaîne publique consacre des efforts à résoudre des problèmes mathématiques, mais ce n'est pas destiné à éduquer le marché.
La exigence fondamentale du test PutnamBench est la vérifiabilité de la machine : la réponse générée par l'IA ne doit pas être simplement un texte, mais doit impérativement inclure un code de preuve rigoureux écrit en Lean 4 (un langage de assistant de preuve largement utilisé).
Ces codes ne doivent pas contenir de failles syntaxiques, ne doivent pas sauter d'étapes de déduction et doivent être vérifiés à 100 % par une machine. En même temps, cela correspond dans le domaine de l'informatique à une technologie clé appelée vérification formelle.
En lien avec l'industrie des cryptomonnaies, les contrats intelligents détiennent des fonds s'élevant à des centaines de millions, voire des milliards de dollars. L'audit traditionnel du code repose sur la détection manuelle de vulnérabilités, tandis que la vérification formelle utilise une logique mathématique rigoureuse pour prouver ligne par ligne que le code ne contient aucune erreur dans tous les états possibles.
Pendant longtemps, le principal défaut de la vérification formelle était son coût élevé et sa lenteur. Elle nécessite des experts en sécurité de premier plan et des cycles prolongés, et n’est généralement accessible qu’aux projets les plus importants disposant de ressources financières importantes.
Ce test de NEAR AI a démontré la faisabilité de générer en masse des preuves mathématiques fiables à l'aide de modèles AI open source, tout en confirmant son faible coût.
Infrastructures démocratisées pour la sécurité sur chaîne
Réduire le coût de la vérification formelle à quelques dizaines de cents, c’est le véritable projet que NEAR est en train de déployer.
Actuellement, ce code intégrant DeepSeek et Lean 4 est entièrement open source. La prochaine étape annoncée officiellement par NEAR consiste à appliquer directement cet outil à faible coût à la vérification de sécurité du protocole NEAR lui-même ainsi que de ses contrats intelligents principaux.
Ainsi, vous pouvez le comprendre comme une décentralisation technologique, ou, plus simplement, comme une action menée par l'équipe du projet liée à la narration AI.
Si l'IA open source peut produire de manière stable des preuves de sécurité de code vérifiables par machine, cela signifie que les développeurs ordinaires et les petites équipes de projets pourront, avant le déploiement des contrats, exécuter une vérification formelle pour quelques centimes, réduisant ainsi la probabilité de problèmes dans les contrats intelligents.
Cependant, objectivement, cela n’a pas de lien direct avec les fluctuations de prix à court terme du token NEAR. Mais dans la compétition fondamentale des écosystèmes de chaînes publiques, dépenser quelques dizaines de cents pour déminer est bien plus valorisant sur le plan commercial que de dépenser des millions pour réparer après coup.