これは株式会社LabBase テックカレンダー Advent Calendar 2025 12日目の記事です。
概要
学生時代から、論文などの議論の精読に対して、「絶対誰かがもう論理的な整合性を確かめたことあるんだろうな〜」と思い、その度に論理的な整合性の再確認に対してめんどくささを感じてきました。
本稿では形式意味論と定理証明支援系を利用して、あらゆる議論を形式化することで、これを打破することを目論みます。
もし自然言語が「コンパイル」できたら？
プログラミング言語では、コードを書くと同時にコンパイラや静的解析ツールが働き、文法ミスや型の不整合、論理的な破綻を検出してくれます。
では、自然言語の文章にも同じような仕組みがあったらどうなるでしょうか。
実は私たち人間は、日常的にそれに近いことを行っています。
たとえば論文を読むとき、仮説から結論までの論理が本当に成立しているかを追いかけます。
数学の証明では、一つひとつのステップが前提から正しく導かれているかを確認します。
技術仕様書や設計書をレビューするときには、要件と設計判断の整合性や、暗黙の前提が紛れ込んでいないかを検証します。
契約書や規約を読む場面でも、条件と例外が矛盾なく定義されているかを慎重に辿ります。
これらはすべて、文章の文法・意味・文脈・論理構造を頭の中で解析する作業です。
言い換えれば、人間は自然言語に対して、高度な「静的解析」を行っていると言えます。
これらの作業は、ともすれば大変めんどうだと思いますが、もしこの作業をコンピュータが担えるようになればどうでしょう。
文脈を考慮した補完やサジェスト、論理的な飛躍の指摘など、人類に知的活動の底上げができるはずです。
この図は自然言語とプログラミング言語についての一般的な認識を整理したものです。
プログラミング言語は、公開されたコードの再利用性は高く（なんならuse crate-name,import package-nameのような文法で簡単に再利用でき）、整合性検査のある言語がほとんどであり、自然言語にはない大変便利な性質がそろっています。
対して、自然言語は普及度・人類が依存している度合いはケタ違いに高いという利点があり、数学の証明ですら地の文が存在することが大多数であるほどです。
本稿では、形式意味論と定理証明支援系の２つをつかい、自然言語で記述されるようなあらゆる議論に対して、再利用性と整合性検査を導入することを考えます。
形式意味論で自然言語を論理式にする
詳細は説明しないのですが、組合せ範疇文法（Combinatory Categorial Grammar）という文法の理論で自然言語を論理式に変換でき、また自然言語がどのような論理式に変換できるかは形式意味論によって定めることができます。
今回はlightblueというソフトウェアをつかい、自然言語を論理式に変換します。
lightblueはお茶大の戸次研で開発されているHaskellで書かれたソフトウェアで、組合せ範疇文法（Combinatory Categorial Grammar）に基づいて日本語をパースし、依存型意味論という形式意味論の理論に基づいて論理式を算出します。
例として、
太郎がパンを食べた。
を入力すると、
$ echo 太郎がパンを食べた。 | ./lightblue jp -m kwja parse -s text
WRAP Sbar[decl] (u0:(x0:entity)✕(x1:entity)✕(パン(x1,x0)))✕(x2:entity)✕(u2:食べる/たべる/ガヲニ(x2,太郎/たろう;太郎/たろう,π1(u0),@entity))✕(＃タ(x2))
といった感じで日本語が論理式にパースされて変換されます。
仕組みを簡単に説明すると、単語ごとに「どの品詞及びその組み合わせを引数に取るか」が決まっており、それを元に日本語をパースするという方法がとられています。
これで最も非自明な部分は乗り越え、自然言語の形式化ができました🎉めでたいですね
定理証明支援系で議論を形式化する
定理証明支援系（proof assistant）は、「論理的に正しいこと」を形式的に保証するためのシステムです。人間の証明を後追いで検算するのではなく、定義・仮定・推論規則をすべて形式化し、暗黙の前提や論理的飛躍が含まれていれば即座に拒否する、非常に強力な整合性検査を備えています。元々の目的は議論の形式化ですが、定理証明支援系の上で議論を扱えれば、便利で理想的な議論の形式化が達成できることでしょう。
定理証明支援系には色々な種類がありますが、今回はLeanをちょっと紹介します。
これはLeanの日本コミュニティのHPであるLEAN JAのトップページにあるLeanのコードの例です。
import Mathlib.Tactic
/-- フィボナッチ数列の線形時間の実装 -/
def fib (n : Nat) : Nat :=
(loop n).1
where
-- ヘルパー関数を定義する
loop : Nat → Nat × Nat
| 0 => (0, 1)
| n + 1 =>
let p := loop n
(p.2, p.1 + p.2)
-- 最初の数個の値に対してテストする
#guard [0, 1, 2, 3, 4, 5].map fib = [0, 1, 1, 2, 3, 5]
/-- `fib` が満たす漸化式 -/
theorem fib_add (n : Nat) : fib n + fib (n + 1) = fib (n + 2) := by rfl
このように、アルゴリズムの実装とそれに対するテスト、さらに実装についての定理とその証明を自由自在に書くことができます。また、mathlibという強力な数学の証明用のライブラリも存在し、他の普通のプログラミング言語と同様に、外部ライブラリの利用もスムーズです。
またLeanは開発環境も優れており、VSCodeやEmacs上で言語サーバーの支援を受けながら、書いた定理やコードをその場で評価したり、証明中や実装中に宣言した変数の情報を専用のパネルで一覧として見ることもできます。
Leanのような定理証明支援系によって、無事に議論を形式化できそうですね。あとは先程日本語から変換した論理式をLean上に読み込む便利な機能があれば十分でしょう。
ところで、ここで紹介したLeanはElaborationという強力なメタプログラミング機能があり、文法を再定義して、パース時に外部プロセスを起動して出力結果からLeanの変数や式をつくることもできます。
elab "ja(" je:ja_expr+ ")" : term => do
let _a: Syntax := (je[0]!).raw
logInfo s!"a{_a}"
logInfo s!"kk{je[1]!}"
pure $ mkStrLit s!"o{je}"
#eval ja(«ほめる» «太郎が» «次郎を»)
つまり、Lean上に日本語で議論を書き、Elaborationをつかってパース中にlightblueを起動して論理式に変換することで、日本語での議論をそのままLean上の式として証明したり、ライブラリとして利用したりできるということです。
これをもって、形式意味論と定理証明支援系を利用して、あらゆる議論の形式化ができるという算段が立ったといえるでしょう🎉
本当にできるのか
じゃあ本当にできるのかという話ですが、前述のように理屈自体には大きな問題はなさそうなので、あとは実用に足りるものができるかどうかという話になると思います。
人間が行うような議論が定理証明支援系で扱えるのかという問題ですが、（のらりくらり定義をはぐらかすようなものでもない限り）たとえ論文でも１文１文の繋がりはそんなに難しいものではなく、むしろ文が多いことが難しさの主な原因であることが大半だと思うので、数学の定理証明ができるシステムならば当然可能だと考えられます。
他に懸念事項の主なものとしては、
- 一般的な議論であれば当然仮定しているような、いわゆる「常識」のようなものは、標準ライブラリとして用意する必要がある
- 形式意味論で捉えにくいような意味を、どのように搦手で解釈するかを、その都度デバッグのように対応する必要がある
といったことが考えられますが、これらについては言わば新興のプログラミング言語と状況が大変似ており（参考になるものが無いことを鑑みると、最初期の高水準プログラミング言語のほうが近いかも）、作りながら少しずつ改善点を洗い出すことで対応するほかないと思います。
結び
本稿では、形式意味論と定理証明支援系を利用して、あらゆる議論を形式化することで、議論の処理を計算機で大幅にエンパワーメントできそう、というアイデアについて紹介してきました。
ここ数年ずっと囚われているアイデアなので、これらが完全に実装されたシステムが靴下に入ってたらうれしいですね🎅
Discussion