論文の概要: AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

• arxiv url: http://arxiv.org/abs/2607.16372v1
• Date: Fri, 17 Jul 2026 14:43:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-21 18:48:37.134188
• Title: AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
• Title（参考訳）: AoA: 再設計された言語の抽象構文木上での定理証明エージェント
• Abstract要約: LLMベースの証明エージェントは、この作業を容易にすることを約束するが、トークンの消費とAPIコストは依然として大きな障害である。 ミニF2F と NTP4VC-Pearl の共通成功セット上の Amazon の Isabelle Agent に対する AST (AoA) 上の emphAgent でのこの設計を実現する。 AoAはAPIコストを2.3--4.7x(正規化入力キャッシュ会計)に削減し、トークンを6.9倍、ツールコールを3.9--8.9倍削減し、1.4-2.0倍高速化した。
• 参考スコア（独自算出の注目度）: 12.171491995365086
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.
• Abstract（参考訳）: 対話的定理証明(英語版)(ITP)は、プログラム検証と形式化された数学の基盤となるが、その手作業はスケーラビリティを制限する。 LLMベースの証明エージェントは、この作業を容易にすることを約束するが、トークンの消費とAPIコストは依然として大きな障害である。 現在のエージェントはシリアライズされた具体的な構文で動作し、ソーステキストとして証明を出力し、別々の行数ベースのクエリを通じて証明状態を回復します。 この具体的な構文への依存は、LLMベースの証明でSOTAに到達した最近の証明言語であるMinilangの採用を阻害するが、LLMのトレーニングコーパスには新すぎる。 モデルでは、MinilangのASTのJSON表現として、 – ツールコールのLLMにネイティブな -- として証明を提供し、証明操作とステートを1つの証明ツリーに融合するツリー編集モデルを通じて、証明を駆動します。 この設計は, AST 上の \emph{Agent over AST} (AoA) で実現している。 Amazonの miniF2F と NTP4VC-Pearl の共通成功セットに対して、AoA は API コストを 2.3--4.7x (正規化入力キャッシュ会計) 削減し、2.9--6.9x のトークンと 3.9--8.9x のツールコールを削減し、1.4-2.0x の高速化を実現した。

関連論文リスト

• RepoReasoner: Evaluating Repository-Level Code Reasoning Ability of Long-Context Language Models [54.53236295237077]
  リポジトリレベルのコード推論を評価するベンチマークであるRepoReasonerを紹介します。 出力予測は、ファイル間でのきめ細かいステートフルな実行推論を計測します。 Call Chain Predictionは、ノイズの多いコンテキスト下での高レベルのアーキテクチャ依存性の理解を評価する。
  論文  参考訳（メタデータ） (2026-07-28T17:12:41Z)
• Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof [0.0]
  LLM駆動のランタイムによってどのようにスキルが消費されるかに忠実なスキル行動に関する正確なセマンティクスを提供します。 本稿では,定式化や定式化によるスキル向上を両立させる構成可能な3つの手法を提案する。 これら3つのメソッドに加えて、バンドルプロデューサと再チェッカーは、オープンソースエンクロードフレームワークのゼロ依存JavaScriptモジュールとして出荷される。
  論文  参考訳（メタデータ） (2026-05-09T19:27:38Z)
• HCRE: LLM-based Hierarchical Classification for Cross-Document Relation Extraction with a Prediction-then-Verification Strategy [54.91468501159335]
  文書間関係抽出 (RE) は, 異なる文書に存在する頭部尾部エンティティ間の関係を識別することを目的としている。 本稿では,各レベルでの多視点検証により信頼性を向上させる推論戦略を提案する。
  論文  参考訳（メタデータ） (2026-04-09T07:55:27Z)
• Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification [21.423111823947867]
  本稿では,システムレベルの検証プロジェクトの証明検索の自動化を目的とした,ニューロシンボリックな証明生成フレームワークを提案する。 このフレームワークは、証明状態に対して最優先のツリー探索を行い、次の候補証明ステップのためにLLMを何度もクエリする。 さらなるベンチマークの結果は強力な一般化を示し、スケーラブルな自動ソフトウェア検証への道のりを示している。
  論文  参考訳（メタデータ） (2026-03-20T07:45:49Z)
