🤖 machine learning

Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation

Este artículo introduce la Distilación en Política Ponderada por Recompensa (RWOPD), un método de entrenamiento novedoso que aprovecha un verificador formal de equivalencia de propiedades para guiar a un modelo estudiante de 7B en la generación de Aserciones en SystemVerilog, logrando un nuevo rendimiento de vanguardia al priorizar la corrección semántica sobre la imitación a nivel de token.

Autores originales: Qingyun Zou, Yingze Li, Tianen Liu, Bingsheng He, Weng-Fai Wong

Publicado 2026-05-14

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Qingyun Zou, Yingze Li, Tianen Liu, Bingsheng He, Weng-Fai Wong

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás intentando enseñar a un aprendiz talentoso pero inexperto (una IA de 7 mil millones de parámetros) cómo redactar contratos legales complejos para chips informáticos. Estos contratos se denominan Aserciones SystemVerilog (SVA). Son las reglas que le indican a un chip: "Si esto sucede, entonces eso debe ocurrir dentro de 3 segundos", o "Esta señal nunca debe estar en alto".

Durante mucho tiempo, los expertos pensaron que los mejores modelos de IA ya habían dominado esta tarea, alcanzando una precisión de aproximadamente el 76 %. Sin embargo, los autores de este artículo descubrieron un defecto oculto: la IA era buena pareciendo que conocía las reglas, pero en realidad solo estaba memorizando algunas estructuras de oraciones simples. Cuando se enfrentaba a reglas temporales complejas, "colapsaba" en una plantilla genérica por defecto que parecía correcta pero era legalmente errónea.

A continuación se explica cómo el artículo resuelve este problema, utilizando analogías sencillas:

1. El Problema: Mimetismo vs. Comprensión

La antigua forma de entrenar a estas IAs era como un estudiante copiando el trabajo de un profesor palabra por palabra. El estudiante recibe una calificación basada en qué tan cerca están su ortografía y gramática de la respuesta del profesor.

El Defecto: En este campo, dos oraciones pueden parecer completamente diferentes pero significar exactamente lo mismo (equivalentes). Por el contrario, dos oraciones pueden parecer casi idénticas pero tener significados opuestos. El antiguo método recompensaba al estudiante por copiar las palabras, no por comprender la lógica.

2. La Solución: La "Destilación en Política Ponderada por Recompensa" (RWOPD)

Los autores crearon un nuevo método de entrenamiento llamado RWOPD. Imagínalo como un proceso de entrenamiento de tres pasos que involucra a un Estudiante, un Maestro Profesor y un Juez estricto.

Paso A: El Estudiante Practica (En Política)

En lugar de simplemente copiar al profesor, se le pide a la IA Estudiante que redacte sus propios contratos (llamados "despliegues" o rollouts) basándose en un prompt. Intenta resolver el problema por sí misma primero.

Paso B: El Juez Estricto (El Verificador Abierto de Equivalencia de Propiedades)

Este es el ingrediente secreto del artículo. Los autores construyeron un "Juez" de código abierto (utilizando herramientas llamadas SymbiYosys y Z3) que no solo verifica si la gramática es correcta. Verifica la lógica.

La Analogía: Imagina que el Juez es un abogado que toma el contrato del Estudiante y el contrato de Referencia y los ejecuta en una simulación.
El Veredicto: El Juez pregunta: "¿Son estos dos contratos legalmente equivalentes?"
- Si el contrato del Estudiante es lógicamente equivalente al de referencia, el Juez dice "Aprobado".
- Si es ligeramente más estricto o más permisivo, el Juez otorga un "Aprobado Parcial".
- Si está mal, el Juez dice "Reprobado".
Punto Crucial: El Juez ignora la respuesta del Estudiante si es lógicamente incorrecta. Actúa como un filtro, permitiendo avanzar solo a los intentos "buenos".

Paso C: El Maestro Profesor (Destilación)

Aquí es donde ocurre la magia. El Estudiante no solo aprende de la puntuación "Aprobado/Reprobado" del Juez.

El Maestro Profesor (una IA mucho más grande, de 14 mil millones de parámetros, que ya es muy buena) observa los intentos exitosos del Estudiante.
El Profesor dice: "Bien, has obtenido la lógica correcta. Ahora, mira exactamente cómo yo habría escrito esas palabras específicas. Te mostraré la probabilidad de cada palabra individual que habría elegido".
El Estudiante actualiza entonces su cerebro para igualar el estilo del Profesor, pero solo en los intentos que el Juez aprobó.

¿Por qué es esto mejor?

Antigua Forma: El Estudiante aprende de cada intento, incluso de los malos, tratando de adivinar las palabras correctas.
Nueva Forma (RWOPD): El Estudiante solo aprende de los intentos "ganadores", y aprende la lógica profunda de cómo un Maestro formularía esas respuestas ganadoras. Es como un estudiante que solo estudia los ensayos que ganaron el premio, pero aprendiendo del comentario de un ganador del Premio Nobel sobre por qué esos ensayos eran buenos.

