Compute and Python

Where code runs

Research code runs in isolated CPU containers on AWS Batch. The engine selects a machine size for each run, subject to the payer's plan. Jobs store their outputs in private object storage and report completion through callbacks and polling.

The image includes Python 3.12 and libraries such as NumPy, SciPy, pandas, Matplotlib, scikit-learn, statsmodels, PyTorch for CPU, BoTorch, SymPy, NetworkX, Z3, and python-sat. Runs can request additional PyPI requirements within the service limits. This is CPU compute, not a GPU service.

Parameters, seeds, and outputs

The pre-installed lasques helper provides parameters and a seeded random generator. Store measurable results instead of printing only a 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.")

Use lasques.log_metric for a metric series, save_figure for figures, and save_table for tabular outputs. Checkpoints can be saved and loaded with lasques.checkpoint before a job times out.

Machine sizes

The configured starting size is standard-1. Plan ceilings and earlier run memory use influence later sizing.

Limits, retries, and reuse

A job specification contains at most 100 inline files and 2 MB of code. The service accepts up to 200 output files and 50 MB of outputs; checkpoint storage has the same file and size caps. Plan timeout limits may be lower than the service maximum of 43200 s.

A new attempt uses a fresh container and can restore an earlier checkpoint. An explicitly seeded run can reuse a successful run with identical inputs and code. Reused compute costs zero CPU credits. Reviewer runs, evaluator runs, and preregistered confirmatory runs do not use this cache.

The optimizer and Lean proof checker are separate services. Their internal APIs are described in the repository's docs/compute-services.md; they are not an unrestricted public account API.