🤖 machine learning

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

Este artigo apresenta a Distilação em Política com Pesos de Recompensa (RWOPD), um método de treinamento inovador que aproveita um verificador formal de equivalência de propriedades para orientar um modelo estudante de 7B na geração de Asserções SystemVerilog, alcançando desempenho novo de última geração ao priorizar a correção semântica em vez da imitação em nível de token.

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

Publicado 2026-05-14

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando ensinar um aprendiz talentoso, mas inexperiente (uma IA de 7 bilhões de parâmetros) a escrever contratos legais complexos para chips de computador. Esses contratos são chamados de Aserções SystemVerilog (SVA). Eles são as regras que dizem a um chip: "Se isso acontecer, então aquilo deve acontecer dentro de 3 segundos", ou "Este sinal nunca deve ficar alto".

Por muito tempo, especialistas pensaram que os melhores modelos de IA já haviam dominado essa tarefa, alcançando cerca de 76% de precisão. Mas os autores deste artigo descobriram um defeito oculto: a IA era boa em parecer que conhecia as regras, mas na verdade estava apenas memorizando algumas estruturas de frases simples. Ao enfrentar regras de temporização complexas, ela "entraria em colapso" em um modelo genérico padrão que parecia correto, mas era legalmente errado.

Veja como o artigo resolve esse problema, usando analogias simples:

1. O Problema: Mimetismo vs. Compreensão

A antiga maneira de treinar essas IAs era como um aluno copiando o dever de casa do professor palavra por palavra. O aluno recebe uma nota baseada em quão perto sua ortografia e gramática estão da resposta do professor.

O Defeito: Neste campo, duas frases podem parecer completamente diferentes, mas significar exatamente a mesma coisa (equivalentes). Por outro lado, duas frases podem parecer quase idênticas, mas ter significados opostos. O método antigo recompensava o aluno por copiar as palavras, e não por entender a lógica.

2. A Solução: "Destilação On-Policy Ponderada por Recompensa" (RWOPD)

Os autores criaram um novo método de treinamento chamado RWOPD. Pense nele como um processo de coaching de três etapas envolvendo um Estudante, um Mestre Professor e um Juiz rigoroso.

Etapa A: O Estudante Pratica (On-Policy)

Em vez de apenas copiar o professor, a IA Estudante é solicitada a escrever seus próprios contratos (chamados de "rollouts") com base em um prompt. Ela tenta resolver o problema sozinha primeiro.

Etapa B: O Juiz Rigoroso (O Verificador Aberto de Equivalência de Propriedades)

Este é o segredo do artigo. Os autores construíram um "Juiz" de código aberto (usando ferramentas chamadas SymbiYosys e Z3) que não verifica apenas se a gramática está correta. Ele verifica a lógica.

A Analogia: Imagine que o Juiz é um advogado que pega o contrato do Estudante e o contrato de Referência e os executa em uma simulação.
O Veredito: O Juiz pergunta: "Estes dois contratos são legalmente equivalentes?"
- Se o contrato do Estudante for logicamente equivalente à referência, o Juiz diz "Aprovado".
- Se for ligeiramente mais estrito ou mais flexível, o Juiz dá um "Aprovado Parcial".
- Se estiver errado, o Juiz diz "Reprovado".
Ponto Crucial: O Juiz ignora a resposta do Estudante se ela for logicamente errada. Ele atua como um filtro, permitindo que apenas tentativas "boas" avancem.

Etapa C: O Mestre Professor (Destilação)

É aqui que a mágica acontece. O Estudante não aprende apenas com a pontuação "Aprovado/Reprovado" do Juiz.

O Mestre Professor (uma IA muito maior, de 14 bilhões de parâmetros, que já é muito boa) olha para as tentativas bem-sucedidas do Estudante.
O Professor diz: "Ok, você acertou a lógica. Agora, veja exatamente como eu teria escrito aquelas palavras específicas. Vou mostrar a você a probabilidade de cada palavra que eu teria escolhido."
O Estudante então atualiza seu cérebro para combinar o estilo do Professor, mas apenas nas tentativas que o Juiz aprovou.

Por que isso é melhor?

Antigo Método: O Estudante aprende de todas as tentativas, mesmo as ruins, tentando adivinhar as palavras certas.
Novo Método (RWOPD): O Estudante aprende apenas das tentativas "vencedoras", e aprende a lógica profunda de como um Mestre formularia essas respostas vencedoras. É como um aluno estudar apenas os ensaios que ganharam o prêmio, mas aprendendo com o comentário de um vencedor do Prêmio Nobel sobre por que esses ensaios eram bons.

