sahibzada-allahyar/Formal-Verification-RSI

解決する課題

AIが作成した証明は有効に見えても偽物であることがよくあります。Leanのようなツールは sorry を警告付きで受け入れ、Dafnyは assume {:axiom} false をエラーゼロとして受け入れます。また、インスタンスのシャドウイングを通じて定理のテキストをバイト単位で同一に保ちながら意味を変えることも可能です。既存のベンチマークチェックではこれらの不正を見逃してしまいます。Millennium Harnessは、ファイルがコンパイルされるだけでなく、凍結された仕様が元の意味を保持し、エスケープハッチなしで証明されたことを検証することで、そのギャップを埋めます。レッドチームがテストした96件の不正をすべて拒否し、25件の誠実な解決策をすべて受け入れました。

仕組み

Lean – このハーネスはステートメントとテストを凍結し、精緻化後のコンパイル環境を検査します。ステートメントの等価性をチェックし、公理をホワイトリストと照合し、凍結された宣言に到達するインスタンスや表記を監視し、コンパイル済みコードの入れ替え（implemented_by/extern）を検出し、精緻化時のコード実行を防ぎ、カーネル検証をリプレイします。

Dafny – 凍結された仕様がそれ自体で変更されずに解決されることを要求し、assume、{:axiom}、ensures を持つ本体のない補題、許可されていない属性やキャプチャされた仕様ヘルパーを拒否し、dafny audit とコンパイルチェックを実行します。

エージェントループ – AIエージェント（OpenCodeまたはClaude Code）で使用する場合、エージェントが停止した後にゲートが実行されます。判定が PROVED でない場合、失敗のフィードバックが次のプロンプトとなるため、エージェントは証明が真に認定されるまで試行を続ける必要があります。

再帰的自己改善 – Millennium RSIはハーネス自体をデータ（戦略および補題ライブラリ）として扱います。提案された補題は、それ自体でコンパイルされ、禁止された構成を使用せず、Leanの標準公理のみに依存する場合にのみ承認されます。子ハーネスは変更されていないステートメントの証明のみをスコアリングするため、報酬を操作（sorryを隠す、定理を編集する、≤を再定義するなど）しても何も得られません。

対象読者

• 機械チェックされた数学や形式検証済みコードを生成するAIシステムを構築する研究者およびエンジニア。
• 操作できない報酬を必要とする再帰的自己改善に取り組むチーム。
• 公開されたAI作成証明の正確性を監査するすべての人。

ハイライト

• 0/96のレッドチームによる不正を拒否 – すべての偽の証明を拒否し、25件の誠実な解決策をすべて受け入れました。
• 4,219件の公開AI解決策の監査 – LeanとDafnyにおける69件の確認された偽物をすべて拒否。120件の受け入れ済みファイルのランダム監査において、誤判定率は0.2%で、見逃しはゼロでした。
• エージェント研究 – 93のタスクでOpenCode + GLM-5.3 Flashを使用した場合、誠実な証明率は41%（標準の終了コード報酬）から、ハーネス使用時には56%に上昇しました。
• 毒性耐性ライブラリ – すべての補題は承認前にカーネルチェックされるため、ライブラリが密かに破損することはありません。
• 不変の報酬 – 子は、変更されていないステートメントの保持された証明をより多く認定した場合にのみ改善します。
• アブレーション機能内蔵 – --reward exit0 は、通常の終了コード基準で同じループを実行し、受け入れられた証明のうちどれだけが偽物かを測定します。
• MITライセンス – オープンソースで自己完結型。Python 3.10+ および固定されたLean/Dafnyツールチェーンを使用。