Σελίδα 1 από 1
Απόδειξη θεωρημάτων/προβλημάτων από μηχανή
Δημοσιεύτηκε: Πέμ Σεπ 24, 2020 2:43 pm
από Τσιαλας Νικολαος
Καλησπέρα σε όλους!Εύχομαι καλά αποτελέσματα και στις 2 ομάδες μας! Κάπου διάβασα ότι του χρόνου στην IMO2021 η microsoft θα "κατεβάσει" υπολογιστή σαν διαγωνιζόμενο

... Γνωρίζει κάποιος αν ισχύει αυτό?
Επεξεργασία από Demetres: Έγινε μεταφορά αναρτήσεων από τη
συζήτηση για τα θέματα της IMO σε αυτό το πιο σχετικό θέμα.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Πέμ Σεπ 24, 2020 4:36 pm
από miltosk
Τσιαλας Νικολαος έγραψε: ↑Πέμ Σεπ 24, 2020 2:43 pm
Καλησπέρα σε όλους!Εύχομαι καλά αποτελέσματα και στις 2 ομάδες μας! Κάπου διάβασα ότι του χρόνου στην IMO2021 η microsoft θα "κατεβάσει" υπολογιστή σαν διαγωνιζόμενο

... Γνωρίζει κάποιος αν ισχύει αυτό?
Καλά αποτελέσματα στις ομάδες μας και από εμένα.
Κάτι λένε στο aops. Αλλά δεν νομίζω να είναι διαγωνιζόμενος. Εξάλλου όλοι ξέρουμε ότι ένας υπολογιστής, και δη της Microsoft που έχει τόσο χρήμα, μπορεί να έχει πολύ περισσότερες δυνατότητες από έναν άνθρωπο πάνω σε ένα και μόνο συγκεκριμένο αντικείμενο. Έχουμε καμία ιδέα σε partial results ή γενικά πότε θα βγουν?
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Πέμ Σεπ 24, 2020 5:03 pm
από Τσιαλας Νικολαος
Τελικά μάλλον ισχύει...
https://imo-grand-challenge.github.io/
Για τα αποτελέσματα δεν γνωρίζω

