VeriLoop E2 運営中

VeriLoop E2は、清華大学深圳国際大学院ロボット研究室がオープンソースで公開する27Bのポストトレーニングモデルです。Qwen3.8-27Bを基盤とし、コード・数学・物理推論に対応。Apache-2.0、ネイティブ262Kコンテキストを備えています。VeriLoop E2の中核となるVGRメカニズムは、「モデルによる提案」と「外部検証・永続化」を分離します。保護対象の証拠座標に劣化がなく、かつ少なくとも1項目が厳密に改善された場合にのみ候補状態をコミットし、それ以外はロールバックします。モデル自身が成功を証明することはできません。

オープンソースのポストトレーニングモデル：Qwen3.8-27Bを基盤とする27Bモデルで、Apache-2.0ライセンスの重みとトークナイザーを公開。ネイティブコンテキスト長は262,144 tokensで、vLLM 0.17.0によりOpenAI互換形式で提供できます。
コードとエージェント能力：リポジトリレベルのソフトウェア修正、ターミナル・ツール実行などに対応し、SWE-bench Pro 76.2%、Terminal-Bench 2.1 88.8%、DeepSWE v1.1 64.6%などのスコアを報告しています。
数学・科学推論：競技数学や高難度の科学質問に対応し、AIME 2026 98.3%、ArXivMath 100%、GPQA Diamond 93.9%、Apex 2025 89.6%を報告しています。
証拠閉包型の科学デモンストレーション：リーマンζ零点の割合67.350003708785593%に関する厳密な有限次元証明書、および漸近グラビトン断層撮影のT1–T9フレームワークと、6/6で合格した実行可能な証明書スイートを公開しています。
監査可能なエンジニアリング契約：14項目のGolden Rulesを公開し、長期タスクが有界・テスト可能・追跡可能であることを求めています。成功の偽造、リソース予算の後回し、ローカル規約の上書きを明確に禁止します。
明確な境界：本番版VeriLoop Harness、非公開のオーケストレーション、学習データは含まれていません。科学成果物とモデルライセンスは別であり、結果をリーマン予想やブラックホール情報パラドックスが解決済みであると解釈することはできません。

WeChatで「开源」と返信すると、AIオープンソースプロジェクト交流グループに参加できます。
VGRの全体機構：VeriLoop-Governed Recurrenceは、1回のタスク解決を、保持済み状態を中心とした候補状態の遷移としてモデル化します。モデルは学習済みproposerとして候補潜在変位または候補成果物を生成し、固定decoderがそれを出力に具現化します。外部verifierは固定された契約に基づき、保護対象の証拠ランクを返します。候補ランクが現行ランクを弱支配し、かつ少なくとも1座標で厳密に改善する場合にのみ原子的にコミットします。それ以外では現行bundle全体を保持し、拒否された変位だけを探索メモリに記録します。
保護付き半順序と原子コミット：検証器の契約は、順序付き義務リストO=(o1​,…,om​)とランクベクトルr∈N0m​を定義します。座標が小さいほど残存違反が少ないことを示します。コミット述語χt​=1{rt′​≺P​rt​}は、各座標の非悪化と、少なくとも1座標の厳密な改善を要求します。そのため、集計スコアの改善によって単一点の退行を隠すことはできず、比較不能または退行した候補はすべて拒否されます。コミット単位は、成果物・潜在状態・検証結果・要約を結合したCertifiedBundleです。拒否時にはbundle全体をそのまま保持するため、ロールバックと再実行が保証され、整数ポテンシャルの低下からコミット回数が有限であることが導かれます。
証拠フィードバックと拒否探索：各試行後、証拠コンパイラΓは現行の検証対象を置き換える前に、「現行結果―候補結果―コミット判断」から、ランクの合計や改善・悪化・維持の割合、コミットおよびゼロランク指標など、上限付きでモデルが参照できる特徴量を計算します。これらは次の提案の条件付けにのみ使われ、コミット権限は持ちません。拒否された変位は探索メモリEt​に入り、後続の探索に影響を与えますが、保護済み状態を上書きすることはありません。失敗の軌跡は「情報を持つが永続化されない」形になります。
ポストトレーニングの教師インターフェース：VGRのラベルはタスク単位の状態遷移上で定義されるため、E2は1,841,831件の構造化レコードを用いてポストトレーニングを行います。検証済みの厳密な進展アクションを修正教師とし、コミット不能な候補を比較用の負例とし、ゼロランク成果物を最終生成目標とします。損失はペアワイズ選好ロジスティック項、アクションNLL、生成NLLを重み付けして構成し、QLoRA-4/bfloat16、勾配チェックポイント、能力面ごとのルーティング、protected-core replayを採用します。報告では、これにより学習が「提案分布」を改善すると説明されています。

