14 · Verificação de random forests¶

Deste lado, um impasse não conclui nada: nem que a propriedade vale, nem que ela falha. Um modelo implantado é retreinado em vez de corrigido, então não há artefato em que um reparo possa ser aplicado, e uma pergunta indecisa continua indecisa até ser feita sobre uma região mais estreita. Toda resposta sobre florestas traz essa frase, como a ressalva forest_stall_is_not_a_verdict, seja qual for o seu resultado.

A Verificação de Random Forests (Random Forest Verification) verifica uma random forest treinada contra propriedades que você declara: robustez, monotonicidade, equidade e alcançabilidade. Cada uma volta decidida, como um contraexemplo conferido no próprio modelo ou como uma prova de que não existe nenhum na região, ou honestamente indecisa. Este capítulo trata das duas perguntas que ela responde, da região a que cada resposta se refere, de como distinguir um contraexemplo que importa de um que não importa, e de um exemplo resolvido sobre um modelo de crédito público.

O modelo¶

O modelo é lido como é implantado: ONNX-ML (TreeEnsembleClassifier, TreeEnsembleRegressor e o TreeEnsemble do opset 5), ou um dump JSON do Treelite 4.x, distinguidos pelo conteúdo. Um modelo do scikit-learn entra por uma exportação ONNX. Uma construção que nenhum dos leitores aceita, como uma divisão por igualdade, um pré-processamento dentro do grafo ou uma transformação que não é monotônica, é recusada pelo nome em vez de aproximada.

Duas perguntas, dois modos¶

forest: as suas próprias propriedades, por mais difíceis que sejam. Uma tabela declara cada propriedade e a região sobre a qual ela é perguntada, e cada uma volta decidida. Uma região difícil é cortada em duas na característica com mais limiares em aberto, de novo e de novo, e cada pedaço é resolvido com o seu próprio limite de tempo: um contraexemplo em qualquer pedaço é um contraexemplo, e a propriedade só vale onde todo pedaço é refutado.

result = client.verify_forest("credit_rf.onnx", "credit.properties.json", anchors="credit.csv")
for record in result.records:
    print(record["id"], record["status"])          # SAT, UNSAT, or STALL, which concludes nothing
for caveat in result.caveats:
    print(caveat["code"])                          # on every forest response, whatever its result

found = client.enumerate_counterexamples("credit_rf.onnx", "search.json", anchors="credit.csv")
for finding in found.findings:
    print(finding["anchor_class"], "->", finding["class"], finding["plausibility"]["label"])

Propriedade	Vale quando
`robustness`	a decisão é a mesma em toda a região em torno de um registro âncora
`monotonicity`	mover uma característica num sentido nunca faz perder a classe, ou nunca baixa a sua pontuação
`fairness`	mudar só as características protegidas nunca muda a decisão
`reachability`	alguma entrada da região chega a uma classe, ou, para um regressor, a um limite

forest_enumeration: a busca rápida, em torno de registros reais. Muitas perguntas estreitas: toda característica de um registro real fixada, menos uma a três, e essas só podem se mover no sentido que você nomeia, up, down ou any. Com quase tudo fixado, cada pergunta é decidida em milissegundos, e decidida nos dois sentidos: um achado é um contraexemplo conferido, e uma pergunta que se manteve é uma prova de que nenhum movimento desses inverte aquele registro. Só os achados mínimos são listados: uma vez que um conjunto de movimentos inverte um registro, nenhum conjunto maior que o contenha é perguntado. Um único movimento ordenado relata a menor mudança que inverte, encontrada exatamente sobre os próprios limiares do modelo. A enumeração devolve só vereditos, e nenhum certificado.

{
  "enumeration": {
    "anchors": {
      "rows": [
        18
      ]
    },
    "moves": {
      "PAY_1": "down",
      "PAY_AMT6": "up"
    },
    "k": 2,
    "label_column": "Default"
  }
}

anchors é uma lista explícita de rows, ou os registros a que o modelo dá uma classe, na ordem do arquivo ou dos mais próximos da decisão primeiro. k é o máximo de movimentos combinados, de um a três. Um achado é uma proposta: a sua property vem escrita como uma linha que você poderia colar numa tabela, sem expect e sem gate, porque promovê-la é uma decisão de um revisor.

A região é a proposição¶

Uma propriedade de floresta é perguntada sobre uma região: um default de fixed (o próprio valor da âncora) ou free (o domínio inteiro da característica) e, por característica, uma bola, um intervalo ou um conjunto de valores. A região é tanto a pergunta quanto a propriedade, então nada a escolhe por você, e a região que o motor usou viaja com todo veredito como region_effective. Toda resposta sobre florestas traz a ressalva forest_region_is_the_proposition: um veredito é sobre a sua região e sobre nada mais amplo.

Cada característica que se move precisa de um domínio, e domínios inferidos dos dados são recusados até uma pessoa confirmá-los. Limites lidos numa amostra são fatos sobre a amostra. Uma tabela cujo domains_status não é confirmed é recusada antes de entrar na fila, como forest_domains_not_confirmed. Uma tabela que nomeia o digest de outro modelo em model_sha256 também é recusada: uma tabela revisada contra um modelo não é evidência sobre outro.

