論文の概要: The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq

• arxiv url: http://arxiv.org/abs/2008.00120v1
• Date: Fri, 31 Jul 2020 23:47:29 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-04 06:56:15.945257
• Title: The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
• Title（参考訳）: the tactician (extended version):coqのためのシームレスでインタラクティブな戦術学習者と証明者
• Authors: Lasse Blaauwbroek, Josef Urban and Herman Geuvers
• Abstract要約: 我々は、Coq Proof Assistantの戦術学習者であり証明者であるTacticianを紹介する。 Tacticianは、一般的な証明戦略のコントロールを維持しながら、ユーザーが戦術的証明決定を行うのを助ける。 本稿では,Tacticianの日常利用とパッケージ依存性管理の問題点について,ユーザの視点から概観する。
• 参考スコア（独自算出の注目度）: 0.6445605125467572
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician learns from previously written tactic scripts and gives users either suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician's goal is to provide users with a seamless, interactive, and intuitive experience together with robust and adaptive proof automation. In this paper, we give an overview of Tactician from the user's point of view, regarding both day-to-day usage and issues of package dependency management while learning in the large. Finally, we give a peek into Tactician's implementation as a Coq plugin and machine learning platform.
• Abstract（参考訳）: 我々はCoq Proof Assistantの戦術学習者であり証明者であるTacticianを紹介する。 Tacticianは、一般的な証明戦略のコントロールを維持しながら、ユーザーが戦術的証明決定を行うのを助ける。 この目的のために、tacticianは以前に書かれた戦術スクリプトから学習し、実行すべき次の戦術について提案するか、証明合成の負担を完全に引き受ける。 Tacticianの目標は、ユーザに対してシームレスでインタラクティブで直感的なエクスペリエンスと、堅牢で適応的な証明自動化を提供することだ。 本稿では,ユーザの視点からのTacticianの概要を概観し,大規模に学習しながら,パッケージ依存管理の日常的利用と課題について述べる。 最後に、tacticianのcoqプラグインと機械学習プラットフォームとしての実装について紹介する。

関連論文リスト

• Learning Rules Explaining Interactive Theorem Proving Tactic Prediction [5.229806149125529]
  この問題を帰納論理プログラミング(ILP)タスクとして表現する。 ILP表現を使用することで、追加で計算コストの高いプロパティをエンコードすることで、機能空間を豊かにしました。 我々は、このリッチな特徴空間を用いて、与えられた証明状態に戦術がいつ適用されたかを説明する規則を学ぶ。
  論文  参考訳（メタデータ） (2024-11-02T09:18:33Z)
• RLIF: Interactive Imitation Learning as Reinforcement Learning [56.997263135104504]
  我々は,対話型模倣学習と類似するが,さらに実践的な仮定の下で,非政治強化学習によってパフォーマンスが向上できることを実証する。 提案手法は,ユーザ介入信号を用いた強化学習を報奨として利用する。 このことは、インタラクティブな模倣学習において介入する専門家がほぼ最適であるべきだという仮定を緩和し、アルゴリズムが潜在的に最適でない人間の専門家よりも改善される行動を学ぶことを可能にする。
  論文  参考訳（メタデータ） (2023-11-21T21:05:21Z)
• TacticAI: an AI assistant for football tactics [41.74699109772055]
  TacticAIは、リバプールFCのドメインエキスパートと緊密に協力して開発されたAIフットボール戦術アシスタントである。 介入や改善の最も直接的な機会をコーチに提供するため、コーナーキックの分析に重点を置いています。 我々は、戦術のモデル提案が実際の戦術と区別できないだけでなく、当時の既存の戦術よりも有利であることを示す。
  論文  参考訳（メタデータ） (2023-10-16T16:25:15Z)
• Chain-of-Thought Predictive Control [32.30974063877643]
  複雑な低レベル制御のための実証から一般化可能な政策学習について研究する。 準最適デモを利用した新しい階層型模倣学習法を提案する。
  論文  参考訳（メタデータ） (2023-04-03T07:59:13Z)
• Transductive Learning for Unsupervised Text Style Transfer [60.65782243927698]
  教師なしスタイル転送モデルは、主に帰納的学習アプローチに基づいている。 本稿では,検索に基づく文脈認識スタイルの表現に基づく新しいトランスダクティブ学習手法を提案する。
  論文  参考訳（メタデータ） (2021-09-16T08:57:20Z)
• Online Machine Learning Techniques for Coq: A Comparison [2.9412498294532856]
  我々は,Coq証明アシスタントにおける戦術学習と証明のためのオンライン機械学習技術の比較を行った。 この仕事は、ユーザーによって書かれた証明から新しい証明を合成するCoq用のプラグインであるTacticianをベースにしています。
  論文  参考訳（メタデータ） (2021-04-12T05:12:35Z)
• Can Semantic Labels Assist Self-Supervised Visual Representation Learning? [194.1681088693248]
  近隣環境におけるコントラスト調整(SCAN)という新しいアルゴリズムを提案する。 一連のダウンストリームタスクにおいて、SCANは従来の完全教師付きおよび自己教師付きメソッドよりも優れたパフォーマンスを達成する。 本研究は, セマンティックラベルが自己指導的手法の補助に有用であることを明らかにする。
  論文  参考訳（メタデータ） (2020-11-17T13:25:00Z)
• Empowering Active Learning to Jointly Optimize System and User Demands [70.66168547821019]
  我々は,アクティブラーニングシステムとユーザを協調的に(効率的に学習)するための,新しいアクティブラーニング手法を提案する。 本手法は,特定のユーザに対して,エクササイズの適切性を予測するために,学習を迅速かつ迅速に行う必要があるため,特に,この手法のメリットを生かした教育アプリケーションで研究する。 複数の学習戦略とユーザタイプを実際のユーザからのデータで評価し,代替手法がエンドユーザに適さない多くのエクササイズをもたらす場合,共同アプローチが両方の目標を満足できることを確認した。
  論文  参考訳（メタデータ） (2020-05-09T16:02:52Z)
• Tactic Learning and Proving for the Coq Proof Assistant [0.5735035463793007]
  我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。 システムの性能は、Coq Standard Libraryで評価される。 CoqHammerシステムと組み合わせると、この2つのシステムは図書館の補題の56.7%を証明している。
  論文  参考訳（メタデータ） (2020-03-20T08:22:30Z)
• Reward-Conditioned Policies [100.64167842905069]
  模倣学習には、ほぼ最適の専門家データが必要である。 実演なしで指導的学習を通じて効果的な政策を学べるか? 政策探索の原則的手法として,このようなアプローチを導出する方法を示す。
  論文  参考訳（メタデータ） (2019-12-31T18:07:43Z)

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

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