LLMSR@XLLM25: SWRV: Empowering Self-Verification of Small Language Models through Step-wise Reasoning and Verification
- 小規模言語モデルの連鎖思考を、問題条件の抽出、推論ステップの抽出、各ステップの検証に分けて扱う枠組みを示す。
- Step-Wise Reasoning and Verification (SWRV) は、Llama-3-8B-Instruct を中心に、プロンプト、少量データによる LoRA 微調整、Z3 ソルバを組み合わせる。
- LLMSR データセット上では、単純な直接推論よりも解析と検証の性能が上がり、とくに外部の記号ソルバを使う検証が有効であることを報告する。
論文の面白いところ
この論文は、言語モデルの答え全体を一度に信じるのではなく、途中の推論を小さな単位に切り分けて確かめる。対象は、巨大なモデルではなく Llama-3-8B-Instruct のような比較的小さなモデルである。大きなモデルなら自己修正できる場合がある、という見方に対し、本論文は小さなモデルでは検証器そのものが弱点になると見る。そのため、推論を生成するモデルと、その推論を検査する仕組みを分けている。Parser は問題文から条件を抜き出し、Chain-of-Thought (CoT) から statement と evidence を取り出す。Verifier は、その evidence から statement が導けるかを True または False で判定する。さらに、判定を言語モデルだけに任せず、Satisfiability Modulo Theories (SMT) ソルバである Z3 に渡す経路を用意している。この構成により、自然言語の推論を、形式論理に近い検査へ接続しようとしている点が本論文の特色である。実験規模は大きくないが、低資源条件で何を分け、どこを外部ツールに任せるべきかが見えやすい。
問題設定
扱う課題は、論理問題に対する言語モデルの CoT を、検査可能な構造に直すことである。入力は自然言語の論理問題 Q と、その問題を解くために言語モデルが生成した CoT である。出力は二つに分かれる。第一に、問題文から必要条件を抽出した question parsing、すなわち QP = {c1, ..., cn} である。第二に、CoT 内の各推論を statement、evidence、検証結果からなる組にした cot parsing、すなわち CP = {(s1, e1, v1), ..., (sm, em, vm)} である。ここで si は推論で主張された文、ei はそれを支える根拠、vi は True または False の検証ラベルである。評価では、問題条件の抽出、statement の抽出、statement と evidence の対応付け、最後の含意判定を別々の指標で測る。データは LogiQA を土台にした LLMSR タスクであり、利用できる注釈例は 24 件に限られる。したがって、十分な教師データで一つの大きなモデルを学習する設定ではない。論文の関心は、少数例でも、推論過程をどこまで構造化して検証できるかにある。
提案手法
提案手法は Step-Wise Reasoning and Verification (SWRV) と呼ばれる。全体は Parser と Verifier の二段階からなる。Parser には question parser、CoT parser、combined parser の三種があり、問題だけ、CoT だけ、または両方を同時に処理する。プロンプトでは、問題文中の条件をできるだけ元の表現のまま抽出し、CoT から statement と evidence の対を取り出すように指示する。少量の教師データを使う場合は、先にプロンプトで得た解析結果を入力に加え、モデルに修正の仕方を学ばせる。基盤モデルには Llama-3-8B-Instruct を用い、LoRA により 24 件のサンプルで微調整する。Verifier は二通りで、ひとつは Llama に statement と evidence を与えて直接 True/False を答えさせる方法である。もうひとつは Z3-Augmented Verifier で、自然言語の条件と推論ステップを中間表現に変換し、Z3 が扱える論理式へ落とす。Z3 の式が壊れている場合には、エラーを言語モデルへ戻し、最大 3 回まで自己修正させる。最後に、Z3 の出力を規則ベースで自然言語側の True/False に対応させる。
結果
実験では、何も工夫せず Llama-3-8B-Instruct に直接解析と検証をさせる場合をベースラインとした。Table 1 では、ベースラインの Question_F1 は 0.5702、Statement_F1 は 0.3341、Statement_Evidence_F1 は 0.0852、Reasoning_F1 は 0.0326 である。プロンプトを調整した Base Question Parser は Question_F1 を 0.7299 まで上げた。Base Combined Parser は Question_F1 0.7187、Statement_F1 0.4247、Statement_Evidence_F1 0.168 を得ている。検証だけを見ると、Llama Verifier の Reasoning_F1 は 0.067、O3-mini-high Verifier は 0.124、Z3 Verifier は 0.078 であった。論文は、Z3 の実行成功率を約 72% と報告している。著者らは、自然言語から論理式への変換が完全に成功すれば、Z3 系の検証は言語モデル単体の検証よりさらに高くなる可能性があると述べている。一方で、24 例だけで微調整した parser は、規則を入れたプロンプトによる parser を常に上回ったわけではない。これは、少数データでは複雑な解析規則を小規模モデルに内面化させにくいことを示している。
具体例
- 論文の例では、F、G、H、I、W、X、Y という 7 人の新兵を、通信兵、工兵、輸送兵に割り当てる論理問題を扱う。
- 問題文には、「H と Y は同じ兵科」「F と G は同じ兵科ではない」「X が輸送兵なら W は工兵」「F は工兵」などの条件がある。
- question parser は、これらの条件を question_parsing の配列として抜き出す。
- CoT には、「X は工兵ではないので通信兵または輸送兵である」といった途中の推論が書かれる。
- CoT parser は、この文を statement として取り出し、その根拠となる文を evidence として対応させる。
- Z3-Augmented Verifier は、recruits = EnumSort([F, G, H, I, W, X, Y]) のように登場人物を記号化する。
- 兵科も communications、engineering、transport のような記号にし、arm_of(X) != engineering などの式で条件を表す。
- 「X は通信兵または輸送兵である」という推論は、Or(arm_of(X) == communications, arm_of(X) == transport) のような式で検査される。
- このように、文章で書かれた CoT を、条件、主張、根拠、検証式へ分けることで、どの段階で推論が崩れたかを追いやすくしている。