プログラム

那須塩原駅からラフォーレ那須までは，ラフォーレが運営するバスでの移動になります．お時間にお気をつけください．

定期運航便の他に，プログラミング・シンポジウム専用の臨時便を出してもらう予定です．

開場 (受付開始) 12:30

オープニング 13:40 - 13:50

セッション 1 : 13:50 - 15:35

[口頭発表ショート] ユーザフレンドリーな Java to Kotlin コンバータの開発

藤原 新 (広島市立大学情報科学部), 川端 英之 (広島市立大学大学院情報科学研究科), 弘中 哲夫 (広島市立大学大学院情報科学研究科)

概要

Java プログラムから Kotlin プログラムへの移行には一定の需要があり,IntelliJ IDEA などの統合開発環境では Java to Kotlin コンバータが提供されている.また,柔軟な変換を目標として先行研究で開発されたコンバータも存在する.しかし,これらの既存コンバータで生成されるコードは不具合が混じることも多く,また,ユーザによる変換方針の決定や,変換時の変換内容の確認ができないなど,実用する上で不十分な場合がある.これに対し,我々は Java から Kotlin への変換を包括的にサポートするコンバータを開発している.このコンバータでは,既存の成熟したツールを用いた高度な情報解析やコード生成,GUI を用いたユーザビリティの向上,段階的な変換のサポートを軸とし,変換したプログラムが正常に動作するまでの一貫した支援により, 従来のコンバータが持つ問題点を総合的に解決することを狙う.

[一般講演] Idrisプログラムにおける部分式の型導出システムの開発 ―依存型付き言語によるプログラムの読解や記述の支援―

林 慶祐 (広島市立大学大学院情報科学研究科), 川端 英之 (広島市立大学大学院情報科学研究科), 弘中 哲夫 (広島市立大学大学院情報科学研究科)

概要

プログラムが正しく動くことを客観的に示すために，試験データに基づくテストや自動テスト生成による検証など様々な方法が考えられるが，網羅性の観点からの追求をかわすには，プログラムが正しく動くことの証明が求められる．これに対し，Idrisのような，記述力の高い型注釈を用いたプログラムの性質の書き下しと証明が可能な言語処理系が実用化されつつあるが，これを使いこなすには多くの場合熟練を要する．我々は，プログラム記述中の任意の部分式の型に関する情報を詳細に描画するシステムを設計し，Idris LSP を VSCode 中で呼び出すプラグインとして実装した．本システムは，プログラム記述の任意の部分が何を証明しているのかを明らかにする役割を果たすことにより，依存型により性質が書き下されたプログラムの記述を支援する．本発表ではこのシステムの特徴と有用性について議論する．

[一般講演] ラムダ計算の拡張に基づく音楽プログラミング言語mimiumとそのVMの実装

松浦 知也(東京藝術大学芸術情報センター)

概要

本発表では筆者が2019年未踏事業で開発した音楽のためのプログラミング言語mimiumの更なる発展について解説する。mimiumは、リアルタイム信号処理を想定した音楽用のDSLだが、特定の音楽表現に基づくプリミティブは用意されていない。代わりに値呼びラムダ計算に遅延とフィードバックという2要素をプリミティブとして追加することで、その言語上でほとんどの信号処理アルゴリズムを表現できる。また、LuaをモデルとしたVMを定義することで、内部状態を持つプロセッサを高階関数で複製したり、ホスト環境との相互運用が容易に可能になる。音楽というドメインに特化しながらも、汎用性を失わない言語の意義について議論する。

休憩 15:35 - 15:45

セッション 2 : 15:45 - 17:00

[口頭発表ショート] PMF前の逆説プログラミング

近藤 佑亮（東京大学）, 大石 澪弥（九州工業大学）

概要

プログラミングの世界では、数多くのベストプラクティスや設計原則が提唱されており、それらは多くの場面で有効に機能する。しかし、これらの原則が前提としているのは、プログラムが特定の目的を果たしているという状態である。スタートアップにおいて、その「目的を果たす」とは端的に、プログラムによって収益が得られていることを意味する。
Product Market Fit（PMF）とは、顧客の課題を解決する製品が市場に受け入れられている状態を指す。PMF達成前のスタートアップでは、既存のベストプラクティスが必ずしも有効に機能しない状況に直面することがある。発表者は、IPA未踏アドバンストに採択されたプロジェクトの解散経験と、AIを活用した医療機器の開発・販売を通じて、この現実を痛感してきた。
本発表では、PMF前のスタートアップにおけるプログラミングの実態について論じる。具体的には、カオスな状態にあるスタートアップで何が起きているのか、どのようなベストプラクティスが通用しないのか、そしてそのような状況下で実際にどのようなアプローチが効果的なのかについて、現在進行形の知見を共有する。これにより、スタートアップ特有のプログラミング環境における実践的な示唆を提供する。

