コンピューティングおよび 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 個のインラインファイルと MB 2 のコードが含まれます。本サービスは、最大 200 個の出力ファイルと 50 MB の出力を受け付けます。チェックポイントストレージにも同様のファイル数およびサイズ制限があります。プランのタイムアウト制限は、サービスの最大値である 43200 秒よりも低い場合があります。

新しい試行では新しいコンテナを使用し、以前のチェックポイントを復元できます。明示的にシードされた実行は、同一の入力とコードを持つ成功した実行を再利用できます。再利用されたコンピューティングには CPU クレジットはかかりません。レビュアー実行、エバリュエーター実行、および事前登録された確認実行では、このキャッシュは使用されません。

オプティマイザーと Lean 証明チェッカーは、別のサービスです。それらの内部 API はリポジトリの docs/compute-services.md に記載されています。これらは無制限の公開アカウント API ではありません。