Plausibilidade e a vizinhança¶

Uma região é uma caixa, então um contraexemplo pode estar num canto que nenhum cliente ocupa. Esse contraexemplo é verdadeiro sobre o modelo e inútil para o seu dono. Todo SAT traz um julgamento de plausibilidade contra os registros que você forneceu como anchors:

o registro real mais próximo, e a sua distância em desvios-padrão;
as características fora da faixa da própria referência;
os pares de características cuja célula conjunta contém o contraexemplo e nenhum registro real;

e um rótulo, supported ou off_support. Nada disso muda o veredito: um UNSAT sobre uma caixa larga vale sobre toda parte realista dela, então só um SAT pode enganar, e o rótulo diz quanto peso ele tem.

A enumeração acrescenta a vizinhança: com que frequência os 25 registros reais mais próximos de um contraexemplo tinham a classe que o modelo lhe dá. Essa é a linha entre um padrão que o modelo aprendeu e uma classificação errada. Um achado cujos vizinhos têm na maioria a classe que o modelo lhe dá é o modelo refletindo os seus dados; um cujos vizinhos na maioria não a têm é o modelo errando sobre as pessoas com quem seria usado.

Um exemplo resolvido¶

O modelo é uma receita pública de inadimplência de crédito, retreinada e fixada: 100 árvores sobre os dados default of credit card clients da UCI, verificadas em torno dos seus 29.601 registros. A linha 18 é um cliente que pagou, e a floresta concorda, com uma probabilidade de inadimplência de 0,464. O seu mês mais recente está um mês atrasado.

A busca pergunta se históricos mais seguros podem levar esse cliente a default: o status do mês mais recente descendo (PAY_1, um atraso menor é mais seguro) e o pagamento de seis meses atrás subindo (PAY_AMT6, um pagamento maior é mais seguro), no máximo dois movimentos juntos. Três perguntas: cada movimento sozinho, e depois o par. Cada movimento sozinho deixa o registro como no_default. Juntos, eles o invertem:

{
  "property": {
    "id": "row18-PAY_1-down-PAY_AMT6-up",
    "kind": "robustness",
    "anchor": {
      "row": 18
    },
    "region": {
      "default": "fixed",
      "PAY_1": {
        "values": [
          -2,
          -1,
          0,
          1
        ]
      },
      "PAY_AMT6": {
        "range": [
          0,
          528666
        ]
      }
    }
  },
  "anchor_class": "no_default",
  "class": "default",
  "change": {
    "PAY_1": [
      1,
      -2
    ],
    "PAY_AMT6": [
      0,
      7
    ]
  },
  "scores": {
    "no_default": 0.4928,
    "default": 0.5072
  },
  "model_verified": true,
  "plausibility": {
    "label": "supported",
    "reference_rows": 29601,
    "nearest": {
      "row": 8062,
      "distance_std": 0.109
    },
    "outside_range": [],
    "empty_pairs": 0,
    "empty_pairs_named": []
  },
  "neighbourhood": {
    "label_column": "Default",
    "k": 25,
    "share_with_predicted_class": 0.24,
    "furthest_std": 1.084
  }
}

O que mudou: o mês mais recente registrado como sem gastos (PAY_1 de 1 para −2) em vez de um mês atrasado, e um pagamento de 7 seis meses atrás (PAY_AMT6 de 0 para 7). Cada um é um histórico mais seguro.
O que o modelo faz: ele passa o cliente para default, com 0,5072, uma mudança de 4,3 pontos. O contraexemplo é conferido de novo no modelo em aritmética exata (model_verified), e o onnxruntime dá a mesma pontuação com quatro casas decimais.
Se isso importa: o ponto é supported, perto de clientes reais, e dos 25 clientes reais mais próximos dele, 24% ficaram inadimplentes. A maioria pagou.

O que é: uma violação verificada da lógica do domínio em torno de um cliente real. A floresta não é monotônica em nenhuma das duas características, e nada no seu treinamento pediu que fosse. Uma equipe que precisa que ela seja tem uma propriedade a acrescentar à sua tabela, e um modelo a retreinar.

O que não é: uma explicação de por que as árvores aprenderam isso. O achado mostra o que o modelo faz; por que ele faz é uma pergunta sobre o treinamento, que a verificação não responde.

Os limites¶

Um impasse não conclui nada, deste lado: nem que a propriedade vale, nem que ela falha. Estreite a região, ou divida a pergunta.
Um UNSAT é a refutação do solver SAT, admitida: correta, e não autocontida. O perfil forest não constrói certificado a menos que você defina certificate_detail: core, e a enumeração não constrói nenhum.
Propriedades de duas cópias sobre regiões largas são difíceis. Equidade e monotonicidade compilam duas cópias da floresta num único circuito e perguntam se duas somas quase iguais caem em lados opostos do limiar, a forma que um solver SAT acha mais difícil. Regiões estreitas se decidem; uma larga é cortada e pode dar impasse.
A busca cobre o que nomeia. Um contraexemplo que precisa de mais de k movimentos, ou de um movimento num sentido que a busca não nomeou, está fora da enumeração, e a sua saída diz isso em enumeration.covers.
Um veredito é sobre a sua região, e os domínios em que ele se apoia são os que uma pessoa confirmou.