Fugu-MT 論文翻訳(概要): Carnap Ten Years Later: Lessons Learned and Next Steps

論文の概要: Carnap Ten Years Later: Lessons Learned and Next Steps

arxiv url: http://arxiv.org/abs/2607.07722v1
Date: Sat, 04 Jul 2026 15:49:36 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-10 14:45:27.277484
Title: Carnap Ten Years Later: Lessons Learned and Next Steps
Title（参考訳）: 10年後のカーナップ:教訓と次のステップ
Abstract要約: Carnapの証明アシスタントフレームワークは、過去10年間に世界中で45,000人以上の学生が利用してきた。新しい設計では、マリオ・カルネイロのメタマスゼロフォーマットをターゲットにした新しい高性能検証カーネルと、新しい証明コンパイラであるAufbau Bytecode Compilerを組み合わせた。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000 students worldwide over the last decade. We cover the good, the bad, and the ugly: what worked well, what didn't work, and what added friction to development and maintenance over time. These insights motivate a bottom-up redesign of the Carnap framework, which is the topic of the paper's second part. Briefly, the new design combines a new high-performance verifier kernel (mm0-zig) targeting Mario Carneiro's metamath zero format, and the Aufbau Bytecode Compiler, (abc), a new proof compiler that can serve as a backend for richly interactive proof-authoring experiences on the web.
Abstract（参考訳）: 本報告の第1部では,過去10年間に全世界で45,000人以上の学生が利用したCarnap証明支援フレームワークの設計と長期維持について報告する。何がうまくいかなかったのか、何がうまくいかなかったのか、そして時間をかけて開発とメンテナンスに摩擦を加えたのか。これらの洞察がCarnapフレームワークのボトムアップ再設計を動機付けている。簡単に言えば、Mario Carneiroのメタマスゼロフォーマットをターゲットにした新しい高性能検証カーネル(mm0-zig)と、Web上でリッチにインタラクティブな証明オーサリングエクスペリエンスのバックエンドとして機能する新しい証明コンパイラであるAufbau Bytecode Compiler(abc)を組み合わせている。

関連論文リスト

MiniGPT: Rebuilding GPT from First Principles [0.0]
MiniGPTは、PyTorchにおけるGPTスタイルの自動回帰言語モデリングのコンパクトなオフスクラッチ実装である。本稿では,文字レベルのトークン化を用いたTiny Shakespeareデータセットの実装について検討する。
論文参考訳（メタデータ） (2026-05-17T11:32:07Z)
Closing the Block-to-Text Gap: A Domain-Specific JavaScript Editor for Early Computational Thinking [0.0]
本稿では,8～10歳児のブロックベースプログラミングへの移行を支援するために,WebベースのJavaScriptエディタを提案する。このシステムは、創造性、自己補正、持続的なエンゲージメントを奨励し、教育者が認証コーディングの実践的なツールを提供する。
論文参考訳（メタデータ） (2025-10-15T18:54:53Z)
Paper2Code: Automating Code Generation from Scientific Papers in Machine Learning [70.04746094652653]
機械学習論文を機能コードリポジトリに変換するフレームワークであるPaperCoderを紹介した。 PaperCoderは3つの段階で動作する。計画、図によるシステムアーキテクチャの設計、ファイル依存の特定、構成ファイルの生成である。次に、モデルベースおよび人的評価の両方に基づいて、機械学習論文からコード実装を生成するPaperCoderを評価する。
論文参考訳（メタデータ） (2025-04-24T01:57:01Z)
Read between the lines -- Functionality Extraction From READMEs [7.302971710984904]
Gitファイルから機能を抽出する,新鮮で有用なバージョンを紹介します。このタスクの背後にあるモチベーションは、コード関連のタスクに大規模言語モデルを使用することに関する研究と開発活動が最近急増したことに起因している。最高の微調整された70億コードラマモデルは、それぞれChatGPTとBardに対するF1スコアに対して70%と20%の利得を示している。
論文参考訳（メタデータ） (2024-03-15T11:11:57Z)
Context Composing for Full Line Code Completion [0.46040036610482665]
本稿では,機能実装のコアとなるTransformerモデルに対するコンテクスト構成のアプローチについて述べる。我々は、機能を改善するための次のステップを共有し、この分野におけるいくつかの研究面の重要性を強調します。
論文参考訳（メタデータ） (2024-02-14T15:17:37Z)
SegNeXt: Rethinking Convolutional Attention Design for Semantic Segmentation [100.89770978711464]
セマンティックセグメンテーションのための単純な畳み込みネットワークアーキテクチャであるSegNeXtを提案する。コンボリューションアテンションは、トランスフォーマーの自己認識メカニズムよりも、文脈情報をエンコードするより効率的で効果的な方法であることを示す。
論文参考訳（メタデータ） (2022-09-18T14:33:49Z)
CodeRetriever: Unimodal and Bimodal Contrastive Learning [128.06072658302165]
関数レベルのコードセマンティック表現を訓練するために,一様および二様のコントラスト学習を組み合わせたCodeRetrieverモデルを提案する。ノンモーダルなコントラスト学習のために、文書と関数名に基づいてポジティブなコードペアを構築するためのセマンティックガイド付き手法を設計する。バイモーダルなコントラスト学習では、コードのドキュメンテーションとインラインコメントを活用して、テキストコードペアを構築します。
論文参考訳（メタデータ） (2022-01-26T10:54:30Z)
Contrastive Learning for Source Code with Structural and Functional Properties [66.10710134948478]
本稿では,ソースコードの特徴に基づいて事前学習に焦点を当てた,新たな自己教師型モデルBOOSTを提案する。私たちは、機能的に等価なコードを生成する自動化された構造誘導型コード変換アルゴリズムを採用しています。私たちは、対照的な学習目標を通じて、機能的に等価なコードをより近く、異なるコードに近づける方法で、モデルをトレーニングします。
論文参考訳（メタデータ） (2021-10-08T02:56:43Z)
ProtoTransformer: A Meta-Learning Approach to Providing Student Feedback [54.142719510638614]
本稿では,フィードバックを数発の分類として提供するという課題について考察する。メタラーナーは、インストラクターによるいくつかの例から、新しいプログラミング質問に関する学生のコードにフィードバックを与えるように適応します。本手法は,第1段階の大学が提供したプログラムコースにおいて,16,000名の学生試験ソリューションに対するフィードバックの提供に成功している。
論文参考訳（メタデータ） (2021-07-23T22:41:28Z)
Distilling Knowledge via Knowledge Review [69.15050871776552]
教師と学生のネットワーク間の接続経路のクロスレベル要因を研究し、その大きな重要性を明らかにします。知識蒸留において初めて, クロスステージ接続経路が提案されている。最終的に設計されたネストでコンパクトなフレームワークは、無視できるオーバーヘッドを必要とし、さまざまなタスクで他のメソッドよりも優れています。
論文参考訳（メタデータ） (2021-04-19T04:36:24Z)

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