モデルの取得：Hugging Faceからtsinghua-sigs-robot-lab/VeriLoop-E2を取得し、リポジトリに付属するtokenizer、chat template、設定をそのまま使用します。
環境の準備：Python 3.12.x、PyTorch 2.10.0 + CUDA 12.9、Transformers 4.57.6、Triton 3.6.0をインストールし、python -m pip install "vllm==0.17.0"を実行します。
サービスの起動：VLLM_USE_MODELSCOPE=true vllm serve --served-model-name veriloop-e2 --dtype bfloat16 --model-impl vllm --language-model-only --max-model-len 131072 --max-num-seqs 16 --gpu-memory-utilization 0.92 --generation-config vllm --host 127.0.0.1 --port 8001を実行します。
まずスモークテストを実施：http://127.0.0.1:8001/v1/chat/completionsにtemperature: 0の小さなリクエストを送信し、8001_OKのような応答が返ることを確認してから本番トラフィックに接続します。
OpenAIプロトコルで呼び出す：model="veriloop-e2"を指定して/v1/chat/completionsを使用します。Python側ではOpenAI(base_url="http://127.0.0.1:8001/v1", api_key="EMPTY")でクライアントを作成します。
テンプレートをプロトコルの一部として扱う：重みが変わらなくてもツール使用やシステム動作が変わる可能性があるため、ロールの区切り文字、ツール呼び出し構文、停止の意味、推論履歴の形式を置き換えないでください。
長いコンテキストのリソースを計画する：公開tokenizerのネイティブ上限は262,144 tokensですが、公開検証サービスの長さは131,072 tokensです。より長いウィンドウを使用する場合は、VRAMとKV cacheを自分で評価してください。
モデルとHarnessの権限を区別する：E2は提案、抽象化、診断、修正のみを担当します。証拠の受け入れ、決定論的チェック、コミット・ロールバック、終了、永続化は、独自のverifier/Harnessで実装する必要があります。

生成と検証の分離：モデルは提案、診断、修正のみを担当し、受け入れ、ロールバック、終了、永続化の権限は外部Harnessが独占します。これにより、モデル自身による成功の証明を防ぎます。
退行を防ぐコミットルール：VGRは「保護対象の証拠座標に劣化がなく、かつ少なくとも1項目が厳密に改善された」場合にのみコミットします。集計値が改善しても、単一点の後退を隠すことはできません。
原子的ロールバックと安全な失敗：拒否された候補は完全なCertifiedBundleとして保持され、失敗の軌跡を再利用しながら、検証済み状態を上書きしません。
実際の検証に基づく教師信号：ポストトレーニングでは、厳密な進展、コミット不能な負例、ゼロランクの最終稿から選好/NLL目標を構成します。
高い総合能力：27B規模でコードエージェント、ターミナル実行、数学・科学推論をカバーし、SWE-bench Pro 76.2%、AIME 2026 98.3%、GPQA Diamond 93.9%などの成績を報告しています。
長いコンテキストとオープンサービス：ネイティブ262,144 tokensのコンテキストとApache-2.0の重みを備え、vLLM 0.17.0で検証されたOpenAI互換サービスの利用経路を提供します。
スコアだけでなく監査可能：評価証拠パッケージは、タスクに紐付いた識別情報、出力、ネイティブ実行・評価記録、合否、完全性メタデータを含みます。

Hugging Faceモデルリポジトリ：https://huggingface.co/tsinghua-sigs-robot-lab/VeriLoop-E2
技術論文：https://openreview.net/pdf?id=P6FIQILHwX

リポジトリレベルのコード修正：SWE系タスクでパッチを生成し、退行を診断して、テスト・評価器が保持の可否を判断する用途に使えます。「変更は検証可能でなければならない」保守シナリオに適しています。
ターミナル・ツールエージェント：Terminal-Bench系の環境でコマンドを実行し、ツールを呼び出し、証拠に基づいて次のステップを起動します。合否の証明書によって進行の可否を制御します。
数学推論と競技問題の解答：AIME/ArXivMath系の高難度な導出に対応し、複数回のサンプリング後に外部判定で再現可能な解答を保持します。単発の回答だけを見ることによる偶然の成功を減らします。
科学計算と理論物理の探索：リーマンζ、量子場理論、漸近グラビトンなどの研究において、構成の提案や証明の欠落箇所の特定を支援します。