MathCode 0.2.0リリース、APIコストを90%削減

ME AI ニュース、動察 Beating の監視によると、Math-AI チームは数学的形式と定理証明用 AI アジェント MathCode 0.2.0 をリリースしました。このバージョンは、プレフィックスキャッシュリクエストの整形とポリシー制御により、API コストを最大 90% 削減します。新バージョンは、大規模モデルが長距離証明やマルチラウンドインタラクションで発生する高コストを軽減するため、プロンプト構造の安定性を最適化し、プロンプトキャッシュのヒット率を向上させました。定理証明のシナリオでは、モデルが大規模なコードライブラリと公理ライブラリを頻繁に読み込む必要があります。MathCode 0.2.0 は、プレフィックスキャッシュリクエストの整形診断とポリシー制御（Prefix-cache request-shape diagnostics and policy controls）メカニズムを導入しました。システムはプロンプトの先頭の帰属をブロックして構造の安定性を確保し、複数のブレークポイントキャッシュ `MATHCODE_CACHE_MULTI_BREAKPOINT`、明示的な最小プレフィックスゲートウェイ、およびアイドリング感知 TTL ポリシーを追加しました。これにより、低レベルのリクエスト形状を整列させ、プロバイダーのネイティブキャッシュヒット率を最大化し、長時間セッションの請求額を1割に削減します。新バージョンはタスク管理と思考深度制御も強化しました。長時間実行による予算超過を防ぐため、システムは MATHCODE_GOAL_MAX_TOKEN_BUDGET を使用してトークン予算上限を設定し、ネストされたスラッシュコマンドの上限を制限して無限ループを防止します。また、証明セッションでは --effort や /effort を使用して思考深度を動的に調整でき、low、medium、high、max などのレベルがサポートされ、いつでもデフォルト設定に戻すことができます。コンパイル加速とデプロイ面では、新バージョンは Project Numina が開発したコンパイラ Kimina Lean Server をサブプロセスとして常駐実行できるように対応し、コンパイルチェックリクエストを /verify インターフェースにルーティングします。また、インストールスクリプト setup.sh が再構築され、--status や --clean などのコマンドが追加され、release のチェックサム自動検証とシステム Lean/Lake 環境の再利用が可能になり、デプロイのハードルが低下しました。（出典：BlockBeats）