S2N-BIGNUM-BENCH 技術サマリー

1. 背景と課題 (Problem)

大規模言語モデル（LLM）を用いた神経記号アプローチは、数学オリンピックやコンペティション形式の定理証明ベンチマーク（例：MiniF2F, PutnamBench）において高い成果を上げています。しかし、これらの成功は「現実のシステム実装」に対する証明構築能力を必ずしも保証するものではありません。

既存のベンチマークは抽象的な数学問題に偏っており、以下の重要なギャップが存在します：

• 実装との乖離: 競争数学はアーキテクチャ状態、エイリアシング、エンディアンなどの低レベルな詳細を扱いませんが、現実の暗号ライブラリやシステムコードの検証にはこれらが不可欠です。
• 検証の難易度: 暗号ライブラリのような低レベルなアセンブリコードの正当性を証明するには、機械語のデコード、実行意味論、および特定の命令セットアーキテクチャ（ISA）に依存した推論が必要です。
• 評価の欠如: 産業レベルの低レベル暗号実装（特に HOL Light 形式で検証済みのもの）を対象とした、機械的に検証可能な証明合成に特化した公開ベンチマークが存在しませんでした。

2. 提案手法とベンチマーク構築 (Methodology)

著者らは、AWS で使用されている暗号ライブラリ「s2n-bignum」から派生した新しいベンチマーク s2n-bignum-bench を提案しました。

2.1 データセットの概要

• ソース: 産業用暗号ライブラリ s2n-bignum（HOL Light で形式検証済み）。
• 規模: 2,284 の証明義務（Proof Obligations）。
• 構成: 各問題は、HOL Light のコンテキスト（setup.ml）と、証明すべきゴール（query.txt）からなる独立したタスクです。元の証明本体は CHEAT TAC（Lean の sorry に相当）で置き換えられており、LLM に証明スクリプトの生成を求めます。
• カテゴリ分類:
  1. Bit-vector lemmas (311 件): ビットベクトルに関する補題。
  2. Program-state lemmas (552 件): プログラム状態に関する補題。
  3. Functional correctness (859 件): 機能正しさの証明（ARM 437 件、x86 422 件）。
  4. Generic (562 件): 上記に分類されない補助的事実。

2.2 評価パイプラインとセキュリティ対策

LLM の回答を厳格かつ安全に評価するためのエンドツーエンドのパイプラインを提供しています。

• オフライン評価: 提出された証明スクリプトを、HOL Light のカーネルで直接実行・検証します。
• 不正防止メカニズム:
  • CHEAT TAC や new_axiom（新しい公理の導入）の使用を検知し、「CHEATING」として却下します。
  • 構文解析器による検証を行い、不正な式や SQL インジェクション類似の複雑な構文を排除します。
  • 公理リスト（axioms()）の前後比較により、無許可の公理追加を検出します。
• 汚染対策: 問題文のタイプ注釈を冗長化して表示する「オブスキュレーション（難読化）」メカニズムを導入し、モデルがトレーニングデータから暗記した定理をそのまま出力するのを防ぎます（※HOL Light のプリンタ/パーサの整合性問題により、全問題で適用は困難ですが、約 70% で機能します）。
• タイムアウト管理: 証明実行時間は問題によって数ミリ秒から数時間まで大きく変動するため、事前のプロファイリングに基づき問題ごとに最適化されたタイムアウトマップ（timeout-map.json）を適用し、計算リソースの無駄遣いと不正な長時間実行を防ぎます。

3. 主要な貢献 (Key Contributions)

1. 初の産業用低レベル暗号アセンブリ向けベンチマーク: HOL Light における機械検証可能な証明合成に焦点を当てた、初の公開ベンチマークです。
2. 再現性の高い評価基盤: 2,284 の問題を独立したアセットとしてパッケージ化し、オフラインで完全再現可能な評価環境を提供します。
3. 堅牢な整合性チェック: 公理の不正追加や不正な構文を検出する仕組みを含み、信頼性の高い評価を可能にします。
4. 現実的な検証ワークフローの模倣: 競争数学ではなく、ISA（命令セットアーキテクチャ）を考慮したビット単位の正確な推論能力を測定します。

4. 結果 (Results)

著者らは、GPT-5.3-Codex をベースラインモデルとして評価を行いました（ゼロショットプロンプト使用）。

• 全体成功率:
  • 中程度の努力モード（Medium-effort）: 4.4% (101/2,284)
  • 高度な努力モード（High-effort）: 5.3% (121/2,284)
• カテゴリ別傾向:
  • 成功は主に「Generic」カテゴリ（約 11-12%）と「Bit-vector」カテゴリ（約 8-9%）に集中しています。
  • 「Functional correctness」（ARM/x86 の機能正しさ）のカテゴリでは、両モードとも 0.0% の成功率でした。これは、低レベルアセンブリコードの複雑な推論が現在の LLM にとって極めて困難であることを示唆しています。
• 構文エラー: 提出された回答の多くが HOL Light の構文エラーで却下されており、証明スクリプトの生成自体が大きなボトルネックとなっています。

5. 意義と将来展望 (Significance)

• 実用的な評価指標の確立: 数学的な推論能力だけでなく、現実のセキュリティクリティカルなシステム（暗号ライブラリなど）の低レベル実装を正しく検証できる能力を評価する新たな基準を提供します。
• 神経定理証明（NTP）の次のステップ: 競争数学から、実際のソフトウェア検証やリポジトリ規模の証明合成へと研究の焦点をシフトさせる契機となります。
• 将来の拡張: 現在のベンチマークは機能的正しさに焦点を当てていますが、将来的には「定時間性（constant-time discipline）」や「最適化済みルーチンと検証用ルーチンの等価性」などの関係性プロパティの証明へと拡張する道筋を示しています。

このベンチマークは、LLM が現実世界の低レベルコードの正当性を証明できるかどうかを厳密に検証するための重要なテストベッドとして機能します。