Coq と大規模言語モデルによる定理証明
鈴木彩加
明治大学 理工学研究科 数学専攻 M2

October 31, 2023

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

1 / 40定理証明支援系

定理証明支援系 (Proof Assistant) とは, コンピュータを用いて「形式化」を行い、その検証1 を行うためのソフトウェアである．[4]ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである. [5]Coq, AutoMath, Lean, Isabelle など様々な定理証明支援系がある．
今回は Coq を扱う．

1

コンピュータによって漏れや間違いがなく証明の確認ができる．

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

2 / 40アイデア

目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

3 / 40

アイデア

アイデア

数学の定理を機械に証明させたい．
定理証明支援系で人間が与えるヒントもコンピュータ上の言語で書かれている．
Coq からの検証結果を見れば次に与えたいヒントも機械が予測できるのではないか．

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

4 / 40アイデア

大規模言語モデル

大規模言語モデル (LLM) とは，深層学習モデルの一種である．テ
キストデータを中心とした大規模なデータセットを学習している．
従来の自然言語モデルと比べ，人間に近い会話が可能であり，自然言語を用いたさまざまな処理を行うことができる．
例：ChatGPT, Bing, · · ·鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

6 / 40Figure: ChatGPT

Figure: ChatGPT形式言語の命題
自然言語

Coq
自然言語

検証結果

自然言語

LLM

形式言語の証明

Figure: やり取りのイメージ図

データセット

目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

10 / 40

データセット

Alpaca 形式の Dataset [1]{ ”instruction” : モデルが実行するタスクを説明する,”input” : タスクのオプションのコンテキストまたは入力,”output” : instruction に対する応答}
例：{ ”instruction” : ” 次の記事を要約してください”,”input” : ” 記事の本文”,”output” : ” 記事の要約文”}

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

11 / 40

データセット現在作成したデータセット
theories ファイルセット2 から作成．（84723 個）• Coq プログラム（拡張子 v）ファイルの n 行目までを Coqtopで実行する．
• show. を最後に実行して返答があったもののみデータセットとして使用する．
show. を最後に実行して返ってきた返答は CoqIDE 上のゴールエリアに表示されるものであり，現在の仮定とゴールである．
• n 行目までを”instruction”，show. を実行して返ってきた返答を”input”，n + 1 行目を”output” とする．
つまり，今まで出した命令を”instruction”，現在の仮定とゴールを”input” 次に出す命令を”output” として情報を与える．
2

Coq に標準で入っている理論ライブラリ

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

13 / 40

学習方法

目次
1 アイデア2 データセット
3 学習方法LLM モデル追加学習方法
データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

14 / 40

学習方法

LLM モデル目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

15 / 40

学習方法

LLM モデル• 多言語対応したモデル

様々な人がモデル作成に取り組んでいるため精度が高いモデ
ルが多くある．
多言語対応しているため必要のない情報に情報量が割かれてしまっている．
• コードに特化したモデル

プログラミング言語に特化したモデルであり，一番多いものは Python のスクリプトの精度を高めたものである．Python，
C++，Java，PHP，Typescript(Javascript)，C#，Bash などの言語をサポートしているものがある．
例：Code Llama，WizardCoder-Python-13B-V1.0• 数学特化の言語モデル

例：WizardMath

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

16 / 40

学習方法

追加学習方法目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

17 / 40

学習方法

追加学習方法LoRA[2]

LoRA (Low-Rank Adaptation) とは，学習にかかる計算コストを抑えつつ，かつ推論時の速度を Fine Tuning した場合と同等に保つことが出来る学習方法である．
LLM の事前学習から変更されていない状態の重みを W0 ∈ Rd×k とする．LLM を Fine Tuning して変更した層の差分を ∆W とする．
LoRA はこの ∆W を比較的小さなサイズの行列 A と B の積 BA で学習する．

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

18 / 40

Figure: LoRA[3] の概要図

学習方法

追加学習方法学習方法• Fine Tuning• LoRA

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

20 / 40

学習方法

データセット目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

21 / 40

学習方法

データセット

現在作成したデータセット
theories ファイルセット3 から作成．（84723 個）• Coq プログラム（拡張子 v）ファイルの n 行目までを Coqtopで実行する．
• show. を最後に実行して返答があったもののみデータセットとして使用する．
show. を最後に実行して返ってきた返答は CoqIDE 上のゴールエリアに表示されるものであり，現在の仮定とゴールである．
• n 行目までを”instruction”，show. を実行して返ってきた返答を”input”，n + 1 行目を”output” とする．
つまり，今まで出した命令を”instruction”，現在の仮定とゴー
ルを”input” 次に出す命令を”output” として情報を与える．
3

Coq に標準で入っている理論ライブラリ

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

22 / 40検証方法

目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

27 / 40

検証方法

簡単な定理の証明について証明できるか検証する．
• 次の tactic 候補複数を LLM に提示してどれが一番良いか予測させる．
• LLM に次の tactic を予測させる．

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

28 / 40

検証方法次の tactic 候補複数を提示してどれが一番良いか予測させる．

apply: A_to_B_is_true.
2 by[].
3 apply: A_is_true.
1

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

30 / 40

検証方法

LLM に次の tactic を予測させる．
tactic がエラーが出ずに証明が進めば正解とする．
可能であれば，最適な tactic を選べているか評価したい．
（証明終了までに必要な tactic が少ない tactic が予測出来ればスコアを高くする等）

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

31 / 40

問題点

目次1 アイデア
2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

32 / 40

問題点### output:
3 goals> HS1 : (A -> (B -> C) ) -> ( (A -> B )->(A-> C) ).
> A_to_B_to_C_is_true : (A -> (B -> C) ) -> ( (A -> B)->(A-> C) ).
> A_to_B_is_true : A -> B
> A_is_true : A .

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

34 / 40

今後

目次
1 アイデア2 データセット
3 学習方法LLM モデル
追加学習方法データセット

4 検証方法
5 問題点
6 今後
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

35 / 40

形式言語の命題
自然言語

Coq
自然言語

検証結果

自然言語

LLM

形式言語の証明

Figure: やり取りのイメージ図

今後

Coq と LLM で交互にやり取りをさせて定理証明できるか検証したい．
Coq からの検証結果だけでなくエラー文も含めて LLM がよりよい
tactic 候補を出せるようにする．

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

37 / 40

今後

参考文献 I[1] Alpaca dataset, 2023.
https://huggingface.co/datasets/tatsu-lab/alpaca.
[2] Llm をカスタマイズする方法として lora について調べてみました。, 2023.
https://techblog.cccmk.co.jp/entry/2023/06/20/154850.
[3] Lora: Low-rank adaptation of large language models,2023.
https://arxiv.org/abs/2106.09685.
鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

38 / 40

今後

参考文献 II[4] 久我健一.
証明支援系を用いたトポロジーの形式化について,2015.
[5] 萩原 学 and Reynald Affeldt.
Coq/ssreflect/mathcomp による定理証明, 2018.

鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

39 / 40

今後終わり鈴木彩加 (明治大学 数学専攻 M2)

Coq と大規模言語モデルによる定理証明

October 31, 2023

40 / 40