Resumo Técnico: Leis de Escala Saturadas para Descoberta Equacional

Declaração do Problema

O artigo investiga se sistemas determinísticos de descoberta simbólica — especificamente aqueles que crescem pela adição de regras de reescrita equacional — obedecem a leis de escala empíricas análogas às encontradas em grandes modelos de linguagem (LLMs). Embora as leis de escala para modelos neurais (Kaplan et al., 2020; Hoffmann et al., 2022) estejam bem estabelecidas, permanece uma questão em aberto se substratos determinísticos, como os utilizados em programação lógica indutiva, saturação de igualdade e síntese de programas, seguem dinâmicas de crescimento comparáveis. Os autores visam caracterizar a fenomenologia do crescimento nesses sistemas, testando se uma simples lei de potência ou uma função saturada mais complexa descreve melhor a acumulação de regras descobertas ao longo do tempo.

Metodologia

O estudo emprega um quadro experimental controlado envolvendo três substratos determinísticos "de brinquedo" de complexidade de tipagem crescente:

1. Aritmética (arith): Identidades equacionais sobre uma gramática tipada com adição, multiplicação e variáveis livres.
2. Booleana (bool): Identidades sobre operadores lógicos (and, or, not).
3. Lista de Alta Ordem (list): Um domínio inspirado no DreamCoder com primitivas como map, fold e cons.

O Loop de Descoberta:
O sistema faz crescer um substrato $S$ (um conjunto de regras de reescrita) em passos discretos $t$. Em cada passo:

• Um gerador propõe equações candidatas com base no estado atual de $S$ (usando estratégias como aleatória, composicional, ponderada por frequência ou MDL-greedy).
• Os candidatos são testados quanto à correção semântica via instanciação aleatória.
• Pares aceitos são generalizados (substituindo variáveis livres por variáveis de padrão).
• Um filtro de aceitação configurável (seja "qualquer" ou "novidade") determina se a regra é comprometida com $S$.

Coleta de Dados:
Os autores geraram 592 trajetórias de descoberta independentes nesses substratos, variando cinco características arquitetônicas: tipo de gerador, rigor do filtro, profundidade de recursão, tamanho do lote e semente aleatória. Eles mediram a contagem total de regras $|S(t)|$ ao longo do tempo.

Abordagem de Modelagem:
Os autores propõem um modelo heurístico de fechamento de campo médio derivado de suposições de cobertura uniforme e independência aproximada. Isso produz uma equação diferencial para o crescimento:
$$\frac{dN}{dt} = K \cdot N^k \cdot e^{-\mu N}$$
onde $N$ é o tamanho do substrato, $k$ relaciona-se à profundidade de recombinação do gerador e $\mu$ representa a fração de cobertura do espaço de candidatos.

• Curto alcance ($\mu N \ll 1$): A equação aproxima-se de uma lei de potência pura $N(t) \propto t^b$, onde $b = 1/(1-k)$.
• Longo alcance ($\mu N \gtrsim 1$): O termo exponencial induz saturação, modelado por uma forma de lei de potência logística.

O estudo ajusta três modelos candidatos (lei de potência pura, exponencial esticada, lei de potência saturada) aos dados usando o Critério de Informação de Akaike (AIC) para seleção de modelos e regressão com gradiente impulsionado para prever o expoente $b$ a partir das características arquitetônicas.

Principais Contribuições e Resultados

1. Dinâmicas de Lei de Potência de Curto Alcance

Através de 592 trajetórias, o crescimento do tamanho do substrato $|S(t)|$ em curtos alcances (até 30 épocas) ajusta-se consistentemente a uma forma de lei de potência $t^b$. O expoente $b$ varia continuamente entre 0 e 1,15 dependendo do domínio e da arquitetura.

• Sensibilidade Arquitetural: Dentro de um único substrato, o expoente $b$ é altamente sensível a escolhas arquitetônicas. Um regressor com gradiente impulsionado usando cinco características arquitetônicas prevê $b$ com um $R^2$ validado cruzadamente $\approx 0,82$ tanto para domínios aritméticos/booleanos quanto para listas.
• Falha de Transferência entre Substratos: Um modelo treinado para prever $b$ em dados aritméticos e booleanos falha completamente quando aplicado ao domínio de listas ($R^2 \approx -0,84$). A arquitetura ótima para crescimento composto em substratos de tipagem plana (por exemplo, filtros de novidade) suprime o crescimento em substratos de tipagem de alta ordem. Isso indica que as dinâmicas de crescimento são condicionais ao substrato, não universais.

