論文の概要: Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
- arxiv url: http://arxiv.org/abs/2610.15258v1
- Date: Sun, 11 Oct 2026 01:10:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-15 21:06:15.18091
- Title: Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
- Title（参考訳）: シークエントプロバー:形式的、チェック可能なSMT推論のためのトレーニングエージェント
- Abstract要約: 本稿では,検証用言語モデルエージェントのファミリーであるSequent-Proverと,それらを生成するポストトレーニングフレームワークを紹介する。
筆者らのレシピ, 検証条件付きトラジェクトリ蒸留法, うるさい教師の提案方針からのブートストラップについて検討した。
37のベンチマークとモデルファミリー当たりの7,254の問題により、4Bモデル毎の精度は85.6%から97.0%に向上した。
また、平均SMTコールを4.10から2.52に減らし、トークンは18.97kから12.72kに減らした。
- 参考スコア（独自算出の注目度）: 35.98681317005019
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce Sequent-Prover, a family of verifier-using language-model agents, and the post-training framework that produces them. Agents reason in an executable SMT-LIB scratchpad: they write complete SMT-LIB programs, query Z3 across turns, inspect solver feedback, repair formalizations, and terminate with an explicit answer. Our recipe, verifier-conditioned trajectory distillation, bootstraps from a noisy teacher proposal policy by sampling multi-turn trajectories, retaining the successful tail that is correct, non-trivial, grounded, and executable, then applying supervised fine-tuning and trajectory-level preference optimization. Because solver success alone does not guarantee semantic faithfulness, we evaluate task accuracy, k-sample reliability, and SMT program quality. Across 37 benchmarks and 7,254 problems per model family, post-training raises the 4B model's per-attempt accuracy from 85.6% to 97.0% and four-sample all-correct reliability (pass^4}) from 64.1% to 91.7%. It also reduces average SMT calls from 4.10 to 2.52 and tokens per attempt from 18.97k to 12.72k. Sequent-Prover agents give answers backed by executable formal artifacts.
- Abstract（参考訳）: 本稿では,検証用言語モデルエージェントのファミリーであるSequent-Proverと,それらを生成するポストトレーニングフレームワークを紹介する。
エージェントは実行可能なSMT-LIBスクラッチパッドで、完全なSMT-LIBプログラムを書き、順番にZ3をクエリし、ソルバのフィードバックを検査し、形式を修復し、明確な答えで終了する。
筆者らのレシピは, 検証条件付きトラジェクトリ蒸留, マルチターントラジェクトリをサンプリングし, 正確で, 非自明で, 接地し, 実行可能で, 教師による微調整とトラジェクトリレベルの選好最適化を施した, ノイズの多い教師提案ポリシからのブートストラップである。
解法の成功だけでは意味的忠実性は保証されないので、タスク精度、kサンプル信頼性、SMTプログラムの品質を評価する。
37のベンチマークとモデルファミリー当たりの7,254の問題により、4Bモデル毎の精度は85.6%から97.0%に向上し、4サンプル全精度(pass^4})は64.1%から91.7%に向上した。
また、平均SMTコールを4.10から2.52に減らし、トークンは18.97kから12.72kに減らした。
シークエント・プロバーのエージェントは、実行可能な形式的なアーティファクトに裏打ちされた回答を与える。
関連論文リスト
- Cross-Benchmark Transfer from RL on Agentic Coding Tasks [0.13579757545152057]
多くの場合、コーディングエージェントは最後の1マイルで失敗する。機能の大部分を構築し、要件をドロップし、実装がすでに処理しているケースのみをテストし、無傷であるはずの動作を壊したり、未確認の仮定に対して検証する。
専門家が構築したエージェントコーディングタスクの強化学習がこのギャップを埋めるか、エージェントが学習するものがトレーニング分布を超えるのかを問う。
我々は,隠れフェール・ツー・パステストとパス・ツー・パステストによって評価された1,700のタスクと,専門家が書いた隠れバリデーションによって評価された700の端末タスクについて,Kim K2.7コードをポストトレーニングした。
論文 参考訳（メタデータ） (2026-10-01T01:12:24Z) - Agent Error Dataset: Scaling 50,000 Error--Diagnosis Pairs for Failure Analysis and Error-Aware Post-Training [45.727227890697556]
我々は,9,961のソースタスクから50,228のエラー診断ペアからなるエージェントエラーデータセット(AED)を紹介した。
5段階のAgenic Error-to-Trainingパイプラインは自然の故障を収集し、診断と修正案を生成し、記録された証拠と照合する。
アクタートレーニングのレシピの比較において、アクションオンリーの修復トレーニングは成功オンリーのトレーニングよりもWebShop-liteの方が6.67ポイント高い。
論文 参考訳（メタデータ） (2026-09-30T16:40:22Z) - MemToC: Benchmarking Memory-Tool Conflict Resolution in Large Language Models [49.47300047353726]
MemToCは、実行時ツールによるポストツール-リターン仲裁のベンチマークである。
MemToCは、542の質制御された事実質問から構築された6,504回の評価エピソードで構成されている。
オープンウェイトな7-9Bモデルでは、ツールが強く支配的なクローズドブックの回答を返す。
論文 参考訳（メタデータ） (2026-08-26T18:22:03Z) - Learning from Failure: Inference-Time Self-Improvement for Computer-Use Agents [80.03824805228719]
コンピュータ利用エージェントを開発する上での大きな課題は、大規模で高品質な軌道を収集することである。
我々は、失敗した軌道をエージェント改善に変換するデータ中心のパラダイムを提案する。
この手法をOSWorldベンチマーク上で,最先端のOpenCUA-72Bモデルを用いて検証する。
論文 参考訳（メタデータ） (2026-06-30T07:44:37Z) - Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
シャノン型エントロピーの不等式を証明することは情報理論の基本的な課題である。
我々は,原子実証のステップを微調整した小規模大規模言語モデルがこのプロセスを自動化することができるか検討する。
GPT-5.5は0ショットプロンプトで1.7%のサンプルを解き、Psitipは33.3%のサンプルを解いた。
論文 参考訳（メタデータ） (2026-06-04T05:43:12Z) - EnactToM: An Evolving Benchmark for Functional Theory of Mind in Embodied Agents [75.01735520608075]
既存のベンチマークは、直観的信念を問うことで、主にリテラル・オブ・マインド(ToM)をテストする。
EnactToMは, 3D 家庭で設定された300個のマルチエージェントタスクの進化ベンチマークである。
ハードスプリットでは、7つの評価されたフロンティアモデルすべてが機能的なタスク完了時に0.0%のPass3を獲得し、リテラルな信念プローブでは平均45.0%であった。
論文 参考訳（メタデータ） (2026-05-11T00:04:19Z) - TEMPO: Scaling Test-time Training for Large Reasoning Models [87.61789183311856]
テストタイムトレーニング(TTT)は、推論時間中にラベルのないテストインスタンスにモデルパラメータを適用する。
TTTフレームワークであるTEMPOを提案する。これは、ラベル付きデータセット上で定期的な批評家の再検討を行い、ラベル付き質問に対するポリシー修正をインターリーブする。
論文 参考訳（メタデータ） (2026-04-21T10:01:04Z) - Multi-Turn Reinforcement Learning for Tool-Calling Agents with Iterative Reward Calibration [0.0]
マルチターンタスクにおける強化学習を伴う訓練ツール呼び出しエージェントは依然として困難である。
本稿では,MT-GRPO と GTPO を用いて,現実的なカスタマーサービスタスクにおけるツールコールエージェントのトレーニングを行う。
論文 参考訳（メタデータ） (2026-04-03T08:36:03Z) - Solver-in-the-Loop: MDP-Based Benchmarks for Self-Correction and Behavioral Rationality in Operations Research [19.31559944205485]
運用 調査実践者は反復的なプロセスを通じて、不可能なモデルを日常的にデバッグする。
評価ループにtextbfsolver を配置するベンチマークを2つ導入する。
ドメイン固有のRLVRトレーニングによって、8BモデルがフロンティアAPIを越えられることが分かりました。
論文 参考訳（メタデータ） (2026-01-28T20:02:44Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。