論文の概要: Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics

• arxiv url: http://arxiv.org/abs/2606.17581v1
• Date: Tue, 16 Jun 2026 06:43:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-17 17:15:32.312107
• Title: Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
• Title（参考訳）: Visored: LLM生成数学のための制御されたNatural-Language Prover
• Authors: Xiyu Zhai, Xinyi Chen, Yiping Wang, Runlong Zhou, Liao Zhang, Simon S. Du,
• Abstract要約: 我々は LLM (および人間) が数学を書く傾向を軸に設計された依存型型証明器を提案する。 その中核となる設計選択は、数学の自然言語を模倣する表面と、教科書が省略するルーチンステップを閉じるルール駆動の自動化層である。 初期の実験では、証明器固有のトレーニングデータなしでも、LLMはminiF2Fベンチマークで効果的に使用することができることが示唆された。
• 参考スコア（独自算出の注目度）: 32.09940762546616
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/
• Abstract（参考訳）: 我々は、LLM(と人間)が数学を書く傾向がある方法に基づいて設計され、LeanやRocqといった既存のシステムを補完する依存型ベースの証明器を提案する。 その中核となる設計選択は、数学的自然言語を模倣する表面と、教科書が省略するルーチンステップを閉じるルール駆動の自動化層である。 初期の実験では、証明器固有のトレーニングデータなしでも、LLMはminiF2Fベンチマークで効果的に使用することができることが示唆された。 Lean output Exerpts: https://github.com/xiyuzhai-husky-lang/visored/

関連論文リスト

• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• Tuna: Instruction Tuning using Feedback from Large Language Models [74.04950416204551]
  本稿では,新しいテキスト確率的ランキングとテキストコンテクスチュアルランキングを用いた命令調整型大規模言語モデルの微調整を提案する。 確率的ランク付けにより、教師のLCMから高品質で低品質なレスポンスの相対的なランク付けを継承することができる。 一方、文脈的ランキングを学習することで、より強いLLMの文脈的理解能力を用いて、モデルが独自の応答分布を洗練できる。
  論文  参考訳（メタデータ） (2023-10-20T09:55:06Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Coarse-Tuning Models of Code with Reinforcement Learning Feedback [0.0]
  コード上で事前訓練されたLarge Language Models (LLM) が、プログラム合成の主流のアプローチとして登場した。 コードの品質を評価する接地関数からのフィードバックを用いて、強化学習により事前学習したLLMをさらに訓練するRCCFを提案する。
  論文  参考訳（メタデータ） (2023-05-25T22:09:08Z)

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

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