Calcul et Python
Exécutez des tâches CPU isolées et enregistrez les métriques, les figures, les tableaux et les points de contrôle.
Où le code s'exécute
Le code de recherche s'exécute dans des conteneurs CPU isolés sur AWS Batch. Le moteur sélectionne une taille de machine pour chaque exécution, sous réserve du forfait du payeur. Les tâches stockent leurs Résultats dans un stockage d'objets privé et signalent leur achèvement via des rappels et du polling.
L'image inclut Python 3.12 et des bibliothèques telles que NumPy, SciPy, pandas, Matplotlib, scikit-learn, statsmodels, PyTorch pour CPU, BoTorch, SymPy, NetworkX, Z3, et python-sat. Les exécutions peuvent demander des exigences PyPI supplémentaires dans les limites du service. Il s'agit de calcul CPU, pas d'un service GPU.
Paramètres, graines et Résultats
L'assistant lasques préinstallé fournit des paramètres et un générateur aléatoire avec une graine. Stockez des résultats mesurables au lieu de simplement imprimer une conclusion.
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.")Utilisez lasques.log_metric pour une série de métriques, save_figure pour les figures, et save_table pour les Résultats tabulaires. Les points de contrôle peuvent être sauvegardés et chargés avec lasques.checkpoint avant qu'une tâche n'expire.
Tailles de machine
| Machine | vCPU | Mémoire | Crédits par minute |
|---|---|---|---|
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 taille de départ configurée est standard-1. Les plafonds de forfait et l'utilisation de la mémoire des exécutions précédentes influencent le dimensionnement ultérieur.
Limites, tentatives et réutilisation
Une spécification de tâche contient au maximum 100 fichiers en ligne et 2 MB de code. Le service accepte jusqu'à 200 fichiers de sortie et 50 MB de Résultats ; le stockage des points de contrôle a les mêmes limites de fichiers et de taille. Les limites de délai d'expiration du forfait peuvent être inférieures au maximum du service de 43200 s.
Une nouvelle tentative utilise un conteneur frais et peut restaurer un point de contrôle antérieur. Une exécution explicitement semée peut réutiliser une exécution réussie avec des entrées et un code identiques. La réutilisation du calcul ne coûte aucun CPU crédit. Les exécutions de réviseurs, les exécutions d'évaluateurs et les exécutions de confirmation pré-enregistrées n'utilisent pas ce cache.
L'optimiseur et le vérificateur de preuves Lean sont des services distincts. Leurs API internes sont décrites dans le docs/compute-services.md du dépôt ; ce ne sont pas des API de compte public sans restriction.