[口頭発表ショート] 自然なデータ表現にコンパイルするクロージャ変換

柏木力哉（慶応義塾大学理工学部）

概要

自然なデータ表現の「自然」とは、ここでは効率的で冗長性がないメモリ配置のことを言う。本発表は、自然に表現されたクロージャへの変換アルゴリズムとその正しさの証明を述べる。
高階関数をサポートする言語の処理系において、高階関数の除去は必須の処理である。これを実現する手法の一つがクロージャ変換である。クロージャ変換は、関数とともにその関数が評価される環境をペアにすることで、呼び出し時に非局所変数へのアクセスを可能にする。
クロージャ変換では、関数と環境を組にするというアイデアが一般的であるためか、環境が独立した領域に配置されることが多い。この手法は慣習的に環境渡しスタイルと呼ばれている。一方で、クロージャ渡しスタイルでは、関数と環境を連続した領域に配置することにより、一度のアクセスで環境の値を取り出せる。これは環境渡しよりも自然な表現といえるが、実装や正しさの証明があまり知られていないようである。発表では特に、独自に研究した再帰関数の変換とその正しさに焦点を当てる。

[口頭発表ショート] 根拠を示しつつ、自ら規則を発見してゆくプログラムの構想。

池上 蒔典 (放送大学 自然と環境コース)

概要

外部との通信も出来ない、新しい環境の中で、自ら考えて立案をして、目的の遂行に向けて行動をするエージェントを創ろうとするときには、何が必要だろうか。新しい環境故に、従来の記憶だけを用いて行動をしていたのなら、すぐに破綻に向かうことだろう。ここで、エージェントが自らプログラムを獲得する必要が生じる。現在私は、自ら発見してゆくプログラムの実装をしようとしており、その概略は以下のようになる。
公理から始めて空間を広げてゆく。その空間の中に法則を仮定して、証明によって論理的にその法則を説明してゆく。獲得した法則を用いて、従来の空間を書き直す。この手続きを繰り返すことで、適用可能な諸法則の空間(エージェント)を得る。
この発表ではこのプログラムの構想について議論したい。

休憩 17:00 - 17:10

ポスター・デモセッションとライトニングトーク 17:10 - 18:00

ポスター・デモセッションでは，ポスターやデモのみの発表に加えて，昼の通常発表と重複してポスター・デモとしても登録しているものがあります．これは，通常発表の議論をポスター形式でも少人数・対面でおこなったり，通常発表の内容をデモとして紹介したりできるようにしているものです．今回は，すべてのポスター・デモ発表が，通常発表をともなうものとなりました．

今回は GPCC や夜のセッションと重ならない，ポスター・デモセッション専用の時間を夕食前に設けました．セッションの最初に，ライトニングトークとして，各ポスター・デモの紹介をしていただきます．

この 1 日目の夜に GPCC のワークショップがあるため，ここで GPCC の報告とワークショップの案内もしていただきます．

ラムダ計算の拡張に基づく音楽プログラミング言語mimiumとそのVMの実装

松浦 知也(東京藝術大学芸術情報センター)

PMF前の逆説プログラミング

近藤 佑亮（東京大学）, 大石 澪弥（九州工業大学）

赤黒木の複数の証明方法

河野真治(琉球大学工学部)

保護属性を用いずに訓練された機械学習モデルの公平性テスト手法

久間 大誠（慶應義塾大学大学院理工学研究科）, 高田 眞吾 （慶應義塾大学理工学部）, 北村 崇師（産総研）

差別データの多様性が再学習に与える影響に関する調査実験と一考察

船本 和希（慶應義塾大学情報工学科）, 北村 崇師（産業技術総合研究所）, 高田 眞吾（慶應義塾大学情報工学科）

