Abstract
型注釈は、再解析や型推論の下でそれらの意味が保存されるように項を出力する際に不可欠である。本研究では、Isabelleで用いられるランク1多相λ-計算の項に対する、完全かつ最小の型注釈の問題を扱う。Smolka、Blanchetteらによる先行研究を土台として、我々はこの問題に対するメタ理論的な説明を与え、完全な形式仕様と証明を提示し、さらにそれをIsabelle/HOLで形式化する。本開発は、人手主導とAI主導の形式化ワークフローを特徴とする一連の実験である。すなわち、人間と、LLMを動力とするAIエージェントがそれぞれ独立に手作業のペン・アンド・ペーパーによる証明を作成し、AIエージェントは両方をIsabelle上で自動形式化する。加えて、人間がヒントを与えたAI介入によって、開発は洗練され、一般化されていく。