3. Os Resultados: Derrotando os Gigantes

Os autores testaram este método em um modelo de 7 bilhões de parâmetros (o Estudante).

A Competição: Eles o compararam contra o melhor modelo especializado anterior (uma IA de 14 bilhões de parâmetros) e até mesmo contra modelos gerais massivos (671 bilhões de parâmetros).
O Resultado: O pequeno Estudante de 7B, usando este novo método de coaching, venceu todos. Ele alcançou a maior precisão nos benchmarks, superando modelos 100 vezes maiores.
A "Fenda Oculta" Corrigida: O artigo mostra que o Estudante ficou especificamente muito melhor nos tipos mais difíceis de regras (aqueles envolvendo tempo e atrasos), que é onde os modelos anteriores estavam falhando.

Resumo

O artigo argumenta que, para ensinar a uma IA lógica complexa, você não deve apenas fazê-la memorizar respostas. Em vez disso, você deve:

Deixá-la tentar resolver o problema.
Usar um verificador de lógica rigoroso para filtrar as respostas erradas.
Pedir a um Mestre Professor que mostre ao Estudante exatamente como formular as respostas corretas.

Ao combinar um verificador de lógica com um Mestre Professor, uma IA pequena pode aprender a pensar como um gigante, resolvendo um problema que anteriormente era considerado quase "saturado" (resolvido).

Resumo Técnico: Destilação On-Policy Ponderada por Recompensa para Geração de NL para SVA

Declaração do Problema
A geração de Aserções em SystemVerilog (SVA) a partir de especificações em linguagem natural (NL) usando Modelos de Linguagem de Grande Escala (LLMs) atingiu um platô de desempenho, com os modelos especializados mais fortes (por exemplo, CodeV-SVA-14B) alcançando aproximadamente 76% de precisão no benchmark NL2SVA-Human. No entanto, essa pontuação agregada mascara uma "lacuna temporal" crítica. Embora os modelos performem bem em lógica combinacional (C1), eles frequentemente falham em especificações de atraso limitado (C2) e vivacidade (C3). O modo de falha dominante é o "colapso de template", onde os modelos recorrem a um pequeno conjunto de templates de implicação (por exemplo, |->) independentemente dos requisitos temporais específicos da especificação.

A causa raiz identificada é o objetivo de treinamento. Sistemas existentes dependem de Ajuste Fino Supervisionado (SFT) em pares NL/SVA, que otimiza a imitação em nível de token de uma única asserção de referência. Essa abordagem falha em capturar a natureza semântica da correção de SVA, onde duas asserções podem estar sintaticamente distantes, mas semanticamente equivalentes, ou sintaticamente similares, mas semanticamente opostas. Além disso, o Aprendizado por Reforço (RL) padrão com feedback de verificador provou ser ineficaz neste cenário; recompensas esparsas em nível de rolagem não fornecem sinal suficiente para modelos de parâmetros pequenos (7B) com orçamentos de adaptação limitados (LoRA), frequentemente falhando em superar a linha de base SFT.

Metodologia: Destilação On-Policy Ponderada por Recompensa (RWOPD)
O artigo propõe a Destilação On-Policy Ponderada por Recompensa (RWOPD), um método que integra um verificador formal ao processo de destilação para guiar um modelo estudante em direção a um comportamento equivalente a propriedades. O pipeline consiste em quatro componentes-chave:

SFT de Currículo Estratificado: Antes da destilação, um modelo estudante de 7B (Qwen2.5-Coder-7B-Instruct) passa por um SFT baseado em currículo. Esta etapa aborda o viés em direção a classes temporais mais fáceis, treinando em três estágios (C1, C2, C3) com um buffer de replay para prevenir o esquecimento catastrófico. Crucialmente, emprega uma perda de entropia cruzada ponderada por token de operador, que aumenta o peso dos tokens de operadores temporais (por exemplo, |->, s_eventually) para garantir que o modelo aprenda a importância estrutural desses tokens.
Verificador de Equivalência de Propriedades Aberto (PEC): Para evitar o custo e a natureza de código fechado de ferramentas industriais como o Cadence JasperGold durante o treinamento, os autores introduzem um verificador de código aberto construído sobre SymbiYosys e Z3. Este verificador realiza verificação de modelo limitada (BMC) nos fragmentos C1 e C2. Ele produz vereditos como EQUIVALENT, IMPLIES_REF_TO_LM, IMPLIES_LM_TO_REF, NOT_EQUIVALENT ou UNSUPPORTED (para casos de vivacidade fora do BMC). O PEC é sólido: qualquer veredito EQUIVALENT que ele produz é garantido como correto, embora possa abster-se em propriedades de vivacidade complexas.
Loop de Treinamento RWOPD:
- O estudante amostra $K$ rolagens para um determinado prompt.
- O PEC aberto filtra essas rolagens, descartando aquelas que estão sintaticamente quebradas ou semanticamente incorretas (NOT_EQUIVALENT).
- As rolagens restantes recebem um peso de recompensa baseado no veredito do PEC (por exemplo, 1.0 para EQUIVALENT, 0.6/0.4 para implicações de um lado).
- Um modelo professor congelado de 14B (CodeV-SVA-14B) fornece um alvo denso de divergência forward-KL (Kullback-Leibler) nas rolagens mantidas.
- O estudante é atualizado usando uma média ponderada por recompensa dessas perdas KL. Isso garante que a supervisão seja densa em nível de token, mas fundamentada em comportamento equivalente a propriedades.
Protocolo de Avaliação: Embora o treinamento dependa do PEC aberto para filtragem e modelagem de recompensa, a avaliação final utiliza o prop_eq_checker do nível industrial Cadence JasperGold para garantir completude e consistência com benchmarks anteriores.