Re: ΙΜΟ 2020
Δημοσιεύτηκε: Πέμ Σεπ 24, 2020 9:57 pm
από mick7
4 προβλήματα συνδιαστικης / θεωρίας αριθμών...Μετά βλέπω τα ονόματα της επιτροπής
Daniel Selsam (Microsoft Research)
Leonardo de Moura (Microsoft Research)
Sarah Loos (Google AI)
Τυχαίο ?

Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 9:40 am
από Demetres
mick7 έγραψε: ↑Πέμ Σεπ 24, 2020 9:57 pm
4 προβλήματα συνδιαστικης / θεωρίας αριθμών...Μετά βλέπω τα ονόματα της επιτροπής
Daniel Selsam (Microsoft Research)
Leonardo de Moura (Microsoft Research)
Sarah Loos (Google AI)
Τυχαίο ?
Υπάρχει μια παρανόηση. Τα άτομα αυτά δεν ήταν στην επιτροπή επιλογής των προβλημάτων για ΙΜΟ. Αντίθετα είναι μέλη της επιτροπής για κατασκευή τεχνητής νοημοσύνης η οποία να μπορεί να λύνει προβλήματα αυτών των διαγωνισμών.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 9:52 am
από Al.Koutsouridis
Demetres έγραψε: ↑Παρ Σεπ 25, 2020 9:40 am
Υπάρχει μια παρανόηση. Τα άτομα αυτά δεν ήταν στην επιτροπή επιλογής των προβλημάτων για ΙΜΟ. Αντίθετα είναι μέλη της επιτροπής για κατασκευή τεχνητής νοημοσύνης η οποία να μπορεί να λύνει προβλήματα αυτών των διαγωνισμών.
Κάτι τέτοιο φαντάστηκα όταν είδα τα ονόματα. Η επιλογή των θεμάτων περισσότερο θυμίζει παίξιμο έδρας. Καλά αποτελέσματα στην Ελληνική και Κυπριακή ομάδα. Πολλά από τα παιδιά γράφουν εδώ συχνά και θα χαρούμε να δούμε τις λύσεις τους, αν δεν δεσμεύονται από άλλους παράγοντες.
Υγ. Ξέρουμε αν η ελληνική πλευρά θα κάνει αίτηση για διαξαγωγή της επόμενης ολυμπιάδας; Είναι καλή ευκαιρία νομίζω.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 1:15 pm
από mick7
Έχετε δίκιο...έπρεπε να το είχα διαβάσει με προσοχή...από την άλλη όμως νομίζω ότι τα προβλήματα που μπορούν να αντιμετωπιστούν "καλύτερα" από υπολογιστές είναι ακριβώς αυτά της συνδυαστικής / θεωρίας αριθμών.
Demetres έγραψε: ↑Παρ Σεπ 25, 2020 9:40 am
Υπάρχει μια παρανόηση. Τα άτομα αυτά δεν ήταν στην επιτροπή επιλογής των προβλημάτων για ΙΜΟ. Αντίθετα είναι μέλη της επιτροπής για κατασκευή τεχνητής νοημοσύνης η οποία να μπορεί να λύνει προβλήματα αυτών των διαγωνισμών.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 2:16 pm
από george visvikis
Ας αφήσουν τους ανθρώπους να διαγωνίζονται με ανθρώπους και τους υπολογιστές με υπολογιστές.
Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 2:41 pm
από Al.Koutsouridis
george visvikis έγραψε: ↑Παρ Σεπ 25, 2020 2:16 pm
Ας αφήσουν τους
ανθρώπους να διαγωνίζονται με
ανθρώπους και τους
υπολογιστές με
υπολογιστές.
Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;
Όχι απαραίτητα. Μπορεί να γίνει αναγωγή στους κανόνες της λογικής και τα αξιώματα της γεωμετρίας.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 2:47 pm
από mick7
O υπολογιστής μπορεί να αντιμετωπίσει ένα οποιοδήποτε πρόβλημα εάν μεταφραστεί στην "γλώσσα" του. Φαντάζομαι εάν γεωμετρικό πρόβλημα μεταφραστεί με ορούς αναλυτικής γεωμετρίας δηλαδή κατά ουσίαν Άλγεβρας και πιο συγκεκριμένα πολυωνύμων τότε ίσως μπορεί να λυθεί.
Φαντάζομαι ότι έτσι δουλεύει το GPS, το Google Maps και άλλα.
Υπάρχει ολόκληρος κλάδος που ασχολείται με την διεπαφή υπολογιστών και Γεωμετρίας η υπολογιστική γεωμετρία.
https://en.wikipedia.org/wiki/Computational_geometry
george visvikis έγραψε: ↑Παρ Σεπ 25, 2020 2:16 pm
Ας αφήσουν τους
ανθρώπους να διαγωνίζονται με
ανθρώπους και τους
υπολογιστές με
υπολογιστές.
Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 2:55 pm
από Al.Koutsouridis
mick7 έγραψε: ↑Παρ Σεπ 25, 2020 2:47 pm
O υπολογιστής μπορεί να αντιμετωπίσει ένα οποιοδήποτε πρόβλημα εάν μεταφραστεί στην "γλώσσα" του. Φαντάζομαι εάν γεωμετρικό πρόβλημα μεταφραστεί με ορούς αναλυτικής γεωμετρίας δηλαδή κατά ουσίαν Άλγεβρας και πιο συγκεκριμένα πολυωνύμων τότε ίσως μπορεί να λυθεί.
Φαντάζομαι ότι έτσι δουλεύει το GPS, το Google Maps και άλλα.
Υπάρχει ολόκληρος κλάδος που ασχολείται με την διεπαφή υπολογιστών και Γεωμετρίας η υπολογιστική γεωμετρία.
https://en.wikipedia.org/wiki/Computational_geometry
Δεν έχουν σχέση τα παραπάνω με την απόδειξη των γεωμετρικών προβλημάτων από μηχανή.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 3:01 pm
από DrStrange
george visvikis έγραψε: ↑Παρ Σεπ 25, 2020 2:16 pm
Ας αφήσουν τους
ανθρώπους να διαγωνίζονται με
ανθρώπους και τους
υπολογιστές με
υπολογιστές.
Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;
Δεν νομίζω ότι έχουμε κάτι να φοβηθούμε. Ίσα ίσα, νομίζω στην συγκεκριμένη μάχη ανθρώπου-μηχανής , θα νικήσει ο άνθρωπος. Κάθε χρόνο υπάρχουν άτομα που παίρνουν perfect-score αυτό μόνο αρκεί.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 3:04 pm
από miltosk
Νομίζω έχει ξεφύγει λίγο η συζήτηση από το θέμα.
Τώρα επί της συζήτησης αν δώσω το παράδειγμα μιγαδικής γεωμετρίας (που αναφέρεται από τον κ.Βισβίκη πιο πάνω) όπου το πρόβλημα είναι οι πράξεις, νομίζω ότι ένας υπολογιστής έχει μεγάλο προβάδισμα.
Re: ΙΜΟ 2020
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 3:16 pm
από mick7
Εξαρτάται πως ορίζουμε ένα γεωμετρικό πρόβλημα πχ "η ελάχιστη απόσταση που πρέπει να διανύσουμε για να φτάσουμε σε ενα σημείο στον αστικό ιστό" Αν αναφερόμαστε στο επίπεδο σχολικής γεωμετρίας ήτοι Ευκλείδειας όντως νομίζω οτι δεν υπάρχει εργαλείο που να δίνει αυτόματες (μηχανικές) αποδείξεις ακόμη.Βέβαια, για να υπάρξει έρευνα πρέπει να υπάρχουν και αντίστοιχα κεφάλαια τα οποία προφανώς θα προέρχονται από την ανάγκη να λυθούν προβλήματά που αντιμετωπίζει μεγάλο μέρος μια κοινωνίας. Τα προβλήματά της Ευκλείδης Γεωμετρίας και αν λύνονται υπολογιστικά δεν νομίζω ότι απασχολεί τους περισσοτέρους.
Φαντάζομαι σαν μηχανικός κατέχετε καλύτερα το R&D.
Al.Koutsouridis έγραψε: ↑Παρ Σεπ 25, 2020 2:55 pm
Δεν έχουν σχέση τα παραπάνω με την απόδειξη των γεωμετρικών προβλημάτων από μηχανή.
Απόδειξη θεωρημάτων/προβλημάτων από μηχανή
Δημοσιεύτηκε: Παρ Σεπ 25, 2020 3:30 pm
από Al.Koutsouridis
Με αφορμή την συζήτηση στο νήμα
https://mathematica.gr/forum/viewtopic.php?f=58&t=67947 μεταφέρω την συζήτηση εδώ για να μείνει το αναφερθέν στο σκοπό του. Η επιμελητές μπορούν να μεταφέρουν τα εκτός θέματος μηνύματα εδώ.
Re: Απόδειξη θεωρημάτων/προβλημάτων από μηχανή
Δημοσιεύτηκε: Σάβ Σεπ 26, 2020 11:15 am
από Μάρκος Βασίλης
Σε ό,τι αφορά το ζήτημα των διαγωνισμών θα ήταν άδικο να συμμετέχουν υπολογιστές διαγωνιστικά, ωστόσο θα ήταν πολύ χρήσιμο ερευνητικά να επιτρέπουμε σε τέτοιες εφαρμογές να επιλύουν τα προβλήματα live την ώρα που το κάνουν και οι διαγωνιζόμενοι/ες.
Σε σχέση τώρα με τις αποδείξεις θεωρημάτων της Ευκλείδειας γεωμετρίας, υπάρχουν πολλές τεχνικές που βασίζονται είτε σε άλγεβρα - μέσω πολυωνύμων αλλά και γεωμετρικών μετασχηματισμών (Klein) - είτε σε αξιωματικές προσεγγίσεις όπως π.χ. μέσω των αξιωμάτων του Tarski, του Hilbert ή υποσυνόλων/παραλλαγών τους. Μάλιστα στη δεύτερη κατηγορία υπάρχουν προσεγγίσεις που υιοθετούν προσεγγίσεις που βασίζονται σε resolution (

) ή προσεγγίσεις που βασίζονται σε κατασκευαστικές/ιντουισιονιστικές προσεγγίσεις.
Γενικά η Ευκλείδεια γεωμετρία είναι από τα πρόσφορα πεδία για να ασχοληθεί κανείς σε ό,τι αφορά τις αξιωματικές προσεγγίσεις μιας και η θεωρία της μπορεί να εκφραστεί όλη σε πρωτοβάθμια λογική - έστω και με ένα μη πεπερασμένο σύνολο αξιωμάτων.