論文の概要: Characterizing initial human-AI proof formalization workflows

• arxiv url: http://arxiv.org/abs/2606.04273v1
• Date: Tue, 02 Jun 2026 22:58:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-04 20:44:18.415359
• Title: Characterizing initial human-AI proof formalization workflows
• Title（参考訳）: 初期人間-AI証明形式化ワークフローの特徴付け
• Authors: Katherine M. Collins, Simon Frieder, Jonas Bayer, Jacob Loader, Jeck Lim, Peiyang Song, Fabian Zaiser, Lexin Zhou, Shanda Li, Sam Looi, Joshua B. Tenenbaum, Umang Bhatt, Adrian Weller, Jose Hernandez-Orallo, Cameron E. Freer, Valerie Chen, Ilia Sucholutsky,
• Abstract要約: AIシステムのコード生成能力の進歩と、証明を形式化し、検証する人々の能力を変えるための高度な数学的推論の約束への関与。 我々は、AIが人々のフォーマル化に与える影響について、混合メソッド分析を行う。 質的な調査では、人々の好みは多様であるが、形式化におけるAI支援に対する一般的な欲求が示されている。
• 参考スコア（独自算出の注目度）: 66.06866890889131
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: For centuries, human mathematicians have written proofs to substantiate their mathematical arguments; yet, the ability to automatically verify the validity of proofs has long been a challenge. Advances in AI systems' ability to generate code and engage in increasingly high-level mathematical reasoning promise to transform people's ability to formalize and thereby verify proofs. While many works focus on benchmarking the current frontier, we instead study how people use these tools. We conduct a mixed-methods analysis into the initial impact of AI on people's formalization workflows: what people claim they want, what they see as the barriers to those visions, and how they actually use and adapt AI in practice. A qualitative survey shows that people's preferences are diverse, but with a general desire for AI assistance in formalization that preserves high-level human control over the proof discovery process. To assess how people actually engage with AI for formalization under such limitations, we conduct a controlled user study in which participants formalize informal math problems and their proofs, with and without AI, across a range of mathematical problems at varying levels of difficulty and domains. Despite limitations of the tools at the time for autoformalization, participants tend to attain higher formalization accuracy when allowed access to AI tools than when formalizing on their own, with most participants flexibly choosing to use multiple different AI tools. Taken together, our work sheds light on the early stages of AI integration into formalization workflows, involving an intimate interplay of human and AI engagement.
• Abstract（参考訳）: 何世紀にもわたって、人間の数学者は数学的議論を裏付ける証明を書いてきたが、証明の妥当性を自動検証する能力は長年にわたって課題であった。 AIシステムのコード生成能力の進歩と、証明を形式化し、検証する人々の能力を変えるための高度な数学的推論の約束への関与。 多くの作業が現在のフロンティアのベンチマークに重点を置いていますが、その代わりに、これらのツールの使い方を研究しています。 私たちは、AIが人々のフォーマル化ワークフローに最初に与える影響について、混合メソッド分析を実施しています。 質的な調査では、人々の嗜好は多様であるが、証明発見プロセスに対する高度な人間の制御を維持するための形式化におけるAI支援に対する一般的な欲求が示されている。 このような制限下でAIが実際にどのように機能するかを評価するために、参加者が非公式な数学問題とその証明をAIなしで形式化する制御されたユーザスタディを、さまざまな難易度や領域の数学問題に対して実施する。 オートフォーマル化のためのツールの制限にもかかわらず、参加者はAIツールへのアクセスを許可するときに、独自のフォーマル化を行う場合よりも高いフォーマル化精度を得る傾向にあり、ほとんどの参加者は複数の異なるAIツールを使用することを柔軟に選択する。 ひとつにまとめると、私たちの仕事は、人間とAIのエンゲージメントの密接な相互作用を含む、フォーマル化ワークフローへのAI統合の初期段階に光を当てています。

関連論文リスト

• AI Phenomenology for Understanding Human-AI Experiences Across Eras [8.54750896635797]
  AI現象学とは、AIシステムと対話する際に「どう感じたか?」と問う研究スタンスである。 私たちはAI現象学を、ユーザーとAIシステム間のアライメントの体験、交渉、更新を捉えるフレームワークとして動機付けています。
  論文  参考訳（メタデータ） (2026-03-09T23:26:46Z)
• The AI Research Assistant: Promise, Peril, and a Proof of Concept [0.0]
  詳細な事例研究を通じて実証的な証拠を提供する。 コラボレーションによって、注目すべき機能と限界の両方が明らかになった。 我々の経験から、適切な懐疑論や検証プロトコルを使用すると、AIツールは数学的発見を有意義に加速させることができることが示唆されている。
  論文  参考訳（メタデータ） (2026-02-26T10:29:05Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。 具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。 我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
  論文  参考訳（メタデータ） (2026-02-10T18:50:15Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• Improving Human-AI Collaboration With Descriptions of AI Behavior [14.904401331154062]
  人々はAIシステムを使って意思決定を改善するが、しばしばAIの予測を過度に、あるいは過度に予測し、手伝わなかったよりも悪いパフォーマンスをする。 人々がAIアシスタントを適切に頼りにするために、行動記述を示すことを提案する。
  論文  参考訳（メタデータ） (2023-01-06T00:33:08Z)
• On the Effect of Information Asymmetry in Human-AI Teams [0.0]
  我々は、人間とAIの相補的ポテンシャルの存在に焦点を当てる。 具体的には、情報非対称性を相補性ポテンシャルの必須源とみなす。 オンライン実験を行うことで、人間がそのような文脈情報を使ってAIの決定を調整できることを実証する。
  論文  参考訳（メタデータ） (2022-05-03T13:02:50Z)
• Cybertrust: From Explainable to Actionable and Interpretable AI (AI2) [58.981120701284816]
  Actionable and Interpretable AI (AI2)は、AIレコメンデーションにユーザの信頼度を明確に定量化し視覚化する。 これにより、AIシステムの予測を調べてテストすることで、システムの意思決定に対する信頼の基盤を確立することができる。
  論文  参考訳（メタデータ） (2022-01-26T18:53:09Z)
• A User-Centred Framework for Explainable Artificial Intelligence in Human-Robot Interaction [70.11080854486953]
  本稿では,XAIのソーシャル・インタラクティブな側面に着目したユーザ中心型フレームワークを提案する。 このフレームワークは、エキスパートでないユーザのために考えられた対話型XAIソリューションのための構造を提供することを目的としている。
  論文  参考訳（メタデータ） (2021-09-27T09:56:23Z)

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

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