Zlepšení logického odvozování ve statistických systémech
| Název práce v češtině: | Zlepšení logického odvozování ve statistických systémech |
|---|---|
| Název v anglickém jazyce: | Advancing Reasoning Capabilities of Statistical Systems |
| Akademický rok vypsání: | 2023/2024 |
| Typ práce: | disertační práce |
| Jazyk práce: | |
| Ústav: | Ústav formální a aplikované lingvistiky (32-UFAL) |
| Vedoucí / školitel: | RNDr. Milan Straka, Ph.D. |
| Řešitel: |
| Zásady pro vypracování |
| Novel multistep reasoning is still hard to achieve reliably using cutting-edge statistical systems trained on big data like large language models. At the same time, improvements in reasoning affect virtually every area of scientific and technological progress.
A natural testbed and training objective for reasoning is theorem proving in mathematics since mathematics is infeasible without precise reasoning, and conversely, reasoning can be trained by self-exploration of mathematics. Thanks to formal verification systems like Lean or Metamath, results in mathematics can be automatically verified, providing a clear training signal. Furthermore, these systems contain tens of thousands of manually written proofs, providing expert traces for supervised pre-training. Formal theorem proving naturally extends also into natural language processing and understanding tasks, including complex query answering on a knowledge graph, common sense reasoning, and fact verification. The goal of this thesis is to explore architectural, training, and other changes to current methods with the aim of enhancing general reasoning capabilities and transferring them to concrete applications. These might include knowledge graph reasoning, theorem proving, software verification, or solving specific problems in areas like medicine, cryptography, education, or manufacturing planning. |
| Seznam odborné literatury |
| Lu, P., Qiu, L., Yu, W., Welleck, S., & Chang, K. (2022). A Survey of Deep Learning for Mathematical Reasoning. ArXiv, abs/2212.10535. https://arxiv.org/abs/2212.10535
Lample, G., Lachaux, M., Lavril, T., Martinet, X., Hayat, A., Ebner, G., Rodriguez, A., & Lacroix, T. (2022). HyperTree Proof Search for Neural Theorem Proving. ArXiv, abs/2205.11491. https://arxiv.org/abs/2205.11491 Trinh, T.H., Wu, Y., Le, Q.V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. Nature, 625, 476 - 482. https://www.nature.com/articles/s41586-023-06747-5 Jiang, A.Q., Welleck, S., Zhou, J.P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., & Lample, G. (2022). Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. ArXiv, abs/2210.12283. https://arxiv.org/abs/2210.12283 |