私たちが取り組んでいるものです。
Aria Language
量子回路のための小さく読みやすい言語。ひとつのソースで実行、学習、そして OpenQASM 2.0 や機械検証済みの Lean 4 へのエクスポートまで。
Aria を見る →最適化Aria-Opt
MILP / QUBO モデルを Aria で一度書けば、HiGHS、CBC、SCIP、CP-SAT、または自社のシミュレーテッド分岐ソルバーに振り分けます。開発中。主要な商用ソルバーでおなじみのパラメータ名とモデルの意味論をそのまま使えます。
Aria-Opt を見る →ライセンスQuantum Toolkit (Sqetch)
Aria ランタイム上のライセンス製ツールキット: 最適化パス、QML、誤り訂正、Lean 4 と Rocq へのエクスポート、金融ラボ。
ツールキットを見る →応用Finance & Trading
合成 OHLC データ、GBDT・DNN・QNN によるレジーム分類、合成系列でのウォークフォワード・バックテスト。
金融を見る →回路は一度書くだけ。あとは Aria が引き受けます。
- libtorch 不要の純 Rust ランタイム
- OpenQASM または Lean 4 へエクスポート
- オプションの Python バインディングとエディタ対応
次期リリースシミュレーションの高速化と、マルチ QPU エミュレーション: 量子光ネットワークで結ばれた複数の QPU を、ひとつの Aria プログラムからエミュレートします。
circuit Bell() {
qreg q[2]
creg c[2]
apply H on q[0]
apply CX on q[0], q[1]
measure q[0] -> c[0]
measure q[1] -> c[1]
}
$ aria run bell.aria --circuit Bell --statevector
|00> +0.707107+0.000000i
|11> +0.707107+0.000000i量子回路で操れる画像生成器を作りました。
16 個の数値で操る画像生成器です。今はその数値を小さな古典ネットワークが選んでいますが、いずれ量子回路に置き換える計画です。
生成器を見る →仕組みについて書いたもの。
量子信号処理を形式的に：Lean 4 による逆定理
量子信号処理の逆基本定理 — 許容される多項式の組はすべて、ある位相列によって実現される — が、Aria に同梱の Lean 4 証明ツリーで sorry なしに機械検証されています。
→Aria Language読める回路から、機械が検証した定理へ
aria export --lean は、回路とそのアノテーションを Lean 4 の定理に変換します。何がエクスポートされるのか、未完だった証明をどう閉じたのか、証明ツリーがどこにあるのかを紹介します。
→Aria Language信頼できる回路オプティマイザ
Aria は独自のランタイムを同梱しています。その回路オプティマイザは 3 つの小さなパスでゲートを書き換え、各パスはユニットテスト済みで、依拠する自己逆元の恒等式は Lean 4 で証明されています。
→