El problema fundamental que FlashProve aborda es la falta de confianza y verificabilidad en la inferencia de modelos de IA a escala. En un ecosistema donde los modelos son cajas negras y la infraestructura de servicio es opaca, los usuarios y reguladores carecen de mecanismos para asegurar que una respuesta proviene del modelo específico que se afirma, o que el hardware se utiliza para el propósito declarado (ej. inferencia vs. entrenamiento). Esto es crítico para la seguridad, la atribución de resultados, el cumplimiento normativo y la prevención de manipulaciones.
Históricamente, la verificación de computaciones complejas ha sido un desafío. Con la proliferación de modelos de IA de gran escala, la re-ejecución para verificación es inviable para la mayoría de los actores. La criptografía de conocimiento cero, particularmente los zkSNARKs, emerge como una solución prometedora al permitir que un 'prover' demuestre la corrección de una computación a un 'verifier' sin revelar los detalles internos de la computación (como los pesos del modelo), y con una prueba que es pequeña y rápida de verificar. La necesidad de esta capacidad se ha intensificado con la creciente complejidad y el impacto social de los modelos de IA, haciendo que la "provable inference" sea una prioridad.
Arquitectura del Sistema
FlashProve es un sistema de software que implementa "provable inference" para modelos de lenguaje grandes, específicamente Mixture-of-Experts (MoE), utilizando zkSNARKs. El sistema se divide en dos fases: una fase offline y una fase online.
En la fase offline, el proveedor del modelo (prover) genera y publica un 'commitment' criptográfico a los pesos del modelo. Este commitment es una huella digital corta que identifica de forma única los pesos del modelo sin revelarlos. Las pruebas de inferencia posteriores se verificarán contra este commitment.
En la fase online, cuando un usuario (verifier) envía un prompt y recibe tokens de salida, el prover genera un archivo de prueba. Este archivo de prueba demuestra criptográficamente que el modelo comprometido produjo esos tokens de salida específicos para el prompt dado. La arquitectura del zkSNARK subyacente se basa en un "interactive oracle proof" (IOP) compilado en una prueba criptográfica mediante funciones hash (ofreciendo seguridad post-cuántica). Utiliza bloques de construcción avanzados como "code proximity tests with linear constraints" y "lookup arguments", derivados de la teoría de codificación y la teoría de la complejidad. El sistema está optimizado para modelos MoE, donde el trabajo del prover es proporcional solo a los expertos activados por token, no a todos los parámetros del modelo. Las solicitudes se prueban en lotes de forma "post-hoc" (después de la inferencia), y el sistema está diseñado para caber en una sola GPU H100, segmentando los pesos del modelo y transmitiéndolos desde la memoria del host. Para la verificación, se proporcionan dos implementaciones: un verifier rápido en C++ y un verifier formalmente verificado en Lean, que garantiza la corrección matemática de las propiedades de seguridad (completitud, solidez, zero-knowledge) en el modelo de oráculo aleatorio.
Flujo de Prueba de Inferencia con FlashProve
- 1 Fase Offline: Prover Genera y publica un 'commitment' criptográfico a los pesos del modelo.
- 2 Fase Online: Verifier Envía un prompt al Prover.
- 3 Fase Online: Prover Ejecuta la inferencia del modelo y genera tokens de salida.
- 4 Fase Online: Prover Genera un zkSNARK demostrando que el modelo comprometido produjo los tokens.
- 5 Fase Online: Prover Envía los tokens de salida y el zkSNARK al Verifier.
- 6 Fase Online: Verifier Verifica el zkSNARK usando el commitment del modelo y los tokens recibidos.
- 7 Fase Online: Verifier Acepta o rechaza la autenticidad de la inferencia.
| Capa | Tecnología | Justificación |
|---|---|---|
| compute | NVIDIA H100 GPU | Hardware principal para la generación de pruebas (prover) debido a su alta capacidad de cómputo paralelo. Una sola H100 con 290 GB de memoria host para streaming de pesos. |
| compute | CPU (24 cores) | Utilizado por el prover para tareas auxiliares y por el verifier para la verificación de pruebas. |
| data-processing | zkSNARKs | Mecanismo criptográfico central para generar pruebas concisas y de conocimiento cero de la inferencia del modelo. vs Trusted Execution Environments (TEEs) Basado en Interactive Oracle Proofs (IOPs) con hash functions, code proximity tests y lookup arguments. |
| orchestration | Lean proof assistant | Lenguaje de verificación formal para especificar el protocolo, probar propiedades de seguridad y generar un verifier formalmente correcto. |
| data-processing | Llama 4 Maverick (400B-parameter MoE) | Modelo de lenguaje de gran escala utilizado como caso de estudio para la implementación y evaluación de FlashProve. Pesos cuantificados a 4-bit, aritmética de enteros en prefill. |
| data-processing | vLLM | Motor de inferencia de código abierto utilizado como benchmark para comparar el rendimiento de la inferencia sin pruebas. FP8 release del modelo en ocho H100s. |
Trade-offs
Ganancias
- ▲ Verificabilidad criptográfica de la inferencia
- ▲ Privacidad de los pesos del modelo
- ▲▲ Reducción del tamaño y tiempo de verificación de pruebas
Costes
- ▲ Mayor tiempo de cómputo para la inferencia (overhead del prover)
- ▲ Complejidad de implementación y verificación formal
- △ Limitaciones en el contexto de inferencia (1024 tokens)
- △ No oculta la arquitectura del modelo
Fundamentos Teóricos
El concepto de pruebas de conocimiento cero (Zero-Knowledge Proofs) fue introducido por Goldwasser, Micali y Rackoff en su seminal paper "The Knowledge Complexity of Interactive Proof Systems" (1985). Este trabajo sentó las bases para los sistemas criptográficos que permiten a una parte probar la posesión de conocimiento o la corrección de una computación sin revelar información adicional. Los zkSNARKs (Zero-Knowledge Succinct Non-Interactive Arguments of Knowledge) son una evolución de estos principios, ofreciendo pruebas que son "succinct" (pequeñas y rápidas de verificar) y "non-interactive" (no requieren interacción continua entre prover y verifier después de una fase de configuración inicial).
FlashProve se basa en esta rica tradición académica, aplicando principios de la teoría de la complejidad y la teoría de codificación para construir sus IOPs. La formalización en Lean, un asistente de pruebas, conecta el sistema con el campo de la verificación formal, que busca garantizar la corrección de software y protocolos mediante pruebas matemáticas rigurosas, un área de investigación activa en ciencias de la computación y lógica.