論文の概要: A Reasoning Engine for the Gamification of Loop-Invariant Discovery
- arxiv url: http://arxiv.org/abs/2109.01121v1
- Date: Thu, 2 Sep 2021 17:47:03 GMT
- ステータス: 処理完了
- システム内更新日: 2021-09-03 13:45:45.125026
- Title: A Reasoning Engine for the Gamification of Loop-Invariant Discovery
- Title(参考訳): ループ不変発見のゲーミフィケーションのための推論エンジン
- Authors: Andrew Walter and Seth Cooper and Panagiotis Manolios
- Abstract要約: 我々の推論エンジンは、学生や計算エージェント、正規のソフトウェアエンジニアが形式的な手法の専門知識を持っていない状態で、興味深い定理を共同で証明することを可能にする。
1時間以内にプレイヤーは、完全に自動化されたツールの能力を超えたプログラムの特性を特定し、検証することができる。
- 参考スコア(独自算出の注目度): 4.125187280299247
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: We describe the design and implementation of a reasoning engine that
facilitates the gamification of loop-invariant discovery. Our reasoning engine
enables students, computational agents and regular software engineers with no
formal methods expertise to collaboratively prove interesting theorems about
simple programs using browser-based, online games. Within an hour, players are
able to specify and verify properties of programs that are beyond the
capabilities of fully-automated tools. The hour limit includes the time for
setting up the system, completing a short tutorial explaining game play and
reasoning about simple imperative programs. Players are never required to
understand formal proofs; they only provide insights by proposing invariants.
The reasoning engine is responsible for managing and evaluating the proposed
invariants, as well as generating actionable feedback.
- Abstract(参考訳): 本稿では,ループ不変発見のゲーミフィケーションを容易にする推論エンジンの設計と実装について述べる。
私たちの推論エンジンは、学生、計算エージェント、正規のソフトウェアエンジニアが、ブラウザベースのオンラインゲームを使って、単純なプログラムに関する興味深い定理を協調的に証明することを可能にする。
1時間以内に、完全に自動化されたツールの能力を超えたプログラムの特性を特定し検証することができる。
時間制限には、システムのセットアップ時間、ゲームプレイを説明する簡単なチュートリアルの完了、単純な命令的プログラムの推論が含まれる。
プレイヤーは形式的な証明を理解する必要はなく、不変量を提案することでのみ洞察を与える。
推論エンジンは提案された不変量を管理し評価し、実用的なフィードバックを生成する。
関連論文リスト
- Exploring Prompt Engineering Practices in the Enterprise [3.7882262667445734]
プロンプト(英: prompt)は、モデルから特定の振る舞いや出力を引き出すように設計された自然言語命令である。
特定の要求のある複雑なタスクやタスクに対して、迅速な設計は簡単ではない。
我々は、プロンプト編集行動のセッションを分析し、ユーザが反復したプロンプトの一部と、それらが行った変更の種類を分類する。
論文 参考訳(メタデータ) (2024-03-13T20:32:32Z) - Learning Guided Automated Reasoning: A Brief Survey [5.607616497275423]
これまでに開発されてきたいくつかの自動推論・定理証明領域と学習・AI手法の概要について概説する。
これには、前提選択、いくつかの設定での証明ガイダンス、推論と学習を繰り返すフィードバックループ、象徴的な分類問題が含まれる。
論文 参考訳(メタデータ) (2024-03-06T19:59:17Z) - When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。
具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。
コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
論文 参考訳(メタデータ) (2023-08-29T17:22:39Z) - Leveraging Large Language Models to Generate Answer Set Programs [5.532477732693001]
大規模言語モデル(LLM)は、様々な自然言語処理タスクにおいて例外的な性能を示した。
本稿では,大規模言語モデルの強みと解集合プログラミングを組み合わせたニューロシンボリック手法を提案する。
論文 参考訳(メタデータ) (2023-07-15T03:40:55Z) - Code Prompting: a Neural Symbolic Method for Complex Reasoning in Large
Language Models [74.95486528482327]
コードプロンプト(code prompting)は、ゼロショットバージョンと少数ショットバージョンの両方を持ち、中間ステップとしてコードをトリガーするニューラルシンボルプロンプトである。
我々は,記号的推論と算術的推論を含む7つの広く使用されているベンチマーク実験を行った。
論文 参考訳(メタデータ) (2023-05-29T15:14:09Z) - Execution Time Program Verification With Tight Bounds [6.36836017515443]
本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。
3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。
証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
論文 参考訳(メタデータ) (2022-10-20T09:02:13Z) - Chain of Thought Imitation with Procedure Cloning [129.62135987416164]
本稿では,一連の専門家計算を模倣するために,教師付きシーケンス予測を適用したプロシージャクローニングを提案する。
本研究では、専門家の行動の中間計算を模倣することで、プロシージャのクローン化により、未知の環境構成に顕著な一般化を示すポリシーを学習できることを示す。
論文 参考訳(メタデータ) (2022-05-22T13:14:09Z) - Fact-driven Logical Reasoning for Machine Reading Comprehension [82.58857437343974]
私たちは、常識と一時的な知識のヒントの両方を階層的にカバーする動機があります。
具体的には,文の背骨成分を抽出し,知識単位の一般的な定式化を提案する。
次に、事実単位の上にスーパーグラフを構築し、文レベル(事実群間の関係)と実体レベルの相互作用の利点を享受する。
論文 参考訳(メタデータ) (2021-05-21T13:11:13Z) - Brain-inspired Search Engine Assistant based on Knowledge Graph [53.89429854626489]
developerbotは脳にインスパイアされた、knowledge graphの名前の検索エンジンアシスタントだ。
複雑なマルチ制約クエリを複数の順序制約に分割することで、多層クエリグラフを構築する。
次に、制約推論プロセスを認知科学の拡散活性化モデルに触発されたサブグラフ探索プロセスとしてモデル化する。
論文 参考訳(メタデータ) (2020-12-25T06:36:11Z) - Towards Interpretable Natural Language Understanding with Explanations
as Latent Variables [146.83882632854485]
そこで本研究では,人間に注釈付き説明文の小さなセットだけを必要とする自然言語理解の枠組みを構築した。
我々のフレームワークは、ニューラルネットワークの基本的な推論過程をモデル化する潜在変数として、自然言語の説明を扱う。
論文 参考訳(メタデータ) (2020-10-24T02:05:56Z) - Extending Automated Deduction for Commonsense Reasoning [0.0]
本論文は,古典的な一階述語論理を自動推論する手法とアルゴリズムを,コモンセンス推論に拡張できると主張している。
提案された拡張は主に通常の証明木に依存しており、不整合、デフォルトルール、トピックの操作、関連性、信頼性、類似度などを含む常識知識ベースを扱うように設計されている。
機械学習はコモンセンスの知識ベースを構築するのに最適であり、拡張された論理ベースの手法はこれらの知識ベースからのクエリに実際に答えるのに適している、と我々は主張する。
論文 参考訳(メタデータ) (2020-03-29T23:17:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。