Calcolo e Python
Esegui esecuzioni CPU isolate e salva metriche, figure, tabelle e checkpoint.
Dove viene eseguito il codice
Il codice di ricerca viene eseguito in container CPU isolati su AWS Batch. Il motore seleziona una dimensione della macchina per ogni esecuzione, in base al piano dell'utente pagante. Le esecuzioni memorizzano i propri Risultati in uno storage di oggetti privato e segnalano il completamento tramite callback e polling.
L'immagine include Python 3.12 e librerie come NumPy, SciPy, pandas, Matplotlib, scikit-learn, statsmodels, PyTorch per CPU, BoTorch, SymPy, NetworkX, Z3 e python-sat. Le esecuzioni possono richiedere requisiti PyPI aggiuntivi entro i limiti del servizio. Questo è calcolo CPU, non un servizio GPU.
Parametri, seed e Risultati
L'helper lasques preinstallato fornisce parametri e un generatore casuale con seed. Memorizza i risultati misurabili invece di stampare solo una conclusione.
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.")Usa lasques.log_metric per una serie di metriche, save_figure per le figure e save_table per Risultati tabulari. I checkpoint possono essere salvati e caricati con lasques.checkpoint prima che un'esecuzione vada in timeout.
Dimensioni della macchina
| Macchina | vCPU | Memoria | Crediti al 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 |
La dimensione iniziale configurata è standard-1. I limiti del piano e l'uso della memoria delle esecuzioni precedenti influenzano la dimensione successiva.
Limiti, tentativi e riutilizzo
Una specifica di esecuzione contiene al massimo 100 file inline e 2 MB di codice. Il servizio accetta fino a 200 file di output e 50 MB di Risultati; lo storage dei checkpoint ha gli stessi limiti di file e dimensione. I limiti di timeout del piano possono essere inferiori al massimo del servizio di 43200 s.
Un nuovo tentativo utilizza un nuovo container e può ripristinare un checkpoint precedente. Un'esecuzione con seed esplicito può riutilizzare un'esecuzione riuscita con input e codice identici. Il riutilizzo del calcolo costa zero crediti CPU. Le esecuzioni di revisione, le esecuzioni di valutazione e le esecuzioni di conferma preregistrate non utilizzano questa cache.
L'ottimizzatore e il verificatore di prove Lean sono servizi separati. Le loro API interne sono descritte nel docs/compute-services.md del repository; non sono API di un account pubblico senza restrizioni.