Contribuições Principais

Algoritmo RWOPD: Um método de destilação novel que restringe e pondera por recompensa a supervisão densa do professor usando um verificador de equivalência de propriedades. Isso combina o sinal denso em nível de token da destilação com o fundamento semântico da verificação formal.
PEC Aberto SymbiYosys+Z3: Um verificador sólido e sem licença para o fragmento de verificação de modelo limitado de SVA. Ele fornece um sinal de verificação reprodutível, em escala de segundos, para filtragem durante o treinamento, distinguindo-se dos oráculos de código fechado usados em trabalhos anteriores.
Estado da Arte Empírico: O método estabelece novos recordes nos benchmarks NL2SVA-Human e NL2SVA-Machine.

Resultados
Os autores avaliaram um modelo estudante de 7B com LoRA (0,53% de parâmetros treináveis) contra modelos especializados de 14B e bases de referência gerais de 671B.

Desempenho: O RWOPD alcançou as maiores pontuações pass@1, pass@5 e pass@10 em ambos os benchmarks. No NL2SVA-Machine, superou o estado da arte especializado anterior (CodeV-SVA-14B) em 2–4 pontos percentuais (pp) e os modelos de 671B (DeepSeek-R1, GPT-5) em 4–7 pp em pass@1.
Decomposição Temporal: Os ganhos foram concentrados nas fatias temporalmente não triviais. O RWOPD melhorou C2 (atraso limitado) em 7,5 pp e C3 (vivacidade) em 11,5 pp sobre o professor de 14B, enquanto o desempenho C1 permaneceu saturado.
Estudos de Ablação:
- Destilação vs. RL: A otimização de recompensa esparsa (GRPO, IPO) usando o mesmo sinal do PEC falhou em superar a linha de base SFT, confirmando que o KL denso do professor é o principal motor do desempenho.
- Filtro vs. Professor: Um SFT de amostragem por rejeição (filtrando rolagens sem o professor) forneceu apenas ganhos marginais (~2,5 pp), isolando a supervisão densa do professor como o principal valor agregado.
- Precisão do Filtro: O RWOPD (usando tanto EQUIVALENT quanto implicações de um lado) superou a filtragem estrita apenas EQUIVALENT, equilibrando a disponibilidade de gradiente com a correção semântica.

Significado e Alegações
O artigo afirma que, para o regime específico de modelos de 7B com adaptação LoRA, o verificador é mais eficaz não como um sinal de recompensa autônomo para RL, mas como um filtro modelado por recompensa para supervisão densa do professor. Os autores argumentam que a "lacuna temporal oculta" na geração de NL para SVA não se deve à falta de dados ou tamanho do modelo, mas sim ao desalinhamento dos objetivos de treinamento (imitação de token vs. equivalência de propriedade). Ao fundamentar o sinal denso de destilação na equivalência de propriedade formal, o RWOPD permite que modelos menores e eficientes superem tanto modelos especializados maiores quanto LLMs gerais massivos na geração de asserções de hardware semanticamente corretas.

O trabalho é apresentado como uma "declaração de regime": na escala de 7B+LoRA, a combinação de um verificador aberto sólido e um professor forte via destilação on-policy é um uso mais eficaz de sinais de verificação do que o aprendizado por reforço esparsos. Os autores reconhecem limitações, incluindo o mecanismo indireto para aprendizado de C3 (confiando na semente do currículo em vez de feedback direto do verificador) e a dependência do JasperGold para avaliação final devido à incompletude do PEC aberto em propriedades de vivacidade.