概要 Bergstra と Klop は,組合せ子 S の非循環性と逆書き換えの停止性を示している.本論文では,Bergstra と Klop の結果を,様々な組合せ子に対し一般化した定理を与える.最初に,この定理を用いてこれらの組合せ子に対する逆書き換えの停止性を示す.次に,この定理が適用できない組合せ子に対し,項書き換えシステムの枠組みを用いて,逆書き換えの停止性を示す.最後に,様々な組合せ子に対して,同じ枠組みを用いて,逆書き換えの合流性を反証する.

概要 書換え対象が項である項書換え系(TRS)や論理制約付き項書換え系(LCTRS)などの書換え系の擬簡約性はすべての被定義記号がどのような基底構成子項を引数にとっても書き換えられるという性質である.TRS の擬簡約性は決定可能であり,近年,擬簡約性を帰着できるパターン照合問題集合に対する効率的なアルゴリズムとしてパターン完全性判定アルゴリズムが提案された.一方,左線形 TRS を対象として未定義パターンを列挙する補パターンアルゴリズムは左線形 LCTRS に拡張された.しかし,左線形ではない LCTRS の擬簡約性の判定に応用できるアルゴリズムは知られていない.本論文では,TRS のシグネチャを対象とするパターン完全性判定アルゴリズムを LCTRS に拡張し,LCTRS の擬簡約性判定アルゴリズムを示す.具体的には,パターン完全性判定アルゴリズムが変換対象とするパターン問題集合に制約を導入して拡張する.そして,パターン部分に関して問題分割を行う既存の変換規則を適用できなくなった後に制約の恒真性を判定する規則を導入することでアルゴリズムを拡張する.

概要 メモリ安全性を担保しつつ実行効率が良い言語として、Rust が近年広く認知されるようになっている。Rust ではメモリ安全性を担保するため、コンパイル時にオブジェクトや参照が利用できる範囲を計算している。そのため、メモリの動的確保、解放についてもソースコード上の位置が実行前に分かる。本研究では Rust の所有権およびライフタイムの可視化ツールである RustOwl に新たに CLI 表示を行うコマンドを実装し、指定された変数について、メモリの動的確保、解放が行われるソースコード上の位置を標準出力に出力できるようにした。この可視化ツールの出力を用いて、メモリ最適化を行うプログラム書き換えタスクを複数種類の大規模言語モデルで、パッケージリポジトリ crates.io 上のユニットテストのある複数のライブラリを対象に実行した。これらのライブラリのユニットテストのメモリ使用量を、本研究の可視化ツールを利用した場合とそうでない場合について測定した。

概要 Real-time task mapping and scheduling on multi-core platforms is often formulated as an integer linear programming (ILP) problem. However, directly enforcing deadlines as hard constraints becomes challenging in practical real-time systems, where periodic tasks and sporadically triggered event-driven tasks coexist, significantly increasing computational cost and sometimes leading to infeasible formulations. To address this issue, this paper presents iterative scheduling framework based on objective and constraint reformulation. The proposed method first solves a simplified ILP formulation to obtain an initial core assignment and schedule. It then iteratively analyzes the results to detect deadline misses. For each deadline-violating task, the method focuses on a part of its dependency chain and a set of tasks that potentially interfere with its execution. Core reassignment is applied to this subset of tasks. The ILP formulation is reformulated to reduce the response time of deadline-violating tasks and mitigate interference with the execution of other tasks. Through numerical simulations on randomly generated application instances, the proposed method achieves higher scheduling success rates than both the original ILP formulation and traditional single-task repair approach by enabling coordinated multi-task reassignment.

概要 自然言語で定義された演繹が必要なタスクに対し,単に解を求めるだけでなく,論理式などによる形式的な証明を求めたい場面は多い.自然言語を論理式に変換できれば自動証明などを利用できるが,機械的な変換は単純な文章表現でなければ実現できなかった.我々は,婉曲表現や多段推論を含むロジックグリッドパズル「MURDLE」を対象に,LLM を併用することで自然言語の問題を Prolog に変換してパズルを解くことを試みる.この変換においては,論理的な飛躍を含まず,人間が理解しやすい翻訳を行うことが重要であり,LLM を単純に利用するだけではこの性質は実現できない.そこで,婉曲表現から連想される名称を定義する,予め頻出する表現をまとめた述語を用意する等の手法を用い,MURDLE 第 1 巻に含まれる 100 問のパズルで検証したところ,90%の高い正答率を示すと同時に,文章を正確に反映した論理式へ変換できていることを確認した.

