| Title |
Analysis of artificial neural networks for solving reasoning tasks |
| Translation of Title |
Loginių samprotavimų uždavinių sprendimo, naudojant dirbtinius neuroninius tinklus, galimybių tyrimas. |
| Authors |
Sadi, Belkacem |
| Full Text |
|
| Pages |
43 |
| Keywords [eng] |
artificial neural networks, theorem proving, Lean 4, beam search, semantic hallucination, value head, Direct Preference Optimization. |
| Abstract [eng] |
This thesis examines the use of artificial neural networks for automated theorem proving in the Lean 4 formal proof assistant. The central problem is semantic hallucination: models often produce proof steps that are syntactically correct but logically incorrect. A formal error probability framework is presented to quantify this problem at the step level. Phase I evaluates three models under identical conditions on 1,000 theorems from the LeanDojo Benchmark 4. InternLM2.5StepProver achieves 45.7% Pass@1, ReProver 44.6%, and DeepSeekProverv1.5RL 40.3%. The framework shows that 75–83% of syntactically valid tactics are logically incorrect across all models. Phase II proposes two modifications of InternLM2.5StepProver. Proposition A introduces a featurebased value head that prunes unpromising proof branches, achieving 51.9% Pass@1 (+6.2pp). Proposition B trains an errorconditioned refiner using Direct Preference Optimization on real Lean 4 compiler error pairs, achieving 45.9% Pass@1 with a 16.3% correction rate. |
| Dissertation Institution |
Vilniaus universitetas. |
| Type |
Master thesis |
| Language |
English |
| Publication date |
2026 |