3. Los Resultados: Venciendo a los Gigantes

Los autores probaron este método en un modelo de 7 mil millones de parámetros (el Estudiante).

La Competencia: Lo compararon contra el mejor modelo especializado anterior (una IA de 14 mil millones de parámetros) e incluso contra modelos generales masivos (de 671 mil millones de parámetros).
El Resultado: El pequeño Estudiante de 7B, utilizando este nuevo método de entrenamiento, venció a todos. Logró la mayor precisión en las pruebas de referencia, superando a modelos que son 100 veces más grandes.
La "Brecha Oculta" Corregida: El artículo muestra que el Estudiante mejoró específicamente mucho más en los tipos de reglas más difíciles (aquellos que involucran tiempo y retrasos), que es donde los modelos anteriores fallaban.

Resumen

El artículo argumenta que para enseñar a una IA lógica compleja, no debes simplemente hacerla memorizar respuestas. En su lugar, debes:

Permitirle intentar resolver el problema.
Utilizar un verificador de lógica estricto para filtrar las respuestas incorrectas.
Tener que un Maestro Profesor le muestre al Estudiante exactamente cómo formular las respuestas correctas.

Al combinar un verificador de lógica con un Maestro Profesor, una IA pequeña puede aprender a pensar como un gigante, resolviendo un problema que anteriormente se pensaba que estaba casi "saturado" (resuelto).

Resumen Técnico: Destilación en Política Ponderada por Recompensa para la Generación de NL a SVA

Enunciado del Problema
La generación de Aserciones en SystemVerilog (SVA) a partir de especificaciones en lenguaje natural (NL) utilizando Modelos de Lenguaje Grandes (LLM) ha alcanzado un estancamiento en el rendimiento, con los modelos especializados más potentes (por ejemplo, CodeV-SVA-14B) logrando una precisión aproximada del 76% en la prueba de referencia NL2SVA-Human. Sin embargo, esta puntuación agregada oculta una "brecha temporal" crítica. Mientras que los modelos rinden bien en lógica combinacional (C1), a menudo fallan en especificaciones de retardo acotado (C2) y de vivacidad (C3). El modo de fallo dominante es el "colapso de plantillas", donde los modelos recurren a un conjunto reducido de plantillas de implicación (por ejemplo, |->) independientemente de los requisitos temporales específicos de la especificación.

La causa raíz identificada es el objetivo de entrenamiento. Los sistemas existentes dependen del Ajuste Fino Supervisado (SFT) en pares NL/SVA, lo cual optimiza la imitación a nivel de token de una única aserción de referencia. Este enfoque falla en capturar la naturaleza semántica de la corrección de SVA, donde dos aserciones pueden estar sintácticamente distantes pero ser semánticamente equivalentes, o sintácticamente similares pero semánticamente opuestas. Además, el Aprendizaje por Refuerzo (RL) estándar con retroalimentación de verificadores ha demostrado ser ineficaz en este contexto; las recompensas dispersas a nivel de despliegue no proporcionan una señal suficiente para modelos de parámetros reducidos (7B) con presupuestos de adaptación limitados (LoRA), fallando a menudo en superar la línea base de SFT.

Metodología: Destilación en Política Ponderada por Recompensa (RWOPD)
El artículo propone la Destilación en Política Ponderada por Recompensa (RWOPD), un método que integra un verificador formal en el proceso de destilación para guiar a un modelo estudiante hacia un comportamiento equivalente en propiedades. La tubería consta de cuatro componentes clave:

SFT de Currículo Estratificado: Antes de la destilación, un modelo estudiante de 7B (Qwen2.5-Coder-7B-Instruct) experimenta un SFT basado en currículo. Esta etapa aborda el sesgo hacia clases temporales más fáciles entrenando en tres fases (C1, C2, C3) con un búfer de reproducción para prevenir el olvido catastrófico. Crucialmente, emplea una función de pérdida de entropía cruzada ponderada por tokens de operador, que aumenta el peso de los tokens de operadores temporales (por ejemplo, |->, s_eventually) para asegurar que el modelo aprenda la importancia estructural de estos tokens.
Verificador de Equivalencia de Propiedades Abierto (PEC): Para evitar el coste y la naturaleza de código cerrado de herramientas industriales como Cadence JasperGold durante el entrenamiento, los autores introducen un verificador de código abierto construido sobre SymbiYosys y Z3. Este verificador realiza verificación de modelos acotada (BMC) en los fragmentos C1 y C2. Genera veredictos como EQUIVALENT, IMPLIES_REF_TO_LM, IMPLIES_LM_TO_REF, NOT_EQUIVALENT o UNSUPPORTED (para casos de vivacidad fuera de BMC). El PEC es sólido: cualquier veredicto EQUIVALENT que produzca está garantizado como correcto, aunque puede abstenerse en propiedades de vivacidad complejas.
Bucle de Entrenamiento RWOPD:
- El estudiante muestrea $K$ despliegues para un prompt dado.
- El PEC abierto filtra estos despliegues, descartando aquellos que están rotos sintácticamente o son semánticamente incorrectos (NOT_EQUIVALENT).
- Los despliegues restantes se asignan un peso de recompensa basado en el veredicto del PEC (por ejemplo, 1.0 para EQUIVALENT, 0.6/0.4 para implicaciones unilaterales).
- Un modelo maestro congelado de 14B (CodeV-SVA-14B) proporciona un objetivo denso de divergencia KL (Kullback-Leibler) hacia adelante en los despliegues retenidos.
- El estudiante se actualiza utilizando un promedio ponderado por recompensa de estas pérdidas KL. Esto asegura que la supervisión sea densa a nivel de token pero fundamentada en un comportamiento equivalente en propiedades.
Protocolo de Evaluación: Mientras que el entrenamiento depende del PEC abierto para el filtrado y la configuración de recompensas, la evaluación final utiliza el prop_eq_checker de nivel industrial Cadence JasperGold para garantizar la completitud y la coherencia con las pruebas de referencia anteriores.

