職位描述
語音識別大模型算法人工智能計算機軟件
【工作內容】
1、使用Lean4形式化數學競賽題目的解題過程，確保形式化結果清晰易懂、符合邏輯并通過Lean驗證
2、學習最新形式化方法和工具，提升技能，協作解決形式化中的技術難題。
薪資面議，可談
【崗位要求】
1、數學/理科相關專業優先，參加過數學競賽且獲獎者優先;精通初高中數學競賽知識和相關運算，成績優異;
2、熟練應用Lean數據編程語言，能依據國際奧賽的解題步驟答案，輸出Lean語言的推理步驟，并驗證無誤;
3、扎實的數學基礎，精通形式化定理證明語言Lean4，具備出色的Lean4編程能力，能夠熟練運用Lean4進行數學定理的形式化工作;
4、優先考慮具有以下經驗者:參與過形式化證明項目對Mathlib有commit經歷，熟悉Lean語言元編程，具備訓練或部署LLM輔助自動定理證明的經驗。
工作地點
北京海淀區清華大學1
入職公司信息
- 入職公司: 交個朋友優選科技有限公司
- 公司地址: 杭州濱江區秋溢路601號5號樓9層903室交個朋友優選科技有限公司2
- 公司人數: 1000-9999人
認證資質
人力資源服務許可認證
人力資源服務許可證是由國家人力資源與社會保障相關部門頒發，代表人才經紀人所在企業可以合法開展人力資源相關業務的資質證件。展示該標簽代表該企業發布此職位時已上傳《人力資源服務許可證》或《人力資源服務備案證書》并經由平臺審驗通過。
相似職位
- AI應用落地開發2.5-3萬
北京 - 海淀
愛多邦(北京)信息技術服務有限公司 - 大模型工程師3-4萬
北京 - 朝陽
中國電子科技集團公司信息科學研究院 - AI算法模型師面議
北京 - 昌平
中移金科 - CAE智能技術與軟件研發1.5-2.5萬
北京 - 海淀
中國久遠高新技術裝備有限公司 - 模型研發崗(算法方向)2-3萬
北京 - 海淀
北京廣監云科技有限公司 - 聲學技術高級人才1.5-3萬
北京 - 懷柔
北京懷芯聲學技術有限公司
熱門公司推薦
- 霸王茶姬招聘
- 肯德基招聘
- 順豐招聘
- 美團招聘
- 京東招聘
- 餓了么招聘
- 比亞迪招聘
- 中國一汽招聘
- 北京汽車招聘
- 蔚來招聘
- 東風汽車招聘
- 長城汽車招聘
- 奇瑞汽車招聘
- 理想汽車招聘
- 長鑫存儲招聘
- 天江藥業招聘
- 藍月亮招聘
- 安踏招聘
- TCL招聘
- 海信招聘
- 聯想招聘
- 海康威視招聘
- 寧德時代招聘
- 中興招聘
- 新松招聘
- 京東方招聘
- 申通招聘
- 圓通招聘
- 中通招聘
- 百世物流招聘
- 德邦物流招聘
- 麥當勞招聘
- 星巴克招聘
- 海底撈招聘
- 蜜雪冰城招聘
- 瑞幸招聘
- 雀巢招聘
- 騰訊招聘
- 百度招聘
- 快手招聘
- 字節跳動招聘
- 新華網招聘
- 小米招聘
- 招商銀行招聘
- 中信銀行招聘
- 北京銀行招聘
- 興業銀行招聘
- 交通銀行招聘
- 建發集團招聘
- 中國移動招聘
- 中國聯通招聘
- 中國電信招聘
- 中糧集團招聘
- 國藥控股招聘
- 中廣核招聘
- 中國船舶招聘
- 強生中國招聘
- 匯豐中國招聘
- 宜家招聘
- 立邦中國招聘
- 伊利招聘
- 青島啤酒招聘
- 京港地鐵招聘
- 寶馬招聘
- 小鵬汽車招聘
- 華為招聘
- 特斯拉招聘
- 吉利招聘
- 奔馳招聘
- 海爾招聘
- 美的招聘
- 京東方招聘
- 施耐德電氣招聘
- 德邦物流招聘
職位發布者
丁女士/招聘者
昨日活躍立即溝通
悠派才選(上海)人力資源有限公司
卡思優派人力資源集團，成立于2007年。集團運行上海和無錫雙總部模式，是國內屈指可數的業務涵蓋高端獵頭服務，白領招聘及外包服務，藍領外包服務及薪酬、人事相關外包、代理服務的綜合性人力資源服務機構。現旗下擁有卡思獵頭、優派外包、優派好工作求職連鎖吧等品牌，是長三角區域品牌影響力最廣、客戶數量最多、團隊規模最大的人力資源服務機構之一。公司使命致力于“放大人的價值”，愿景是“成為人才驅動，數據驅動，產品驅動，技術驅動的面向客戶的令人敬仰的組織”，成為中國招聘與外包領域領先的人力資源服務商。
公司主頁