大規模言語モデル（LLM）を用いて自然言語を一階述語論理に変換し、定理証明器で推論する手法は、正しく変換すれば正確な結果を得ることができる。しかしながら、実際にはLLMによる変換時に様々な変換ミスが発生し、自然言語のまま推論させる場合と比べても精度が低下してしまうことがある。
本研究では、自然言語推論のベンチマークデータを用い、前提と結論の段階的形式化などの複数の変換戦略と、複数のLLMの適用による比較実験を行う。実験から、変換誤りの抑制に与える影響、自然言語のままLLMで推論する場合も含めた各アプローチの特性と有効範囲について報告する。