A Survey on Deep Learning for Theorem Proving

要約

定理の証明は数学の基本的な側面であり、自然言語での非形式的な推論から形式的なシステムでの厳密な導出まで多岐にわたります。
近年、深層学習の進歩、特に大規模な言語モデルの出現により、定理証明のプロセスを強化するためにこれらの手法を探求する研究が顕著に急増しています。
この論文は、定理証明のための深層学習の包括的な調査を提供するものであり、(i) 自動形式化、前提の選択、証明ステップの生成、証明検索などのさまざまなタスクにわたる既存のアプローチを徹底的にレビューします。
(ii) 厳選されたデータセットと合成データ生成戦略の広範な概要。
(iii) 評価指標と最先端の手法のパフォーマンスの詳細な分析。
(iv) 根強い課題と将来の探求に向けた有望な道筋についての批判的な議論。
私たちの調査は、定理の証明におけるディープ ラーニング アプローチの基礎的な参考資料として機能し、この急速に成長している分野におけるさらなる研究努力を刺激し、促進することを目的としています。
厳選された論文リストは https://github.com/zhaoyu-li/DL4TP で入手できます。

要約(オリジナル)

Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a comprehensive survey of deep learning for theorem proving by offering (i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; (ii) an extensive summary of curated datasets and strategies for synthetic data generation; (iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art methods; and (iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, inspiring and catalyzing further research endeavors in this rapidly growing field. A curated list of papers is available at https://github.com/zhaoyu-li/DL4TP.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google