論文の概要: Vibe Coding an LLM-powered Theorem Prover

• arxiv url: http://arxiv.org/abs/2601.04653v1
• Date: Thu, 08 Jan 2026 07:00:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-09 17:01:53.072068
• Title: Vibe Coding an LLM-powered Theorem Prover
• Title（参考訳）: LLMを用いたセオリームプローブのバイブ符号化
• Authors: Zhe Hou,
• Abstract要約: イザベルム(Isabellm)は、イザベル/HOLのLLMによる定理証明である。 コンシューマグレードコンピュータで動作するように設計されている。 最先端のLLMでさえ、意図した補充と修復のメカニズムを確実に実装するのに苦労していることがわかった。
• 参考スコア（独自算出の注目度）: 0.9272925490418525
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade computers. The system combines a stepwise prover, which uses large language models to propose proof commands validated by Isabelle in a bounded search loop, with a higher-level proof planner that generates structured Isar outlines and attempts to fill and repair remaining gaps. The framework includes beam search for tactics, tactics reranker ML and RL models, premise selection with small transformer models, micro-RAG for Isar proofs built from AFP, and counter-example guided proof repair. All the code is implemented by GPT 4.1 - 5.2, Gemini 3 Pro, and Claude 4.5. Empirically, Isabellm can prove certain lemmas that defeat Isabelle's standard automation, including Sledgehammer, demonstrating the practical value of LLM-guided proof search. At the same time, we find that even state-of-the-art LLMs, such as GPT 5.2 Extended Thinking and Gemini 3 Pro struggle to reliably implement the intended fill-and-repair mechanisms with complex algorithmic designs, highlighting fundamental challenges in LLM code generation and reasoning. The code of Isabellm is available at https://github.com/zhehou/llm-isabelle
• Abstract（参考訳）: 完全自動証明合成を行うIsabelle/HOLのLCMによる定理証明であるIsabellmを提案する。 Isabellm は Ollama や Gemini CLI などの API 上の任意のローカル LLM で動作する。 このシステムは、大きな言語モデルを用いて、Isabelleが検証した証明コマンドを有界探索ループで提案するステップワイズ証明器と、構造化されたIsarアウトラインを生成し、残りのギャップを埋め、修復しようとする高レベルな証明プランナーを組み合わせる。 このフレームワークには、戦術のビームサーチ、戦術リランカーMLとRLモデル、小さなトランスフォーマーモデルによる前提選択、AFPから構築されたIsar証明のためのマイクロRAG、および反例証明修復が含まれる。 すべてのコードは GPT 4.1 - 5.2, Gemini 3 Pro, Claude 4.5 で実装されている。 経験的に、Isabellmは、Sledgehammerを含むIsabelleの標準的な自動化を破るある種の補題を証明でき、LLM誘導の証明探索の実用的価値を実証することができる。 同時に、GPT 5.2 Extended Thinking や Gemini 3 Pro のような最先端の LLM でさえ、複雑なアルゴリズム設計で意図した補修機構を確実に実装することに苦労し、LLM コード生成と推論における根本的な課題を浮き彫りにした。 Isabellmのコードはhttps://github.com/zhehou/llm-isabelleで公開されている。

関連論文リスト

• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• 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)
• ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
  ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。 LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
  論文  参考訳（メタデータ） (2023-11-16T12:03:21Z)
• LLatrieval: LLM-Verified Retrieval for Verifiable Generation [67.93134176912477]
  検証可能な生成は、大きな言語モデル(LLM)がドキュメントをサポートするテキストを生成することを目的としている。 本稿では,LLatrieval (Large Language Model Verified Retrieval)を提案する。 実験により、LLatrievalは幅広いベースラインを著しく上回り、最先端の結果が得られることが示された。
  論文  参考訳（メタデータ） (2023-11-14T01:38:02Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)

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

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