Computação e Python
Execute trabalhos CPU isolados e salve métricas, figuras, tabelas e checkpoints.
Onde o código é executado
O código de pesquisa é executado em contêineres CPU isolados no AWS Batch. O motor seleciona o tamanho da máquina para cada execução, sujeito ao plano do pagador. Os trabalhos armazenam seus Resultados em armazenamento de objetos privado e relatam a conclusão por meio de callbacks e polling.
A imagem inclui Python 3.12 e bibliotecas como NumPy, SciPy, pandas, Matplotlib, scikit-learn, statsmodels, PyTorch para CPU, BoTorch, SymPy, NetworkX, Z3 e python-sat. As execuções podem solicitar requisitos de PyPI adicionais dentro dos limites do serviço. Isso é computação CPU, não um serviço GPU.
Parâmetros, sementes e Resultados
O auxiliar lasques pré-instalado fornece parâmetros e um gerador aleatório com semente. Armazene resultados mensuráveis em vez de imprimir apenas uma conclusão.
import lasques
params = lasques.params()
rng = lasques.rng()
values = rng.normal(size=int(params.get("n", 1000)))
lasques.set_metrics({"mean": float(values.mean())})
lasques.save_json({"seed": lasques.seed()}, "run-info")
lasques.summary("The mean is stored in the run metrics.")Use lasques.log_metric para uma série de métricas, save_figure para figuras e save_table para Resultados tabulares. Checkpoints podem ser salvos e carregados com lasques.checkpoint antes que um trabalho expire.
Tamanhos de máquina
| Máquina | vCPU | Memória | Créditos por minuto |
|---|---|---|---|
basic | 1 | 1024 MiB | 2 |
standard-1 | 1 | 4096 MiB | 3 |
standard-2 | 1 | 6144 MiB | 5 |
standard-3 | 2 | 8192 MiB | 9 |
standard-4 | 4 | 12288 MiB | 16 |
O tamanho inicial configurado é standard-1. Os tetos do plano e o uso de memória de execuções anteriores influenciam o dimensionamento posterior.
Limites, tentativas e reutilização
Uma especificação de trabalho contém no máximo 100 arquivos inline e 2 MB de código. O serviço aceita até 200 arquivos de saída e 50 MB de Resultados; o armazenamento de checkpoints tem os mesmos limites de arquivo e tamanho. Os limites de tempo do plano podem ser menores que o máximo do serviço de 43200 s.
Uma nova tentativa usa um contêiner novo e pode restaurar um checkpoint anterior. Uma execução explicitamente semeada pode reutilizar uma execução bem-sucedida com entradas e código idênticos. O custo de computação reutilizada é de zero créditos CPU. Execuções de revisor, execuções de avaliador e execuções confirmatórias pré-registradas não utilizam este cache.
O otimizador e o verificador de provas Lean são serviços separados. Suas APIs internas são descritas no docs/compute-services.md do repositório; elas não são uma API de conta pública irrestrita.