ポスター・デモセッションの会場は 2 日目の夜までそのままです． 2 日日の夜も，夜のセッションと並行してポスターやデモの議論をおこなっていただけます．

夕食 18:00 - 19:30

GPCC と並行してポスター・デモセッション (続き) 19:30 - 21:00

セッション 3 : 9:00 - 10:20

[一般講演] オブジェクト指向プログラミングのふるまいの理解を補助する双六ゲーム

矢野開人（明星大学大学院情報学研究科）, 長慎也（明星大学大学院情報学研究科）

概要

オブジェクト指向の基礎を学ぶ際、初学者が直面する課題の一つは、クラスやオブジェクトのふるまいを理解することが挙げられる。特に、オブジェクト同士のメソッド呼出において、主体となるオブジェクト（thisやselfなど）や引数の内容を把握しながら動作を追うことが難しいとされている。本研究では、双六ゲームを題材に、マスやコマをオブジェクトとして表現し、そのクラス定義をプレイヤーが確認できるようにした。ゲーム内のマスに止まった際のイベントの内容はすべてクラス定義で書かれており、マスに止まった際に発生するメソッド呼出のふるまいを理解することでプレイヤーはゲームを有利に進行できる。これにより、ゲームの勝利へのモチベーションをオブジェクト指向の学習のモチベーションに結びつけることが期待される。評価は情報学部生を対象に事前事後テストで行い、記述式問題を用いて理解度の向上を測定する。

[口頭発表] 大学入試を中心とした情報分野の学力評価手法の検討 〜プログラミング問題を中心とした EMIU 情報模試 2024 夏の結果分析〜

谷 聖一（日本大学文理学部）, 植原 啓介（慶應義塾大学）, 西田 知博（大阪学院大学）, 辰己 丈夫（放送大学）, 角田 博保（電気通信大学）, 筧 捷彦（東京通信大学）, 高橋 尚子（國學院大學）, 中野 由章（工学院大学）, 中山 泰一（電気通信大学）, 萩原 兼一（大阪大学）, 坂東 宏和（獨協医科大学）, 安田 豊（京都産業大学）

概要

大学入試を念頭において，(1) 典型的な大問中問による学力評価手法，(2)IRT を想定した多肢選択による学力評価手法，(3)CBT を前提とした出題方式による学力評価手法の開発をおこなっている. その基礎的なデータを収集するため， IRT を想定した多肢選択による学力評価手法及び典型的な大問中問による学力評価手法を検討し，実際に問題を作成し2024年6月・7月に「EMIU 情報模試2024夏」として高校生を対象とした CBT による模試を実施した。この模試の出題分野は，プログラミングおよびデータ 分析とした。学習指導要領では，プログラミングは 「(3)コンピュータとプログラミング」の「アルゴリズムとプログラミング」の部分に相当し，データ分析は「(3)コンピュータとプログラミング」の「モデル化とシミュレーション」の部分「(4)情報通信ネットワークとデータの活用」のデー タ活用の部分に相当する。今後の研究の基礎とするため，典型的な大問中問による学力評価手法による出題では，CBT での実施ではあるが共通テストなどで採用されているマークシートによる出題を前提とした作問を行った。本発表では，特に，プログラミングに関する問題の結果について分析をする。

休憩 10:20 - 10:30

セッション 4 : 10:30 - 12:00

[口頭発表] 差別データの多様性が再学習に与える影響に関する調査実験と一考察

船本 和希（慶應義塾大学情報工学科）, 北村 崇師（産業技術総合研究所）, 高田 眞吾（慶應義塾大学情報工学科）

概要

近年、機械学習(ML)モデルは実社会の様々な場面(ローン審査や裁判等)で人間の代わりに予測・判断を担っている一方で、時に差別的な予測・判断を行うことがあり、大きな社会問題となっている。
公平性テストとは、そのようなMLモデルの引き起こす差別データを検出するためのテストである。これまでに様々な公平性テストが提案されているが、その大半が、差別データを大量に検出することを目的としている。
ところが最近では、差別データを再学習に利用することでMLモデルの公平性を向上させられることを考慮し、多様性の高い差別データや自然性の高い差別データの検出を目的とした公平性テストが提案されている。しかし、差別データの多様性や自然性がMLモデルの再学習にどれだけ影響を与えるのかについて、十分に検証されていない。
本研究では、差別データの多様性に焦点を当て、それがMLモデルの再学習に与える影響について調査及び考察する。

