Page 59 - profile2012.indd

Research Faculty 研究人員

副研究員 研究員
王柏堯 Bow-Yaw Wang 王新民 Hsin-Min Wang

Associate Research Fellow Research Fellow
Ph.D., Computer Science, University of Pennsylvania Ph.D., Electrical Engineering, National Taiwan University

Tel: +886-2-2788-3799 ext.1717 Fax: +886-2-2782-4814 Tel: +886-2-2788-3799 ext. 1714 Fax: +886-2-2782-4814
Email: bywang@iis.sinica.edu.tw Email: whm@iis.sinica.edu.tw
http://www.iis.sinica.edu.tw/~bywang http://www.iis.sinica.edu.tw/pages/whm

● Adjunct Associate Professor at National Taiwan University (2009-) ● Adjunct Assistant Professor at National Taiwan University (2004- ● Research Fellow, IIS, Academia Sinica (2010 - ) ● B.S., EE, National Taiwan University (1989)
● Associate Research Fellow (2008-) 2009) ● Associate Research Fellow, IIS, Academia Sinica (2002 – 2010) ● Editorial board member, IJCLCLP (2004 - )
● Invited Professor at INRIA (2009-2011) ● Assistant Research Fellow (2003-2008) ● Assistant Research Fellow, IIS, Academia Sinica (1996 - 2002) ● Managing editor, Journal of Information Science and Engineer-
● Invited Associate Professor at Tsinghua University (2009-2010) ● Postdoctoral Fellow, IIS, Academia Sinica (1995 - 1996) ing (2012 - )
● Ph.D., EE, National Taiwan University (1995)
Research Description Publications Research Description Publications

My research interests include model checking, automata 1. Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, and Kwang- My research interests include speech processing, natural 1. Wei-Ho Tsai and Hsin-Min Wang, “Automatic singer recogni-

theory, formal veri cation, and computational logic. For- keun Yi. Predicate Generation for Learning-Based Quantifier- language processing, multimedia information retrieval, tion of popular music recordings via estimation and modeling
th

mal veri cation is a mathematical and logical method that Free Loop Invariant Inference. 17 International Conference machine learning and pattern recognition. The research of solo vocal signals,” IEEE Trans. on Audio, Speech, and
checks properties about computer systems. Among sev- on Tools and Algorithms for the Construction and Analysis of goal is to develop methods for analyzing, extracting, rec- Language Processing, 14(1), pp. 330-341, January 2006.
Systems (TACAS ‘11). Saarbruecken, Germany. March 28 -

eral techniques in formal veri cation, I am most interested 31, 2011. ognizing, indexing, and retrieving information from audio 2. Wei-Ho Tsai, Shih-Sian Cheng, and Hsin-Min Wang, “Auto-
in model checking. Given a formal property and a system 2. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, data, with the special emphasis on speech and music. In matic speaker clustering using a voice characteristic reference
description, a model checker veri es whether the system Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, and Lei the speech area, the research has been focused mainly space and maximum purity estimation,” IEEE Trans. on Au-

description conforms to the property. The model check- Zhu. Comparing Learning Algorithms in Automated Assume- on speech recognition, speaker recognition, speaker dio, Speech and Language Processing, 15(4), pp. 1461-1474,
May 2007.
th
ing problem in general is computationally hard. I have Guarantee Reasoning. 4 International Symposium On Lev- segmentation/clustering/diarization, spoken document

been developing algorithms and heuristics to improve the eraging Applications of Formal Methods, Verification and 3. Yi-Hsiang Chao, Wei-Ho Tsai, Hsin-Min Wang, and Ruei-
Validation (ISOLA ‘10). Crete, Greece. 18 - 20 October, 2010.

e ciency of model checking. In order to evaluate the ef- 3. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming- retrieval/summarization, etc. The recent achievements Chuan Chang, “Using kernel discriminant analysis to improve

the characterization of the alternative hypothesis for speaker

fectiveness of veri cation algorithms, I have implemented Hsien Tsai, Yih-Kuen Tsay, and Bow-Yaw Wang. Automated include a minimum-boundary-error-based discrimina- verification,” IEEE Trans. on Audio, Speech and Language

the model checker OMOCHA. The model checker sup- Assume-Guarantee Reasoning through Implicit Learning. tive acoustic model training and decoding framework for Processing, 16(8), pp. 1675-1684, November 2008.
ports both BDD- and SAT-based algorithms. It is used as a 22nd International Conference on Computer Aided Verifica- automatic phone segmentation, a novel characterization 4. Hung-Ming Yu, Wei-Ho Tsai, and Hsin-Min Wang, “A query-

research prototype system in the past. tion (CAV ‘10). Edinburgh, UK. July 15 - July 19, 2010. of the alternative hypothesis using kernel discriminant by-singing system for retrieving karaoke music,” IEEE Trans.

4. Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwang- analysis for likelihood ratio-based speaker veri cation, a on Multimedia, 10(8), pp. 1626-1637, December 2008.
Lately, I apply algorithmic learning to formal veri cation. keun Yi. Deriving Invariants by Algorithmic Learning, Deci- new divide-and-conquer framework for fast speaker seg-

