01 / UNDERSTAND
仕組みと使いどころ
形式化は、非形式的に表された内容を形式的な表現へ移す作業である。提示資料では、自然言語で書かれた数学を形式仕様や証明へ変換する処理や、非形式的な入力を形式論理表現へ変換する処理が扱われている。この作業を自動化することは自動形式化と呼ばれ、大規模言語モデルを利用した研究も行われている。形式化は作業自体を指し、自動形式化はその自動化、証明の形式化は対象を証明に限定した形態である。
02 / IN PRACTICE
Formalizationの活用例
たとえば、こんな場面で
自然言語で書かれた数学問題を、Isabelle/HOLで扱える形式仕様へ変換する。
03 / GOOD TO KNOW
使うときのポイント
対象となる非形式的記述と、変換先が形式仕様、証明、その他の論理表現のどれであるかを明確にする。自動処理を指す場合は自動形式化と区別する。
参考資料
Autoformalization with Large Language Models （新しいタブで開きます）Towards a Common Framework for Autoformalization （新しいタブで開きます）用語の説明や活用例に関連する参考資料です。
READ & LEARN
記事一覧を見る 用語を知ったら、活用を知る。
AI LABで、AIの動向や業務に取り入れるヒントを読む。