[口頭発表ショート] 保護属性を用いずに訓練された機械学習モデルの公平性テスト手法

久間 大誠（慶應義塾大学大学院理工学研究科）, 高田 眞吾 （慶應義塾大学理工学部）, 北村 崇師（産総研）

概要

近年、機械学習技術の進展により、ローン審査や採用活動などの社会的に重要な場面で、機械学習を活用したソフトウェアの利用が増加している。それに伴って、機械学習モデルの公平性がますます重要視され、公平性をテストする手法の研究が活発に進められている。しかし、既存のテスト手法は、性別や人種といった保護属性のみが異なる個体間でのモデルの挙動に焦点を当てるものが主流であるため、保護属性を用いずに訓練されたモデルのテスト手法は自明でない。そこで、本研究では、そのような機械学習モデルに対して、事前に入手した訓練データを利用することで非保護属性を基に保護属性を推定し、従来の公平性テストのような手法を適用するアプローチの有効性を検証する。このアプローチは、ソフトウェア開発者が保護属性を除いてモデルを訓練することで公平性を高めようとする場合や、法令により保護属性の利用が制限されている状況で有効であると期待される。

[口頭発表ショート] ソフトウェア開発のための日本語指示調整データセットの開発に向けて

西潟 優羽(日本女子大学理学部), 前田 遥香(日本女子大学理学部), 小原 有以(日本女子大学大学院理学研究科), 佐藤 美唯(日本女子大学大学院理学研究科), 高橋 舞衣(日本女子大学大学院理学研究科), 倉光 君郎(日本女子大学理学部)

概要

ソフトウェア開発に大規模言語モデル(Large Language Model, LLM)を導入することで、ソフトウェア開発の自動化や効率化が期待されている。LLMはプロンプトで与えられた指示に基づき、自然言語からのコード生成やコード修正などの幅広いタスクに対応することができる。LLMが指示に対してより適切に対応するためには、指示調整が重要である。ただし、自然言語処理の分野では指示調整データセットの開発が進められているものの、ソフトウェア開発の分野における指示調整データセットの整備は不十分である。また、英語と比べて日本語データセットは不足している。そのため、本研究では指示調整に使用するソフトウェア開発のための日本語データセットの開発を目的とする。本発表ではソフトウェア開発のための日本語指示調整データセットの開発に向けた取り組みと今後の展望について紹介する。

昼食 12:00 - 13:00

招待講演 13:00 - 14:30

休憩 14:30 - 14:45

セッション 5 : 14:45 - 16:30

[一般講演] 赤黒木の複数の証明方法

河野真治(琉球大学工学部)

概要

赤黒木のアルゴリズムと正しさに関してGearsAgdaという継続形式を用いて示す。
Agda にはいろいろなモードがあり、safe と呼ばれるモードがある。さらに Cubical compatible というモードがある。これらのモードにそった証明の展開がある。
これらのモードの差と役割、モードによる差の吸収などについて考察する。

[口頭発表] Formal development of operating systems in Rust

尾田莉瑠 (早稲田大学基幹理工学部情報理工学科)

概要

プログラミング言語Rustはその高い性能と安全性から、OSカーネルのような低レベルなソフトウェアの開発で注目されています。Rustは検証の観点からも扱いやすい言語であり、CruesotやVerusといった様々な検証器が開発されています。本発表ではRustの形式検証ツールを活用してOSカーネルを開発した経験について話します。例えば、AtmosphereやNrOSといった研究事例では、Rustの所有権システムとSMTソルバーを効果的に活用することで、検証にかかるコストを大幅に削減し、OSカーネルのような大規模で低レベルなソフトウェアの形式検証を現実的に行えることが示されています。本発表では、これらの知見を踏まえ、OSカーネルの形式検証における課題や今後の展望について議論を深めたいと考えています。

[口頭発表ショート] コード最適化器の等価性と有効性の形式検証の研究構想

山崎 進 (北九州市立大学)

概要

