SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation

技術要約: SymCode

問題提起

大規模言語モデル（LLM）は自然言語において顕著な習熟度を示す一方で、複雑な数学的推論においては苦戦する。プローズ（散文）ベースの生成（例：Chain of Thought）を用いて多段階の問題を解くよう促すと、モデルは微細な算術エラー、論理的な誤謬、あるいは幻覚（ハルシネーション）による中間ステップを含む解を生成することが頻繁にある。これらの自然言語による根拠は不透明であることが多く、専門家による検証を困難にし、誤った回答を反復的に洗練させるための自動フィードバックループの構築を妨げている。既存の推論時戦略であるChain of Thought (CoT) や Tree of Thoughts (ToT) は、これら信頼性の低い媒体内で動作しており、決定論的な検証メカニズムを欠いている。

手法: SymCodeフレームワーク

これらの限界に対処するため、著者らは、数学的問題解決を「検証可能なコード生成」のタスクとして再定義するニューロシンボリック・フレームワークであるSymCodeを導入する。LLMにプローズで推論を記述させるのではなく、SymCodeは、コード自体が推論の痕跡（リーズニング・トレース）として機能する、自己完結的で実行可能なPythonスクリプトを構築するよう指示する。

本フレームワークは、主に以下の3つのコンポーネントで構成される：

1. 記号的翻訳 (Symbolic Translation): LLMに対し、自然言語の問題を解釈し、SymPy（計算代数システム：CAS）を活用したPythonスクリプトを生成するよう促す。近似的な浮動小数点演算に依存する標準的な数値ライブラリとは異なり、SymPyは数学的表現を正確な記号形式で操作する。これにより、丸め誤差を排除し、真の代数的推論（例：連立方程式の解法、式の簡略化）を完全な忠実度で実現する。
2. 決定論的検証 (Deterministic Verification): 生成されたスクリプトは、サンドボックス化されたPythonインタープリタ内で実行される。これにより、決定論的なパス/失敗の信号が得られる。プロンプトでは、解が元の制約（例：正値性や整数性などのドメイン要件）を満たすことを確認するためのassert文を含めることが明示的に要求される。
3. 反復的自己デバッグ (Iterative Self-Debugging: SymCode+): 初期スクリプトが失敗した場合（構文エラー、型エラー、またはアサーション失敗による）、エラーメッセージとトレースバックがLLMにフィードバックされる。モデルは、そのエラーをデバッグしてコードを修正するよう指示される。このサイクルは、スクリプトが正常に実行されるか、リトライ制限に達するまで繰り返される。

コアとなるプロンプトテンプレートは、構造化された出力を強制する。モデルはSymPyをインポートし、適切な仮定の下で記号を定義し、推論ステップをコメントとして記録し、代数的操作を行い、制約を検証し、最終的な答えを特定のLaTeX \boxed{} 形式で出力しなければならない。

主な貢献

本論文は以下の貢献を行う：

• SymCodeの定式化: LLMを高度な数学的推論のための自己完結的で検証可能なPythonスクリプトを生成するニューロシンボリック・リーズナーへと変貌させる、プロンプトベースのフレームワーク。
• 反復的自己修正: LLMLが決定論的なインタープリタのフィードバックを利用して、自身のプログラム上のエラーを修正する堅牢な検証プロセスを導入した。これはプローズベースのリーズナーには不可能な能力である。
• 実証的検証: 3つの困難なベンチマーク（MATH-500、OlympiadBench、AIME 2024/2025）を用いた広範な実験により、SymCodeが従来のプロンプティング・ベースライン（CoT、ToT、Decomposition）に対して最大13.6パーセントポイントの精度向上を実現したことを示した。問題の難易度が高まるにつれて、この性能差は拡大する。
• トークン効率: 推論をコードとして扱うことは、プローズベースの手法よりも大幅にトークン効率が高いことを示す詳細な分析。プローズによる手法と比較して、トークン使用量を約**60%から77%**削減している。
• エラーモード分析: 本フレームワークが、モデルの失敗を、不透明な論理的誤謬や算術ミスから、透明なプログラムエラー（例：APIの誤用や解釈ミス）へとシフトさせるという証拠。これらは診断および修正がより容易である。

結果

評価には、Llama 3.2 (90B)、GPT-5-nano、GPT-OSS (20B) を含む最先端のモデルが含まれた。

• 精度: 最も困難なデータセット（OlympiadBenchおよびAIME）において、SymCode+は顕著な利得を得た。例えば、GPT-5-nanoを用いた場合、OlympiadBenchでの精度は80%、AIMEでは65%に達し、最良のプローズベースのベースライン（ToT）に対して、絶対値で約12〜13パーセントポイントの向上を示した。
• モデル依存性: フレームワークの有効性は、ベースモデルのコーディング習熟度と相関している。強力なコーダー（GPT-5-nano）は即座に恩恵を受ける一方で、コーディングスキルが弱いモデル（Llama 3.2）は、初期の構文エラーや論理エラーを克服するために自己デバッグループに大きく依存するが、修正後に同等の利得を達成する。
• トークン効率: すべてのモデルとデータセットにおいて、SymCodeの解は平均699出力トークンであった（ToTは1,770、Decompositionは1,962、CoTは2,991）。自己デバッグループのオーバーヘッドを考慮しても（これによりSymCode+の平均は890トークンに上昇）、この手法は依然として大幅に簡潔である。
• アブレーション研究: 主要なコンポーネント（自己デバッグ、検証アサーション、または数値Pythonに代わるSymPyライブラリ）を取り除くと、測定可能な性能低下が見られた。これは、各要素がピークパフォーマンスのために不可欠であることを裏付けている。

意義と主張

本論文は、SymCodeが、フォーマルな領域におけるより正確で信頼できるAIへの重要な一歩であると断じている。LLMの推論を決定論的な記号エンジンに接地させることで、本フレームワークはモデルの失敗の本質を根本的に変える。検証されていない幻覚的なプローズを生成する代わりに、モデルは透明で、監査可能で、機械実行可能な推論の痕跡を生成する。

著者らは、このアプローチが、コードを単なる外部の計算機として利用する（Program-Aided Language Models、すなわちPALのような）段階から、コードを推論のモダリティそのものとして利用するパラダイムへと移行させるものであると主張している。これにより、LLMの役割は単純な計算機から、自然言語の問題を形式的で検証可能な記号表現へと変換するエキスパート・トランスレーターへと昇格する。本研究は、プログラム的に定式化可能な問題に対しては、このニューロシンボリックなアプローチが、自然言語におけるテスト時計算量（test-time compute）のスケーリングよりも優れた代替案を提供し、モデルのファインチューニングを必要とせずに、より高い精度と効率への道を開くことを示唆している。

なお、論文内では限界についても認めており、性能はベースモデルのコーディング流暢度に依存すること、また、SymPyでの定式化が困難な抽象的推論（例：合成幾何学の証明や複雑な組合せ論的議論）を必要とするタスクには苦戦すること、さらにシステムの信頼性はPythonインタープリタとSymPyライブラリの正確性に依存することを指摘している。