Fugu-MT 論文翻訳(概要): The Coq Proof Script Visualiser (coq-psv)

論文の概要: The Coq Proof Script Visualiser (coq-psv)

arxiv url: http://arxiv.org/abs/2101.07761v1
Date: Fri, 15 Jan 2021 08:52:31 GMT
ステータス: 処理完了
システム内更新日: 2023-04-15 02:55:57.746343
Title: The Coq Proof Script Visualiser (coq-psv)
Title（参考訳）: coq 証明スクリプト visualiser (coq-psv)
Authors: Mario Frank
Abstract要約: このツールは、すべての証明ステップを視覚化できるので、教育とレビューのプロセスの両方をサポートする。証明をハイパーテキストやマークダウン文書として視覚化する一般的な手法とは対照的に、生成されたファイルを簡単に印刷することができる。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by-sa/4.0/
Abstract: In this work, we present a visualisation tool that is able to process Coq proof scripts and generate a table representation of the contained proofs as $\LaTeX$ or PDF files. This tool has the aim to support both education and review processes as all proof steps can be visualised. Thus, there is no need to use Coq in order to review proofs or use them as examples in teaching. In contrast to the usual approach of visualising proofs as hypertext or markdown documents, the generated files can be easily printed.
Abstract（参考訳）: 本稿では,coq証明スクリプトを処理し,格納された証明のテーブル表現を$\latex$またはpdfファイルとして生成する可視化ツールを提案する。このツールは、すべての証明ステップを可視化できるため、教育とレビュープロセスの両方をサポートすることを目的としている。したがって、証明をレビューしたり、教えの例として使うためにCoqを使う必要はない。証明をハイパーテキストやマークダウンドキュメントとして視覚化するという一般的なアプローチとは対照的に、生成されたファイルを簡単に印刷できる。

関連論文リスト

Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
論文参考訳（メタデータ） (2024-10-25T19:25:00Z)
CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
論文参考訳（メタデータ） (2024-05-07T12:50:28Z)
Visually Guided Generative Text-Layout Pre-training for Document Intelligence [51.09853181377696]
視覚誘導型生成テキスト事前学習(ViTLP)を提案する。文書画像が与えられた場合、モデルは階層言語とレイアウトモデリングの目的を最適化し、インターリーブされたテキストとレイアウトシーケンスを生成する。 ViTLPは、文書画像のテキストをローカライズし、認識するためのネイティブなOCRモデルとして機能する。
論文参考訳（メタデータ） (2024-03-25T08:00:43Z)
Towards Automatic Transformations of Coq Proof Scripts [0.0]
後続スクリプト変換を行うためのフレームワークを提案する。これらの変換は、証明が完了すると、自動化された後処理ステップとして適用される。当社のツールは,GeoCoqライブラリなど,さまざまなCoq証明スクリプトに適用しています。
論文参考訳（メタデータ） (2024-01-22T12:48:34Z)
Text-Conditioned Resampler For Long Form Video Understanding [94.81955667020867]
トレーニング済みのビジュアルエンコーダと大言語モデル(LLM)を用いたテキストコンディショニングビデオリサンプラー(TCR)モジュールを提案する。 TCRは、最適化された実装なしで、平易な注意で一度に100フレーム以上を処理できる。
論文参考訳（メタデータ） (2023-12-19T06:42:47Z)
Advancing Visual Grounding with Scene Knowledge: Benchmark and Method [74.72663425217522]
ビジュアルグラウンドディング(VG)は、視覚と言語の間にきめ細かいアライメントを確立することを目的としている。既存のVGデータセットの多くは、単純な記述テキストを使って構築されている。我々は、アンダーラインScene underline-guided underlineVisual underlineGroundingの新たなベンチマークを提案する。
論文参考訳（メタデータ） (2023-07-21T13:06:02Z)
Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
仮説文書埋め込み(英: hypothetical Document Embeddings, HyDE)は、ゼロショット高密度検索システムである。我々は,HyDEが最先端の非教師付き高密度検索器であるContrieverを著しく上回っていることを示す。
論文参考訳（メタデータ） (2022-12-20T18:09:52Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
Proof Blocks: Autogradable Scaffolding Activities for Learning to Write Proofs [0.4588028371034407]
Proof Blocksは、学生が事前に書かれた証明行を正しい順序にドラッグ&ドロップすることで、証明を書くことができるソフトウェアツールである。これらの証明は完全に自動的に評価され、学生は自分の証明で何をしているのかを素早くフィードバックすることができる。問題を構築する際、インストラクターは証明の行の依存性グラフを指定し、行の正しい配置をフルクレジットで受け取れるようにする。
論文参考訳（メタデータ） (2021-06-07T17:03:58Z)
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。 Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文参考訳（メタデータ） (2020-12-20T18:15:12Z)
Evidence-Aware Inferential Text Generation with Vector Quantised Variational AutoEncoder [104.25716317141321]
本稿では,大規模なテキストコーパスからイベントの証拠を自動的に発見し,その証拠を利用して推論テキストの生成を導く手法を提案する。このアプローチは、Event2MindとATOMICの両方のデータセットで最先端のパフォーマンスを提供します。
論文参考訳（メタデータ） (2020-06-15T02:59:52Z)

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