要旨: LLMが自然言語を形式化するとき、出力が忠実（faithful）であることをどのように確かめるのでしょうか。私たちは、教師となる正解注釈を必要としない往復検証（roundtrip verification）アプローチを提案します。すなわち、ある主張を形式化し、その結果を自然言語へ翻訳し、再度形式化し、形式的ツールを用いて論理的同値性を検査します。2つの形式化が一致すれば、それは忠実な形式化であることの証拠になります。一致しない場合、診断ステップがどの翻訳段階が失敗したかを特定し、対象を絞った修復オペレーターがその段階を修正しようとします。私たちは、Claude Opus 4.6およびGPT-5.2を用いて、150の交通ルールに対してこの手法を評価します。診断に導かれた修復により、形式的同値性は両モデルで45--61%から83--85%へと向上し、ランダム修復のベースラインを上回ります。独立したNLI分析により、形式的同値性がより少ないセマンティック・ドリフトと相関していることが確認されます。
ラウンドトリップ検証と修復による忠実な自動形式化
arXiv cs.CL / 2026/4/29
📰 ニュースModels & Research
要点
- 本論文は、LLMが自然言語から形式言語へ変換する際の「忠実性」をどう検証するかを扱い、形式同値性チェックを組み込んだラウンドトリップ手法を提案している。
- 手法は、まず文を形式化し、得られた形式結果を自然言語へ戻して再形式化したうえで、形式ツールを用いて論理同値性を確認する。
- 両者の形式化が一致すれば忠実な形式化の証拠となり、一致しない場合は診断ステップで失敗した変換段階を特定し、特定の修復オペレータでその段階を修正する。
- 実験では交通ルール150件に対しClaude Opus 4.6とGPT-5.2を用い、診断に基づく修復により形式同値性が45–61%から83–85%へ向上し、ランダム修復のベースラインを上回った。
- さらに独立したNLI解析により、形式同値性が高いほど意味のドリフトが小さいことが示され、論理チェックにとどまらない有効性が支持されている。
