論文の概要: Online Machine Learning Techniques for Coq: A Comparison

• arxiv url: http://arxiv.org/abs/2104.05207v1
• Date: Mon, 12 Apr 2021 05:12:35 GMT
• ステータス: 処理完了
• システム内更新日: 2021-04-13 13:59:24.645368
• Title: Online Machine Learning Techniques for Coq: A Comparison
• Title（参考訳）: coqのためのオンライン機械学習技術:比較
• Authors: Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop \v{C}ern\'y, Cezary Kaliszyk, and Josef Urban
• Abstract要約: 我々は,Coq証明アシスタントにおける戦術学習と証明のためのオンライン機械学習技術の比較を行った。 この仕事は、ユーザーによって書かれた証明から新しい証明を合成するCoq用のプラグインであるTacticianをベースにしています。
• 参考スコア（独自算出の注目度）: 2.9412498294532856
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. This learning happens in an online manner -- meaning that Tactician's machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate $k$-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq's standard library.
• Abstract（参考訳）: 我々は,Coq証明アシスタントにおける戦術学習と証明のためのオンライン機械学習技術の比較を行った。 この作業は、ユーザが書いた証明から学び、新しい証明を合成する、Coq用のプラグインであるTacticianの上に構築されている。 つまり、Tacticianの機械学習モデルは、ユーザが対話的な証明でステップを実行するたびに即座に更新される。 これは、より研究されたオフライン学習システムと比較すると重要な利点がある: (1) ストラテジアンによるシームレスでインタラクティブな体験を提供し、(2) 証明の類似性の局所性を利用する。 局所性に敏感な湿原林と無作為な決定林に基づく,およそ$k$-nearest近くの2つのオンライン手法を実装した。 さらに,xgboost を用いたオフライン環境で勾配ブースト木を用いた実験を行った。 coqの標準ライブラリ上で,これら3つの学習手法を用いて,戦術の相対的性能を比較する。

関連論文リスト

• Adapting Vision-Language Models to Open Classes via Test-Time Prompt Tuning [50.26965628047682]
  学習済みのモデルをオープンクラスに適応させることは、機械学習において難しい問題である。 本稿では,両者の利点を組み合わせたテスト時プロンプトチューニング手法を提案する。 提案手法は,基本クラスと新クラスの両方を考慮し,すべての比較手法を平均的に上回る結果を得た。
  論文  参考訳（メタデータ） (2024-08-29T12:34:01Z)
• NeCo: Improving DINOv2's spatial representations in 19 GPU hours with Patch Neighbor Consistency [35.768260232640756]
  NeCo: Patch Neighbor Consistencyは、学生モデルと教師モデルにまたがる、パッチレベルの近接一貫性を強制する新しいトレーニング損失である。 本手法は,DINOv2-Registersのような事前学習された表現の上に適用された微分可能なソート手法を用いて学習信号をブートストラップする。 この厳密な事前トレーニングは、単一のGPUで19時間しか必要とせず、さまざまなモデルやデータセットでパフォーマンスが向上する。
  論文  参考訳（メタデータ） (2024-08-20T17:58:59Z)
• Graph2Tac: Online Representation Learning of Formal Math Concepts [0.6597195879147557]
  証明において、2つの形式的な数学的概念の間の物理的近接は、それらの相互関係の強い予測因子である。 この局所性特性はオンライン学習技術によって利用でき、オフライン学習者を超えている問題解決エージェントが得られることを示す。 我々は、Coq証明アシスタントのためにTacticianプラットフォームで実装された2つのオンライン解決器をベンチマークした。
  論文  参考訳（メタデータ） (2024-01-05T18:52:09Z)
• RLIF: Interactive Imitation Learning as Reinforcement Learning [56.997263135104504]
  我々は,対話型模倣学習と類似するが,さらに実践的な仮定の下で,非政治強化学習によってパフォーマンスが向上できることを実証する。 提案手法は,ユーザ介入信号を用いた強化学習を報奨として利用する。 このことは、インタラクティブな模倣学習において介入する専門家がほぼ最適であるべきだという仮定を緩和し、アルゴリズムが潜在的に最適でない人間の専門家よりも改善される行動を学ぶことを可能にする。
  論文  参考訳（メタデータ） (2023-11-21T21:05:21Z)
• CLAWSAT: Towards Both Robust and Accurate Code Models [74.57590254102311]
  比較学習(CL)と逆学習を統合して、コードモデルの堅牢性と精度を協調的に最適化する。 私たちの知る限りでは、これはコードモデルにおける(マルチビュー)コードの難読化の堅牢性と正確性について調査し、活用する最初の体系的な研究です。
  論文  参考訳（メタデータ） (2022-11-21T18:32:50Z)
• Co-training an Unsupervised Constituency Parser with Weak Supervision [33.63314110665062]
  本稿では,あるノードが文中の特定のスパンを支配しているかどうかを識別するために,ブートストラップ分類器に依存する教師なし解析手法を提案する。 両者の相互作用が両者の精度の向上に役立ち、その結果、効果的に解析できることが示される。
  論文  参考訳（メタデータ） (2021-10-05T18:45:06Z)
• Transductive Learning for Unsupervised Text Style Transfer [60.65782243927698]
  教師なしスタイル転送モデルは、主に帰納的学習アプローチに基づいている。 本稿では,検索に基づく文脈認識スタイルの表現に基づく新しいトランスダクティブ学習手法を提案する。
  論文  参考訳（メタデータ） (2021-09-16T08:57:20Z)
• CoMatch: Semi-supervised Learning with Contrastive Graph Regularization [86.84486065798735]
  CoMatchは、支配的なアプローチを統一する、新しい半教師付き学習手法である。 複数のデータセット上で最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2020-11-23T02:54:57Z)
• The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq [0.6445605125467572]
  我々は、Coq Proof Assistantの戦術学習者であり証明者であるTacticianを紹介する。 Tacticianは、一般的な証明戦略のコントロールを維持しながら、ユーザーが戦術的証明決定を行うのを助ける。 本稿では,Tacticianの日常利用とパッケージ依存性管理の問題点について,ユーザの視点から概観する。
  論文  参考訳（メタデータ） (2020-07-31T23:47:29Z)
• Rethinking Few-Shot Image Classification: a Good Embedding Is All You Need? [72.00712736992618]
  メタトレーニングセット上で教師付きあるいは自己教師型表現を学習する単純なベースラインが、最先端の数ショット学習方法より優れていることを示す。 追加の増量は自己蒸留によって達成できる。 我々は,この発見が,画像分類ベンチマークとメタ学習アルゴリズムの役割を再考する動機となっていると考えている。
  論文  参考訳（メタデータ） (2020-03-25T17:58:42Z)
• Tactic Learning and Proving for the Coq Proof Assistant [0.5735035463793007]
  我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。 システムの性能は、Coq Standard Libraryで評価される。 CoqHammerシステムと組み合わせると、この2つのシステムは図書館の補題の56.7%を証明している。
  論文  参考訳（メタデータ） (2020-03-20T08:22:30Z)

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

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