• ESAA: Event Sourcing for Autonomous Agents in LLM-Based Software Engineering [0.0]
  本稿では,ESAA(Event Sourcing for Autonomous Agents)アーキテクチャについて述べる。 アーキテクチャは、イベントソーシングパターンにインスパイアされた、認知意図とプロジェクトの状態突然変異を分離する。 2つのケーススタディは、アーキテクチャを検証し、単一エージェントのシナリオを超えたアーキテクチャのスケーラビリティの実証的な証拠を提供する。
  論文  参考訳（メタデータ） (2026-02-26T16:45:59Z)
• TabTracer: Monte Carlo Tree Search for Complex Table Reasoning with Large Language Models [10.584052101655537]
  TabTracerは、中間テーブル状態上のマルチステップツールコールをコーディネートするエージェントフレームワークである。 型付き操作と軽量数値およびフォーマットチェックによるステップレベルの検証を実施する。 予算を意識したプルーニング、重複解消、トークンコスト削減のためのモノトニティゲートによる状態ハッシュによる冗長性を低減する。
  論文  参考訳（メタデータ） (2026-02-15T10:39:43Z)
• ConvexBench: Can LLMs Recognize Convex Functions? [70.53167848190624]
  凸解析は数学の現代的な分野であり、多くの応用がある。 大規模言語モデル(LLM)が研究レベルの数学と科学を自動化し始めるにつれ、LLMが凸性を理解し、推論する能力を示すことが重要である。 我々は,LLMが深い機能的構成下での象徴的対象の凸性を識別できるかどうかを,スケーラブルで機械的に検証できるベンチマークであるcbを紹介する。
  論文  参考訳（メタデータ） (2026-02-01T07:41:17Z)
• Don't Get Lost in the Trees: Streamlining LLM Reasoning by Overcoming Tree Search Exploration Pitfalls [83.89771461061903]
  検証者による木探索アルゴリズムの最近の進歩は、大規模言語モデル(LLM)の推論能力を大幅に向上させた。 検証者による木探索アルゴリズムの最近の進歩は、大規模言語モデル(LLM)の推論能力を大幅に向上させた。 意味論的に等価なコンテンツを持つ冗長な状態による$textitover-Exploration$と、検証器のスコアリングにおける高いばらつきに起因する$textitunder-Exploration$である。 各種木探索アルゴリズムに適合するフレキシブルなプラグアンドプレイシステムであるFETCHを提案する。
  論文  参考訳（メタデータ） (2025-02-16T16:12:01Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Laurel: Unblocking Automated Verification with Large Language Models [2.6942525604796366]
  大規模言語モデルを用いてアサーションを自動的に生成するツールであるLaurellを提案する。 実世界の3つのDafnysから抽出した複雑な補題のデータセットであるDafnyGymを、新しいベンチマークで評価した。
  論文  参考訳（メタデータ） (2024-05-27T03:26:01Z)
• Tree Prompting: Efficient Task Adaptation without Fine-Tuning [112.71020326388029]
  Tree Promptingはプロンプトの決定ツリーを構築し、複数のLMコールをリンクしてタスクを解決する。 分類データセットの実験により、Tree Promptingは競合するメソッドよりも精度が向上し、微調整と競合することが示された。
  論文  参考訳（メタデータ） (2023-10-21T15:18:22Z)
• Allies: Prompting Large Language Model with Beam Search [107.38790111856761]
  本研究では,ALIESと呼ばれる新しい手法を提案する。 入力クエリが与えられた場合、ALLIESはLLMを活用して、元のクエリに関連する新しいクエリを反復的に生成する。 元のクエリのスコープを反復的に精錬して拡張することにより、ALLIESは直接検索できない隠れた知識をキャプチャし、利用する。
  論文  参考訳（メタデータ） (2023-05-24T06:16:44Z)

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

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