LemmaHead: RAG Assisted Proof Generation Using Large Language Models

要約

数学的な問題を解決したり数学的証拠を書いたりするために必要なロジックを開発することは、大規模な言語モデル（LLM）にとってより困難な目的の1つです。
現在、文献で最も人気のある方法は、モデルが数学的執筆のスタイルをエミュレートすることを学ぶことができるように、アカデミック出版物や教科書などの書面による数学的コンテンツのモデルを微調整することで構成されています。
このプロジェクトでは、LLMSの数学的推論のギャップに対処するために検索拡張生成（RAG）を使用することの有効性を調査します。
公開された教科書のコンテキストに特に焦点を当てて、関連する数学的コンテキストでモデルに質問を補足するぼろきれの知識ベースであるLemmaheadを開発します。
数学的推論におけるモデルのパフォーマンスを測定するために、テストパラダイムは、無駄のない正式な言語での特定の数学的主張への証明を生成することで証明する自動定理のタスクに焦点を当てています。

要約(オリジナル)

Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the most popular methods in literature consists of fine-tuning the model on written mathematical content such as academic publications and textbooks, so that the model can learn to emulate the style of mathematical writing. In this project, we explore the effectiveness of using retrieval augmented generation (RAG) to address gaps in the mathematical reasoning of LLMs. We develop LemmaHead, a RAG knowledge base that supplements queries to the model with relevant mathematical context, with particular focus on context from published textbooks. To measure our model’s performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving via generating proofs to a given mathematical claim in the Lean formal language.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google