形式的表現に基づけて、書かれた定理を探索可能にする

概要: LLMが生成した説明は技術的な内容をよりアクセスしやすくできますが、対話的にサポートできることには限界があります。LLMの出力は静的なテキストであるため、実行したり、ステップごとに追跡したりすることはできません。私たちは、説明を形式化された表現に基づけることで、静的テキストが支えられる以上の対話的な足場（affordances）を可能にすると主張します。この考えを、数学的証明の理解に対して具体化します。すなわち、探究可能な定理（explorable theorems）というシステムで、LLMを用いて定理とその文章による証明を、機械検証された証明のためのプログラミング言語であるLeanへと翻訳し、文章による証明とLeanのコードを結び付けます。読者は、証明をステップ単位の粒度で進め、カスタムの例や反例をテストし、各ステップをつなぐ論理的依存関係を追跡できます。各ように展開されたステップは、その例に対してLeanの証明を実行し、その中間状態を抽出することで生成されます。ユーザー調査（n = 16）により、このアプローチの潜在的な利点が示されます。証明の読み合わせタスクにおいて、提供された探究可能性機能にアクセスできた参加者は、理解度に関する質問に対してより良く、より正確で、より詳細な回答を示し、基礎となる数学への全体的な理解がより強いことが裏付けられました。