Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

要約

既存の数学的証明の形式化は、非常に難しいプロセスです。
自動化と証明アシスタントに関する何十年にもわたる研究にもかかわらず、正式な証明を書くことは依然として困難であり、少数の専門家しかアクセスできません。
形式化を自動化するための以前の研究では、強力な検索アルゴリズムに焦点が当てられていましたが、利用可能な非公式の証明を利用する試みは行われませんでした。
この作業では、ドラフト、スケッチ、および証明 (DSP) を紹介します。これは、非公式の証明を正式な証明のスケッチにマッピングし、スケッチを使用して、検索をより簡単なサブ問題に向けることで自動証明者を導きます。
非公式な証明が人間によって書かれたか、言語モデルによって生成された 2 つの関連するセットアップを調査します。
私たちの実験とアブレーション研究は、大規模な言語モデルが、非公式の証明と同じ推論手順に従う、適切に構造化された正式なスケッチを生成できることを示しています。
これらのスケッチを使用して自動証明器をガイドすると、一連の数学的競争問題でのパフォーマンスが 20.9% から 39.3% に向上します。

要約(オリジナル)

The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts. While previous studies to automate formalization focused on powerful search algorithms, no attempts were made to take advantage of available informal proofs. In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems. We investigate two relevant setups where informal proofs are either written by humans or generated by a language model. Our experiments and ablation studies show that large language models are able to produce well-structured formal sketches that follow the same reasoning steps as the informal proofs. Guiding an automated prover with these sketches enhances its performance from 20.9% to 39.3% on a collection of mathematical competition problems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google