Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

要約

自動形式化、つまり自然言語の記述を形式言語に自動的に変換するタスクは、さまざまな領域、特に数学において重大な課題を引き起こします。
大規模言語モデル (LLM) の最近の進歩により、競技レベルの数学問題さえも形式化できる有望な機能が明らかになりました。
ただし、LLM で生成された形式化では、pass@1 と pass@k の精度の間にかなりの差異があることが観察されます。
このギャップに対処するために、記号等価性と意味的一貫性という 2 つの相補的な自己一貫性手法に基づいて、k 個の自動形式化候補から最良の結果をスコアリングして選択する新しいフレームワークを導入します。
詳細には、記号等価性は自動定理証明器を使用して自動形式化候補間の論理的均一性を特定し、意味的一貫性は候補を形式化して元のテキストと形式化されたテキストの埋め込み間の類似性を計算することによって元の意味の保存を評価します。
MATH および miniF2F データセットに対する広範な実験により、私たちのアプローチが自動形式化の精度を大幅に向上させ、さまざまな LLM およびベースライン手法全体で最大 0.22 ～ 1.35 倍の相対的改善を達成することが実証されました。

要約(オリジナル)

Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google