論文の概要: LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
- arxiv url: http://arxiv.org/abs/2507.14722v1
- Date: Sat, 19 Jul 2025 18:50:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-22 20:51:32.019916
- Title: LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
- Title（参考訳）: LeanTree: リーン4における要因付き状態でのWhite-Box Proof Searchの高速化
- Authors: Matěj Kripner, Michal Šustr, Milan Straka,
- Abstract要約: LeanTreeは、複雑な証明状態をシンプルで独立したブランチに分解する、Lean 4言語で構築されたツールです。
予備的な結果は、ホワイトボックスが一部の設定でブラックボックスの代替よりも優れていることを示唆している。
- 参考スコア（独自算出の注目度）: 0.9619839248195652
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Large language models (LLMs) have recently emerged as a promising heuristic for ATP, but they lack correctness guarantees and thus require interaction with a proof verifier. Such interactions typically follow one of two approaches: black-box interaction, which does not utilize intermediate proof states, or white-box approaches, which allow for incremental proof construction and examination of intermediate states. While black-box approaches have directly benefited from recent LLM advances, white-box methods have comparatively lagged behind. In this paper, we address this gap by introducing LeanTree, which consists of (i) a tool built in the Lean 4 language that factorizes complex proof states into simpler, independent branches, and (ii) a dataset of these factorized intermediate states. Our white-box tooling offers several advantages over black-box approaches: it simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient reuse of states, and provides feedback in case of errors. Our preliminary results hint that white-box approaches outperform black-box alternatives in some settings.
- Abstract（参考訳）: 自動定理証明(ATP、Automated theorem Proving)は、人工知能の誕生以来、古典的な問題となっているが、その膨大な状態と行動空間のため、依然として困難である。
大規模言語モデル(LLM)は、最近ATPの有望なヒューリスティックとして登場したが、正確性保証が欠如しており、証明検証器との相互作用が必要である。
このような相互作用は通常、中間証明状態を使用しないブラックボックス相互作用と、中間状態の漸進的な証明構築と検証を可能にするホワイトボックスアプローチの2つのアプローチの1つに従う。
ブラックボックスのアプローチは最近のLCMの進歩から直接恩恵を受けているが、ホワイトボックスの手法は比較的遅れを取っている。
本稿では,LeanTreeを導入することで,このギャップに対処する。
i) 複雑な証明状態を単純で独立したブランチに分解するLean 4言語で構築されたツール。
(ii)これらの因子化中間状態のデータセット。
評価を単純化し、必要なコンテキストを減らし、よりリッチなトレーニングデータを生成し、複数の状態にまたがる並列検索を可能にし、状態の効率的な再利用をサポートし、エラー発生時にフィードバックを提供する。
予備的な結果は、ホワイトボックスが一部の設定でブラックボックスの代替よりも優れていることを示唆している。
関連論文リスト
- Solving Inequality Proofs with Large Language Models [46.71658812761115]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - Auditing Black-Box LLM APIs with a Rank-Based Uniformity Test [24.393978712663618]
APIプロバイダは、コスト削減やモデル動作の不正な変更のために、量子化または微調整の亜種を慎重に提供することができる。
そこで我々は,ブラックボックスLLMの挙動等式を局所的に展開した認証モデルに検証できるランクベース均一性試験を提案する。
我々は、量子化、有害な微調整、脱獄プロンプト、完全なモデル置換など、さまざまな脅威シナリオに対するアプローチを評価する。
論文 参考訳（メタデータ） (2025-06-08T03:00:31Z) - Unsupervised Visual Chain-of-Thought Reasoning via Preference Optimization [69.29207684569695]
CoT推論は多モーダル大言語モデル(MLLM)の解釈可能性と問題解決能力を大幅に向上させる
既存のアプローチはテキストCoTに重点を置いており、視覚的手がかりを活用する能力を制限する。
本稿では、優先最適化による画像レベルのCoT推論のための新しいフレームワークであるUnsupervised Visual CoT (UV-CoT)を紹介する。
論文 参考訳（メタデータ） (2025-04-25T14:48:18Z) - Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [60.881609323604685]
ブラックボックスAPIを通じてアクセスされるLarge Language Models (LLM)は、信頼の課題をもたらす。
ユーザーは、宣伝されたモデル機能に基づいたサービスの料金を支払う。
プロバイダは、運用コストを削減するために、特定のモデルを安価で低品質の代替品に隠蔽的に置き換えることができる。
この透明性の欠如は、公正性を損なうとともに、信頼を損なうとともに、信頼性の高いベンチマークを複雑にする。
論文 参考訳（メタデータ） (2025-04-07T03:57:41Z) - MAFT: Efficient Model-Agnostic Fairness Testing for Deep Neural Networks via Zero-Order Gradient Search [20.48306648223519]
モデル非依存フェアネステスト(MAFT)と呼ばれる新しいブラックボックス個別フェアネステスト法を提案する。
我々は,MAFTが大規模ネットワークへの適用性を向上しつつ,最先端のホワイトボックス手法と同等の有効性を実証した。
論文 参考訳（メタデータ） (2024-12-28T09:07:06Z) - A Probabilistic Framework for LLM Hallucination Detection via Belief Tree Propagation [72.93327642336078]
本稿では,幻覚検出のための確率的フレームワークであるBelief Tree Propagation (BTProp)を提案する。
BTPropは、親ステートメントを子ステートメントに分解することで、論理的に関連するステートメントの信念ツリーを導入する。
複数の幻覚検出ベンチマークにおいて,AUROCとAUC-PRにより評価された基準線を3%-9%改善する。
論文 参考訳（メタデータ） (2024-06-11T05:21:37Z) - Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。
提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文 参考訳（メタデータ） (2024-05-24T17:11:27Z) - Theoretically Achieving Continuous Representation of Oriented Bounding Boxes [64.15627958879053]
本論文は,オブジェクト指向境界ボックス表現における不連続性を完全に解決しようとする試みである。
本研究では,既存の検出器に容易に統合可能なCOBB(Continuous OBB)という新しい表現法を提案する。
OOD評価のためのオープンソースのディープラーニングフレームワークJittorの検出ツールボックスJDetをベースとした,モジュール化されたベンチマークを開発した。
論文 参考訳（メタデータ） (2024-02-29T09:27:40Z) - Ten Words Only Still Help: Improving Black-Box AI-Generated Text
Detection via Proxy-Guided Efficient Re-Sampling [19.780068724002888]
POGERは、ブラックボックスAIGT検出のためのプロキシ誘導効率的な再サンプリング手法である。
マクロF1のすべてのベースラインをブラックボックス、部分的なホワイトボックス、アウト・オブ・ディストリビューション設定で上回る。
論文 参考訳（メタデータ） (2024-02-14T14:32:16Z) - Language Models as Black-Box Optimizers for Vision-Language Models [62.80817942316398]
Webスケールデータセットで事前トレーニングされた視覚言語モデル(VLM)は、最小限のデータで微調整された場合、下流タスクに顕著な機能を示す。
我々は,自然言語のプロンプトを通じてVLMを最適化するためのブラックボックスアプローチを開発することを目指している。
論文 参考訳（メタデータ） (2023-09-12T04:03:41Z) - PromptBoosting: Black-Box Text Classification with Ten Forward Passes [61.38341243907045]
PromptBoostingは、LMのパラメータ、勾配、隠された表現にアクセスすることなく、ニューラルネットワークモデル(LM)からテキスト分類器を構築するためのクエリ効率のよい手順である。
実験によると、PromptBoostingは複数のブラックボックスのいくつかのショット分類タスクで最先端のパフォーマンスを達成し、既存のブラックボックスメソッドよりも10倍速くトレーニングしながら、少数ショットと標準学習のパラダイムの両方で完全な微調整をマッチまたは上回っている。
論文 参考訳（メタデータ） (2022-12-19T06:04:54Z) - Automating Reasoning with Standpoint Logic via Nested Sequents [0.0]
スタンドポイント論理は多面的アプローチを提唱し、多種多様で恐らく矛盾するスタンドポイントの選択による推論を許容する。
非決定論的証明探索アルゴリズムを用いて視点推論を自動化する方法を示す。
論文 参考訳（メタデータ） (2022-05-05T16:27:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。