Zobrazeno 1 - 10
of 237
pro vyhledávání: '"Yang, Kaiyu"'
Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformalization. In this paper, we intro
Externí odkaz:
http://arxiv.org/abs/2405.17216
Theorem proving is an important challenge for large language models (LLMs), as formal proofs can be checked rigorously by proof assistants such as Lean, leaving no room for hallucination. Existing LLM-based provers try to prove theorems in a fully au
Externí odkaz:
http://arxiv.org/abs/2404.12534
Autor:
Li, Zhaoyu, Sun, Jialiang, Murphy, Logan, Su, Qidong, Li, Zenan, Zhang, Xian, Yang, Kaiyu, Si, Xujie
Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language mode
Externí odkaz:
http://arxiv.org/abs/2404.09939
Autor:
Zhang, Dan, Hu, Ziniu, Zhoubian, Sining, Du, Zhengxiao, Yang, Kaiyu, Wang, Zihan, Yue, Yisong, Dong, Yuxiao, Tang, Jie
Large Language Models (LLMs) have shown promise in assisting scientific discovery. However, such applications are currently limited by LLMs' deficiencies in understanding intricate scientific concepts, deriving symbolic equations, and solving advance
Externí odkaz:
http://arxiv.org/abs/2401.07950
Autor:
Yang, Kaiyu, Swope, Aidan M., Gu, Alex, Chalamala, Rahul, Song, Peiyang, Yu, Shixing, Godil, Saad, Prenger, Ryan, Anandkumar, Anima
Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has crea
Externí odkaz:
http://arxiv.org/abs/2306.15626
Autor:
Raistrick, Alexander, Lipson, Lahav, Ma, Zeyu, Mei, Lingjie, Wang, Mingzhe, Zuo, Yiming, Kayan, Karhan, Wen, Hongyu, Han, Beining, Wang, Yihan, Newell, Alejandro, Law, Hei, Goyal, Ankit, Yang, Kaiyu, Deng, Jia
We introduce Infinigen, a procedural generator of photorealistic 3D scenes of the natural world. Infinigen is entirely procedural: every asset, from shape to texture, is generated from scratch via randomized mathematical rules, using no external sour
Externí odkaz:
http://arxiv.org/abs/2306.09310
Car-hailing services have become a prominent data source for urban traffic studies. Extracting useful information from car-hailing trace data is essential for effective traffic management, while discrepancies between car-hailing vehicles and urban tr
Externí odkaz:
http://arxiv.org/abs/2306.07456
Reasoning over natural language is a challenging problem in NLP. In this work, we focus on proof generation: Given a hypothesis and a set of supporting facts, the model generates a proof tree indicating how to derive the hypothesis from supporting fa
Externí odkaz:
http://arxiv.org/abs/2205.12443
We establish a general optimization framework for the design of automated bidding agent in dynamic online marketplaces. It optimizes solely for the buyer's interest and is agnostic to the auction mechanism imposed by the seller. As a result, the fram
Externí odkaz:
http://arxiv.org/abs/2202.12472
Autor:
Chen, Chaolan, Gao, Linna, Ding, Pei, Zhang, Shuyuan, Wang, Xiaowei, Yang, Kaiyu, Zhou, Yikun, Chi, Baozhu, Tuo, Xun
Publikováno v:
In Chemosphere August 2024 362