Lean4AgenticRL、Lean4による多層プロセス報酬でエージェント強化学習を改善

導入

ソフトウェア開発やターミナル操作をLLMエージェントに任せる場合、最終的な答えだけを評価しても、途中で何が起きたのかは分かりません。エージェントは課題を分解し、適切なツールを選び、出力を解釈しながら、複数段階の処理を進める必要があります。しかし、現在のエージェント強化学習では、最終的な成功・失敗を中心とする報酬設計が多く、ツール呼び出しや中間段階への監督は限られています。

arXivで公開されたLean4AgenticRLは、この問題に形式手法を用いて取り組むフレームワークです。Lean4を共通の形式化スキーマとして利用し、オープンエンドなエージェント行動に対して、複数レベルのプロセス報酬を与えます。論文では、この仕組みを用いてLAR-9BとLAR-27Bを学習しています。

主なポイント

• 複数レベルの報酬を導入。 最終成果だけでなく、低レベルのツール呼び出しと、中レベルのワークフロー段階を評価対象にします。
• 問題ごとのワークフローを構築。 各課題に固有のワークフローを作り、エージェントの自律性と実行の制御可能性のバランスを取る設計です。
• 形式化と検証を統合。 ワークフローを形式的に記述し、汎用ハーネスでエージェントの行動を検証して、報酬のアノテーションにつなげます。
• 段階正規化GRPOを使用。 多層報酬をworkflow-stage-normalized GRPOに組み込み、異なる段階の報酬を学習に利用します。
• 端末タスクで結果を報告。 LAR-27BはTerminalBench-2.1で77.3%を達成しました。LAR-9B/27Bは基盤モデルを平均9.89%上回り、著者らが把握する同程度の規模の次点モデルに対して5.07%の差を示したとされています。

意義と今後の論点

この研究の重要な点は、エージェントの行動を「最終的に成功したか」だけでなく、「途中の選択が妥当だったか」「各段階を完了できたか」という単位に分解しようとしたことです。長いツール利用の軌跡では、失敗の原因が不適切なコマンド、段階の移行ミス、終盤でのエラーのいずれなのかを区別できる方が、学習信号を設計しやすくなります。

Lean4の利用は、形式手法をプログラム検証や数学的推論だけでなく、オープンなエージェント行動の監督にも広げる試みといえます。検証可能なワークフローを用意できれば、長期タスクの学習過程をより分析しやすくなる可能性があります。

一方、提供された資料だけでは、異なるタスクやワークフローへの汎化、より大規模なモデルでの安定性までは判断できません。課題ごとのワークフロー作成にかかるコスト、検証の計算負荷、形式化が探索の自由度に与える影響も、今後検討すべき論点です。

Lean4AgenticRLは、形式検証、プロセス報酬、エージェント強化学習を接続し、長いツール利用で生じる報酬の疎さに対する一つの実践的な方向性を示しています。

出典：arXiv