コンパイラにおけるコード最適化の要件としては、全てのプログラム・コードについて、変換前と変換後で等価であること、変換前より変換後の実行クロックサイクルが短縮されることなどが考えられる。今まで、コード最適化器が前述の要件を満たしていることを暗黙のうちに仮定しているだけであるというのが実情であろう。しかし、将来的に高度なコード最適化器を部品として流通させることを考えたときに、誤ったコード最適化器や性能に劣るコード最適化器、悪意あるコード最適化器が組み込まれることを未然に防止する技術が必要である。本発表では、その研究構想を提案し、どのような研究計画で臨むのが妥当かを論じたい。

休憩 16:30 - 16:40

山内奨励賞受賞講演 : 16:40 - 17:20

各種報告 : 17:20 - 17:50

夏のプログラミング・シンポジウム報告

情報科学若手の会報告

GPCC 報告と案内

アナウンスなど

休憩・移動 17:50 - 18:00

夕食 18:00 - 19:30

夜のセッション 19:30 - 21:00

夜のセッション

ポスター・デモセッション (続き)

初日のポスター・デモセッションの会場は 2 日目の夜もそのまま開いています．この日も引き続き，ポスターやデモの議論をおこなっていただけます．

その他，詳細未定

セッション 6 : 9:30 - 11:30

[一般講演] 深層学習を用いた逆算法による詰将棋の自動創作

黒瀧 大地（名古屋大学大学院情報学研究科）

概要

深層学習を用いた逆算法による詰将棋創作プログラムを開発した。
近年、ビッグデータを活用した生成AIが急速に発展しているが、データが十分に存在しない分野では生成の難易度が高い。詰将棋はそのような分野の一つである。そこで、新たな詰将棋創作プログラムを開発することで、新たなデータ生成のヒントが得られるのではと考えた。
逆算法とは、ある初期局面から詰将棋のルールに従うように一手戻すことを繰り返し、長手数詰将棋を創作する手法である。従来、コンピュータ上での逆算法による長手数詰将棋の創作は難しいと考えられてきたが、詰将棋の逆算手を学習したニューラルネットワークを用いて良い逆算を選ぶようにすることで、長手数の詰将棋が創作できると仮説を立てた。
創作実験を行った結果、7日間の計算で約5100題、最大で73手詰を創作することに成功し、深層学習を用いた逆算法が詰将棋創作のような問題に対して有効であることが示唆された。

[一般講演] ミニ2048の完全解析を用いたNタプルネットワーク+モンテカルロ木探索プレイヤの分析

寺内 俊輔(高知工科大学), 松崎 公紀(高知工科大学)

概要

確率的一人ゲーム「2048」では、コンピュータ・プレイヤについて多くの研究がなされており、人間プレイヤよりもずっと高いレベルで競われている。それらコンピュータプレイヤの多くは、探索手法としてExpectimax探索かモンテカルロ木探索を採用している。著者らは先行研究において、3×3サイズのミニ2048を対象として完全解析を行い、その結果を用いてNタプルネットワークとExpectimax探索を組み合わせの特性と有用性を分析した。本研究ではこれをさらに発展させ、Nタプルネットワークと複数のモンテカルロ木探索手法を組み合わせ、モンテカルロ木探索の特性と有用性について分析を試みる。加えて、Expectimaxとモンテカルロ木探索の特徴を比較することで、それぞれの探索手法が優位性を持つ条件を見出すことが最終的な目標である。

[一般講演] ミニ 2048 における ニューラルネットワークプレイヤの解析

金子智弥 (高知工科大学), 松崎公紀 (高知工科大学)

概要

確率的一人ゲーム「2048」のコンピュータ・プレイヤについては多くの研究がなされており，人間プレイヤよりもずっと高いレベルで競われている．近年，さまざまなゲームでニューラルネットワークを用いたプレイヤが大きな成功を収めているが「2048」の研究においてはこの限りでなく，N タプルネットワークプレイヤがニューラルネットワークプレイヤよりも強いことが知られている．本研究では，その現状を打破するために，ミニ 2048 を用いてニューラルネットワークプレイヤの解析・性能向上に取り組む．ミニ 2048 とは，2048 を 3×3 盤面に縮小したものであり，すでに完全解析なされているゲームである．複数のニューラルネットワークモデルを作成し，既存研究の N タプルネットワークとニューラルネットワークの比較を行う．比較から得られた知見をもとに，「2048」におけるニューラルネットワークの改善方法を提案したい．

クロージング 11:30 -

12:00 前後に，ラフォーレ那須から那須塩原駅までのバスを出してもらう予定です．