概要 可逆計算モデルでは,中間状態の情報を全く破棄できないため,通常の(非可逆)アルゴリズムをそのまま移植すると多量の余剰データであるゴミを生じたり,実装が複雑化したりする.本稿では,多次元配列照合に対して,素朴な方法および Rabin–Karp 法を対象に,可逆プログラミング言語 Janus により可逆プログラムを設計・実装する.特に,多次元 Rabin–Karp 法におけるローリングハッシュ更新を可逆に扱うため,更新と逆更新を対として実装し,実行終了時に入力以外のゴミを残さない構成を与える.2 次元および 3 次元の場合について Janus コードを実装して動作を確認し,さらに,手続きの入れ子による構成規則を整理することで,4 次元以上についても同様の方針で機械的にプログラムを構成できる見通しを示す.

概要 In introductory programming courses, students increasingly submit code generated by large language models (LLMs) instead of solving problems independently. This growing reliance raises concerns about students’ development of programming skills. To reduce the overreliance and promote independent problem solving, we propose an explainable detection framework that predicts whether a code submission was generated by an LLM and provides an explanation for its prediction. Such explanations are crucial in educational settings, where transparency and feedback are essential. To support this, we construct a dataset of student-written and LLM-generated code, paired with explanations automatically produced using GPT-4o. We finetune several code-specialized LLMs using both binary labels (student-written or LLM-generated) and explanations. The resulting models achieve over 99% accuracy and generate informative explanations aligned with their predictions, both validated by human instructors. We also apply our detector to past programming course data, revealing a sharp increase in LLM-generated submissions—from nearly 0% in 2022A to over 40% in 2024A. We conclude with a discussion of false positives and suggest how explainable detection can be responsibly deployed in programming courses. Code and prompts will be released upon acceptance.

概要 大規模言語モデル(LLM)は高度なコード生成能力を持つが,その内部で「プログラミング言語の意味」がどのように表現・処理されているか(または,そもそもそのような意味に相当するものを持っていないかも含めて)はブラックボックスのままである.現在,第二プログラミング言語習得(SPLA)シミュレーションについて研究を進めている.本発表では,SPLA を,「操作的意味論ルール集合の適応過程」としてシミュレーションする枠組みを提案する.対象言語は同一構文のまま,評価戦略やスコープといった意味論的差異のみが異なる言語間での言語習得を想定する.学習者はスモールステップの推論規則からなる既習得の意味論のルール集合を保持した状態からスタートし,学習は実行失敗のトレースに基づき,その意味論ルール集合を変異させる過程としてシミュレーションされる.シミュレーターは,学習時の探索をどのように行うかのポリシーと,指導者にあたるテンプレートを切り換えて,学習過程の種々の指標を観測可能である.本発表では,シミュレーション環境の設計と,Python による実装,その挙動を分析可能な形で観測できることを示す.

概要 プログラミング言語処理系 (以下、処理系) が出力するエラーメッセージは一般的に難解であると言われている。その一つの要因は、処理系の実装者が、実装者視点でエラーメッセージの出力を実装している点にある。ある程度プログラミングの経験がある人でも、新たな言語に触れるときには、必ずしも処理系が出力するエラーメッセージを的確に捉えられるとは限らない。このため、デフォルトのエラーメッセージを利用者にとって理解しやすいエラーメッセージに変更できる仕組みがあることが望ましい。
本研究では、利用者がエラーメッセージをカスタマイズ可能となる仕組みを、特定の言語処理系の実装に依存しないように、言語処理系の生成系の機能として提供する仕組みを提案する。ここで求められるのは、利用者に固有のメッセージを言語処理系が保持できる仕組みである。さらに言語の進化等の仕様の変更として文法の変更が生じても各使用者が変更したメッセージを維持できる仕組みも必要である。本研究ではこの点に着目し、構文解析における内部の状態とそのメッセージを紐づける仕組み、および、言語仕様 (文法) の変更に対応できる仕組みを考案した。この仕組みの有用性を調べるため、Python および PHP を対象としてバージョンアップによる文法の変化に対して、対応できることを確認した。