|
2023年度は生成AIや大規模言語モデル(LLM)の開発と利用が世界的に急速に進展した。昨年度我々が利用対象としたT5もその一つであるが、GPT4やLLama3等、次々に規模と性能を拡大、向上させている現状と、このようなLLMの構築と事前学習は当該研究の規模では不可能であることとから、さまざまなモデルでの転移学習（あるいはファインチューニング）を見据えて、特定のモデルや特殊なプロトコルによらない数学証明の動的なデータセットの作成手法と作成が現時点で最も重要であると考えるに至った。通常のプログラミング汎用言語の学習データと異なり、Coqのような証明支援系の言語では、作成の難しさから、ファイル自体の量が少ないことに加え、プログラミング段階で、証明状態を対話的に使用する必要がある。そのような観点から作成したCoqデータセットと、これを作成するプログラム等を GitHub上で公開した。
https://github.com/kenkuga/picoq
ここに公開したデータの一つは441Mbのcsvファイルで、各行は２項目からなり、第１項目はCoqをemacs上で利用するときに対話的に返される情報であり、第２項目はそれに対するTacticとそれに与えられるパラメータである。また第１項目には、現れる各項のタイプ情報も付与されているが、これはShow Allで得られる情報であり、特殊なプロトコルを用いないため、利用が容易である。
LLM等を用いた数学定理の形式化の実用化のためには、通常の数学証明を直ちに形式化できるわけではないため、まず証明を数学言語で細かいステップに分解する段階が必要である。その観点からの利用を想定して、ウェブ上のProofwikiやn Lab等の証明データベースを作成した。
http://163.43.192.18:8000/proofs/index3（PWは下記）
|
