NEAR Protocol ha esbozado planes para aplicar verificación formal asistida por IA a su protocolo y contratos inteligentes principales tras reportar 672 problemas matemáticos resueltos a un costo de modelo en el momento de la presentación de $111.85.
Resumen
- NEAR planea aplicar verificación formal asistida por IA a su protocolo y contratos inteligentes principales.
- NEAR AI reportó haber resuelto 672 problemas de PutnamBench a un costo de modelo en el momento de la presentación de $111.85.
- La verificación en producción requiere modelos de software precisos, requisitos definidos y pruebas que cubran la implementación desplegada.
- La verificación formal complementa las pruebas y las revisiones de código, con garantías limitadas a propiedades y supuestos especificados.
NEAR Protocol dijo en un anuncio del 16 de octubre que su investigación busca reducir el trabajo especializado y los costos computacionales involucrados en probar que el software sigue reglas definidas.
La aplicación planificada cubre el protocolo de la red y los contratos principales, junto con herramientas para desarrolladores del ecosistema. NEAR describió la verificación en producción como un objetivo, mientras que su trabajo de referencia completado se refiere a la generación automatizada de pruebas matemáticas.
NEAR planea llevar la generación de pruebas al software de producción
Según el anuncio de NEAR, aplicar la investigación al software en funcionamiento implica tres etapas. Los desarrolladores deben representar un programa matemáticamente, definir las propiedades que debe satisfacer y construir pruebas que demuestren que esas propiedades se cumplen.
Los resultados recientes de referencia de NEAR AI demuestran progreso en la tercera etapa. El anuncio señala que el trabajo de producción aún requiere modelos precisos del comportamiento del software y una conexión clara entre las pruebas y la implementación en la que confían los usuarios.
En su explicación, NEAR distingue una prueba que cubre una regla contable particular de una garantía de que una aplicación entera es segura. Un contrato podría preservar los saldos durante las transferencias mientras requiere una prueba separada de que solo las cuentas autorizadas pueden iniciarlas.
El cofundador de NEAR, Illia Polosukhin, ha vinculado la investigación con los riesgos del software generado por IA y las herramientas que ayudan a los atacantes a identificar debilidades.
"El futuro de la IA, y del código generado por IA, es emocionante, pero solo una vez que logremos garantías verificables y matemáticas de su comportamiento."
El anuncio reproduce la declaración de los escritos de Polosukhin sobre seguridad del software. NEAR afirma que la verificación formal debe complementar las pruebas, la revisión de código y las prácticas de seguridad operativa.
El resultado de $111.85 mide pruebas matemáticas
El anuncio de NEAR informa que su agente de IA resolvió 672 problemas de Lean de PutnamBench, un punto de referencia basado en la competencia de matemáticas de pregrado Putnam. El costo medio reportado fue de aproximadamente $0.17 por problema a los precios de modelo utilizados para la presentación.
El repositorio público del proyecto describe el resultado como 670 problemas originales más versiones corregidas de dos problemas con formalizaciones defectuosas. NEAR afirma que el gasto reportado excluye el costo total de desarrollar el sistema y no estima el precio de verificar un contrato de producción.
En el repositorio, el equipo informa que reproducir el mismo uso a los precios fuera de hora posteriores listados de DeepSeek costaría $331. Su metodología incluye intentos fallidos, aunque los autores identifican un experimento paralelo separado usando Kimi que excluyeron de la contabilidad de costos.
El repositorio describe verificaciones contra pruebas inacabadas y cambios en el enunciado matemático que se está probando. Informa que la ejecución más larga duró más de tres días.
Junto con PutnamBench, NEAR afirma que su equipo alcanzó el primer lugar por total de soluciones en la tabla de clasificación de formalización Lean Eval v1. El anuncio especifica esa medida de clasificación, distinguiéndola de las primeras soluciones y las soluciones únicas.
Según NEAR, los benchmarks matemáticos ejercitan una capacidad necesaria para la verificación de software porque los desarrolladores traducen los requisitos de software en enunciados matemáticos. La empresa separa esos resultados del trabajo de demostrar propiedades del código desplegado.
Las pruebas formales dependen de las reglas que eligen los desarrolladores
En el ejemplo de transferencia de NEAR, una prueba convencional verifica una transacción seleccionada, como mover cinco tokens entre dos cuentas. Una prueba puede establecer que toda transferencia exitosa cubierta por el modelo matemático preserva el saldo combinado de las cuentas.
El anuncio explica que los desarrolladores primero eligen un requisito, expresan el comportamiento relevante del software matemáticamente y envían una prueba propuesta a un verificador. La garantía resultante depende de las definiciones y suposiciones utilizadas.
El enfoque de NEAR utiliza Lean, un lenguaje de programación de código abierto y asistente de pruebas. Un agente de IA puede proponer una prueba, ejecutar Lean, inspeccionar sus comentarios y revisar el intento, mientras el núcleo de Lean comprueba si la prueba sigue sus reglas lógicas.
Un intento fallido no identifica necesariamente un defecto del software, según NEAR. El requisito puede ser incorrecto, la implementación puede violarlo, o el agente puede no lograr encontrar una prueba válida.
La verificación formal ya tiene aplicaciones documentadas dentro del ecosistema NEAR. La evaluación de Certora del 30 de marzo de Templar, un protocolo de préstamos desplegado en NEAR, describe la revisión manual de sus contratos en Rust y la especificación y verificación formal de su contrato de mercado. La página de la evaluación de Certora identifica las propiedades demostradas y los problemas descubiertos como temas del informe completo.
Otros equipos de blockchain han buscado la verificación asistida por IA
En mayo, Aptos Labs describió el soporte para la verificación formal asistida por IA que involucra el despacho dinámico en contratos Move. Su flujo de trabajo declarado utiliza especificaciones generadas por IA con Move Prover, según la cobertura del anuncio.
El cofundador de Ethereum, Vitalik Buterin, ha discutido una combinación similar de herramientas de IA y pruebas verificadas por máquina. Como crypto.news informó anteriormente, sus comentarios de mayo identificaron aplicaciones en toda la hoja de ruta de Ethereum, incluidos el consenso, la criptografía resistente a la cuántica y los sistemas de conocimiento cero.
Buterin advirtió que demostrar una capa no establece que todo un sistema se comporte como se pretende. Su discusión abarcó la verificación desde especificaciones de alto nivel hasta la implementación de nivel inferior.
La investigación de seguridad separada de NEAR ha abordado la firma resistente a la cuántica. La propuesta de mayo de Near One seleccionó el soporte de firmas FIPS-204, utilizando el estándar ML-DSA aprobado por el Instituto Nacional de Estándares y Tecnología de EE. UU.
La propuesta de mayo describió un objetivo de testnet para el final del segundo trimestre de 2026. Near One dijo que el software de billetera, las billeteras de hardware, los endpoints y las API requerirían cambios coordinados para admitir los nuevos esquemas de firma.