2. Hipótese de Saturação de Longo Alcance

Os autores testaram se o crescimento eventualmente satura conforme previsto por seu modelo de fechamento.

• Dados de Brinquedo (Domínio de Listas): Estendendo cinco trajetórias do domínio de listas para 500 épocas, o modelo de lei de potência saturada vence comparações de AIC intra-amostral para trajetórias com mais de 200 épocas. No entanto, a previsão fora da amostra (ajustando nos primeiros 100 épocas e prevendo as próximas 400) é vencida pela lei de potência pura em todos os 5 casos. Os autores concluem que as trajetórias de brinquedo não atingem realmente o regime de saturação dentro de 500 épocas; a preferência do modelo saturado intra-amostral é provavelmente um artefato de ajuste que extrapola mal.
• Dados do Mundo Real (Mathlib4): A análise das adições mensais de novos arquivos .lean na biblioteca Mathlib4 (60 meses, 9.701 arquivos) apoia a forma saturada. O modelo saturado supera a lei de potência pura na previsão fora da amostra por um fator de $\sim 7\times$ (RMSE 3.279 vs 23.896), sugerindo que o Mathlib4 atingiu um regime de saturação.
• Dados do Mundo Real (Coq Mathcomp): A análise dos commits mensais na biblioteca Coq Mathcomp (129 meses) favorece a lei de potência pura. O parâmetro de saturação $\mu$ colapsa para zero, e a lei de potência pura supera o modelo saturado na previsão fora da amostra por $\sim 67\times$. Isso sugere que o Mathcomp ainda não atingiu um regime de saturação.

3. Enquadramento Fenomenológico

O artigo propõe um enquadramento de trabalho: "Crescimento de lei de potência saturada com $(k, \mu)$ condicional ao substrato, observável quando o substrato atingiu seu regime de saturação." As dinâmicas são condicionais em dois níveis:

1. Parâmetros arquitetônicos que preveem o expoente de crescimento não transferem-se entre diferentes tipos de substrato.
2. A família funcional que descreve o crescimento (lei de potência pura vs. saturada) depende do estágio específico do ciclo de vida do substrato.

Significado e Alegações

O artigo posiciona-se como uma primeira investigação empírica e teórica sobre as leis de escala da descoberta equacional determinística, oferecendo uma fenomenologia em vez de uma teoria definitiva.

• Escopo Modesto: Os autores afirmam explicitamente que a evidência é limitada a três substratos de brinquedo e dois proxies do mundo real (que são grosseiros, baseando-se em contagens de commits/arquivos). Eles reconhecem que os resultados de longo alcance de brinquedo são "consistentes com, não confirmados" devido à falha da previsão fora da amostra nos dados de brinquedo.
• Insight Chave: A principal descoberta é que as dinâmicas de descoberta simbólica são condicionais ao substrato. Diferentemente das leis de escala neurais que frequentemente assumem universalidade entre arquiteturas, o comportamento de crescimento aqui depende pesadamente da "geometria de fechamento" específica (parâmetro de cobertura $\mu$) do sistema de tipos do substrato.
• Direções Futuras: Os autores identificam três melhorias concretas necessárias para elevar este trabalho de "fenomenologia de brinquedo" a um "fenômeno genuíno":
  1. Replicação em um substrato não de brinquedo com granularidade ao nível de trajetória (não apenas contagens de commits).
  2. Previsão preditiva bem-sucedida fora da amostra para o modelo saturado.
  3. Uma derivação teórica do parâmetro de saturação $\mu$ a partir da combinatória do substrato (por exemplo, entropia de tipos) para tornar a transferência entre substratos falseável.

O artigo conclui que, embora o quadro de lei de potência saturada seja consistente com os dados observados em regimes onde a saturação é plausível, não é uma lei universal para todos os sistemas de descoberta simbólica. O trabalho serve como ponto de partida para uma potencial "mecânica estatística da descoberta simbólica".