Consider the problem of loop invariant generation. A sion Procedures, and Predicate Abstraction. 11th International mentation and diarization, and a probabilistic generative 5. Yi-Ting Chen, Berlin Chen, and Hsin-Min Wang, “A proba-

pre-condition for a loop speci es the assumptions before Conference on Verification, Model Checking and Abstract In- bilistic generative framework for extractive broadcast news
executing the loop; a post-condition for a loop speci es terpretation (VMCAI ‘10). Madrid, Spain. January 17 - Janu- framework for extractive spoken document summariza- speech summarization,” IEEE Trans. on Audio, Speech and

intended e ects after its execution. Given an annotated ary 19, 2010. tion. The ongoing research includes attribute-detection- Language Processing, 17(1), pp.95-106, January 2009.

loop, we want to compute a loop invariant to establish 5. Yih-Kuen Tsay, Bow-Yaw Wang. Automated Compositional based speech/language recognition, language modeling 6. Shih-Sian Cheng, Hsin-Chia Fu, and Hsin-Min Wang, “Mod-

the post-condition under the assumption of the pre-con- Reasoning of Intuitionistically Closed Regular Properties. for speech recognition/document classi cation/informa- el-based clustering by probabilistic self-organizing maps,”
International Journal of Foundations of Computer Science.

dition. If a person is asked to nd a loop invariant, she is 20(4): 747-762 (2009). tion retrieval, voice conversion, speech synthesis, etc. In IEEE Trans. on Neural Networks, 20(5), pp. 805-826, May
2009.
likely to test and rectify several candidates before one is 6. Yih-Kuen Tsay and Bow-Yaw Wang. Automated Composi- the music area, the research has been focused mainly on
found. In the setting of algorithmic learning, the person tional Reasoning of Intuitionistically Closed Regular Prop- vocal melody extraction, query by singing/humming, solo 7. Shih-Sian Cheng, Hsin-Min Wang, and Hsin-Chia Fu, “BIC-
is trying to “learn” a loop invariant from counterexamples. erties . 13 International Conference on Implementation and vocal modeling, music tag annotation, tag-based music based speaker segmentation using divide-and-conquer strate-
th
gies with application to speaker diarization,” IEEE Trans. on
The learning-based loop invariant generation technique Application of Autoamta (CIAA ‘08). San Francisco, USA. information retrieval (MIR), etc. The recent achievements Audio, Speech, and Language Processing, 18(1), pp. 141-157,
automates the process by deploying a learning algorithm July 21-24, 2008. include a novel cost-sensitive multi-label (CSML) learning January 2010.
instead of a person. 7. Bow-Yaw Wang. Automatic Derivation of Compositional framework for automatic music tagging, a novel query
th
Rules in Automated Compositional Reasoning. 18 Interna- 8. Chih-Yi Chiu, Hsin-Min Wang, and Chu-Song Chen, “Fast
In compositional reasoning, algorithmic learning is ap- tional Conference on Concurrency Theory (CONCUR ‘07). by multiple tags with multiple levels of preference (de- min-hashing indexing and robust spatio-temporal matching
plied to synthesize contextual assumptions. In this appli- Lisbon, Portugal. September 3-8, 2007. noted as an MTML query) scenario and a corresponding for detecting video copies,” ACM Trans. on Multimedia Com-
cation, a learning algorithm for Boolean functions infers a 8. Ming-Hsien Tasi and Bow-Yaw Wang. Formalization of CTL* tag cloud-based query interface for MIR. We have partici- puting, Communications and Applications, 6(2), 10: 1-23,
March 2010.
th

simple contextual assumption to reduce the cost of veri- in the Calculus of Inductive Constructions. 11 Annual Asian pated in the MIREX audio tag classi cation task since 2009

cation. Since contextual assumptions can be succinctly Computing Science Conference (ASIAN ‘06). Tokyo, Japan. and achieved top performance. The ongoing research 9. Chih-Yi Chiu and Hsin-Min Wang, “Time-series linear search
December 6-8, 2006.
represented by Boolean functions, implicit learning can 9. Bow-Yaw Wang. On the Satisfiability of Modular Arithmetic includes continuous improving of our own technologies for video copies based on compact signature manipulation and
containment relation modeling,” IEEE Trans. on Circuits and

improve the capacity of formal veri cation in several hard- Formulae. 4 Automated chnology for Verifi cation and Analy- and systems, audio feature analysis, semantic visualiza- Systems for Video Technology, 20(11), pp. 1603-1613, No-
th
ware examples. sis. Beijing, China. October 2006. tion of music tags, and vocal separation, so as to facilitate vember 2010.
10. Bow-Yaw Wang. Modeling and Analyzing Applications with the management and retrieval of a large music database. 10. Hung-Yi Lo, Ju-Chiang Wang, Hsin-Min Wang, and Shou-De
Domain-Specific Languages by Reflective Rewriting: a Case The future research directions also include real-time music Lin, “Cost-sensitive multi-label learning for audio tag anno-

Study. 21 ACM Symposium on Applied Computing. Dijon, tagging and singing voice synthesis. tation and retrieval,” IEEE Trans. on Multimedia, 13(3), pp.
st
France. April 23-27, 2006. 518-529, June 2011.
研究人員
58 Research Faculty
59