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

Nos anos 90, um excelente trabalho foi feito por Mhaskar, Pinkus e outros em versões *quantitativas* dos celebrados Teoremas Universais de Aproximação para redes neurais: com que precisão uma rede neural rasa com N neurônios ocultos pode aproximar uma função de dimensão d? (3/15)

Mas esses limites de erro no pior caso dependem todos crucialmente da suavidade da função que está sendo aproximada (ou seja, escalas de erro do pior caso 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 extrapolação. (4/15)

Como poderemos saber algo sobre a suavidade de uma função, fora do subdomínio no qual treinamos? Essa é a razão essencial pela qual não se pode limitar erros em aproximações de redes neurais de funções distantes do invólucro convexo dos dados de treinamento. (5/15)

Mas com os BEACONS - Solucionadores Neurais de Erro Limitado, Algebraicamente Computáveis - exploramos o fato de que a função que estamos aprendendo não é arbitrária, mas sim a solução para uma EDP (ou sistema de EDPs). Então 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 do espaço ou tempo, até mesmo arbitrariamente longe do domínio de treinamento, explorando a estrutura analítica das próprias EDPs. Daí a parte do "Erro Limitado". (15/7)

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 aplicada das categorias... (8/15)

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

... de modo que os grandes limites dos erros para partes descontínuas da solução sejam arbitrariamente suprimidos por pequenos limites nos erros para partes suaves e lentamente variáveis da solução, generalizando efetivamente a teoria dos limitadores de fluxo não lineares. (10/15)

Basta especificar as equações que você quer resolver, além dos hiperparâmetros da rede neural para resolvê-las, e nosso framework gera automaticamente código C altamente otimizado para treinar e validar uma arquitetura BEACONS para essas equações, além de 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 bootstrapped, com limites extrapolatórios rigorosos nos piores casos de erros L^infinito tanto para soluções suaves quanto não suaves. (13/15)

Essas provas são representadas como código simbólico de 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, constatamos 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 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)