LLMEval-Logic解説:LLMの「論理的に見える答え」を、ソルバーで検査するベンチマーク
2026年5月19日、復旦大学NLP Lab系のLLMEvalチームが、LLM向け論理推論ベンチマーク「LLMEval-Logic」をarXivに投稿した。対象は中国語の自然言語論理問題で、単にモデルの最終回答を採点するだけではなく、自然言語を命題論理・一階述語論理へ正しく形式化できているかまで検査する点が特徴だ。論文は査読済み発表ではなくarXiv投稿段階だが、コード、公開データ、評価手順が同時に公開されている。([arxiv.org](htt...
LLMEval-Logic解説:LLMの「論理的に見える答え」を、ソルバーで検査するベンチマーク
2026年5月19日、復旦大学NLP Lab系のLLMEvalチームが、LLM向け論理推論ベンチマーク「LLMEval-Logic」をarXivに投稿した。対象は中国語の自然言語論理問題で、単にモデルの最終回答を採点するだけではなく、自然言語を命題論理・一階述語論理へ正しく形式化できているかまで検査する点が特徴だ。論文は査読済み発表ではなくarXiv投稿段階だが、コード、公開データ、評価手順が同時に公開されている。(arxiv.org)
今回の面白さは、「LLMは論理問題に強くなったのか」という問いを、かなり厳密に分解しているところにある。従来の論理推論ベンチマークには、形式論理式から自然言語問題をテンプレート生成するものが多く、問題文が人工的になりやすい。また、最終回答だけを見ると、途中の形式化が誤っていても偶然正解する可能性がある。LLMEval-Logicはこの弱点を避けるため、まず現実的・物語的な中国語シナリオから問題を作り、その後に専門家が形式化を監査し、Z3 SMTソルバーで答えを検証する流れを採っている。(arxiv.org)
構成は大きく二つに分かれる。Baseは単一質問の命題論理・一階述語論理問題で、完全版246問のうち197問が公開されている。各問にはZ3で検証された答え、ゴールド形式化、自然言語から形式論理への対応を評価するルーブリックが付く。HardはBaseをもとに、分岐、撹乱要素、不確実性、集合値出力、反事実、照応・別名表現などで難化した複数サブ質問型の問題で、完全版190問・938サブ質問のうち154問・766サブ質問が公開されている。残り20%は汚染耐性のため非公開ホールドアウトとして維持される。(github.com)
発表値として最も目を引くのは、14のフロンティアLLMを評価したところ、HardのItem Accuracyで最良モデルでも37.5%にとどまったという点だ。さらに、参照シンボルを与えた条件でも、Z3とルーブリックを同時に満たす形式化スコアの最高値は60.16%だったと論文は報告している。これは「答えをそれらしく説明する能力」と「前提から結論が形式的に従うことを保つ能力」の間に、まだ大きな差があることを示唆する。ただし、この数値は著者らの評価設定に依存するため、今後の第三者再現が必要だ。(arxiv.org)
技術的に重要なのは、評価軸が二段になっていることだ。ひとつは自然言語のまま答えを出す直接回答評価。もうひとつは、モデルに自然言語問題を形式論理へ変換させ、その形式化がZ3で正しい答えを導くか、さらに人手設計の原子的ルーブリックを満たすかを見る形式化評価である。GitHubの説明では、評価はnl-base、nl-hard、fl-free、fl-fixedの4段階に分かれ、OpenAI互換エンドポイントから任意のモデルを差し替えて実行できる設計になっている。(github.com)
ここで効いているのがZ3の存在だ。Z3はMicrosoft Research由来のSMTソルバーで、論理式の充足可能性や制約の整合性を機械的に検査するための道具である。LLMの出力をLLMだけで採点すると、採点者モデルの好みや曖昧さが入り込む。もちろんLLMEval-Logicも一部でLLM-as-Judgeを使っているが、少なくとも形式論理に落ちた部分については、ソルバーで機械的に照合できる。これは「AIがAIを採点する」流れに対する、一つの現実的な補強線だ。(microsoft.com)
ただし限界も明確だ。第一に、中国語論理推論に特化しているため、多言語一般の論理能力をそのまま代表するわけではない。第二に、完全版でも436問規模であり、評価対象は厳密な論理推論の一部に限られる。第三に、公開版351行はHugging Face上で取得可能だが、公開データは将来的に学習データへ混入する可能性があるため、非公開ホールドアウトの運用がどれだけ継続されるかが信頼性を左右する。なおデータセットはevaluation-onlyライセンスで、学習・微調整・蒸留・RLHFラベル生成などへの利用を制限している。(huggingface.co)
それでも、この発表は最近のLLM評価の方向性をよく表している。これからのベンチマークは、単なる正答率表ではなく、自然言語、形式検証、非公開テスト、実行可能な評価コードを組み合わせた「評価インフラ」へ近づいていく。特に法律、契約、科学、セキュリティ、金融のように、もっともらしい説明よりも厳密な含意関係が重要な領域では、LLM単体の流暢さではなく、ソルバーや検証器と接続された推論設計がより重要になる。
LLMEval-Logicが示しているのは、LLMが「論理を語れる」ことと「論理を保存できる」ことは別だという、地味だが重要な事実だ。今後のモデル競争では、長い思考連鎖を出せるかだけでなく、その思考を外部検証可能な構造へ変換できるかが問われる。LLMの推論能力を測る物差しは、少しずつ、文章の説得力から検証可能性へ移っている。
出典URL:
https://arxiv.org/abs/2605.19597
https://github.com/llmeval/LLMEval-Logic
https://huggingface.co/datasets/llmeval-fdu/LLMEval-Logic
https://llmeval.com/
https://www.microsoft.com/en-us/research/project/z3-3/