2025-11-22T16:49:15.454007

Towards Autoformalization of LLM-generated Outputs for Requirement Verification

Gupte, S
Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models (LLMs). While LLMs show promise in generating structured outputs from natural language (NL), such as Gherkin Scenarios from NL feature requirements, there's currently no formal method to verify if these outputs are accurate. This paper takes a preliminary step toward addressing this gap by exploring the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements. We conducted two distinct experiments. In the first one, the autoformalizer successfully identified that two differently-worded NL requirements were logically equivalent, demonstrating the pipeline's potential for consistency checks. In the second, the autoformalizer was used to identify a logical inconsistency between a given NL requirement and an LLM-generated output, highlighting its utility as a formal verification tool. Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs, laying a crucial foundation for future, more extensive studies into this novel application.
academic

LLM生成出力の要件検証に向けた自動形式化

基本情報

  • 論文ID: 2511.11829
  • タイトル: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
  • 著者: Mihir Gupte, Ramesh S. (General Motors)
  • 分類: cs.CL, cs.AI, cs.FL, cs.LO
  • 発表日: 2025年11月18日（arXiv プレプリント）
  • 論文リンク: https://arxiv.org/abs/2511.11829

概要

本論文は、自動形式化（Autoformalization）技術を用いて大規模言語モデル（LLM）の生成出力を検証する可行性を探索している。LLMが自然言語要件を構造化出力（Gherkinシナリオなど）に変換する際の潜在性が示されている一方で、これらの出力の正確性を形式的に検証することが重要な課題となっている。研究チームは2つの実験グループを実施した：第1グループでは、異なる表現の自然言語要件が論理的に等価であることを成功裏に識別し、第2グループではLLM生成出力と元の要件の間の論理的矛盾を識別した。研究の範囲は限定的であるが、結果は自動形式化がLLM生成出力の忠実性と論理的一貫性を確保する上で顕著な可能性を有することを示唆している。

研究背景と動機

1. 核心的問題

LLMの応用が普及するにつれ、特にテストシナリオの自動生成などの工学的タスクにおいて、重要な課題が生じている：LLM生成出力が元の自然言語要件を正確に反映しているかどうかを検証するための形式的方法の欠如。例えば、「車速≥10かつシートベルト未装着時にシートベルト警告を開始する」という要件からGherkinシナリオを生成した後、生成内容の論理的正確性を保証することができない。

2. 問題の重要性

自動車工学などの安全関連領域では、要件検証が極めて重要である。誤った要件変換は以下をもたらす可能性がある：

  • テストケースの不完全性または誤り
  • システム動作と期待値の不一致
  • 潜在的な安全上の危険

3. 既存方法の限界

  • 従来の形式化方法：主に数学定理証明に適用され、工学要件検証への応用が不足している
  • LLM評価方法：人工検査またはヒューリスティック方法に依存し、厳密な論理検証が不足している
  • 自動形式化研究：主にデータセット構築とモデル訓練に焦点を当て、実際の工学応用への関心が少ない

4. 研究動機

本論文は、自動形式化技術をLLM出力検証という新しいシナリオに適用することを提案し、自然言語要件とLLM生成出力の両方を形式論理表現（Lean 4）に変換し、定理証明器を利用して論理等価性を検証する。

核心的貢献

  1. LLM生成出力検証のための初の自動形式化パイプラインを提案：自然言語要件とLLM出力をLean 4形式化表現に変換し、双条件等価証明により論理的一貫性を検証する
  2. 2つの具体的応用シナリオを検証：
    • 異なる表現の自然言語要件の論理等価性を識別
    • LLM生成出力と元の要件の論理的矛盾を検出
  3. 重要な技術的課題を識別：
    • 変数接地（variable grounding）の必要性と自動化の困難さ
    • LLMの非決定性が形式化に与える影響
    • 自然言語の曖昧性の処理
  4. 将来の研究方向を提案：信頼できるLLM出力検証フレームワークの構築に基礎を提供する

方法の詳細説明

タスク定義

入力：

  • 論理関係を検証する必要がある陳述のペア（S₁, S₂）：
    • 2つの自然言語要件
    • 1つの自然言語要件と1つのLLM生成Gherkinシナリオ

出力：

  • 論理等価性判定：等価（S₁ ↔ S₂を証明可能）または非等価（証明失敗）

制約条件：

  • 陳述は命題論理に形式化可能である必要がある
  • 変数接地のためにシステムコンテキスト情報が必要

モデルアーキテクチャ

全体的なパイプラインは4つの重要なステップを含む（図9参照）：

ステップ1：自動形式化

**DeepSeek-Prover-v2（7Bモデル）**を使用して自然言語陳述をLean 4命題に変換：

-- 例：要件R1の形式化
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

