Novo artigo! E se você pudesse garantir (usando uma mistura de verificação formal e teoria de PDE) que uma rede neural *sempre* lhe daria a resposta correta, mesmo ao fazer inferências arbitrariamente distantes dos dados de treinamento? Apresentando os BEACONS. Link do arXiv abaixo. (1/15)

Nos anos 90, um excelente trabalho foi realizado por Mhaskar, Pinkus e outros sobre versões *quantitativas* dos aclamados Teoremas de Aproximação Universal para redes neurais: quão precisamente pode uma rede neural rasa com N neurônios ocultos aproximar uma função d-dimensional? (3/15)

Mas esses limites de erro em pior caso dependem crucialmente da suavidade da função que está sendo aproximada (ou seja, o erro em pior caso escala como N^(-n/d), onde n é o número de derivadas contínuas que a função possui). O que apresenta um grande problema para a extrapolação. (4/15)

Como podemos saber alguma coisa sobre a suavidade de uma função, fora do subdomínio em que treinamos? Esta é a razão essencial pela qual não se pode limitar os erros nas aproximações de funções por redes neurais longe do casco convexo dos dados de treinamento. (5/15)

Mas com os BEACONS - Solvers Neurais Composicionais com Erro Bounded - exploramos o fato de que a função que estamos aprendendo não é arbitrária, mas sim a solução de uma PDE (ou sistema de PDEs). Portanto, podemos aplicar técnicas como o método das características... (6/15)

...ou teoremas de regularidade elíptica para prever *a priori* quantas derivadas contínuas devem existir, em qualquer lugar no espaço ou no tempo, mesmo arbitrariamente longe do domínio de treino, explorando a estrutura analítica das PDEs em si. Daí, a parte "Erro Limitado". (7/15)

Mas tais limites rigorosos só são prováveis para redes neurais rasas (com uma única camada oculta). E se quisermos construir uma arquitetura mais profunda e expressiva? É aí que entra a parte "Algebraicamente Componível". Usando ideias da teoria das categorias aplicadas... (8/15)

...mostramos como é possível construir arquiteturas BEACONS mais profundas como composições de arquiteturas mais rasas, de tal forma que os limites de erro permaneçam rigorosamente controlados. Especificamente, "fatorizamos" nossa solução PDE complicada em uma composição de funções mais simples... (9/15)

...de tal forma que os grandes limites nos erros para partes descontínuas da solução são arbitrariamente suprimidos por pequenos limites nos erros para partes suaves e de variação lenta da solução, generalizando efetivamente a teoria dos limitadores de fluxo não lineares. (10/15)

Basta especificar as equações que deseja resolver, além dos hiperparâmetros da rede neural para resolvê-las, e nossa estrutura gera automaticamente código C altamente otimizado para treinar e validar uma arquitetura BEACONS para essas equações e inferir novas soluções. (12/15)

Simultaneamente, gera provas formais de correção para o solucionador clássico subjacente, bem como para o solucionador baseado em rede neural bootstrap, com limites extrapolatórios rigorosos sobre os erros L^infinity no pior caso para soluções suaves e não suaves. (13/15)

Estas provas são representadas como código simbólico Racket e, portanto, são totalmente executáveis (e, portanto, verificáveis por máquina). Para uma variedade de sistemas de equações lineares e não lineares, descobrimos que as arquiteturas BEACONS superam dramaticamente as redes neurais tradicionais. (14/15)

O objetivo é elevar o nível geral de rigor matemático subjacente ao ML científico, colocando os métodos baseados em redes neurais em pé de igualdade com os métodos numéricos clássicos, e garantindo propriedades como conservação, convergência, estabilidade e correção. (15/15)