論文の概要: FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification

• arxiv url: http://arxiv.org/abs/2610.00885v1
• Date: Thu, 01 Oct 2026 01:00:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-03 01:19:23.835922
• Title: FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
• Title（参考訳）: Forall-Lean-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification (特集:情報工学)
• Abstract要約: FORALLLEAN-AGENTは、形式数学とソフトウェア検証における監査可能な推論のためのフレームワークである。 独立したワークスペース、リーンツール、ステートメント比較による新たなレビュー、公理監査、独立した証明チェックを組み合わせたものだ。 We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification. The framework combines isolated workspaces, Lean tools, and fresh review with statement comparison, axiom audits, and independent proof checking where supported. Verification evidence and reviewer decisions are bound to the same candidate artifact, making acceptance traceable. We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track. On the 100-task VeriSoftBench subset, integration with FORALLLEAN-AGENT raises benchmark-rule success from 93 to 100 for GPT-5.6 Sol at low effort while reducing cost from $69 to $62. The PutnamBench evaluation accepts all 672 problems at an average of $4.72 each. These results show that agent harness design can improve correctness and efficiency while providing evidence beyond aggregate solve counts.
• Abstract（参考訳）: コーディングエージェントはリーンの証明開発をますます自動化しますが、成功したコンパイルだけでは、候補が許容できる前提の下で意図したステートメントを証明することは証明できません。 ForALL-LEAN-AGENTは,形式数学およびソフトウェア検証における聴覚的推論のためのフロントエンドに依存しないフレームワークである。 このフレームワークは、独立したワークスペース、リーンツール、ステートメント比較、公理監査、サポート対象の独立した証明チェックを備えた新しいレビューを組み合わせたものだ。 検証証拠とレビュアーの決定は、同じ候補アーティファクトに拘束され、受け入れが追跡可能である。 We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track。 100タスクのVeriSoftBenchサブセットでは、FOALLLEAN-AGENTとの統合により、ベンチマークルルが93から100に上昇し、GPT-5.6ソルは、コストを69から62に削減した。 パットナムベンチの評価では、平均4.72ドルで672の問題を全て受け入れている。 これらの結果から, エージェントハーネス設計は, 集合解数を超える証拠を提供しながら, 精度と効率を向上できることが示された。

関連論文リスト

• VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks [56.74345405508208]
  LLMエージェントはますます複雑で長期のタスクをこなし、そのアウトプットを検証することがますます困難になっている。 本研究では, 基準応答へのアクセスや試験時の潤滑油の分解を行わずに, 固定ベースモデルで検証能力を強化する方法について検討する。 コンセンサスによってエラーを隠蔽できる一方で、不一致はしばしば正しい代替手段を公開することに気付きました。 これらの観察はVeriHarnessを動機付け、ジェネレータが使用する基礎となるLLMを、ワークスペース、エビデンスツール、再利用可能な検証スキルを与えることによって、エージェント検証器に変える。
  論文  参考訳（メタデータ） (2026-10-01T03:02:17Z)
• SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? [39.004582663385364]
  Benchprooferは、既知の正しいパッチでコーディングタスクを正式に認証されたパイプラインに変換するパイプラインです。 SWE-bench Verified に適用すると SWE-Proof が得られる。
  論文  参考訳（メタデータ） (2026-09-18T01:16:53Z)
• CFAgentBench: A Reproducible Environment and Benchmark for Autonomous Construction-Finance Agents [0.0]
  CFAgentBenchは、自律的な建設ファイナンスエージェントのベンチマークである。 8つのドメインと77のファミリーにまたがる1014のマシングレード可能なタスク仕様を含んでいる。 最強のエージェントはpass1 = 0.67に達するが、pass5 = 0.38のみである。
  論文  参考訳（メタデータ） (2026-06-20T11:34:52Z)
• FinVerBench: Benchmark Validity and Calibration in Large Language Model Financial Statement Verification [0.0]
  FinVerBenchは、ファイナンシャルステートメント検証のためのベンチマークおよび妥当性調査である。 SEC 10-K の S&P 500 社への提出書類から作成されている。
  論文  参考訳（メタデータ） (2026-05-28T08:30:15Z)
• $V_1$: Unifying Generation and Self-Verification for Parallel Reasoners [69.66089681814013]
  $V_$は、効率的なペアワイドランキングを通じて生成と検証を統合するフレームワークである。 V_$-Inferはポイントワイド検証でPass@1を最大10%改善する。 V_$-PairRLは、標準のRLとポイントワイドのジョイントトレーニングよりも、テストタイムのスケーリングが7ドル--9%で向上する。
  論文  参考訳（メタデータ） (2026-03-04T17:22:16Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)
• Proving the Coding Interview: A Benchmark for Formally Verified Code Generation [3.5319285228327417]
  FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムの記述と正確性を証明するための4715サンプルのベンチマークである。 我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
  論文  参考訳（メタデータ） (2025-02-08T22:54:58Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。