Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions

要約

彼らの言語能力のおかげで、LLMSは、オートフォーマル化を通じて、非公式の数学と正式な言語のギャップを埋める機会を提供します。
ただし、LLMSが洗練された自然に発生する数学的なステートメントにどれだけよく一般化するかはまだ不明です。
このギャップに対処するために、現実世界の数学的定義を自動占領するタスク、つまり数学的談話の重要な要素を調査します。
具体的には、オートフォーマル化のための2つの新しいリソースを導入し、ウィキペディア（def_wiki）とarxivペーパー（def_arxiv）から定義を収集します。
次に、LLMSの範囲を体系的に評価し、定義をイザベル/ホルに形式化する能力を分析します。
さらに、プルーフアシスタントからの外部フィードバックを介した改良を含むLLMSのパフォーマンスを強化する戦略を調査し、正式な数学ライブラリから関連するコンテキスト要素を介してLLMを導く正式な定義の基礎を調査します。
私たちの調査結果は、MINIF2Fなどの既存のベンチマークと比較して、定義がより大きな課題を提示することを明らかにしています。
特に、LLMは依然として自己修正に苦労しており、関連する数学ライブラリと協力することがわかりました。
同時に、構造化された改良方法と定義の接地戦略により、自己修正能力が最大16％、未定義のエラーの減少が43％の顕著な改善が得られ、実際のシナリオでのLLMベースの自己体系化を強化するための有望な方向性が強調されています。

要約(オリジナル)

Thanks to their linguistic capabilities, LLMs offer an opportunity to bridge the gap between informal mathematics and formal languages through autoformalization. However, it is still unclear how well LLMs generalize to sophisticated and naturally occurring mathematical statements. To address this gap, we investigate the task of autoformalizing real-world mathematical definitions — a critical component of mathematical discourse. Specifically, we introduce two novel resources for autoformalisation, collecting definitions from Wikipedia (Def_Wiki) and arXiv papers (Def_ArXiv). We then systematically evaluate a range of LLMs, analyzing their ability to formalize definitions into Isabelle/HOL. Furthermore, we investigate strategies to enhance LLMs’ performance including refinement through external feedback from Proof Assistants, and formal definition grounding, where we guide LLMs through relevant contextual elements from formal mathematical libraries. Our findings reveal that definitions present a greater challenge compared to existing benchmarks, such as miniF2F. In particular, we found that LLMs still struggle with self-correction, and aligning with relevant mathematical libraries. At the same time, structured refinement methods and definition grounding strategies yield notable improvements of up to 16% on self-correction capabilities and 43% on the reduction of undefined errors, highlighting promising directions for enhancing LLM-based autoformalization in real-world scenarios.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google