論文の概要: Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints

• arxiv url: http://arxiv.org/abs/2604.15713v1
• Date: Fri, 17 Apr 2026 05:34:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-20 22:00:19.750154
• Title: Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
• Title（参考訳）: イザベルでタイプする! 人間のヒントからAIエージェントを引き出し、機械化し、一般化する
• Authors: Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel,
• Abstract要約: 階数 1 の多型 $$calculus 項に対する完全および最小型アノテーションの問題について検討する。 私たちの開発は、人間駆動とAI駆動の形式化を特徴とする一連の実験です。
• 参考スコア（独自算出の注目度）: 10.25873520360893
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annotations for rank-one polymorphic $λ$-calculus terms, as used in Isabelle. Building on prior work by Smolka, Blanchette et al., we give a metatheoretical account of the problem, with a full formal specification and proofs, and formalize it in Isabelle/HOL. Our development is a series of experiments featuring human-driven and AI-driven formalization workflows: a human and an LLM-powered AI agent independently produce pen-and-paper proofs, and the AI agent autoformalizes both in Isabelle, with further human-hinted AI interventions refining and generalizing the development.
• Abstract（参考訳）: 型アノテーションは、リパースと型推論の下でそれらの意味を保存する方法で用語を印刷する際に必須である。 階数 1 の多型 $λ$-calculus 項に対する完全および最小型アノテーションの問題をイザベルで用いられるように研究する。 Smolka, Blanchette et al の先行研究に基づいて、問題のメタ理論的な説明を行い、完全な形式的な仕様と証明を与え、Isabelle/HOL で形式化する。 我々の開発は、人間駆動とAI駆動の形式化ワークフローを特徴とする一連の実験である。人間とLLM駆動のAIエージェントは、独立してペンと紙の証明を作成し、AIエージェントは、イザベルで両方のオートフォーマル化を行い、さらに人間によるAI介入によって、開発を洗練し、一般化する。

関連論文リスト

• Mining Type Constructs Using Patterns in AI-Generated Code [1.2107297090229683]
  AIが、型関連プログラミングタスクにおいて、人間より本質的に優れているかどうかはまだわからない。 TypeScriptプロジェクトのドメインで、これらの質問に答える最初の経験的分析を提示します。 驚くべきことに、これらすべての問題にもかかわらず、AgenticプルリクエストはTypeScriptの人間よりも1.8倍高い受け入れ率を持つ。
  論文  参考訳（メタデータ） (2026-02-20T03:17:42Z)
• Lemmanaid: Neuro-Symbolic Lemma Conjecturing [4.821473821650318]
  レマナイド(Lemmanaid)は、実用的な神経象徴性レムマ注射器具である。 LLM(Large Language Models)とシンボリックメソッドを組み合わせる。 我々はIsabelle証明アシスタントの証明ライブラリ上で評価する。
  論文  参考訳（メタデータ） (2025-04-07T11:30:36Z)
• Memento No More: Coaching AI Agents to Master Multiple Tasks via Hints Internalization [56.674356045200696]
  本稿では,複雑なメモシステムや事前の高品質な実演データを必要としない,複数のタスクに対する知識とスキルを取り入れたAIエージェントの訓練手法を提案する。 このアプローチでは,エージェントが新たな経験を収集し,ヒントの形で人間から補正フィードバックを受け取り,このフィードバックを重みに組み込む,反復的なプロセスを採用している。 Llama-3をベースとしたエージェントに実装することで,数ラウンドのフィードバックの後,高度なモデルGPT-4oとDeepSeek-V3をタスクセットで性能向上させる手法の有効性を実証する。
  論文  参考訳（メタデータ） (2025-02-03T17:45:46Z)
• Pangu-Agent: A Fine-Tunable Generalist Agent with Structured Reasoning [50.47568731994238]
  人工知能(AI)エージェント作成の鍵となる方法は強化学習(RL)である 本稿では,構造化推論をAIエージェントのポリシーに統合し,学習するための一般的なフレームワークモデルを提案する。
  論文  参考訳（メタデータ） (2023-12-22T17:57:57Z)
• Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
  本研究では、Boundless DASを用いて、命令に従う間、大規模言語モデルにおける解釈可能な因果構造を効率的に探索する。 私たちの発見は、成長し、最も広くデプロイされている言語モデルの内部構造を忠実に理解するための第一歩です。
  論文  参考訳（メタデータ） (2023-05-15T17:15:40Z)
• Principle-Driven Self-Alignment of Language Models from Scratch with Minimal Human Supervision [84.31474052176343]
  ChatGPTのような最近のAIアシスタントエージェントは、人間のアノテーションと人間のフィードバックからの強化学習を教師付き微調整(SFT)に頼り、アウトプットを人間の意図に合わせる。 この依存は、人間の監督を得るために高いコストがかかるため、AIアシスタントエージェントの真の可能性を大幅に制限することができる。 本稿では,AIエージェントの自己調整と人間監督の最小化のために,原則駆動推論とLLMの生成能力を組み合わせたSELF-ALIGNという新しいアプローチを提案する。
  論文  参考訳（メタデータ） (2023-05-04T17:59:28Z)

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

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