Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach

要約

大規模な言語モデル（LLM）は、数学的証明生成など、厳密な論理的控除と象徴的な推論を必要とする正式なドメインと闘っています。
この課題を克服するために、LLMSの生成強度と構造化されたコンポーネントを組み合わせた神経腫瘍アプローチを提案します。
概念実証として、幾何学の問題に焦点を当てます。
私たちのアプローチは2つあります。（1）類似の問題を取得し、それらの証明を使用してLLMを導き、（2）正式な検証剤が生成された証明を評価し、フィードバックを提供し、モデルが誤った証明を修正するのに役立ちます。
私たちの方法は、OpenaiのO1モデルの証明精度を大幅に改善することを実証します（58％-70％の改善）。
類似の問題と検証者のフィードバックの両方が、これらの利益に貢献します。
より広く、実証的に正しい結論を生成するLLMSに移行すると、信頼性、精度、一貫性が劇的に改善され、複雑なタスクと信頼性を必要とする重要な現実世界のアプリケーションのロックが解除される可能性があります。

要約(オリジナル)

Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning, such as mathematical proof generation. We propose a neuro-symbolic approach that combines LLMs’ generative strengths with structured components to overcome this challenge. As a proof-of-concept, we focus on geometry problems. Our approach is two-fold: (1) we retrieve analogous problems and use their proofs to guide the LLM, and (2) a formal verifier evaluates the generated proofs and provides feedback, helping the model fix incorrect proofs. We demonstrate that our method significantly improves proof accuracy for OpenAI’s o1 model (58%-70% improvement); both analogous problems and the verifier’s feedback contribute to these gains. More broadly, shifting to LLMs that generate provably correct conclusions could dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google