プロンプトテンプレート（付録A.1参照）：

  • Lean 4のdefステートメント生成を明確に要求
  • 命題論理（Prop型）の使用を指定
  • 条件を含意関係（A ∧ B → C）として表現することを要求

ステップ2：変数接地（Variable Grounding）

現在の実装：異なる形式化で同じ概念を指す変数を手動で識別し統一

問題例：

  • R1のvehicle_speed_avgとR2のmean_vehicle_speedは同じ物理量を指す
  • Leanコンパイラにこの等価性を明確に伝える必要がある
-- 手動接地の例
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

ステップ3：双条件等価定理の構築

論理等価性を検証するための形式化定理を構築：

theorem req1_eq_req2 
  (h_grounding : <変数接地仮説>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <証明プロセス>

ステップ4：自動定理証明

DeepSeek-Prover-v2を再度使用してLean証明コードを生成：

  • 証明成功 → 2つの陳述は論理的に等価
  • 証明失敗 → 論理的矛盾が存在

技術的革新点

  1. 分野横断的応用の革新：数学定理証明領域の自動形式化技術をソフトウェア工学要件検証に初めて適用
  2. 二層LLM使用：
    • 第1層：形式化翻訳（自然言語 → Lean）
    • 第2層：定理証明（等価性検証）
  3. 失敗ベースの検証メカニズム：定理証明器の失敗を論理的矛盾の指示器として利用する革新的な負の検証方法
  4. 変数接地の識別：変数接地が自動形式化パイプラインに不可欠なステップであることを明確に提案し、これまでの研究では十分に強調されていなかった

実験設定

データセット

実験1：要件等価性検証

  • R1: "If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime"
  • R2: "If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt"

実験2：LLM出力検証

  • R3: "When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE."
  • G3: LLM生成Gherkinシナリオ（4つの例行を含み、seat_occupancyなどの追加変数を導入）

評価指標

定性指標：

  • Lean 4コンパイル成功/失敗
  • 定理証明成功/失敗

検証基準：

  • 論理等価：定理PA ↔ PBが証明可能
  • 論理的矛盾：定理証明失敗またはLeanコードがコンパイル不可

実装の詳細

モデル選択：

  • DeepSeek-Prover-v2 (7B)
  • 選択理由：
    1. Lean 4で訓練されている
    2. 自然言語理解能力を備えている
    3. 部分目標分解戦略を採用している

形式化言語：Lean 4

  • 強力な定理証明能力
  • 正確な論理表現
  • DeepSeek-Prover-v2との互換性

手動介入：

  • 変数接地ステップは完全に手動
  • 形式化出力の検証はLeanコンパイラに依存

実験結果

主要な結果

実験1：要件等価性検証（成功事例）

形式化出力：

  • R1とR2は正常にLean命題に変換された（図3、図4）
  • 変数マッピングが手動で確立された：
    • vehicle_speed_avg ≡ mean_vehicle_speed
    • seatbelt_active ≡ seatbelt_plugged_in

検証結果（図5）：

  • ✅ Leanコンパイル成功
  • ✅ 定理req1_eq_req2証明成功
  • 結論：R1とR2は論理的に等価

意義：パイプラインが意味的に同一だが表現が異なる要件を識別できることを証明し、要件一貫性チェックに役立つ。

実験2：LLM出力検証（失敗事例）

形式化出力：

  • R3：シンプルな命題、シートベルト状態変化条件のみを含む（図6）
  • G3：複雑な命題、追加変数を含む（seat_occupancy, initial_seatbelt_status）（図7）

重要な発見：

  • G3はR3に言及されていない変数を導入している
  • 論理構造がより複雑（4つのシナリオ例を含む）

検証結果（図8）：

  • ❌ Leanコードのコンパイル失敗または証明失敗
  • 結論：G3とR3は論理的に矛盾している

意義：LLM生成出力の「過剰生成」問題を成功裏に検出—元の要件に存在しない制約条件を追加している。

ケース分析

ケース：曖昧性の問題（R4）

要件：

"When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE."

問題：「vehicle in motion」の形式化に曖昧性が存在

2つの可能な形式化（図10）：

  1. pass@1: ブール変数 vehicle_in_motion : Bool
  2. pass@2: 数値変数 vehicle_speed > 0

分析：

  • 両方の形式化はシステム意味論的に正しい可能性がある
  • しかし形式論理上では等価ではない（異なる型）
  • 自然言語の曖昧性が形式化に与える影響を強調している

実験的発見

  1. 形式化は解釈可能性に依存：LLMの非決定性により、同じ要件が異なるが「合理的な」形式化表現を生成する可能性がある
  2. 変数接地がボトルネック：
    • 最も時間を要するステップ
    • システムドメイン知識が必要
    • 現在は手動でのみ実行可能
  3. システムコンテキストが極めて重要：明確なシステム定義（データ辞書など）の欠如は形式化の不一貫性をもたらす
  4. 負の検証が有効：証明失敗は論理的矛盾を効果的に指示できる

関連研究

自動形式化のデータセット構築

  • ProofNet：学部レベルの数学の自動形式化
  • MiniF2F：オリンピック級数学ベンチマーク
  • 多言語データセット：Lean、Isabelle、Coqの組み合わせ訓練がパフォーマンスを向上

LLM訓練戦略

  • 「ドラフト-スケッチ-証明」方法（Jiang et al.）：証明アウトラインを生成して形式化をガイド
  • 部分目標分解：DeepSeek-Proverが採用する再帰的探索戦略
  • 強化学習：定理証明成功率を向上

非決定性への対応

  • シンボル等価フレームワーク：pass@1とpass@kの差異を処理
  • RAG方法：正確な形式定義を検索してコンテキストを提供

応用領域の拡張

  • 数学問題解法：高校から学部レベルの数学
  • コード検証：プログラム正確性検証
  • 生物医学：事実検証

本論文の貢献：自動形式化を工学要件検証とLLM出力検証に初めて適用し、新しい応用方向を開拓した。

結論と議論

主要な結論

  1. 可行性の検証：自動形式化パイプラインはLLM生成出力と元の要件の論理的一貫性を効果的に検証できる
  2. 二重の応用価値：
    • 要件一貫性チェック（等価要件の識別）
    • LLM出力品質管理（論理エラーの検出）
  3. 概念実証：サンプルは限定的であるが、定理証明技術をソフトウェア工学に適用する可能性を成功裏に実証した

限界

  1. 規模の制限：
    • わずか3つの要件ペアのテスト
    • 大規模評価の欠如
    • 統計的有意性分析なし
  2. 手動依存：
    • 変数接地は完全に手動
    • 時間がかかり誤りやすい
    • スケーラビリティを制限
  3. モデルの制限：
    • 7Bモデルを使用（リソース制限）
    • より大きなモデル（671B）がより良いパフォーマンスを示す可能性
    • 形式化品質はモデル能力に依存
  4. 曖昧性が未解決：
    • 自然言語の固有の曖昧性
    • システム本体論のサポート欠如
    • 複数の「正しい」が等価でない形式化を生成する可能性
  5. ドメイン特異性：
    • 実験は自動車安全要件に限定
    • 汎化能力が不明

将来の方向

論文は3つの重要な研究質問（RQ）を提案している：

RQ1：最適な形式化方法

  • k-pass戦略の探索（複数の形式化を生成し、最も可能性の高いものを選択）
  • 単一変換と複数サンプリングの正確性の比較

RQ2：変数接地の自動化

  • 方法1：コンテキスト単一形式化（単一呼び出しで全陳述を処理）
  • 方法2：類似度ベースの接地（埋め込みを使用してシステム本体にマッチング）
  • 課題：LLMの接地仮説自体の正確性をどのように検証するか

RQ3：制約システムにおけるLLM検証

  • システムアクションの知識グラフを構築
  • LLMトラバーサルメカニズムを開発
  • 自動形式化を使用して出力の論理的一貫性を保証
  • 応用シナリオ：スマートホーム、車載アシスタントなど限定されたアクション空間を持つシステム

その他の方向：

  • 自動変数正規化技術の開発
  • ドメイン特異的本体論の統合（自動車システムデータ辞書など）
  • より複雑な論理表現への拡張（時間論理など）

深度評価

長所

  1. 問題定義が新規：
    • 自動形式化をLLM出力検証に初めて体系的に適用
    • 工学実践における実際の痛点を解決
    • 新しい研究方向を開拓
  2. 方法論が明確：
    • パイプライン設計が簡潔明瞭
    • 成熟したツール（Lean 4、DeepSeek-Prover）を活用
    • 再現性が強い
  3. 問題識別が深い：
    • 変数接地の重要性を明確に指摘
    • 曖昧性問題を深く分析
    • LLM非決定性の影響を誠実に議論
  4. 実用価値が高い：
    • 安全関連領域（自動車工学）を対象
    • 要件工学プロセスに直接適用可能
    • LLM応用の信頼性向上に貢献
  5. 執筆品質が優秀：
    • 構造が明確で論理が厳密
    • 詳細なプロンプトテンプレートを提供（付録）
    • 図表が豊富で理解しやすい

不足

  1. 実験規模が極めて不十分：
    • わずか3サンプル：統計学的結論を導き出せない
    • 異なるドメイン、異なる複雑度の要件テストの欠如
    • より大規模なデータセット上でのパフォーマンス評価なし
    • 推奨：最低50～100の要件ペアで十分な評価が必要
  2. 定量評価の欠如：
    • 精度、再現率などの指標がない
    • 形式化成功率の報告なし
    • 人工検証との比較欠如
    • 推奨：標注データセットを構築し、精度指標を計算
  3. 手動介入が多すぎる：
    • 変数接地は完全に手動で、自動化の主張を弱める
    • 自動化方案の具体的実装がない
    • スケーラビリティが疑わしい
    • 推奨：少なくとも原型的な自動接地システムを実装
  4. モデル選択が制限的：
    • リソース制限により7Bモデルのみを使用
    • 671Bモデルまたは他の代替案の探索なし
    • モデルサイズが結果に与える影響の分析欠如
    • 推奨：少なくとも少数のサンプルで異なるモデルを比較
  5. 失敗ケース分析の欠如：
    • 定理証明失敗の原因を詳細に分析していない
    • 形式化エラーと真の論理的矛盾を区別していない
    • 偽陽性/偽陰性分析がない
    • 推奨：エラー分類体系を確立
  6. 評価基準が単一：
    • Leanコンパイル成功/失敗のみに依存
    • 部分的に正しいケースを考慮していない
    • 細粒度のエラータイプ分析がない
  7. 汎化能力が不明：
    • 自動車安全要件のみテスト
    • 他のドメイン（医療、金融など）での適用可能性を検証していない
    • Gherkinシナリオの特殊性が方法の汎用性を制限する可能性

影響力

領域への貢献：

  • ⭐⭐⭐⭐ 概念的貢献が高い：新しい研究方向と応用シナリオを提案
  • ⭐⭐ 技術的貢献が中程度：主に既存技術の組み合わせ応用
  • ⭐⭐⭐ 実用価値がやや高い：工学実践における実際の問題を解決

実用価値：

  • 短期：要件エンジニアに検証思考を提供
  • 中期：専門的な要件検証ツールの開発を促進する可能性
  • 長期：LLM応用品質保証の標準プロセスになる可能性

再現性：

  • ✅ オープンソースツール（Lean 4、DeepSeek-Prover）を使用
  • ✅ 詳細なプロンプトテンプレートを提供
  • ❌ コードまたはデータを公開していない
  • ❌ 手動ステップが再現困難
  • 評価：⭐⭐⭐（中程度）

予想される影響：

  • LLM出力の形式化検証に関するより多くの研究を引き起こす可能性
  • 要件工学と形式化方法の結合を推進する可能性
  • 変数接地問題が新しい研究ホットスポットになる可能性

適用シナリオ

高度に適用可能：

  • ✅ 安全関連システムの要件検証（自動車、航空、医療）
  • ✅ 要件一貫性チェックと重複排除
  • ✅ LLM生成テストケースの品質管理

中程度に適用可能：

  • ⚠️ 複雑なビジネスロジックの検証（形式化能力の拡張が必要）
  • ⚠️ マルチモーダル要件（図表を含む要件など）
  • ⚠️ リアルタイムシステム（時間論理拡張が必要）

適用不可：

  • ❌ 高度に曖昧な自然言語テキスト
  • ❌ 明確なシステム定義がないシナリオ
  • ❌ リアルタイム応答が必要なシナリオ（現在の手動ステップが遅すぎる）

改善提案

  1. 即座に実行可能：
    • 最低50の要件ペアに拡張
    • 基本的な自動変数接地原型を実装
    • エラー分類体系を確立
  2. 短期的改善：
    • 異なるサイズのモデルを比較
    • 定量評価指標を導入
    • 複数のドメインでテスト
  3. 長期的目標：
    • パイプラインの完全自動化
    • ドメイン知識グラフの統合
    • 時間論理と複雑な制約のサポート

参考文献（主要文献）

  1. Weng et al. (2025): Autoformalization in the era of large language models: A survey - サーベイ文献
  2. Wu et al. (2022): Autoformalization with large language models - 自動形式化の基礎研究
  3. Ren et al. (2025): DeepSeek-Prover-v2 - 本論文で使用されたコアモデル
  4. Jiang et al. (2022): Draft, sketch, and prove - 部分目標分解方法
  5. de Moura & Ullrich (2021): The Lean 4 theorem prover - 形式化言語

総合評価：これは概念実証型の探索的論文であり、価値のある新しい研究方向を提案しているが、実験検証が極めて不十分である。プレプリントと初期研究として、重要な問題を識別し実行可能な技術パスを提供することに成功しているが、成熟したソリューションまでにはまだ大きな距離がある。論文の主な価値は問題定義と方向指引にあり、技術的ブレークスルーではない。後続の研究は、変数接地の自動化と大規模評価の問題解決に重点を置くことを推奨する。