Presenters

• 肖 俊廷 (九州大学大学院数理学府)
• Efficient implementation of discrete Gaussian sampling for lattice-based cryptography on multiple platforms
• Abstract:

For the sake of new cryptographic algorithms to resist attacks from the quantum computers, lattice-based cryptography has become one of the most popular research field in post-quantum cryptography. However, a number of lattice-based cryptographic schemes suffer from large-scale numbers sampled from discrete Gaussian distribution which can affect their efficiency remarkably on multiple platforms. JavaScript is a kind of scripting language for Web application development. JavaScript programs could execute on multi-platforms (such as Windows, Linux, Android, iOS, etc.). On the other hand, it is also necessary to implement discrete Gaussian sampling on widely used smart cards in the IoT era. Java Card is a mainstream applet development technology for deployed smart card virtual machine. Since high precision floating-point arithmetic is essential for most discrete Gaussian sampling methods. With limited memory or computing power, it is a challenge to implement discrete Gaussian sampling on JavaScript platforms and Java Card. We proposed the approaches to implement several classical discrete Gaussian sampling methods efficiently and compared them on several JavaScript platforms (Web browsers) on PCs and Java Card platforms. The results show that our sampling methods run efficiently on these platforms. After comparisons, we indicate the sampling method which has the best performance.

• 宮木 希 (九州大学大学院数理学府)
• レイアウト問題の整数計画法を用いた解法
• Abstract:

都市計画やショッピングセンターの出店計画といった大きな問題から部屋のレイアウトの問題まで様々な問題がタイリング問題に帰着できる。 このタイリング問題の中のペントミノ問題について0-1整数計画問題としてタイリング問題の定式化を行い、数理計画ソルバーを用いて解を得ました。 プログラミング言語はpythonを、数理計画ソルバーはGurobi Optimizerを使用しました。

• 平河 尭 (九州大学大学院数理学府)
• 論理式表現された問題の混合整数計画問題への自動変換
• Abstract:

産業や科学技術など 幅広い分野における多く 現実問題が線形計画問題として定式化できることが知られている。 本研究では論理式で定式化された問題に対して、必要なら補助変数を加えて、線形計画問題を生成する方法を提案する。 そして、この生成方法に基づき、論理式で与えらた問題に対して線形計画問題を自動生成するプログラムALLC(Automatic Logical formula to Linear equation Compiler)を開発したので紹介する。これを使うことで、ユーザーは線形制約式などを意識することなく問題の論理式による定式化に集中することができ、問題の定式化についての正当性 や等価性を論理式レベルで検証することができる。 このライブラリはプログラム言語pythonにおいて線形計画問題を解くためのライブラリであるPuLPを拡張したものである。

• 山田 智史 (九州大学大学院数理学府)
• FreeFem++を用いて作成したメッシュ上での数値計算
• Abstract:

私の研究テーマは網膜血管網における血管新生の数理モデルの構築とその数値シミュレーションである． 血管網は動脈，静脈，毛細血管などの様々な種類の血管から形成されており，その中でも毛細血管は網目状に拡がっていることが知られている． 構築した数理モデルのシミュレーションを行うために，血管網に見立てた網目状の経路をFreeFem++とC言語を用いて作成し，その経路上で数値計算を行った． 数値計算結果の可視化にはGLSC(Graphic Library for Scientific Computing)を用いた． 本発表では，まず円環領域をFreeFem++を用いて三角形分割し，さらにC言語を用いて網目状の経路を作成した方法について紹介する． さらに作成した経路上での実際の数値シミュレーション結果についてデモンストレーションを行う．

• 池松 泰彦 (九州大学IMI)
• GVWアルゴリズムの改良と実験結果
• Abstract:

グレブナー基底導出アルゴリズムの1つとして，2010 年に S. Gao, F. Volny IV, M. Wang ら によって提案されたGVWアルゴリズムがある． GVWアルゴリズムではBuchbergerアルゴリズム同様多くの “reduction” を実行するが，Buchbergerにおける高速化手法をGVWアルゴリズムに拡張することで，アルゴリズム中の reduction 数を削減できる． 今回は，そのようにして得られた改良アルゴリズムを数式処理ソフトMagmaで実装し，オリジナルのGVWアルゴリズムと比較評価することでその効果を説明する．

• 松藤 ちひろ (九州大学大学院数理学府)
• 最適化された回転中心を用いた実時間スキニングアルゴリズムのBlenderでの実装
• Abstract:

3DCGモデルとスケルトンを関連づけ, スケルトンの動きに対して3DCGモデルの頂点がどうように追従するかを定めるスキニングアルゴリズムについて考察する. 今回, SIGGRAPH2016でDisney ResearchのB.H.LeとJ.K.Hodginsにより紹介された線形手法と双対四元数の長所を活かした回転中心の事前計算を活かした新しい手法「Real-time Skeletal Skinning with Optimized Centers of Rotation」についてPython言語を用いてBlenderソフト上に実装したので紹介する.

• 安東 昂希 (九州大学理学部数学科)
• 計算体系に基づく古典論理の自動定理証明器の実装
• Abstract:

古典論理命題論理の自動定理証明器を、計算体系Dual Calculusに基づいて実装しました。 関数型言語Haskellによって、帰納的定義により簡潔に記述することが可能でした。 関数として、solveInhabitRとsolveInhabitLが存在し、これによってそれぞれ恒真,恒偽であることが証明可能です。次のように記述することで、実際に自動で定理が証明されます。

<例:入力>
  solveInhabitanceR [] []
  (Imp (Not (And (Ax (TVar "X")) (Ax (TVar "Y"))))
       (Or (Not (Ax (TVar "X"))) (Not (Ax (TVar "Y")))))
  solveInhabitanceL [] [] (And (Ax (TVar "X")) (Not (Ax (TVar "X"))))
<例:出力>
  Just (λ_0.(_1.(_0・not<<(_4.(fst・_1)),
			  (_4.(snd・_1))>>)))
  Just (_0.(_0・fst[(_2.(_0・snd[not<_2>]))]))