Leanでコンパイルできても、定理の意味が正しいとは限らない

導入

自然言語の数学命題をLeanの宣言へ変換するシステムでは、生成コードがコンパイルできるかどうかが成功の主要な指標になりがちです。しかしLeanが確認するのは、構文、型、そして形式環境上の整合性です。元の文章が意図した定理を表しているかどうかは、コンパイラだけでは分かりません。仮定を落としたり、量化の範囲を変えたり、数学用語を誤解したりしても、別の命題としてコンパイルできる場合があります。

論文「Beyond Compilation」は、比較対象となる標準Leanターゲットが存在しない状況で、この問題を検討しています。焦点は、自然言語からLeanへの変換が、意味をどれだけ忠実に保っているかを測る方法です。

主なポイント

• コンパイルは必要条件にすぎません。 提案された基準では、まずLeanでコンパイルできることを求めます。そのうえで、異なるモデル系列に属する2つのLLM判定者が、形式化された命題と自然言語の内容が一致すると判断する必要があります。
• 人間の判断との一致率は91.5%。 独立したランダム監査では、この基準が人間の多数意見と91.5%一致しました。不忠実な出力を受理することは少ない一方、実際には忠実な出力を一部拒否する性質もあります。
• コンパイル率と受理率には差がある。 8システム、大学レベルの227件を調べたところ、両者の差は1.3〜29.5ポイントでした。ツールを利用するGPT-5.2エージェントは87.2%をコンパイルできましたが、忠実だと受理されたのは57.7%でした。
• 差の多くは翻訳ミスだった。 同エージェントの拒否例を人間が確認すると、29.5ポイントの差のうち23.8ポイントが実際の翻訳エラーでした。7つのワンショットシステムでも、6システムについて差の78〜100%が翻訳エラーと判定されました。
• 評価者の能力も結果に影響する。 GPT-5.2がGPT-6 AstraとClaude Opus 5.5を評価した場合、両モデルはそれぞれ83%が受理されました。一方、ワンショットGPT-5.2は21%でした。新しい2モデルの拒否54件を確認すると、翻訳エラーは4件だけで、差の大部分は判定者側の誤りと考えられます。

意義

この研究は、コンパイル率だけで進歩を測ることの危うさを示します。コンパイルは構造や型の誤りを除く重要な指標ですが、意味の同値性を保証する十分条件ではありません。仮定を省略したり命題を弱めたりすることで、システムは見かけ上のコンパイル率を上げられてしまいます。

今後のベンチマークでは、コンパイル率、意味的な受理率、人間による監査、評価者の誤りを分けて報告する必要があります。生成モデルが改善しても、判定モデルが追いつかなければ、評価器そのものがボトルネックになります。信頼できる形式化には、コード生成だけでなく、生成された定理の意味を監査する仕組みが欠かせません。

出典：Hugging Face Daily Papers