计算与 Python

代码运行位置

研究代码在 AWS Batch 上的隔离 CPU 容器中运行。引擎会根据付款人的计划为每次运行选择机型大小。任务将其输出结果存储在私有对象存储中，并通过回调和轮询报告完成情况。

镜像包含 Python 3.12 以及诸如 NumPy、SciPy、pandas、Matplotlib、scikit-learn、statsmodels、PyTorch（用于 CPU、BoTorch、SymPy、NetworkX、Z3）和 python-sat 等库。在服务限制范围内，运行可以请求额外的 PyPI 需求。这是 CPU 计算，而非 GPU 服务。

参数、种子和输出结果

预装的 lasques 助手提供参数和带种子的随机生成器。请存储可测量的结果，而不仅仅是打印结论。

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.")

使用 lasques.log_metric 保存指标序列，使用 save_figure 保存图表，使用 save_table 保存表格输出结果。在任务超时之前，可以使用 lasques.checkpoint 保存和加载检查点。

机型大小

配置的起始大小为 standard-1。计划上限和早前运行的内存使用情况会影响后续的大小选择。

限制、重试与重用

任务规范最多包含 100 个内联文件和 2 MB 代码。服务最多接受 200 个输出文件和 50 MB 的输出结果；检查点存储具有相同的文件和大小上限。计划超时限制可能低于服务最大值 43200 秒。

新的尝试会使用全新的容器，并可以恢复早前的检查点。显式设置种子的运行可以重用具有相同输入和代码的成功运行。重用的计算不消耗 CPU 积分。评审运行、评估运行和预注册的确认运行不使用此缓存。

优化器与 Lean 证明检查器是独立的。它们的内部 API 在仓库的 docs/compute-services.md 中有描述；它们并非不受限制的公共账户 API。