Contribuciones Clave

Algoritmo RWOPD: Un método de destilación novedoso que restringe y pondera por recompensa la supervisión densa del maestro utilizando un verificador de equivalencia de propiedades. Esto combina la señal densa a nivel de token de la destilación con la fundamentación semántica de la verificación formal.
PEC Abierto SymbiYosys+Z3: Un verificador sin licencia y sólido para el fragmento de verificación de modelos acotada de SVA. Proporciona una señal de verificación reproducible en segundos para el filtrado durante el entrenamiento, distinguiéndose de los oráculos de código cerrado utilizados en trabajos anteriores.
Estado del Arte Empírico: El método establece nuevos récords en las pruebas de referencia NL2SVA-Human y NL2SVA-Machine.

Resultados
Los autores evaluaron un modelo estudiante de 7B con LoRA (0.53% de parámetros entrenables) frente a modelos especializados de 14B y líneas base de propósito general de 671B.

Rendimiento: RWOPD logró las puntuaciones más altas en pass@1, pass@5 y pass@10 en ambas pruebas de referencia. En NL2SVA-Machine, superó al anterior SOTA especializado (CodeV-SVA-14B) en 2–4 puntos porcentuales (pp) y a los modelos de 671B (DeepSeek-R1, GPT-5) en 4–7 pp en pass@1.
Desglose Temporal: Las ganancias se concentraron en los segmentos temporalmente no triviales. RWOPD mejoró C2 (retardo acotado) en 7.5 pp y C3 (vivacidad) en 11.5 pp sobre el maestro de 14B, mientras que el rendimiento en C1 permaneció saturado.
Estudios de Ablación:
- Destilación vs. RL: La optimización de recompensas dispersas (GRPO, IPO) utilizando la misma señal del PEC no logró superar la línea base de SFT, confirmando que la KL densa del maestro es el principal motor del rendimiento.
- Filtro vs. Maestro: Un SFT de muestreo por rechazo (filtrando despliegues sin el maestro) proporcionó solo ganancias marginales (~2.5 pp), aislando la supervisión densa del maestro como el valor añadido dominante.
- Precisión del Filtro: RWOPD (utilizando tanto EQUIVALENT como implicaciones unilaterales) superó al filtrado estricto solo EQUIVALENT, equilibrando la disponibilidad de gradientes con la corrección semántica.

Significado y Afirmaciones
El artículo afirma que, para el régimen específico de modelos de 7B con adaptación LoRA, el verificador es más efectivo no como una señal de recompensa independiente para RL, sino como un filtro configurado por recompensa para la supervisión densa del maestro. Los autores argumentan que la "brecha temporal oculta" en la generación de NL a SVA no se debe a una falta de datos o tamaño del modelo, sino a la desalineación de los objetivos de entrenamiento (imitación de tokens vs. equivalencia de propiedades). Al fundamentar la señal densa de destilación en la equivalencia formal de propiedades, RWOPD permite que modelos más pequeños y eficientes superen tanto a modelos especializados más grandes como a LLMs masivos de propósito general en la generación de aserciones de hardware semánticamente correctas.

El trabajo se presenta como una "declaración de régimen": a la escala de 7B+LoRA, la combinación de un verificador abierto sólido y un maestro fuerte mediante destilación en política es un uso más efectivo de las señales de verificación que el aprendizaje por refuerzo disperso. Los autores reconocen limitaciones, incluido el mecanismo indirecto para el aprendizaje de C3 (confiando en la semilla del currículo en lugar de la retroalimentación directa del verificador) y la dependencia de JasperGold para la evaluación final debido a la incompletitud del PEC abierto en propiedades de vivacidad.