■工学部_研究紹介_2017_英語版ファイル161220

31/80

ShidamaLabThehumansmakemistakes,soitisimportanttoverifythecorrectnessofmathematicaltheoremswithacomputer.InShidamaLaboratory,studentsworkonformalizationofmathematicsandcomputeraidedverification.Toverifyamathematicaltheoremwithacomputer,wewriteaproofofthetheorembytheformalizationlanguage.Thenwecanverifythecorrectnesswithacomputerlogicallyandmathematically.Thismethodcanbeappliedtotheinspectionofthedevelopmentoftheengineeringsystemanditsmovement.Acomputerprogramisadescriptionwithlogicaloperationsthatmakesoutputdatafrominputdatabyaformallanguage,thuswecanexpresstheoperationsasamathematicalproposition.Itisanincompletemethodforhumanstoinspectresultsusingdataandtoanalyzealloperations,aswemakemistakes.Weshouldverifythemathematicalcorrectnessofacomputerprogramwithacomputer.Thenwecanmakeacomputerprograminwhichnormaloperationsaremathematicallyguaranteed.Weparticipateinaninternationalinvestigationproject,thataimstomakethelibraryofformalizedtheoremsandproofsofallmathematics.Thepurposeistoapplyformalizedmathematicstocomputersoftwaredevelopment.Andwearedevelopingasystemthatcanmakeacomputerprogramthatnormaloperationsaremathematicallyguaranteed.YasunariShidamaProfessorHas been on the faculty in the Dept. of Computer Science and Engineering since 1990.Are interested in Formalization of Mathematics and Computer Aided Verification.Formalization of Mathematics and Computer Aided VerificationOurgraduatesareworkingascomputerscienceengineersastheyhavelogicalandmathematicalthinkingskills.After GraduationIn the FutureVerify the correctnessof a specification sheetTheinteractiveteachingmaterialsoftheissueofproofElectrical& Computer EngineeringMaruyamaLabInMaruyamaLab.,ourresearchfocusesonimageunderstanding,contentbasedimagesearch,patternrecognition,3Drecoveryfromimages,andcomputergraphics.Especiallyweareveryinterestedintechniquestoimproveimageunderstandingandpatternrecognitionperformancebylearningfromexamples.We can easily recognize and understand the contents included in the image. This ability is improved through learning from our everyday experience. Our research goal is to providing such significant ability of learning to recognize various kinds of information to computer.Weareinvestigatingmethodsforimageunderstandingsuchasimagemodelingbasedonprobabilistictopicmodels,imagesegmentationviaenergyminimization,recoveryof3Dstructurefromimagesequence,Ourresearchinterestalsoincludecomputergraphicssuchasphoto-realisticrenderingalgorithms.Thesetechniquescanbeusedforvariouskindsofapplicationsincludingcontentbasedimagequeryontheweb,human-computerinteraction,MinoruMaruyamaProfessorSince 1996, he is with ShinshuUniv. Before joining ShinshuUniv., he was with Mitsubishi Electric Corp. 1990-1991, he was a visiting scientist of MIT AI Lab.Improving Image Understanding Performance by Learning from ExamplesOverhalfofthegraduatesgotograduateschool(masterprogramofShinshuUniversity).Graduatesofourlabareemployedbyelectronicscompanies,ITcompanies,includingvideogamecompaniesetc.Manygraduatesareworkingassoftware/ITengineers.We also study on computer graphics techniques such as photo-realistic rendering algorithms, semi-automatic character animation synthesis via reinforcement learning etc.Our work on the application of topic models to pattern classification received best paper award honorable mention at the International Workshop on Document Analysis Systems 2009 (DAS2009).After GraduationIn the FutureElectrical& Computer Engineering29

※このページを正しく表示するにはFlashPlayer10.2以上が必要です